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

\begin{document}
  \chapter{Euclidean division}\label{chapter:euclidean-division}

  \filename{arithmetic/sections/08_euclidean-division.ftl.tex}

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

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

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


  \section{Quotients and remainders}

  \begin{forthel}
    \begin{theorem}\printlabel{ARITHMETIC_08_7743986617810944}
      Let $n, m$ be natural numbers such that $m \neq 0$.
      Then there exist natural numbers $q, r$ such that
      \[ n = (m \cdot q) + r \] and $r < m$.
    \end{theorem}
    \begin{proof}
      Define $\Phi = \{ n' \in \Nat \mid$ there exist natural numbers $q, r$
      such that $r < m$ and $n' = (m \cdot q) + r \}$.

      (1) $\Phi$ contains $0$.
      Proof.
        Take $q = 0$ and $r = 0$.
        Then $r < m$ and $0 = (m \cdot q) + r$.
        Hence $0 \in \Phi$.
      Qed.

      (2) For all $n' \in \Phi$ we have $n' + 1 \in \Phi$.
      Proof.
        Let $n' \in \Phi$.

        Let us show that there exist natural numbers $q, r$ such that $r < m$
        and $n' + 1 = (m \cdot q) + r$.
          Take natural numbers $q', r'$ such that $r' < m$ and
          $n' = (m \cdot q') + r'$.
          We have $r' + 1 < m$ or $r' + 1 = m$.

          Case $r' + 1 < m$.
            Take $q = q' + 0$ and $r = r' + 1$. %!
            Then $r < m$ and $n' + 1
              = ((q' \cdot m) + r') + 1
              = (q' \cdot m) + (r' + 1)
              = (q \cdot m) + r$.
          End.

          Case $r' + 1 = m$.
            Take  $q = q' + 1$ and $r = 0$.
            Then $r < m$ and
            $n' + 1
              = ((q' \cdot m) + r') + 1
              = (q' \cdot m) + (r' + 1)
              = (q' \cdot m) + m
              = (q' \cdot m) + (1 \cdot m)
              = (q' + 1) \cdot m
              = (q \cdot m) + r$.
          End.
        End.

        Hence $n' + 1 \in \Phi$.
      Qed.

      Then $\Phi$ contains every natural number.
      Thus there exist natural numbers $q, r$ such that $n = (m \cdot q) + r$
      and $r < m$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_08_7801804481888256}
      Let $n, m$ be natural numbers such that $m \neq 0$.
      Let $q, r$ be natural numbers such that $(m \cdot q) + r = n$ and $r < m$.
      Let $q', r'$ be natural numbers such that $(m \cdot q') + r' = n$ and
      $r' < m$.
      Then $q = q'$ and $r = r'$.
    \end{proposition}
    \begin{proof}
      We have $(m \cdot q) + r = (m \cdot q') + r'$.

      Case $q \geq q'$ and $r \geq r'$.
        (1) $((m \cdot q) + r) - r' = (m \cdot q) + (r - r')$
        (by \cref{ARITHMETIC_05_7578468875239424}).
        (2) $((m \cdot q') + r') - r'
          = (m \cdot q') + (r' - r')
          = m \cdot q'$.
        Hence $(m \cdot q) + (r - r') = m \cdot q'$.
        Thus $((m \cdot q) - (m \cdot q')) + (r - r') = 0$.
        Consequently $(m \cdot q) - (m \cdot q') = 0$ and $r - r' = 0$.
        If $(m \cdot q) - (m \cdot q') = 0$ then $q - q' = 0$.
        Therefore $q - q' = 0$ and $r - r' = 0$.
        Thus we have $q = q'$ and $r = r'$.
      End.

      Case $q \geq q'$ and $r < r'$.
        Take $q'' = q - q'$ and $r'' = r' - r$.
        Then $(m \cdot (q' + q'')) + r = (m \cdot q') + (r + r'')$.
        We have $(m \cdot q') + (r + r'')
          = (m \cdot q') + (r'' + r)
          = ((m \cdot q') + r'') + r$.
        Hence $(m \cdot (q' + q'')) + r = ((m \cdot q') + r'') + r$.
        Thus $m \cdot (q' + q'') = (m \cdot q') + r''$
        (by \cref{ARITHMETIC_03_3137702874578944}).
        We have $m \cdot (q' + q'') = (m \cdot q') + (m \cdot q'')$.
        Hence $(m \cdot q') + (m \cdot q'') = (m \cdot q') + r''$.
        [prover vampire]
        Thus $m \cdot q'' = r''$ (by \cref{ARITHMETIC_03_8445946379632640}).
        Then we have $m \cdot q'' < m \cdot 1$.
        Indeed $m \cdot q''
          = r''
          \leq r'
          < m
          = m \cdot 1$.
        Therefore $q'' < 1$ (by \cref{ARITHMETIC_06_5048640368279552}).
        Consequently $q - q' = q'' = 0$.
        Hence $q = q'$.
        Thus $(m \cdot q) + r = (m \cdot q) + r'$.
        Therefore $r = r'$.
      End.

      Case $q < q'$ and $r \geq r'$.
        Take $q'' = q' - q$ and $r'' = r - r'$.
        Then $(m \cdot q) + (r' + r'') = (m \cdot (q + q'')) + r'$.
        We have $(m \cdot q) + (r' + r'')
          = (m \cdot q) + (r'' + r')
          = ((m \cdot q) + r'') + r'$.
        Hence $((m \cdot q) + r'') + r' = (m \cdot (q + q'')) + r'$.
        Thus $(m \cdot q) + r'' = m \cdot (q + q'')$
        (by \cref{ARITHMETIC_03_3137702874578944}).
        We have $m \cdot (q + q'') = (m \cdot q) + (m \cdot q'')$.
        Hence $(m \cdot q) + r'' = (m \cdot q) + (m \cdot q'')$.
        [prover vampire]
        Thus $r'' = m \cdot q''$.
        Then we have $m \cdot q'' < m \cdot 1$.
        Indeed $m \cdot q''
          = r''
          \leq r
          < m
          = m \cdot 1$.
        Therefore $q'' < 1$ (by \cref{ARITHMETIC_06_5048640368279552}).
        Consequently $q' - q = q'' = 0$.
        Hence $q' = q$.
        Thus $(m \cdot q) + r = (m \cdot q) + r'$.
        Therefore $r = r'$.
      End.

      Case $q < q'$ and $r < r'$.
        (1) $((m \cdot q') + r') - r = (m \cdot q') + (r' - r)$
        (by \cref{ARITHMETIC_05_7578468875239424}).
        (2) $((m \cdot q) + r) - r
          = (m \cdot q) + (r - r)
          = m \cdot q$.
        Hence $(m \cdot q') + (r' - r) = m \cdot q$.
        Thus $((m \cdot q') - (m \cdot q)) + (r' - r) = 0$.
        Consequently $(m \cdot q') - (m \cdot q) = 0$ and $r' - r = 0$.
        If $(m \cdot q') - (m \cdot q) = 0$ then $q' - q = 0$.
        Therefore $q' - q = 0$ and $r' - r = 0$.
        Thus we have $q' = q$ and $r' = r$.
      End.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_08_8621463798022144}
      Let $n, m$ be natural numbers such that $m \neq 0$.
      $n \div m$ is the natural number $q$ such that $n = (m \cdot q) + r$ for
      some natural number $r$ that is less than $m$.
    \end{definition}

    Let the quotient of $n$ over $m$ stand for $n \div m$.
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_08_3560980160184320}
      Let $n, m$ be natural numbers such that $m \neq 0$.
      $n \mod m$ is the natural number $r$ such that $r < m$ and there exists a
      natural number $q$ such that $n = (m \cdot q) + r$.
    \end{definition}

    Let the remainder of $n$ over $m$ stand for $n \mod m$.
  \end{forthel}


  \section{Modular arithmetic}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_08_5448561831444480}
      Let $n, m, k$ be natural numbers such that $k \neq 0$.
      $n \equiv m \pmod{k}$ iff $n \mod k = m \mod k$.
    \end{definition}

    Let $n$ and $m$ are congruent modulo $k$ stand for $n \equiv m \pmod{k}$.
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_08_3818318544764928}
      Let $n, k$ be natural numbers such that $k \neq 0$.
      Then \[ n \equiv n \pmod{k}. \]
    \end{proposition}
    \begin{proof}
      We have $n \mod k = n \mod k$.
      Hence $n \equiv n \pmod{k}$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_08_2337210737098752}
      Let $n, m, k$ be natural numbers such that $k \neq 0$.
      Then \[ n \equiv m \pmod{k} \implies m \equiv n \pmod{k}. \]
    \end{proposition}
    \begin{proof}
      Assume $n \equiv m \pmod{k}$.
      Then $n \mod k = m \mod k$.
      Hence $m \mod k = n \mod k$.
      Thus $m \equiv n \pmod{k}$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_08_7464329746055168}
      Let $n, m, l, k$ be natural numbers such that $k \neq 0$.
      Then \[ (\text{$n \equiv m \pmod{k}$ and $m \equiv l \pmod{k}$}) \implies
      n \equiv l \pmod{k}. \]
    \end{proposition}
    \begin{proof}
      Assume $n \equiv m \pmod{k}$ and $m \equiv l \pmod{k}$.
      Then $n \mod k = m \mod k$ and $m \mod k = l \mod k$.
      Hence $n \mod k = l \mod k$.
      Thus $n \equiv l \pmod{k}$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_08_2034122983735296}
      Let $n, m, k$ be natural numbers such that $k \neq 0$.
      Assume $n \geq m$.
      Then $n \equiv m \pmod{k}$ iff $n = (k \cdot x) + m$ for some natural
      number $x$.
    \end{proposition}
    \begin{proof}
      Case $n \equiv m \pmod{k}$.
        Then $n \mod k = m \mod k$.
        Take a natural number $r$ such that $r < k$ and
        $n \mod k = r = m \mod k$.
        Take a nonzero natural number $l$ such that $k = r + l$.
        Consider natural numbers $q,q'$ such that $n = (q \cdot k) + r$ and
        $m = (q' \cdot k) + r$.

        Then $q \geq q'$. \\
        Proof.
          Assume the contrary.
          Then $q < q'$.
          Hence $q \cdot k < q' \cdot k$.
          Thus $(q \cdot k) + r < (q' \cdot k) + r$
          (by \cref{ARITHMETIC_04_7354062662008832}).
          Indeed $q \cdot k$ and $q' \cdot k$ are natural numbers.
          Therefore $n < m$.
          Contradiction.
        Qed.

        Take a natural number $x$ such that $q = q' + x$.

        Let us show that $n = (k \cdot x) + m$.
          We have
          \[  (k \cdot x) + m                       \]
          \[    = (k \cdot x) + ((q' \cdot k) + r)  \]
          \[    = ((k \cdot x) + (q' \cdot k)) + r  \]
          \[    = ((k \cdot x) + (k \cdot q')) + r  \]
          \[    = (k \cdot (q' + x)) + r            \]
          \[    = (k \cdot q) + r                   \]
          \[    = n.                                \]
        End.
      End.

      Case $n = (k \cdot x) + m$ for some natural number $x$.
        Consider a natural number $x$ such that $n = (k \cdot x) + m$.
        Take natural numbers $r, r'$ such that $n \mod k = r$ and
        $m \mod k = r'$.
        Then $r, r' < k$.
        Take natural numbers $q, q'$ such that $n = (k \cdot q) + r$ and
        $m = (k \cdot q') + r'$.
        Then
        \[  (k \cdot q) + r                         \]
        \[    = n                                   \]
        \[    = (k \cdot x) + m                     \]
        \[    = (k \cdot x) + ((k \cdot q') + r')   \]
        \[    = ((k \cdot x) + (k \cdot q')) + r'   \]
        \[    = (k \cdot (x + q')) + r'.            \]
        Hence $r = r'$.
        Thus $n \mod k = m \mod k$.
        Therefore $n \equiv m \pmod{k}$.
      End.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_08_2988318228742144}
      Let $n, m, k, k'$ be natural numbers such that $k, k' \neq 0$.
      Then \[ n \equiv m \pmod{k \cdot k'} \implies n \equiv m \pmod{k}. \]
    \end{proposition}
    \begin{proof}
      Assume $n \equiv m \pmod{k \cdot k'}$.

      Case $n \geq m$.
        We can take a natural number $x$ such that
        $n = ((k \cdot k') \cdot x) + m$.
        Then $n = (k \cdot (k' \cdot x)) + m$.
        Hence $n \equiv m \pmod{k}$.
      End.

      Case $m \geq n$.
        We have $m \equiv n \pmod{k \cdot k'}$.
        Hence we can take a natural number $x$ such that
        $m = ((k \cdot k') \cdot x) + n$.
        Then $m = (k \cdot (k' \cdot x)) + n$.
        Thus $m \equiv n \pmod{k}$.
        Therefore $n \equiv m \pmod{k}$.
      End.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{corollary}\printlabel{ARITHMETIC_08_5895145169879040}
      Let $n, m, k, k'$ be natural numbers such that $k, k' \neq 0$.
      Then \[ n \equiv m \pmod{k \cdot k'} \implies n \equiv m \pmod{k'}. \]
    \end{corollary}
    \begin{proof}
      Assume $n \equiv m \pmod{k \cdot k'}$.
      Then $n \equiv m \pmod{k' \cdot k}$.
      Hence $n \equiv m \pmod{k'}$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_08_5984712287846400}
      Let $n, k$ be natural numbers such that $k \neq 0$.
      Then \[ n + k \equiv n \pmod{k}. \]
    \end{proposition}
    \begin{proof}
      Take $r = n \mod k$ and $r' = (n + k) \mod k$.
      Consider a $q \in \Nat$ such that $n = (k \cdot q) + r$ and $r < k$.
      Consider a $q' \in \Nat$ such that $n + k = (k \cdot q') + r'$ and
      $r' < k$.
      Then $(k \cdot q') + r'
        = n + k
        = ((k \cdot q) + r) + k
        = (k + (k \cdot q)) + r
        = (k \cdot (q + 1)) + r$.
      Hence $r = r'$.
      Consequently $n \mod k = (n + k) \mod k$.
      Thus $n + k \equiv n \pmod{k}$.
    \end{proof}
  \end{forthel}
\end{document}
