Enderton. Prove out addition/multiplication properties.

Bookshelf/Enderton/Set.tex

@@ -3057,6 +3057,7 @@ If not, then under what conditions does equality hold?
 
 \subsection{\verified{Lemma 1}}%
 \hyperlabel{sub:lemma-1}
+\hyperlabel{sub:one-to-one-inverse}
 
 \begin{lemma}[1]
 
@@ -3125,8 +3126,8 @@ If not, then under what conditions does equality hold?
     {Enderton.Set.Chapter\_3.theorem\_3g\_ii}
 
   Suppose $F$ is a one-to-one \nameref{ref:function}.
-  Then \nameref{sub:lemma-1} indicates $F^{-1}$ is a one-to-one function with
+  Then \nameref{sub:one-to-one-inverse} indicates $F^{-1}$ is a one-to-one
-    domain $\ran{F}$ and range $\dom{F}$.
+    function with domain $\ran{F}$ and range $\dom{F}$.
 
   For all $x \in \dom{F}$, $\pair{x, F(x)} \in F$.
   Then $\pair{F(x), x} \in F^{-1}$.
@@ -3275,8 +3276,8 @@ If not, then under what conditions does equality hold?
           F^{-1}(y) & \text{if } y \in \ran{F} \\
           a & \text{otherwise}.
         \end{cases}$$
-      $G$ is a function by virtue of \nameref{sub:lemma-1} and choice of mapping
+      $G$ is a function by virtue of \nameref{sub:one-to-one-inverse} and choice
-        for all values $y \not\in \ran{F}$.
+        of mapping for all values $y \not\in \ran{F}$.
       Furthermore, for all $x \in A$, $F(x) \in \ran{F}$.
       Thus $(G \circ F)(x) = G(F(x)) = F^{-1}(F(x)) = x$ by
         \nameref{sub:theorem-3g}.
@@ -6469,46 +6470,78 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 \section{Arithmetic}%
 \hyperlabel{sec:arithmetic}
 
-\subsection{\sorry{Theorem 4I}}
+\subsection{\verified{Theorem 4I}}
 \hyperlabel{sub:theorem-4i}
 
 \begin{theorem}[4I]
 
   For natural numbers $m$ and $n$,
-    \begin{align*}
+    \begin{align}
-      m + 0 & = m, \\
+      m + 0 & = m, \hyperlabel{sub:theorem-4i-eq1} \\
-      m + n^+ & = (m + n)^+.
+      m + n^+ & = (m + n)^+. \hyperlabel{sub:theorem-4i-eq2}
-    \end{align*}
+    \end{align}
 
 \end{theorem}
 
 \begin{proof}
 
-  TODO
+  \statementpadding
+
+  \lean*{Init/Data/Nat/Basic}{Nat.add\_zero}
+
+  \lean{Init/Prelude}{Nat.add}
+
+  \paragraph{\eqref{sub:theorem-4i-eq1}}%
+
+    Let $m$ be a \nameref{ref:natural-number}.
+    By definition of \nameref{ref:addition}, $m + 0 = A_m(0)$.
+    By definition of $A_m$, $A_m(0) = m$.
+    Thus $m + 0 = m$.
+
+  \paragraph{\eqref{sub:theorem-4i-eq2}}%
+
+    Let $m$ and $n$ be natural numbers.
+    By definition of \nameref{ref:addition},
+      $$m + n^+ = A_m(n^+) = A_m(n)^+ = (m + n)^+.$$
 
 \end{proof}
 
-\subsection{\sorry{Theorem 4J}}
+\subsection{\verified{Theorem 4J}}
 \hyperlabel{sub:theorem-4j}
 
 \begin{theorem}[4J]
 
   For natural numbers $m$ and $n$,
-    \begin{align*}
+    \begin{align}
-      m \cdot 0 & = 0, \\
+      m \cdot 0 & = 0, \hyperlabel{sub:theorem-4j-eq1} \\
-      m \cdot n^+ & = m \cdot n + m.
+      m \cdot n^+ & = m \cdot n + m. \hyperlabel{sub:theorem-4j-eq2}
-    \end{align*}
+    \end{align}
 
 \end{theorem}
 
 \begin{proof}
 
