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

\begin{document}
  \chapter{Ordering}\label{chapter:ordering}

  \filename{arithmetic/sections/04_ordering.ftl.tex}

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

    [readtex \path{foundations/sections/11_binary-relations.ftl.tex}]

    [readtex \path{arithmetic/sections/03_addition.ftl.tex}]

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


  \section{Definitions and immediate consequences}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_04_1926295512416256}
      Let $n, m$ be natural numbers.
      $n < m$ iff there exists a nonzero natural number $k$ such that
      $m = n + k$.
    \end{definition}

    Let $n$ is less than $m$ stand for $n < m$.
    Let $n > m$ stand for $m < n$.
    Let $n$ is greater than $m$ stand for $n > m$.
    Let $n \nless m$ stand for $n$ is not less than $m$.
    Let $n \ngtr m$ stand for $n$ is not greater than $m$.
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_04_3668680374222848}
      Let $n$ be a natural number.
      $\Nat_{< n} = \{ k \in \Nat \mid k < n \}$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_04_3670333934534656}
      Let $n$ be a natural number.
      $\Nat_{> n} = \{ k \in \Nat \mid k > n \}$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_04_7916616566177792}
      Let $n$ be a natural number.
      $n$ is positive iff $n > 0$.
    \end{definition}
  \end{forthel}

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

    Let $n$ is less than or equal to $m$ stand for $n \leq m$.
    Let $n \geq m$ stand for $m \leq n$.
    Let $n$ is greater than or equal to $m$ stand for $n \geq m$.
    Let $n \nleq m$ stand for $n$ is not less than or equal to $m$.
    Let $n \ngeq m$ stand for $n$ is not greater than or equal to $m$.
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_04_72501526790144}
      Let $n$ be a natural number.
      $\Nat_{\leq n} = \{ k \in \Nat \mid k \leq n \}$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_04_1706933421604864}
      Let $n$ be a natural number.
      $\Nat_{\geq n} = \{ k \in \Nat \mid k \geq n \}$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_04_5385415374667776}
      Let $n, m$ be natural numbers.
      $n \leq m$ iff $n < m$ or $n = m$.
    \end{proposition}
    \begin{proof}
      Case $n \leq m$.
        Take a natural number $k$ such that $m = n + k$.
        If $k = 0$ then $n = m$. If $k \neq 0$ then $n < m$.
      End.

      Case $n < m$ or $n = m$.
        If $n < m$ then there is a positive natural number $k$ such that
        $m = n + k$.
        If $n = m$ then $m = n + 0$.
        Thus if $n < m$ then there is a natural number $k$ such that
        $m = n + k$.
      End.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_04_6232154608500736}
      Let $n$ be a natural number.
      A predecessor of $n$ is a natural number that is less than $n$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_04_8147686326796288}
      Let $n$ be a natural number.
      A successor of $n$ is a natural number that is greater than $n$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_04_4826285599621120}
      Let $n$ be a natural number.
      Then $n$ is positive iff $n$ is nonzero.
    \end{proposition}
    \begin{proof}
      Case $n$ is positive.
        Take a positive natural number $k$ such that $n = 0 + k = k$.
        Then we have $n \neq 0$.
      End.

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


  \section{Basic properties}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_04_1037693395927040}
      Let $n$ be a natural number.
      Then \[ n \nless n. \]
    \end{proposition}
    \begin{proof}
      Assume the contrary.
      Then we can take a positive natural number $k$ such that $n = n + k$.
      Then we have $0 = k$.
      Contradiction.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_04_8266284905005056}
      Let $n, m$ be natural numbers.
      Then \[ n < m \implies n \neq m. \]
    \end{proposition}
    \begin{proof}
      Assume $n < m$.
      Take a positive natural number $k$ such that $m = n + k$.
      If $n = m$ then $k = 0$.
      Hence $n \neq m$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_04_4190604718243840}
      Let $n, m$ be natural numbers.
      Then \[ (\text{$n \leq m$ and $m \leq n$}) \implies n = m. \]
    \end{proposition}
    \begin{proof}
      Assume $n \leq m$ and $m \leq n$.
      Take natural numbers $k, l$ such that $m = n + k$ and $n = m + l$.
      Then $m
        = (m + l) + k
        = m + (l + k)$.
      Hence $l + k = 0$.
      Thus $l = 0 = k$.
      Indeed if $l \neq 0$ or $k \neq 0$ then $l + k$ is the direct successor of
      some natural number.
      Therefore $m = n$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_04_6413905244979200}
      Let $n, m, k$ be natural numbers.
      Then \[ n < m < k \implies n < k. \]
    \end{proposition}
    \begin{proof}
      Assume $n < m < k$.
      Take a positive natural number $a$ such that $m = n + a$.
      Take a positive natural number $b$ such that $k = m + b$.
      Then $k
        = (n + a) + b
        = n + (a + b)$.
      $a + b$ is positive.
      Hence $n < k$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_04_5480385953660928}
      Let $n, m, k$ be natural numbers.
      Then \[ n \leq m \leq k \implies n \leq k. \]
    \end{proposition}
    \begin{proof}
      Assume $n \leq m \leq k$.
      Case $n = m = k$. Obvious.
      Case $n = m < k$. Obvious.
      Case $n < m = k$. Obvious.
      Case $n < m < k$. Obvious.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_04_5098403656630272}
      Let $n, m, k$ be natural numbers.
      Then \[ n \leq m < k \implies n < k. \]
    \end{proposition}
    \begin{proof}
      Assume $n \leq m < k$.
      If $n = m$ then $n < k$.
      If $n < m$ then $n < k$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_04_4809599527944192}
      Let $n, m, k$ be natural numbers.
      Then \[ n < m \leq k \implies n < k. \]
    \end{proposition}
    \begin{proof}
      Assume $n < m \leq k$.
      If $m = k$ then $n < k$.
      If $m < k$ then $n < k$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_04_8584998051381248}
      Let $n, m$ be natural numbers.
      Then \[ n < m \implies n + 1 \leq m. \]
    \end{proposition}
    \begin{proof}
      Assume $n < m$.
      Take a positive natural number $k$ such that $m = n + k$.

      Case $k = 1$.
        Then $m = n + 1$.
        Hence $n + 1 \leq m$.
      End.

      Case $k \neq 1$.
        Then we can take a natural number $l$ such that $k = l + 1$.
        Then $m
          = n + (l + 1)
          = (n + l) + 1
          = (n + 1) + l$.
        $l$ is positive.
        Thus $n + 1 < m$.
      End.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_04_8201937860165632}
      Let $n, m$ be natural numbers.
      Then $n < m$ or $n = m$ or $n > m$.
    \end{proposition}
    \begin{proof}
      Define $\Phi = \{ m' \in \Nat \mid n < m'$ or $n = m'$ or $n > m' \}$.

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

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

        Case $n < m'$. Obvious.

        Case $n = m'$. Obvious.

        Case $n > m'$.
          Take a positive natural number $k$ such that $n = m' + k$.

          Case $k = 1$. Obvious.

          Case$k \neq 1$.
            Take a natural number $l$ such that $n = (m' + 1) + l$.
            Hence $n > m' + 1$.
            Indeed $l$ is positive.
          End.
        Qed.
      Qed.

      Thus every natural number is contained in $\Phi$.
      Therefore $n < m$ or $n = m$ or $n > m$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_04_6991525988794368}
      Let $n, m$ be natural numbers.
      Then \[ n \nless m \iff n \geq m. \]
    \end{proposition}
    \begin{proof}
      Case $n \nless m$.
        Then $n = m$ or $n > m$.
        Hence $n \geq m$.
      End.

      Case $n \geq m$.
        Assume $n < m$.
        Then $n \leq m$.
        Hence $n = m$.
        Contradiction.
      End.
    \end{proof}
  \end{forthel}


  \section{Ordering and successors}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_04_7006203091615744}
      Let $n, m$ be natural numbers.
      Then \[ n < m \leq n + 1 \implies m = n + 1. \]
    \end{proposition}
    \begin{proof}
      Assume $n < m \leq n + 1$.
      Take a positive natural number $k$ such that $m = n + k$.
      Take a natural number $l$ such that $n + 1 = m + l$.
      Then $n + 1
        = m + l
        = (n + k) + l
        = n + (k + l)$.
      Hence $k + l = 1$.

      We have $l = 0$. \\
      Proof.
        Assume the contrary.
        Then $k,l > 0$.

        Case $k,l = 1$.
          Then $k + l
            = 2
            \neq 1$.
          Contradiction.
        End.

        Case $k = 1 and l \neq 1$.
          Then $l > 1$.
          Hence $k + l
            > 1 + l
            > 1$.
          Contradiction.
        End.

        Case $k \neq 1 and l = 1$.
          Then $k > 1$.
          Hence $k + l
            > k + 1
            > 1$.
          Contradiction.
        End.

        Case $k, l \neq 1$.
          Take natural numbers $a, b$ such that $k = a + 1$ and $l = b + 1$.
          Indeed $k, l \neq 0$.
          Hence $k = a + 1$ and $l = b + 1$.
          Thus $k, l > 1$. Indeed $a, b$ are positive.
        End.
      Qed.

      Then we have $n + 1
        = m + l
        = m + 0
        = m$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_04_8792330561650688}
      Let $n, m$ be natural numbers.
      Then \[ n \leq m < n + 1 \implies n = m. \]
    \end{proposition}
    \begin{proof}
      Assume $n \leq m < n + 1$.

      Case $n = m$. Obvious.

      Case $n < m$.
        Then $n < m \leq n + 1$.
        Hence $n = m$.
      End.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{corollary}\printlabel{ARITHMETIC_04_1802826644717568}
      Let $n$ be a natural number.
      There is no natural number $m$ such that $n < m < n + 1$.
    \end{corollary}
    \begin{proof}
      Assume the contrary.
      Take a natural number $m$ such that $n < m < n + 1$.
      Then $n < m \leq n + 1$ and $n \leq m < n + 1$.
      Hence $m = n + 1$ and $m = n$.
      Hence $n = n + 1$.
      Contradiction.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_04_990407185924096}
      Let $n$ be a natural number.
      Then \[ n + 1 \geq 1. \]
    \end{proposition}
    \begin{proof}
      Case $n = 0$. Obvious.

      Case $n \neq 0$.
        Then $n > 0$.
        Hence $n + 1 > 0 + 1 = 1$.
      End.
    \end{proof}
  \end{forthel}


  \section{Ordering and addition}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_04_7354062662008832}
      Let $n, m, k$ be natural numbers.
      Then \[ n < m \iff n + k < m + k. \]
    \end{proposition}
    \begin{proof}
      Case $n < m$.
        Take a positive natural number $l$ such that $m = n + l$.
        Then $m + k
          = (n + l) + k
          = (n + k) + l$.
        Hence $n + k < m + k$.
      End.

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

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

  \begin{forthel}
    \begin{corollary}\printlabel{ARITHMETIC_04_4203390999461888}
      Let $n, m, k$ be natural numbers.
      Then \[ n \leq m \iff k + n \leq k + m. \]
    \end{corollary}
  \end{forthel}

  \begin{forthel}
    \begin{corollary}\printlabel{ARITHMETIC_04_5512590832697344}
      Let $n, m, k$ be natural numbers.
      Then \[ n \leq m \iff n + k \leq m + k. \]
    \end{corollary}
  \end{forthel}


  \section{The natural numbers are well-ordered}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_04_4059354166722560}
      \[ {<} = \{ (n, m) \mid \text{$n$ and $m$ are natural numbers such that
      $n < m$} \}. \]
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_04_5933477660721152}
      Let $A$ be a nonempty subclass of $\Nat$.
      Let $n, m$ be least elements of $A$ regarding ${<}$.
      Then $n = m$.
    \end{proposition}
    \begin{proof}
      Assume $n \neq m$.
      Then $n < m$ or $m < n$.
      If $n < m$ then $n \notin A$.
      If $m < n$ then $m \notin A$.
      Hence $n, m \notin A$.
      Contradiction.
      Therefore $n = m$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_04_272317502455808}
      Let $A$ be a nonempty subclass of $\Nat$.
      Then $A$ has a least element regarding ${<}$.
    \end{proposition}
    \begin{proof}
      Assume the contrary.

      Let us show that for each $n \in A$ there exists a $m \in A$ such that
      $m < n$.
        Let $n \in A$.
        $A$ has no least element regarding ${<}$.
        Assume that there exists no $m \in A$ such that $m < n$.
        Then $n \leq m$ for all $m \in A$.
        Hence $n$ is a least element of $A$ regarding ${<}$.
        Contradiction.
      End.

      Define $\Phi = \{ n \in \Nat \mid n$ is less than any element of $A \}$.

      (1) $\Phi$ contains $0$. \\
      Proof.
        $0 \notin A$.
        Hence $0$ is less than every element of $A$.
        Thus $0 \in \Phi$.
      Qed.

      (2) For all $n \in \Phi$ we have $n + 1 \in \Phi$. \\
      Proof.
        Let $n \in \Phi$.
        Then $n$ is less than any element of $A$.
        Assume that $\Phi$ does not contain $n + 1$.
        Then we can take an $m \in A$ such that $n + 1 \nless m$.
        Then $n < m \leq n + 1$.
        Hence $m = n + 1$.
        Thus $n + 1$ is a least element of $A$ regarding ${<}$.
        Contradiction.
      Qed.

      Then $\Phi$ contains every natural number.
      Therefore every natural number is less than any element of $A$.
      Consequently $A$ is empty.
      Contradiction.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{corollary}\printlabel{ARITHMETIC_04_4280275783647232}
      ${<}$ is a wellorder on every nonempty subclass of $\Nat$.
    \end{corollary}
    \begin{proof}
      Let $A$ be a nonempty subclass of $\Nat$.
      For any $n, m \in A$ we have $(n, m) \in {<}$ iff $n < m$.

      (1) ${<}$ is irreflexive on $A$.
      Indeed for any $n \in A$ we have $n \nless n$.

      (2) ${<}$ is transitive on $A$.
      Indeed for any $n, m, k \in A$ if $n < m$ and $m < k$ then $n < k$.

      (3) ${<}$ is connected on $A$.
      Indeed for any distinct $n, m \in A$ we have $n < m$ or $m < n$.

      Hence ${<}$ is a strict linear order on $A$.
      ${<}$ is wellfounded on $A$.
      Indeed every nonempty subclass of $A$ has a least element regarding ${<}$.
      Thus ${<}$ is a wellorder on $A$.
    \end{proof}
  \end{forthel}


  \section{Induction revisited}

  \begin{forthel}
    \begin{theorem}\printlabel{ARITHMETIC_04_3609801697263616}
      Let $A$ be a class.
      Assume for all $n \in \Nat$ if $A$ contains all predecessors of $n$ then
      $A$ contains $n$.
      Then $A$ contains every natural number.
    \end{theorem}
    \begin{proof}
      Assume the contrary.
      Take a natural number $n$ that is not contained in $A$.
      Then $n$ is contained in $\Nat \setminus A$.
      Hence we can take a least element $m$ of $\Nat \setminus A$ regarding
      ${<}$.
      Then $\Nat \setminus A$ does not contain any predecessor of $m$.
      Therefore $A$ contains all predecessors of $m$.
      Consequently $A$ contains $m$.
      Contradiction.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{theorem}\printlabel{ARITHMETIC_04_4976599269113856}
      Let $A$ be a class.
      Let $k$ be a natural number such that $k \in A$.
      Assume that for all $n \in \Nat_{\geq k}$ if $n \in A$ then $n + 1 \in A$.
      Then for all $n \in \Nat_{\geq k}$ we have $n \in A$.
    \end{theorem}
    \begin{proof}
      Define $\Phi = \{n \in \Nat \mid$ if $n \geq k$ then $n \in A \}$.

      (1) $\Phi$ contains $0$.
      Indeed if $0 \geq k$ then $0 = k \in A$.

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

        Let us show that if $n + 1 \geq k$ then $n + 1 \in A$.
          Assume $n + 1 \geq k$.

          Case $n < k$.
            Then $n + 1 = k$.
            Hence $n + 1 \in A$.
          End.

          Case $n \geq k$.
            Then $n \in A$.
            Hence $n + 1 \in A$.
          End.
        End.

        Therefore $n + 1 \in \Phi$.
      Qed.

      Thus $\Phi$ contains every natural number.
      Consequently for all $n \in \Nat_{\geq k}$ we have $n \in A$.
    \end{proof}
  \end{forthel}
\end{document}
