\documentclass[../arithmetic.tex]{subfiles}

\begin{document}
  \chapter{Divisibility}\label{chapter:divisibility}

  \filename{arithmetic/sections/07_divisibility.ftl.tex}

  \begin{forthel}
    %[prove off][check off]

    [readtex \path{arithmetic/sections/06_multiplication.ftl.tex}]

    %[prove on][check on]
  \end{forthel}


  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_07_4239998993825792}
      Let $n, m$ be natural numbers.
      $n$ divides $m$ iff there exists a natural number $k$ such that
      $n \cdot k = m$.
    \end{definition}

    Let $m$ is divisible by $n$ stand for $n$ divides $m$.
    Let $n \mid m$ stand for $n$ divides $m$.
    Let $n \nmid m$ stand for $n$ does not divide $m$.
  \end{forthel}

  \begin{forthel}
    \begin{lemma}\printlabel{ARITHMETIC_07_1478855118290944}
      Let $n, m$ be natural numbers.
      $n$ divides $m$ iff there exists a natural number $k$ such that
      $k \cdot n = m$.
    \end{lemma}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_07_1311437490225152}
      Let $n$ be a natural number.
      A factor of $n$ is a natural number that divides $n$.
    \end{definition}

    Let a divisor of $n$ stand for a factor of $n$.
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_07_2242720387039232}
      Let $n$ be a natural number.
      Then \[ n \mid 0. \]
    \end{proposition}
    \begin{proof}
      We have $n \cdot 0 = 0$.
      Hence $n \mid 0$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_07_8611150130315264}
      Let $n$ be a natural number.
      Then \[ 0 \mid n \implies n = 0. \]
    \end{proposition}
    \begin{proof}
      Assume $0 \mid n$.
      Consider a natural number $k$ such that $0 \cdot k = n$.
      Then $n = 0$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_07_1259086070939648}
      Let $n$ be a natural number.
      Then \[ 1 \mid n. \]
    \end{proposition}
    \begin{proof}
      We have $1 \cdot n = n$.
      Hence $1 \mid n$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_07_3944887330275328}
      Let $n$ be a natural number.
      Then \[ n \mid n. \]
    \end{proposition}
    \begin{proof}
      We have $n \cdot 1 = n$.
      Hence $n \mid n$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_07_6917446193643520}
      Let $n$ be a natural number.
      Then \[ n \mid 1 \implies n = 1. \]
    \end{proposition}
    \begin{proof}
      Assume $n \mid 1$.
      Take a natural number $k$ such that $n \cdot k = 1$.
      Suppose $n \neq 1$.
      Then $n < 1$ or $n > 1$.

      Case $n < 1$.
        Then $n = 0$.
        Hence $0
          = 0 \cdot k
          = n \cdot k
          = 1$.
        Contradiction.
      End.

      Case $n > 1$.
        We have $k \neq 0$.
        Indeed if $k = 0$ then
        $1
          = n \cdot k
          = n \cdot 0
          = 0$.
        Hence $k \geq 1$.
        Take a positive natural number $l$ such that $n = 1 + l$.
        Then $1
          < 1 + l
          = n
          = n \cdot 1
          \leq n \cdot k$.
        Hence $1 < n$.
        Contradiction.
      End.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_07_7463519983239168}
      Let $n, m, k$ be natural numbers.
      Then \[ n \mid m \implies n \mid m \cdot k. \]
    \end{proposition}
    \begin{proof}
      Assume $n \mid m$.
      Take $l \in \Nat$ such that $n \cdot l = m$.
      Then $n \cdot (l \cdot k)
        = (n \cdot l) \cdot k
        = m \cdot k$.
      Hence $n \mid m \cdot k$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{corollary}\printlabel{ARITHMETIC_07_1588185794609152}
      Let $n, m, k$ be natural numbers.
      Then \[ n \mid m \implies n \mid k \cdot m. \]
    \end{corollary}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_07_7863858316181504}
      Let $n, m, k$ be natural numbers.
      Then \[ n \mid m \mid k \implies n \mid k. \]
    \end{proposition}
    \begin{proof}
      Assume $n \mid m$ and $m \mid k$.
      Take natural numbers $l,l'$ such that $n \cdot l = m$ and $m \cdot l' = k$.
      Then $n \cdot (l \cdot l')
        = (n \cdot l) \cdot l'
        = m \cdot l'
        = k$.
      Hence $n \mid k$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_07_4933275640397824}
      Let $n, m$ be natural numbers such that $n \neq 0$.
      Then \[ (\text{$n \mid m$ and $m \mid n$}) \implies n = m. \]
    \end{proposition}
    \begin{proof}
      Assume $n \mid m$ and $m \mid n$.
      Take natural numbers $k,k'$ such that $n \cdot k = m$ and $m \cdot k' = n$.
      Then $n
        = m \cdot k'
        = (n \cdot k) \cdot k'
        = n \cdot (k \cdot k')$.
      Hence $k \cdot k' = 1$.
      Thus $k = 1 = k'$.
      Therefore $n = m$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_07_1283495225720832}
      Let $n, m, k$ be natural numbers.
      Then \[ n \mid m \implies k \cdot n \mid k \cdot m. \]
    \end{proposition}
    \begin{proof}
      Assume $n \mid m$.
      Take a natural number $l$ such that $n \cdot l = m$.
      Then $(k \cdot n) \cdot l
        = k \cdot (n \cdot l)
        = k \cdot m$.
      Hence $k \cdot n \mid k \cdot m$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_07_6469492028735488}
      Let $n, m, k$ be natural numbers.
      Assume $k \neq 0$.
      Then \[ k \cdot n \mid k \cdot m \implies n \mid m. \]
    \end{proposition}
    \begin{proof}
      Assume $k \cdot n \mid k \cdot m$.
      Take a natural number $l$ such that $(k \cdot n) \cdot l = k \cdot m$.
      Then $k \cdot (n \cdot l) = k \cdot m$.
      Hence $n \cdot l = m$.
      Thus $n \mid m$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_07_4700711333920768}
      Let $n, m, k$ be natural numbers.
      Then \[ (\text{$k \mid n$ and $k \mid m$}) \implies
      (\text{$k \mid (n' \cdot n) + (m' \cdot m)$
      for all natural numbers $n', m'$}). \]
    \end{proposition}
    \begin{proof}
      Assume $k \mid n$ and $k \mid m$.
      Let $n', m'$ be natural numbers.
      Take natural numbers $l,l'$ such that $k \cdot l = n$ and $k \cdot l' = m$.
      Then
      \[  k \cdot ((n' \cdot l) + (m' \cdot l'))                \]
      \[    = (k \cdot (n' \cdot l)) + (k \cdot (m' \cdot l'))  \]
      \[    = ((k \cdot n') \cdot l) + ((k \cdot m') \cdot l')  \]
      \[    = (n' \cdot (k \cdot l)) + (m' \cdot (k \cdot l'))  \]
      \[    = (n' \cdot n) + (m' \cdot m).                      \]
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{corollary}\printlabel{ARITHMETIC_07_1556786209357824}
      Let $n, m, k$ be natural numbers.
      Then \[ (\text{$k \mid n$ and $k \mid m$}) \implies k \mid n + m. \]
    \end{corollary}
    \begin{proof}
      Assume $k \mid n$ and $k \mid m$.
      Take $n' = 1$ and $m' = 1$.
      Then $k \mid (n' \cdot n) + (m' \cdot m)$.
      $(n' \cdot n) + (m' \cdot m) = n + m$.
      Hence $k \mid n + m$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_07_1076947887063040}
      Let $n, m, k$ be natural numbers.
      Then \[ (\text{$k \mid n$ and $k \mid n + m$}) \implies k \mid m. \]
    \end{proposition}
    \begin{proof}
      Assume $k \mid n$ and $k \mid n + m$.

      Case $k = 0$. Obvious.

      Case $k \neq 0$.
        Take a natural number $l$ such that $n = k \cdot l$.
        Take a natural number $l'$ such that $n + m = k \cdot l'$.
        Then $(k \cdot l) + m = k \cdot l'$.
        We have $l' \geq l$.
        Indeed if $l' < l$ then
        $n + m
          = k \cdot l'
          < k \cdot l
          = n$.
        Hence we can take a natural number $l''$ such that $l' = l + l''$.
        Then $(k \cdot l) + m
          = k \cdot l'
          = k \cdot (l + l'')
          = (k \cdot l) + (k \cdot l'')$.
        Indeed $k \cdot (l + l'') = (k \cdot l) + (k \cdot l'')$
        (by \cref{ARITHMETIC_06_9001524774567936}).
        Thus $m = (k \cdot l'')$.
        Therefore $k \mid m$.
      End.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_07_2187144577679360}
      Let $n, m$ be natural numbers such that $n, m \neq 0$.
      Then \[ m \mid n \implies m \leq n. \]
    \end{proposition}
    \begin{proof}
      Assume $m \mid n$.
      Take a natural number $k$ such that $m \cdot k = n$.
      If $k = 0$ then
      $n
        = m \cdot k
        = m \cdot 0
        = 0$.
      Thus $k \geq 1$.
      Assume $m > n$.
      Then $n
        = m \cdot k
        \geq m \cdot 1
        = m
        > n$.
      Hence $n > n$.
      Contradiction.
    \end{proof}
  \end{forthel}
\end{document}