-  TODO
+  \statementpadding
+
+  \lean*{Init/Data/Nat/Basic}{Nat.mul\_zero}
+
+  \lean{Init/Prelude}{Nat.mul}
+
+  \paragraph{\eqref{sub:theorem-4j-eq1}}%
+
+    Let $m$ be a \nameref{ref:natural-number}.
+    By definition of \nameref{ref:multiplication}, $$m \cdot 0 = M_m(0) = 0.$$
+
+  \paragraph{\eqref{sub:theorem-4j-eq2}}%
+
+    Let $m$ and $n$ be natural numbers.
+    By definition of \nameref{ref:multiplication},
+      $$m \cdot n^+ = M_m(n^+) = M_m(n) + m = m \cdot n + m.$$
 
 \end{proof}
 
-\subsection{\pending{Lemma 2}}%
+\subsection{\verified{Left Additive Identity}}%
-\label{sub:lemma-2}
+\hyperlabel{sub:left-additive-identity}
 
 \begin{lemma}[2]
 
@@ -6519,35 +6552,39 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \begin{proof}
 
-  Let $S = \{n \in \omega \mid A_0(n) = n\}$.
+  \lean{Init/Data/Nat/Basic}{Nat.zero\_add}
+
+  Let $S = \{n \in \omega \mid 0 + n = n\}$.
   We prove that (i) $0 \in S$ and (ii) if $n \in S$ then $n^+ \in S$.
   Afterwards we show that (iii) our theorem holds.
 
   \paragraph{(i)}%
-  \hyperlabel{par:lemma-2-i}
+  \hyperlabel{par:left-additive-identity-i}
 
-    By definition of \nameref{ref:addition}, $A_0(0) = 0$.
+    By \nameref{sub:theorem-4i}, $0 + 0 = 0$.
     Thus $0 \in S$.
 
   \paragraph{(ii)}%
-  \hyperlabel{par:lemma-2-ii}
+  \hyperlabel{par:left-additive-identity-ii}
 
     Suppose $n \in S$.
-    By definition of addition, $A_0(n^+) = A_0(n)^+$.
+    By \nameref{sub:theorem-4i}, $0 + n^+ = (0 + n)^+$.
-    Since $n \in S$, $A_0(n) = n$ which in turn implies that $A_0(n)^+ = n^+$.
+    Since $n \in S$, $0 + n = n$ which in turn implies that $(0 + n)^+ = n^+$.
     Thus $n^+ \in S$.
 
   \paragraph{(iii)}%
 
-    By \nameref{par:lemma-2-i} and \nameref{par:lemma-2-ii}, $S$ is an
+    By \nameref{par:left-additive-identity-i} and
+      \nameref{par:left-additive-identity-ii}, $S$ is an
       \nameref{ref:inductive-set}.
     Hence \nameref{sub:theorem-4b} implies $S = \omega$.
-    Thus for all $n \in \omega$, $A_0(n) = n$.
+    Thus for all $n \in \omega$, $0 + n = n$.
 
 \end{proof}
 
-\subsection{\pending{Lemma 3}}%
+\subsection{\verified{Lemma 3}}%
-\label{sub:lemma-3}
+\hyperlabel{sub:lemma-3}
+\hyperlabel{sub:succ-add-eq-add-succ}
 
 \begin{lemma}[3]
 
@@ -6558,103 +6595,41 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \begin{proof}
 
+  \lean{Std/Data/Nat/Lemmas}{Nat.succ\_add\_eq\_succ\_add}
+
   Let $m \in \omega$ and define
-    $$S = \{n \in \omega \mid A_{m^+}(n) = A_m(n^+)\}.$$
+    $$S = \{n \in \omega \mid m^+ + n = m + n^+\}.$$
   We prove that (i) $0 \in S$ and (ii) if $n \in S$ then $n^+ \in S$.
   Afterwards we show that (iii) our theorem holds.
 
   \paragraph{(i)}%
-  \label{par:lemma-3-i}
+  \hyperlabel{par:lemma-3-i}
 
-    By definition of \nameref{ref:addition}, $A_{m^+}(0) = m^+$.
+    By \nameref{sub:theorem-4i}, $m^+ + 0 = m^+$.
-    Likewise, $$A_m(0^+) = A_m(0)^+ = m^+.$$
+    Likewise, $m + 0^+ = (m + 0)^+ = m^+$.
     Thus $0 \in S$.
 
   \paragraph{(ii)}%
