2.3.5 Prove Proposition proposition 2.3.9 (Hint: fix \(q\) and induct on \(n\).)
- \(\bullet\) Show that \(\exists m\exists r\in\mathbb{N}\) such that \(0\leq r<q\) and \(n=mq+r\), when
- – \(q\neq0\)
-
\(\Vdash\) { Proof by induction on \(n\) }
- \(\bullet\) Base case: show that \(\exists m\exists r\in\mathbb{N}\) such that \(0\leq r<q\) and \(n=mq+r\), when
- – \(n=0\)
- \(\Vdash\) \(0\)
-
\(=\) { Definition of addition: \(0+m:=m\); \(0+0=0\) }
- \(0+0\)
-
\(=\) { Definition of multiplication: \(0\times m:=0\) }
- \(0\times q+0\)
- \(\square\)
- \(\bullet\) Inductive step: show that \(\exists m\exists r\in\mathbb{N}\) such that \(0\leq r<q\) and \(n\pp=mq+r\), when
- –\(\exists m'\exists r'\in\mathbb{N}\) such that \(0\leq r'<q'\) and \(n=m'q'+r'\)
- \(\Vdash\) \(n\pp\)
-
\(=\) { \(n\pp=n+1\) and the inductive hypothesis }
- \(m'q'+r'+1\)
-
\(=\) { Proof by cases: \(r'<q'\implies r'\pp=r'+1\leq q'\) by Proposition 2.2.12 (e) }
- \(\bullet\) case1: \(r'+1=q'\)
- \(\Vdash\) \(m'q'+r'+1\)
-
\(=\) { substitue \(r'+1\) with \(q'\) }
- \(m'q'+q'\)
-
\(=\) { Definition of multiplication: \((n\pp)\times m:=(n\times m)+m\); \(n\pp=n+1\) }
- \((m'+1)q'\)
-
\(=\) { Definition of addition: \(0+m:=m\) }
- \((m'+1)q'+0\)
-
\(=\) { Let \(m=m'+1,~q=q',~r=0\) }
- \(mq+r\)
- \(\square\)
- \(\bullet\) case2: \(r'+1<q'\)
- \(\Vdash\) \(m'q'+r'+1\)
-
\(=\) { Let \(r=r'+1\) }
- \(m'q'+r\)
-
\(=\) { Let \(m=m',~q=q'\) }
- \(mq+r\)
- \(\square\)
- \(\square\)
- \(\square\)