A calculus of the absurd
\(\newcommand{\footnotename}{footnote}\)
\(\def \LWRfootnote {1}\)
\(\newcommand {\footnote }[2][\LWRfootnote ]{{}^{\mathrm {#1}}}\)
\(\newcommand {\footnotemark }[1][\LWRfootnote ]{{}^{\mathrm {#1}}}\)
\(\let \LWRorighspace \hspace \)
\(\renewcommand {\hspace }{\ifstar \LWRorighspace \LWRorighspace }\)
\(\newcommand {\mathnormal }[1]{{#1}}\)
\(\newcommand \ensuremath [1]{#1}\)
\(\newcommand {\LWRframebox }[2][]{\fbox {#2}} \newcommand {\framebox }[1][]{\LWRframebox } \)
\(\newcommand {\setlength }[2]{}\)
\(\newcommand {\addtolength }[2]{}\)
\(\newcommand {\setcounter }[2]{}\)
\(\newcommand {\addtocounter }[2]{}\)
\(\newcommand {\arabic }[1]{}\)
\(\newcommand {\number }[1]{}\)
\(\newcommand {\noalign }[1]{\text {#1}\notag \\}\)
\(\newcommand {\cline }[1]{}\)
\(\newcommand {\directlua }[1]{\text {(directlua)}}\)
\(\newcommand {\luatexdirectlua }[1]{\text {(directlua)}}\)
\(\newcommand {\protect }{}\)
\(\def \LWRabsorbnumber #1 {}\)
\(\def \LWRabsorbquotenumber "#1 {}\)
\(\newcommand {\LWRabsorboption }[1][]{}\)
\(\newcommand {\LWRabsorbtwooptions }[1][]{\LWRabsorboption }\)
\(\def \mathchar {\ifnextchar "\LWRabsorbquotenumber \LWRabsorbnumber }\)
\(\def \mathcode #1={\mathchar }\)
\(\let \delcode \mathcode \)
\(\let \delimiter \mathchar \)
\(\def \oe {\unicode {x0153}}\)
\(\def \OE {\unicode {x0152}}\)
\(\def \ae {\unicode {x00E6}}\)
\(\def \AE {\unicode {x00C6}}\)
\(\def \aa {\unicode {x00E5}}\)
\(\def \AA {\unicode {x00C5}}\)
\(\def \o {\unicode {x00F8}}\)
\(\def \O {\unicode {x00D8}}\)
\(\def \l {\unicode {x0142}}\)
\(\def \L {\unicode {x0141}}\)
\(\def \ss {\unicode {x00DF}}\)
\(\def \SS {\unicode {x1E9E}}\)
\(\def \dag {\unicode {x2020}}\)
\(\def \ddag {\unicode {x2021}}\)
\(\def \P {\unicode {x00B6}}\)
\(\def \copyright {\unicode {x00A9}}\)
\(\def \pounds {\unicode {x00A3}}\)
\(\let \LWRref \ref \)
\(\renewcommand {\ref }{\ifstar \LWRref \LWRref }\)
\( \newcommand {\multicolumn }[3]{#3}\)
\(\require {textcomp}\)
\(\newcommand {\LWRmarginnote }[1][]{}\)
\(\newcommand {\marginnote }[2][]{\qquad {\small \textrm {#2}}\LWRmarginnote }\)
\(\def \LWRsidenote {1}\)
\(\newcommand {\sidenotemark }[1][\LWRsidenote ]{{}^{\mathrm {#1}}}\)
\(\newcommand {\intertext }[1]{\text {#1}\notag \\}\)
\(\let \Hat \hat \)
\(\let \Check \check \)
\(\let \Tilde \tilde \)
\(\let \Acute \acute \)
\(\let \Grave \grave \)
\(\let \Dot \dot \)
\(\let \Ddot \ddot \)
\(\let \Breve \breve \)
\(\let \Bar \bar \)
\(\let \Vec \vec \)
\(\newcommand {\nicefrac }[3][]{\mathinner {{}^{#2}\!/\!_{#3}}}\)
\(\newcommand {\unit }[2][]{#1 \mathinner {#2}}\)
\(\newcommand {\unitfrac }[3][]{#1 \mathinner {{}^{#2}\!/\!_{#3}}}\)
\(\newcommand {\bm }[1]{\boldsymbol {#1}}\)
\(\require {mathtools}\)
\(\newenvironment {crampedsubarray}[1]{}{}\)
\(\newcommand {\smashoperator }[2][]{#2\limits }\)
\(\newcommand {\SwapAboveDisplaySkip }{}\)
\(\newcommand {\LaTeXunderbrace }[1]{\underbrace {#1}}\)
\(\newcommand {\LaTeXoverbrace }[1]{\overbrace {#1}}\)
\(\newcommand {\LWRmultlined }[1][]{\begin {multline*}}\)
\(\newenvironment {multlined}[1][]{\LWRmultlined }{\end {multline*}}\)
\(\let \LWRorigshoveleft \shoveleft \)
\(\renewcommand {\shoveleft }[1][]{\LWRorigshoveleft }\)
\(\let \LWRorigshoveright \shoveright \)
\(\renewcommand {\shoveright }[1][]{\LWRorigshoveright }\)
\(\newcommand {\shortintertext }[1]{\text {#1}\notag \\}\)
\(\newcommand {\vcentcolon }{\mathrel {\unicode {x2236}}}\)
\(\newcommand {\Var }{\operatorname {Var}}\)
\(\newcommand {\Expected }{\operatorname {E}}\)
\(\newcommand {\abs }[1]{\left \lvert #1\right \rvert }\)
\(\newcommand {\norm }[1]{\left \lVert #1\right \rVert }\)
\(\newcommand {\rbrackets }[1]{\left (#1\right )}\)
\(\newcommand {\sbrackets }[1]{\left [#1\right ]}\)
\(\newcommand {\cbrackets }[1]{\left \{#1\right \}}\)
\(\newcommand {\RE }{\operatorname {Re}}\)
\(\newcommand {\IM }{\operatorname {IM}}\)
\(\newcommand {\Span }{\operatorname {span}}\)
19.2 Modular arithmetic
Given that we now know that division really exists (as if there was ever any doubt), we can start to talk about remainders.
19.2.1 Core definitions
-
Definition 19.2.1 We say that for \(x, y, m \in \mathbb {Z}\) that
\(\seteqnumber{0}{19.}{21}\)
\begin{equation}
x \equiv _m y
\end{equation}
if and only if \(m | (x - y)\).
-
Theorem 19.2.1 For \(x, y, m \in \mathbb {Z}\), \(x \equiv _m y\) if and only if \(R_{m}(x) = R_m(y)\).
Proof: first we prove the “if” direction; suppose that \(x = a \times m + r\) and \(y = b \times m + r\) where we define \(r = R_m(x) = R_m(y)\). In this case
\(\seteqnumber{0}{19.}{22}\)
\begin{align}
x - y &= a \times m + r - b \times m - r \\ &= (a - b) \times m
\end{align}
and thus \(m | (x - y)\).
For the “only if” direction, things are marginally more hairy. Let us suppose that \(x \equiv _m y\), then
\(\seteqnumber{0}{19.}{24}\)
\begin{equation}
m | (y - x) \iff y - x = km.
\end{equation}
Here we will apply the division algorithm (Theorem 19.1.1), which tells us that we have unique \(R_m(a)\) and \(R_m(b)\) such that
\(\seteqnumber{0}{19.}{25}\)
\begin{align}
x = am + R_m(x) & y = bm + R_m(y) & 0 \leqq R_m(x), R_m(y) < m
\end{align}
Then, it follows from \(0 \leqq R_m(x), R_m(y) < m\) that
\(\seteqnumber{0}{19.}{26}\)
\begin{equation}
-R_m(y) \leqq R_m(x) - R_m(y) < m - R_m(y)
\end{equation}
which in turn implies that
\(\seteqnumber{0}{19.}{27}\)
\begin{equation}
- m < R_m(x) - R_m(y) < m.
\end{equation}
Therefore, we can write that
\(\seteqnumber{0}{19.}{28}\)
\begin{equation}
x - y = am + R_m(x) - (bm + R_m(y))
\end{equation}
from which we can show that \(m | (R_m(x) - R_m(y))\); as \(m | (x - y)\) by definition there exists integer \(k\) such that \(x - y = km\), and thus that
\(\seteqnumber{0}{19.}{29}\)
\begin{equation}
(k - a + b)m = R_m(x) - R_m(y).
\end{equation}
Then as \(-m < R_m(x) - R_m(y) < m\) it must be true that
\(\seteqnumber{0}{19.}{30}\)
\begin{equation}
R_m(x) - R_m(y) = 0m = 0
\end{equation}
and thus the desired equality holds.