-  \label{par:lemma-3-ii}
+  \hyperlabel{par:lemma-3-ii}
 
     Suppose $n \in S$.
-    By definition of addition, $A_{m^+}(n^+) = \left[A_{m^+}(n)\right]^+$.
+    By \nameref{sub:theorem-4i}, $m^+ + n^+ = (m^+ + n)^+$.
-    Since $n \in S$, $A_{m^+}(n) = A_m(n^+)$ which in turn implies that
+    Since $n \in S$, $m^+ + n = m + n^+$.
-      $$\left[A_{m^+}(n)\right]^+ = \left[A_m(n^+)\right]^+ = A_m(n^{++}).$$
+    Therefore $(m^+ + n)^+ = (m + n^+)^+ = m + n^{++}$.
     Thus $n^+ \in S$.
 
   \paragraph{(iii)}%
 
     By \nameref{par:lemma-3-i} and \nameref{par:lemma-3-ii}, $S$ is inductive.
     Hence \nameref{sub:theorem-4b} implies $S = \omega$.
-    Thus for all $n \in \omega$, $A_{m^+}(n) = A_m(n^+)$.
+    Thus for all $n \in \omega$, $m^+ + n = m + n^+$.
 
 \end{proof}
 
-\subsection{\pending{Lemma 4}}%
+\subsection{\verified{Theorem 4K-1}}%
-\hyperlabel{sub:lemma-4}
-
-\begin{lemma}[4]
-
-  For all $n \in \omega$, $M_0(n) = 0$.
-  In other words, $$0 \cdot n = 0.$$
-
-\end{lemma}
-
-\begin{proof}
-
-  Define
-    \begin{equation}
-      \hyperlabel{sub:lemma-4-eq1}
-      S = \{n \in \omega \mid M_0(n) = 0\}.
-    \end{equation}
-  We prove that (i) $0 \in S$ and (ii) that if $n \in S$, then $n^+ \in S$.
-  Afterwards we show that (iii) our theorem holds.
-
-  \paragraph{(i)}%
-  \hyperlabel{par:lemma-4-i}
-
-    By definition of \nameref{ref:multiplication}, $M_0(0) = 0$.
-    Thus $0 \in S$.
-
-  \paragraph{(ii)}%
-  \hyperlabel{par:lemma-4-ii}
-
-    Suppose $n \in S$.
-    Then, by definition of \nameref{ref:multiplication},
-      \begin{align*}
-        M_0(n^+)
-          & = M_0(n) + 0 \\
-          & = 0 + 0 & \eqref{sub:lemma-4-eq1} \\
-          & = 0. & \textref{ref:addition}
-      \end{align*}
-    Thus $n^+ \in S$.
-
-  \paragraph{(iii)}%
-
-    By \nameref{par:lemma-4-i} and \nameref{par:lemma-4-ii}, $S$ is an
-      \nameref{ref:inductive-set}.
-    Hence \nameref{sub:theorem-4b} implies $S = \omega$.
-    Thus for all $n \in \omega$, $M_0(n) = 0$.
-
-\end{proof}
-
-\subsection{\sorry{Lemma 5}}%
-\hyperlabel{sub:lemma-5}
-
-\begin{lemma}[5]
-
-  For all $m, n \in \omega$, $M_{m^+}(n) = M_m(n) + n$.
-  In other words, $$m^+ \cdot n = m \cdot n + n.$$
-
-\end{lemma}
-
-\begin{proof}
-
-  TODO
-
-\end{proof}
-
-\subsection{\pending{Theorem 4k (1)}}%
 \label{sub:theorem-4k-1}
 
-\begin{theorem}[4K.1]
+\begin{theorem}[4K-1]
 
   Associative law for addition.
   For $m, n, p \in \omega$, $$m + (n + p) = (m + n) + p.$$
@@ -6663,6 +6638,8 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \begin{proof}
 
+  \lean{Mathlib/Algebra/Group/Defs}{add\_assoc}
+
   Fix $n, p \in \omega$ and define
     \begin{equation}
       \hyperlabel{sub:theorem-4k-1-eq1}
@@ -6674,28 +6651,24 @@ Show that $<_L$ is a linear ordering on $A \times B$.
   \paragraph{(i)}%
   \hyperlabel{par:theorem-4k-1-i}
 
