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

\begin{document}
  \chapter{Multiplication}\label{chapter:multiplication}

  \filename{arithmetic/sections/05_multiplication.ftl.tex}

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

    [readtex \path{arithmetic/sections/05_subtraction.ftl.tex}]

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


  \section{Definition of multiplication}

  \begin{forthel}
    \begin{lemma}\printlabel{ARITHMETIC_06_7897906468093952}
      There exists a $\varphi : \Nat \times \Nat \to \Nat$ such
      that for all $n \in \Nat$ we have $\varphi(n, 0) = 0$ and
      $\varphi(n, m + 1) = \varphi(n,m) + n$ for any $m \in \Nat$.
    \end{lemma}
    \begin{proof}
      Take $A = [\Nat \to \Nat]$.
      Define $a(n) = 0$ for $n \in \Nat$.
      Then $A$ is a set and $a \in A$.

      [skipfail on] % Wrong proof task %!!
      Define $f(g) = \fun n \in \Nat. g(n) + n$ for $g \in A$.
      [skipfail off]

      Then $f : A \to A$.
      Indeed $f(g)$ is a map from $\Nat$ to $\Nat$ for any $g \in A$.
      Consider a $\psi : \Nat \to A$ such that $\psi$ is recursively defined by
      $a$ and $f$ (by \cref{ARITHMETIC_02_2489427471368192}).
      For any objects $n, m$ we have $(n,m) \in \Nat \times \Nat$ iff
      $n, m \in \Nat$.
      Define $\varphi(n,m) = \psi(m)(n)$ for $(n,m) \in \Nat \times \Nat$.
      Then $\varphi$ is a map from $\Nat \times \Nat$ to $\Nat$.
      Indeed $\varphi(n,m) \in \Nat$ for all $n, m \in \Nat$.

      (1) For all $n \in \Nat$ we have $\varphi(n,0) = 0$. \\
      Proof.
        Let $n \in \Nat$.
        Then $\varphi(n,0)
          = \psi(0)(n)
          = a(0)
          = 0$.
      Qed.

      (2) For all $n, m \in \Nat$ we have $\varphi(n, m + 1) =
      \varphi(n,m) + n$. \\
      Proof.
        Let $n, m \in \Nat$.
        Then $\varphi(n, m + 1)
          = \psi(m + 1)(n)
          = f(\psi(m))(n)
          = \psi(m)(n) + n
          = \varphi(n,m) + n$.
      Qed.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{lemma}\printlabel{ARITHMETIC_06_2076592937369600}
      Let $\varphi, \varphi' : \Nat \times \Nat \to \Nat$.
      Assume that for all $n \in \Nat$ we have $\varphi(n, 0) = 0$ and
      $\varphi(n, m + 1) = \varphi(n,m) + n$ for any $m \in \Nat$.
      Assume that for all $n \in \Nat$ we have $\varphi'(n, 0) = 0$ and
      $\varphi'(n, m + 1) = \varphi'(n,m) + n$ for any $m \in \Nat$.
      Then $\varphi = \varphi'$.
    \end{lemma}
    \begin{proof}
      Define $\Phi = \{ m \in \Nat \mid \varphi(n,m) = \varphi'(n,m)$ for
      all $n \in \Nat \}$.

      (1) $0 \in \Phi$.
      Indeed $\varphi(n,0) = 0 = \varphi'(n,0)$ for all $n \in \Nat$.

      (2) For all $m \in \Phi$ we have $m + 1 \in \Phi$. \\
      Proof.
        Let $m \in \Phi$.
        Then $\varphi(n,m) = \varphi'(n,m)$ for all $n \in \Nat$.
        Hence $\varphi(n, m + 1)
          = \varphi(n,m) + n
          = \varphi'(n,m) + n
          = \varphi'(n, m + 1)$
        for all $n \in \Nat$.
      Qed.

      Thus $\Phi$ contains every natural number.
      Therefore $\varphi(n,m) = \varphi'(n,m)$ for all $n, m \in \Nat$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_06_6626346484629504}
      $\mul$ is the map from $\Nat \times \Nat$ to $\Nat$ such that for all
      $n \in \Nat$ we have $\mul(n, 0) = 0$ and $\mul(n, m + 1) =
      \mul(n, m) + n$ for any $m \in \Nat$.
    \end{definition}

    Let $n \cdot m$ stand for $\mul(n, m)$.
    Let the product of $n$ and $m$ stand for $n \cdot m$.
  \end{forthel}

  \begin{forthel}
    \begin{lemma}\printlabel{ARITHMETIC_06_1682857820946432}
      Let $n, m$ be natural numbers.
      Then $(n,m) \in \dom(\mul)$.
    \end{lemma}
  \end{forthel}

  \begin{forthel}
    \begin{lemma}\printlabel{ARITHMETIC_06_8420678923452416}
      Let $n, m$ be natural numbers.
      Then $n \cdot m$ is a natural number.
    \end{lemma}
  \end{forthel}

  \begin{forthel}
    \begin{lemma}\printlabel{ARITHMETIC_06_8941041092657152}
      Let $n$ be a natural number.
      Then $n \cdot 0 = 0$.
    \end{lemma}
  \end{forthel}

  \begin{forthel}
    \begin{lemma}\printlabel{ARITHMETIC_06_2211275408932864}
      Let $n, m$ be natural numbers.
      Then $n \cdot (m + 1) = (n \cdot m) + n$.
    \end{lemma}
  \end{forthel}


  \section{Computation laws}

  \subsection*{Distributivity}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_06_9001524774567936}
      Let $n, m, k$ be natural numbers.
      Then \[ n \cdot (m + k) = (n \cdot m) + (n \cdot k). \]
    \end{proposition}
    \begin{proof}
      Define $\Phi = \{ k' \in \Nat \mid n \cdot (m + k') =
      (n \cdot m) + (n \cdot k') \}$.

      (1) $0$ is an element of $\Phi$.
      Indeed $n \cdot (m + 0)
        = n \cdot m
        = (n \cdot m) + 0
        = (n \cdot m) + (n \cdot 0)$.

      (2) For all $k' \in \Phi$ we have $k' + 1 \in \Phi$. \\
      Proof.
        Let $k'\in \Phi$.
        Then
        \[  n \cdot (m + (k' + 1))                  \]
        \[    = n \cdot ((m + k') + 1)              \]
        \[    = (n \cdot (m + k')) + n              \]
        \[    = ((n \cdot m) + (n \cdot k')) + n    \]
        \[    = (n \cdot m) + ((n \cdot k') + n)    \]
        \[    = (n \cdot m) + (n \cdot (k' + 1)).   \]
        Hence $n \cdot (m + (k' + 1)) = (n \cdot m) + (n \cdot (k' + 1))$.
        Thus $k' + 1 \in \Phi$.
      Qed.

      Thus every natural number is contained in $\Phi$.
      Therefore $n \cdot (m + k) = (n \cdot m) + (n \cdot k)$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_06_5742967566368768}
      Let $n, m, k$ be natural numbers.
      Then \[ (n + m) \cdot k = (n \cdot k) + (m \cdot k). \]
    \end{proposition}
    \begin{proof}
      Define $\Phi = \{ k' \in \Nat \mid (n + m) \cdot k' =
      (n \cdot k') + (m \cdot k') \}$.

      (1) $0$ belongs to $\Phi$.
      Indeed $(n + m) \cdot 0
        = 0
        = 0 + 0
        = (n \cdot 0) + (m \cdot 0)$.

      (2) For all $k' \in \Phi$ we have $k' + 1 \in \Phi$. \\
      Proof.
        Let $k' \in \Phi$.
        Then
        \[  (n + m) \cdot (k' + 1)                        \]
        \[    = ((n + m) \cdot k') + (n + m)              \]
        \[    = ((n \cdot k') + (m \cdot k')) + (n + m)   \]
        \[    = (((n \cdot k') + (m \cdot k')) + n) + m   \]
        \[    = ((n \cdot k') + ((m \cdot k') + n)) + m   \]
        \[    = ((n \cdot k') + (n + (m \cdot k'))) + m   \]
        \[    = (((n \cdot k') + n) + (m \cdot k')) + m   \]
        \[    = ((n \cdot k') + n) + ((m \cdot k') + m)   \]
        \[    = (n \cdot (k' + 1)) + (m \cdot (k' + 1)).  \]
        Thus $(n + m) \cdot (k' + 1) = (n \cdot (k' + 1)) + (m \cdot (k' + 1))$.
      Qed.

      Thus every natural number is an element of $\Phi$.
      Therefore $(n + m) \cdot k = (n \cdot k) + (m \cdot k)$.
    \end{proof}
  \end{forthel}


  \subsection*{Multiplication with $1$ and $2$}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_06_2910559821365248}
      Let $n$ be a natural number.
      Then \[ n \cdot 1 = n. \]
    \end{proposition}
    \begin{proof}
      $n \cdot 1
        = n \cdot (0 + 1)
        = (n \cdot 0) + n
        = 0 + n
        = n$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{corollary}\printlabel{ARITHMETIC_06_5679541582299136}
      Let $n$ be a natural number.
      Then \[ n \cdot 2 = n + n. \]
    \end{corollary}
    \begin{proof}
      $n \cdot 2
        = n \cdot (1 + 1)
        = (n \cdot 1) + n
        = n + n$.
    \end{proof}
  \end{forthel}


  \subsection*{Associativity}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_06_347295585402880}
      Let $n, m, k$ be natural numbers.
      Then \[ n \cdot (m \cdot k) = (n \cdot m) \cdot k. \]
    \end{proposition}
    \begin{proof}
      Define $\Phi = \{ k' \in \Nat \mid n \cdot (m \cdot k') =
      (n \cdot m) \cdot k' \}$.

      (1) $0$ is contained in $\Phi$.
      Indeed $n \cdot (m \cdot 0)
        = n \cdot 0
        = 0
        = (n \cdot m) \cdot 0$.

      (2) For all $k' \in \Phi$ we have $k' + 1 \in \Phi$. \\
      Proof.
        Let $k' \in \Phi$.
        Then
        \[  n \cdot (m \cdot (k' + 1))                          \]
        \[    = n \cdot ((m \cdot k') + m)                      \]
        \[    = (n \cdot (m \cdot k')) + (n \cdot m)            \]
        \[    = ((n \cdot m) \cdot k') + (n \cdot m)            \]
        \[    = ((n \cdot m) \cdot k') + ((n \cdot m) \cdot 1)  \]
        \[    = (n \cdot m) \cdot (k' + 1).                     \]
      Qed.

      Hence every natural number is contained in $\Phi$.
      Thus $n \cdot (m \cdot k) = (n \cdot m) \cdot k$.
    \end{proof}
  \end{forthel}


  \subsection*{Commutativity}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_06_1764759896588288}
      Let $n, m$ be natural numbers.
      Then \[ n \cdot m = m \cdot n. \]
    \end{proposition}
    \begin{proof}
      Define $\Phi = \{ m' \in \Nat \mid n \cdot m' = m' \cdot n \}$.

      (1) $0$ is contained in $\Phi$. \\
      Proof.
        Define $\Psi = \{ n' \in \Nat \mid n' \cdot 0 = 0 \cdot n' \}$.

        (1a) $0$ is contained in $\Psi$.

        (1b) For all $n' \in \Psi$ we have $n' + 1 \in \Psi$. \\
        Proof.
          Let $n' \in \Psi$.
          Then
          \[ (n' + 1) \cdot 0
            = 0
            = n' \cdot 0
            = 0 \cdot n'
            = (0 \cdot n') + 0
            = 0 \cdot (n' + 1). \]
        Qed.

        Hence every natural number is contained in $\Psi$.
        Thus $n \cdot 0 = 0 \cdot n$.
      Qed.

      (2) $1$ belongs to $\Phi$. \\
      Proof.
        Define $\Theta = \{ n' \in \Nat \mid n' \cdot 1 = 1 \cdot n' \}$.

        (2a) $0$ is contained in $\Theta$.

        (2b) For all $n' \in \Theta$ we have $n' + 1 \in \Theta$. \\
        Proof.
          Let $n' \in \Theta$.
          Then
          \[  (n' + 1) \cdot 1        \]
          \[    = (n' \cdot 1) + 1    \]
          \[    = (1 \cdot n') + 1    \]
          \[    = 1 \cdot (n' + 1).   \]
        Qed.

        Thus every natural number is contained in $\Theta$.
        Therefore $n \cdot 1 = 1 \cdot n$.
      Qed.

      (3) For all $m' \in \Phi$ we have $m' + 1 \in \Phi$. \\
      Proof.
        Let $m' \in \Phi$.
        Then
        \[  n \cdot (m' + 1)                \]
        \[    = (n \cdot m') + (n \cdot 1)  \]
        \[    = (m' \cdot n) + (1 \cdot n)  \]
        \[    = (1 \cdot n) + (m' \cdot n)  \]
        \[    = (1 + m') \cdot n            \]
        \[    = (m' + 1) \cdot n.           \]
        Indeed $((1 \cdot n) + (m' \cdot n)) = (1 + m') \cdot n$. %!
      Qed.

      Hence every natural number is contained in $\Phi$.
      Thus $n \cdot m = m \cdot n$.
    \end{proof}
  \end{forthel}


  \subsection*{Non-existence of zero-divisors}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_06_3843962875936768}
      Let $n, m$ be natural numbers such that $n \cdot m = 0$.
      Then $n = 0$ or $m = 0$.
    \end{proposition}
    \begin{proof}
      Suppose $n, m \neq 0$.
      Take natural numbers $n', m'$ such that $n = (n' + 1)$ and $m = (m' + 1)$.
      Then
      \[  0                                     \]
      \[    = n \cdot m                         \]
      \[    = (n' + 1) \cdot (m' + 1)           \]
      \[    = ((n' + 1) \cdot m') + (n' + 1)    \]
      \[    = (((n' + 1) \cdot m') + n') + 1.   \]
      Hence $0 = k + 1$ for some natural number $k$.
      Contradiction.
    \end{proof}
  \end{forthel}


  \subsection*{Cancellation}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_06_31055184658432}
      Let $n, m, k$ be natural numbers.
      Assume $k \neq 0$.
      Then \[ n \cdot k = m \cdot k \implies n = m. \]
    \end{proposition}
    \begin{proof}
      Define $\Phi = \{ n' \in \Nat \mid$ for all $m' \in \Nat$ if
      $n' \cdot k = m' \cdot k$ and $k \neq 0$ then $n' = m' \}$.

      (1) $0$ is contained in $\Phi$. \\
      Proof.
        Let $m' \in \Nat$.
        Assume $0 \cdot k = m' \cdot k$ and $k \neq 0$.
        Then $m' \cdot k = 0$.
        Hence $m' = 0$ or $k = 0$.
        Thus $m' = 0$.
      Qed.

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

        Let us show that for all $m' \in \Nat$ if $(n' + 1) \cdot k =
        m' \cdot k$ and $k \neq 0$ then $n' + 1 = m'$.
          Let $m' \in \Nat$.
          Assume $(n' + 1) \cdot k = m' \cdot k$ and $k \neq 0$.

          Case $m' = 0$.
            Then $(n' + 1) \cdot k = 0$.
            Hence $n' + 1 = 0$.
            Contradiction.
          End.

          Case $m' \neq 0$.
            Take a natural number $l$ such that $m' = l + 1$.
            Then $(n' + 1) \cdot k = (l + 1) \cdot k$.
            Hence $(n' \cdot k) + k
              = (n' \cdot k) + (1 \cdot k)
              = (n' \cdot k) + k
              = (l + 1) \cdot k
              = (l \cdot k) + (1 \cdot k)
              = (l \cdot k) + k$.
            Thus $n' \cdot k = l \cdot k$.
            Then we have $n' = l$.
            Indeed if $n' \cdot k = l \cdot k$ and $k \neq 0$ then $n' = l$.
            Therefore $n' + 1 = l + 1 = m'$.
          End.
        End.

        [prover vampire]
        Hence $n' + 1 \in \Phi$.
      Qed.

      Thus every natural number is contained in $\Phi$.
      Therefore if $n \cdot k = m \cdot k$ then $n = m$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{corollary}\printlabel{ARITHMETIC_06_8575191374364672}
      Let $n, m, k$ be natural numbers.
      Assume $k \neq 0$.
      Then \[ k \cdot n = k \cdot m \implies n = m. \]
    \end{corollary}
    \begin{proof}
      Assume $k \cdot n = k \cdot m$.
      We have $k \cdot n = n \cdot k$ and $k \cdot m = m \cdot k$.
      Hence $n \cdot k = m \cdot k$.
      Thus $n = m$ (by \cref{ARITHMETIC_06_31055184658432}).
    \end{proof}
  \end{forthel}


  \section{Ordering and multiplication}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_06_8817333933965312}
      Let $n, m, k$ be natural numbers.
      Assume $k \neq 0$.
      Then \[ n < m \iff n \cdot k < m \cdot k. \]
    \end{proposition}
    \begin{proof}
      Case $n \cdot k < m \cdot k$.
        Define $\Phi = \{ n' \in \Nat \mid$ if $n' \cdot k < m \cdot k$ then
        $n' < m \}$.

        (1) $\Phi$ contains $0$.

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

          Let us show that if $(n' + 1) \cdot k < m \cdot k$ then $n' + 1 < m$.
            Assume $(n' + 1) \cdot k < m \cdot k$.
            Then $(n' \cdot k) + k < m \cdot k$.
            Hence $n' \cdot k < m \cdot k$.
            Thus $n' < m$.
            Then $n' + 1 \leq m$.
            If $n' + 1 = m$ then $(n' + 1) \cdot k = m \cdot k$.
            Hence $n' + 1 < m$.
          End.
        Qed.

        Therefore every natural number is contained in $\Phi$.
        Consequently $n < m$.
      End.

      Case $n < m$.
        Take a positive natural number $l$ such that $m = n + l$.
        Then $m \cdot k = (n + l) \cdot k = (n \cdot k) + (l \cdot k)$.
        $l \cdot k$ is positive.
        Hence $n \cdot k < m \cdot k$.
      End.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{corollary}\printlabel{ARITHMETIC_06_5048640368279552}
      Let $n, m, k$ be natural numbers.
      Assume $k \neq 0$.
      Then \[ n < m \iff k \cdot n < k \cdot m. \]
    \end{corollary}
    \begin{proof}
      We have $k \cdot n = n \cdot k$ and $k \cdot m = m \cdot k$.
      Hence $k \cdot n < k \cdot m$ iff $n \cdot k < m \cdot k$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_06_1826268599287808}
      Let $n, m, k$ be natural numbers.
      Then \[ n, m > k \implies n \cdot m > k. \]
    \end{proposition}
    \begin{proof}
      Define $\Phi = \{ n' \in \Nat \mid$ if $n', m > k$ then $n' \cdot m > k \}$.

      (1) $\Phi$ contains $0$.

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

        Let us show that if $n' + 1, m > k$ then $(n' + 1) \cdot m > k$.
          Assume $n' + 1, m > k$.
          Then $(n' + 1) \cdot m = (n' \cdot m) + m$.
          If $n' = 0$ then
          $(n' \cdot m) + m
            = 0 + m
            = m
            > k$.
          If $n' \neq 0$ then
          $(n' \cdot m) + m
            > m
            > k$.
          Indeed if $n' \neq 0$ then $n' \cdot m > 0$.
          Indeed $m > 0$.
          Hence $(n' + 1) \cdot m > k$.
        Qed.
      Qed.

      Thus every natural number is contained in $\Phi$.
      Therefore if $n, m > k$ then $n \cdot m > k$.
    \end{proof}
  \end{forthel}

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

  \begin{forthel}
    \begin{corollary}\printlabel{ARITHMETIC_06_3965209318260736}
      Let $n, m, k$ be natural numbers.
      Assume $k \neq 0$.
      Then \[ k \cdot n \leq k \cdot m \implies n \leq m. \]
    \end{corollary}
  \end{forthel}

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

  \begin{forthel}
    \begin{corollary}\printlabel{ARITHMETIC_06_4374428949413888}
      Let $n, m, k$ be natural numbers.
      Assume $k \neq 0$.
      Then \[ n \cdot k \leq m \cdot k \implies n \leq m. \]
    \end{corollary}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_06_8813409145454592}
      Let $n, m, k$ be natural numbers.
      Assume $m > 0$ and $k > 1$.
      Then $k \cdot m > m$.
    \end{proposition}
    \begin{proof}
      Take a natural number $l$ such that $k = l + 2$.
      Then
      \[  k \cdot m                       \]
      \[    = (l + 2) \cdot m             \]
      \[    = (l \cdot m) + (2 \cdot m)   \]
      \[    = (l \cdot m) + (m + m)       \]
      \[    = ((l \cdot m) + m) + m       \]
      \[    = ((l + 1) \cdot m) + m       \]
      \[    \geq 1 + m                    \]
      \[    > m.                          \]
      Indeed $((l + 1) \cdot m) + m \geq 1 + m$.
    \end{proof}
  \end{forthel}


  \section{Multiplication and subtraction}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_06_5458841930039296}
      Let $n, m, k$ be natural numbers such that $n \geq m$.
      Then \[ (n - m) \cdot k = (n \cdot k) - (m \cdot k). \]
    \end{proposition}
    \begin{proof}
      We have
      \[  ((n - m) \cdot k) + (m \cdot k)                 \]
      \[    = ((n - m) + m) \cdot k                       \]
      \[    = n \cdot k                                   \]
      \[    = ((n \cdot k) - (m \cdot k)) + (m \cdot k).  \]

      Hence $(n - m) \cdot k = (n \cdot k) - (m \cdot k)$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{corollary}\printlabel{ARITHMETIC_06_8461123277815808}
      Let $n, m, k$ be natural numbers such that $n \geq m$.
      Then \[ k \cdot (n - m) = (k \cdot n) - (k \cdot m). \]
    \end{corollary}
  \end{forthel}
\end{document}