-    By definition of \nameref{ref:addition},
+    By \nameref{sub:left-additive-identity},
-      \begin{align*}
+      $$0 + (n + p) = n + p = (0 + n) + p.$$
-        0 + (n + p)
-          & = n + p & \textref{sub:lemma-2} \\
-          & = (0 + n) + p. & \textref{sub:lemma-2} \\
-      \end{align*}
     Thus $0 \in S$.
 
   \paragraph{(ii)}%
   \hyperlabel{par:theorem-4k-1-ii}
 
     Suppose $m \in S$.
-    By definition of \nameref{ref:addition},
+    Then
       \begin{align*}
         m^+ + (n + p)
-          & = m + (n + p)^+ & \textref{sub:lemma-3} \\
+          & = m + (n + p)^+ & \textref{sub:succ-add-eq-add-succ} \\
           & = (m + (n + p))^+ & \textref{sub:theorem-4i} \\
           & = ((m + n) + p)^+ & \eqref{sub:theorem-4k-1-eq1} \\
           & = (m + n) + p^+ & \textref{sub:theorem-4i} \\
-          & = (m + n)^+ + p & \textref{sub:lemma-3} \\
+          & = (m + n)^+ + p & \textref{sub:succ-add-eq-add-succ} \\
           & = (m + n^+) + p & \textref{sub:theorem-4i} \\
-          & = (m^+ + n) + p. & \textref{sub:lemma-3}
+          & = (m^+ + n) + p. & \textref{sub:succ-add-eq-add-succ}
       \end{align*}
     Thus $m^+ \in S$.
 
@@ -6709,10 +6682,10 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \end{proof}
 
-\subsection{\pending{Theorem 4k (2)}}%
+\subsection{\verified{Theorem 4K-2}}%
 \label{sub:theorem-4k-2}
 
-\begin{theorem}[4K.2]
+\begin{theorem}[4K-2]
 
   Commutative law for addition.
   For $m, n \in \omega$, $$m + n = n + m.$$
@@ -6721,6 +6694,8 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \begin{proof}
 
+  \lean{Mathlib/Algebra/Group/Defs}{add\_comm}
+
   Fix $n \in \omega$ and define
     \begin{equation}
       \hyperlabel{sub:theorem-4k-2-eq1}
@@ -6732,25 +6707,21 @@ Show that $<_L$ is a linear ordering on $A \times B$.
   \paragraph{(i)}%
   \hyperlabel{par:theorem-4k-2-i}
 
-    By definition of \nameref{ref:addition},
+    By definition of \nameref{ref:addition} and
-      \begin{align*}
+      \nameref{sub:left-additive-identity}, $$0 + n = n = n + 0.$$
-        0 + n
-          & = n & \textref{sub:lemma-2} \\
-          & = n + 0. \\
-      \end{align*}
     Thus $0 \in S$.
 
   \paragraph{(ii)}%
   \hyperlabel{par:theorem-4k-2-ii}
 
     Suppose $m \in S$.
-    By definition of \nameref{ref:addition},
+    Then
       \begin{align*}
         m^+ + n
-          & = m + n^+ & \textref{sub:lemma-3} \\
+          & = m + n^+ & \textref{sub:succ-add-eq-add-succ} \\
-          & = (m + n)^+ \\
+          & = (m + n)^+ & \textref{sub:theorem-4i} \\
           & = (n + m)^+ & \eqref{sub:theorem-4k-2-eq1} \\
-          & = n + m^+.
+          & = n + m^+. & \textref{sub:theorem-4i}
       \end{align*}
     Thus $m^+ \in S$.
 
@@ -6763,10 +6734,116 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \end{proof}
 
-\subsection{\pending{Theorem 4k (3)}}%
+\subsection{\verified{Zero Multiplicand}}%
-\label{sub:theorem-4k-3}
+\hyperlabel{sub:zero-multiplicand}
 
-\begin{theorem}[4K.3]
+\begin{lemma}[4]
+
+  For all $n \in \omega$, $M_0(n) = 0$.
+  In other words, $$0 \cdot n = 0.$$
+
+\end{lemma}
+
+\begin{proof}
+
+  \lean{Init/Data/Nat/Basic}{Nat.zero\_mul}
+
+  Define
+    \begin{equation}
+      \hyperlabel{sub:zero-multiplicand-eq1}
+      S = \{n \in \omega \mid 0 \cdot n = 0\}.
+    \end{equation}
+  We prove that (i) $0 \in S$ and (ii) that if $n \in S$, then $n^+ \in S$.
+  Afterwards we show that (iii) our theorem holds.
+
+  \paragraph{(i)}%
+  \hyperlabel{par:zero-multiplicand-i}
+
+    By \nameref{sub:theorem-4j}, $0 \cdot 0 = 0$.
+    Thus $0 \in S$.
+
+  \paragraph{(ii)}%
+  \hyperlabel{par:zero-multiplicand-ii}
+
+    Suppose $n \in S$.
+    Then
+      \begin{align*}
+        0 \cdot n^+
+          & = 0 \cdot n + 0 & \textref{sub:theorem-4j} \\
+          & = 0 + 0 & \eqref{sub:zero-multiplicand-eq1} \\
+          & = 0. & \textref{ref:addition}
+      \end{align*}
+    Thus $n^+ \in S$.
+
+  \paragraph{(iii)}%
+
+    By \nameref{par:zero-multiplicand-i} and \nameref{par:zero-multiplicand-ii},
+      $S$ is an \nameref{ref:inductive-set}.
+    Hence \nameref{sub:theorem-4b} implies $S = \omega$.
+    Thus for all $n \in \omega$, $0 \cdot n = 0$.
+
+\end{proof}
+
+\subsection{\verified{Successor Distribution}}%
+\hyperlabel{sub:successor-distribution}
+
+\begin{lemma}[5]
+
+  For all $m, n \in \omega$, $M_{m^+}(n) = M_m(n) + n$.
+  In other words, $$m^+ \cdot n = m \cdot n + n.$$
+
+\end{lemma}
+
+\begin{proof}
+
+  \lean{Init/Data/Nat/Basic}{Nat.succ\_mul}
+
+  Let $m \in \omega$ and define
+    \begin{equation}
+      \hyperlabel{sub:successor-distribution-eq1}
+      S = \{n \in \omega \mid m^+ \cdot n = m \cdot n + n\}.
+    \end{equation}
+  We prove that (i) $0 \in S$ and (ii) that if $n \in S$, then $n^+ \in S$.
+  Afterwards we show that (iii) our theorem holds.
+
+  \paragraph{(i)}%
+  \hyperlabel{par:successor-distribution-i}
+
+    By \nameref{sub:theorem-4j}, $m^+ \cdot 0 = 0$.
+    Likewise, by \nameref{sub:theorem-4i}, $m \cdot 0 + 0 = 0$.
+    Thus $0 \in S$.
+
+  \paragraph{(ii)}%
+  \hyperlabel{par:successor-distribution-ii}
+
+    Suppose $n \in S$.
+    Then
+      \begin{align*}
+        m^+ \cdot n^+
+          & = m^+ \cdot n + m^+ & \textref{sub:theorem-4j} \\
+          & = (m \cdot n + n) + m^+ & \eqref{sub:successor-distribution-eq1} \\
+          & = m \cdot n + (n + m^+) & \textref{sub:theorem-4k-1} \\
+          & = m \cdot n + (n^+ + m) & \textref{sub:succ-add-eq-add-succ} \\
+          & = m \cdot n + (m + n^+) & \textref{sub:theorem-4k-2} \\
+          & = (m \cdot n + m) + n^+ & \textref{sub:theorem-4k-1} \\
+          & = m \cdot n^+ + n^+. & \textref{sub:theorem-4j}
+      \end{align*}
+    Thus $n^+ \in S$.
+
+  \paragraph{(iii)}%
+
+    By \nameref{par:successor-distribution-i} and
+      \nameref{par:successor-distribution-ii}, $S$ is an
+      \nameref{ref:inductive-set}.
+    By \nameref{sub:theorem-4b}, $S = \omega$.
+    Thus for all $m, n \in \omega$, $m^+ \cdot n = m \cdot n + n$.
+
+\end{proof}
+
+\subsection{\verified{Theorem 4K-3}}
+\hyperlabel{sub:theorem-4k-3}
+
+\begin{theorem}[4K-3]
 
   Distributive law.
   For $m, n, p \in \omega$, $$m \cdot (n + p) = m \cdot n + m \cdot p.$$
@@ -6775,10 +6852,12 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \begin{proof}
 
+  \lean{Init/Data/Nat/Basic}{Nat.left\_distrib}
+
   Fix $n, p \in \omega$ and define
     \begin{equation}
       \hyperlabel{sub:theorem-4k-3-eq1}
-      S = \{m \in \omega m \cdot (n + p) = m \cdot n + m \cdot p\}.
+      S = \{m \in \omega \mid m \cdot (n + p) = m \cdot n + m \cdot p\}.
     \end{equation}
   We show that (i) $0 \in S$ and (ii) if $m \in S$ then $m^+ \in S$.
   Afterward we show that (iii) the distributive law holds.
@@ -6789,9 +6868,9 @@ Show that $<_L$ is a linear ordering on $A \times B$.
     By definition of \nameref{ref:multiplication} and \nameref{ref:addition},
       \begin{align*}
         0 \cdot (n + p)
-          & = 0 & \textref{sub:lemma-4} \\
+          & = 0 & \textref{sub:zero-multiplicand} \\
           & = 0 + 0 & \textref{ref:addition} \\
-          & = 0 \cdot n + 0 \cdot p. & \textref{sub:lemma-4}
+          & = 0 \cdot n + 0 \cdot p. & \textref{sub:zero-multiplicand}
       \end{align*}
     Thus $0 \in S$.
 
@@ -6802,17 +6881,17 @@ Show that $<_L$ is a linear ordering on $A \times B$.
     By definition of \nameref{ref:multiplication} and \nameref{ref:addition},
       \begin{align*}
         m^+ \cdot (n + p)
-          & = m \cdot (n + p) + (n + p) & \textref{sub:lemma-5} \\
+          & = m \cdot (n + p) + (n + p)
+            & \textref{sub:successor-distribution} \\
           & = m \cdot (n + p) + n + p & \textref{sub:theorem-4k-1} \\
           & = m \cdot n + m \cdot p + n + p
             & \eqref{sub:theorem-4k-3-eq1} \\
           & = m \cdot n + n + m \cdot p + p & \textref{sub:theorem-4k-2} \\
-          & = m^+ \cdot n + m^+ \cdot p. & \textref{sub:lemma-5}
+          & = m^+ \cdot n + m^+ \cdot p. & \textref{sub:successor-distribution}
       \end{align*}
     Thus $m^+ \in S$.
 
   \paragraph{(iii)}%
-  \hyperlabel{par:theorem-4k-3-iii}
 
     By \nameref{par:theorem-4k-3-i} and \nameref{par:theorem-4k-3-ii}, $S$
       is an \nameref{ref:inductive-set}.
@@ -6822,10 +6901,174 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \end{proof}
 
-\subsection{\sorry{Theorem 4k (4)}}%
+\subsection{\verified{Successor Identity}}%
-\label{sub:theorem-4k-4}
+\hyperlabel{sub:successor-identity}
 
-\begin{theorem}[4K.4]
+\begin{lemma}[6]
+
+  For all $m \in \omega$, $A_m(1) = m^+$.
+  In other words, $$m + 1 = m^+.$$
+
+\end{lemma}
+
+\begin{proof}
+
+  \lean{Init/Prelude}{Nat.succ}
+
+  Let
+    \begin{equation}
+      \hyperlabel{sub:successor-identity-eq1}
+      S = \{m \in \omega \mid m + 1 = m^+\}.
+    \end{equation}
+  We prove that (i) $0 \in S$ and (ii) if $m \in S$, then $m^+ \in S$.
+  Afterwards we show that (iii) our theorem holds.
+
+  \paragraph{(i)}%
+  \hyperlabel{par:successor-identity-i}
+
+    By \nameref{sub:left-additive-identity}, $0 + 1 = 1$.
+    By definition of the \nameref{ref:successor},
+      $0^+ = \emptyset \cup \{\emptyset\} = 1$.
+    Thus $0 \in S$.
+
+  \paragraph{(ii)}%
+  \hyperlabel{par:successor-identity-ii}
+
+    Let $m \in S$.
+    Then
+      \begin{align*}
+        m^+ + 1
+          & = m + 1^+ & \textref{sub:succ-add-eq-add-succ} \\
+          & = (m + 1)^+ & \textref{sub:theorem-4i} \\
+          & = (m^+)^+. & \eqref{sub:successor-identity-eq1}
+      \end{align*}
+    Thus $m^+ \in S$.
+
+  \paragraph{(iii)}%
+
+    By \nameref{par:successor-identity-i} and
+      \nameref{par:successor-identity-ii}, $S$ is an
+      \nameref{ref:inductive-set}.
+    Hence \nameref{sub:theorem-4b} implies $S = \omega$.
+    Thus for all $m \in \omega$, $m + 1 = m^+$.
+
+\end{proof}
+
+\subsection{\verified{Right Multiplicative Identity}}%
+\hyperlabel{sub:right-multiplicative-identity}
+
+\begin{lemma}[7]
+
+  For all $m \in \omega$, $M_m(1) = m$.
+  In other words, $$m \cdot 1 = m.$$
+
+\end{lemma}
+
+\begin{proof}
+
+  \lean{Init/Data/Nat/Basic}{mul\_one}
+
+  Let
+    \begin{equation}
+      \hyperlabel{sub:right-multiplicative-identity-eq1}
+      S = \{m \in \omega \mid m \cdot 1 = m\}.
+    \end{equation}
+  We prove that (i) $0 \in S$ and (ii) if $m \in S$, then $m^+ \in S$.
+  Afterwards we show that (iii) our theorem holds.
+
+  \paragraph{(i)}%
+  \hyperlabel{par:right-multiplicative-identity-i}
+
+    By \nameref{sub:zero-multiplicand}, $0 \cdot 1 = 0$.
+    Thus $0 \in S$.
+
+  \paragraph{(ii)}%
+  \hyperlabel{par:right-multiplicative-identity-ii}
+
+    Suppose $m \in S$.
+    Then
+      \begin{align*}
+        m^+ \cdot 1
+          & = m \cdot 1 + 1 & \textref{sub:successor-distribution} \\
+          & = m + 1 & \eqref{sub:right-multiplicative-identity-eq1} \\
+          & = m^+. & \textref{sub:successor-identity}
+      \end{align*}
+    Thus $m^+ \in S$.
+
+  \paragraph{(iii)}%
+
+    By \nameref{par:right-multiplicative-identity-i} and
+      \nameref{par:right-multiplicative-identity-ii}, $S$
+      is an \nameref{ref:inductive-set}.
+    By \nameref{sub:theorem-4b}, $S = \omega$.
+    Thus for all $m \in \omega$, $m \cdot 1 = m$.
+
+\end{proof}
+
+\subsection{\verified{Theorem 4K-5}}
+\hyperlabel{sub:theorem-4k-5}
+
+\begin{theorem}[4K-5]
+
+  Commutative law for multiplication.
+  For $m, n \in \omega$, $$m \cdot n = n \cdot m.$$
+
+\end{theorem}
+
+\begin{note}
+  We prove commutativity before associativity, though Enderton orders these
+  two properties in the opposite direction.
+\end{note}
+
+\begin{proof}
+
+  \lean{Mathlib/Algebra/Group/Defs}{mul\_comm}
+
+  Fix $n \in \omega$ and define
+    \begin{equation}
+      \hyperlabel{sub:theorem-4k-5-eq1}
+      S = \{m \in \omega \mid m \cdot n = n \cdot m\}.
+    \end{equation}
+  We show that (i) $0 \in S$ and (ii) if $m \in S$ then $m^+ \in S$.
+  Afterward we show that (iii) the commutative law for multiplication holds.
+
+  \paragraph{(i)}%
+  \hyperlabel{par:theorem-4k-5-i}
+
+    By \nameref{sub:theorem-4j} and \nameref{sub:zero-multiplicand},
+      $$0 \cdot n = 0 = n \cdot 0.$$
+    Thus $0 \in S$.
+
+  \paragraph{(ii)}%
+  \hyperlabel{par:theorem-4k-5-ii}
+
+    Suppose $m \in S$.
+    Then
+      \begin{align*}
+        m^+ \cdot n
+          & = m \cdot n + n & \textref{sub:successor-distribution} \\
+          & = n \cdot m + n & \eqref{sub:theorem-4k-5-eq1} \\
+          & = n \cdot m + n \cdot 1
+            & \textref{sub:right-multiplicative-identity} \\
+          & = n \cdot (m + 1) & \textref{sub:theorem-4k-3} \\
+          & = n \cdot m^+. & \textref{sub:successor-identity}
+      \end{align*}
+    Thus $m^+ \in S$.
+
+  \paragraph{(iii)}%
+  \hyperlabel{par:theorem-4k-5-iii}
+
+    By \nameref{par:theorem-4k-5-i} and \nameref{par:theorem-4k-5-ii}, $S$
+      is an \nameref{ref:inductive-set}.
+    By \nameref{sub:theorem-4b}, $S = \omega$.
+    Thus for all $m, n \in \omega$, $m \cdot n = n \cdot m$.
+
+\end{proof}
+
+\subsection{\verified{Theorem 4K-4}}%
+\hyperlabel{sub:theorem-4k-4}
+
+\begin{theorem}[4K-4]
 
   Associative law for multiplication.
   For $m, n, p \in \omega$, $$m \cdot (n \cdot p) = (m \cdot n) \cdot p.$$
@@ -6834,23 +7077,46 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \begin{proof}
 
-  TODO
+  \lean{Mathlib/Algebra/Group/Defs}{mul\_assoc}
 
-\end{proof}
+  Fix $m, n \in \omega$ and define
+    \begin{equation}
+      \hyperlabel{sub:theorem-4k-4-eq1}
+      S = \{p \in \omega \mid m \cdot (n \cdot p) = (m \cdot n) \cdot p\}.
+    \end{equation}
+  We show that (i) $0 \in S$ and (ii) if $p \in S$ then $p^+ \in S$.
+  Afterward we show that (iii) the associative law for multiplication holds.
 
-\subsection{\sorry{Theorem 4K (5)}}
+  \paragraph{(i)}%
-\hyperlabel{sub:theorem-4k}
+  \hyperlabel{par:theorem-4k-4-i}
 
-\begin{theorem}[4K.5]
+    By \nameref{sub:theorem-4j},
+      $$m \cdot (n \cdot 0) = 0 = (m \cdot n) \cdot 0.$$
+    Thus $0 \in S$.
 
-  Commutative law for multiplication.
+  \paragraph{(ii)}%
-  For $m, n \in \omega$, $$m \cdot n = n \cdot m.$$
+  \hyperlabel{par:theorem-4k-4-ii}
 
-\end{theorem}
+    Suppose $p \in S$.
+    Then
+      \begin{align*}
+        m \cdot (n \cdot p^+)
+          & = m \cdot (n \cdot p + n) & \textref{sub:theorem-4j} \\
+          & = m \cdot (n \cdot p) + m \cdot n & \textref{sub:theorem-4k-3} \\
+          & = (m \cdot n) \cdot p + m \cdot n & \eqref{sub:theorem-4k-4-eq1} \\
+          & = p \cdot (m \cdot n) + m \cdot n & \textref{sub:theorem-4k-5} \\
+          & = p^+ \cdot (m \cdot n) & \textref{sub:successor-distribution} \\
+          & = (m \cdot n) \cdot p^+ & \textref{sub:theorem-4k-5}
+      \end{align*}
+    Thus $p^+ \in S$.
 
-\begin{proof}
+  \paragraph{(iii)}%
 
-  TODO
+    By \nameref{par:theorem-4k-4-i} and \nameref{par:theorem-4k-4-ii}, $S$
+      is an \nameref{ref:inductive-set}.
+    By \nameref{sub:theorem-4b}, $S = \omega$.
+    Thus for all $m, n, p \in \omega$,
+      $m \cdot (n \cdot p) = (m \cdot n) \cdot p$.
 
 \end{proof}
 
@@ -7249,7 +7515,7 @@ Show that each natural number is either even or odd, but never both.
 \subsection{\sorry{Exercise 4.15}}%
 \hyperlabel{sub:exercise-4.15}
 
-Complete the proof of part (1) of \nameref{sub:theorem-4k}.
+Complete the proof of \nameref{sub:theorem-4k-1}.
 
 \begin{proof}
 
@@ -7260,7 +7526,7 @@ Complete the proof of part (1) of \nameref{sub:theorem-4k}.
 \subsection{\sorry{Exercise 4.16}}%
 \hyperlabel{sub:exercise-4.16}
 
-Complete the proof of part (5) of \nameref{sub:theorem-4k}.
+Complete the proof of \nameref{sub:theorem-4k-5}.
 
 \begin{proof}