avewright/proofwiki-math huggingface dataset:
Theorem: Product of Coprime Factors

Let $a, b, c \in \Z$ such that $a$ and $b$ are coprime.
Let both $a$ and $b$ be divisors of $c$.
Then $a b$ is also a divisor of $c$.
That is:
:$a \perp b \land a \divides c \land b \divides c \implies a b \divides c$

Proof:
By definition of divisor:
:$a \divides c \implies \exists r \in \Z: c = a r$
:$b \divides c \implies \exists s \in \Z: c = b s$
So:
{{begin-eqn}}
{{eqn | l = a
      | o = \perp
      | r = b
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists m, n \in \Z
      | l = m a + n b
      | r = 1
      | c = Integer Combination of Coprime Integers
}}
{{eqn | ll= \leadsto
      | l = c m a + c n b
      | r = c
      | c = 
}}
{{eqn | ll= \leadsto
      | l = b s m a + a r n b
      | r = c
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a b \paren {s m + r n}
      | r = c
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a b
      | o = \divides
      | r = c
      | c = {{Defof|Divisor of Integer}}
}}
{{end-eqn}}
{{qed}}
Theorem: Existence of Lowest Common Multiple

Let $a, b \in \Z: a b \ne 0$.
The lowest common multiple of $a$ and $b$, denoted $\lcm \set {a, b}$, always exists.

Proof:
We prove its existence thus:
$a b \ne 0 \implies \size {a b} \ne 0$
Also $\size {a b} = \pm a b = a \paren {\pm b} = \paren {\pm a} b$.
So the lowest common multiple definitely exists, and we can say that:
:$0 < \lcm \set {a, b} \le \size {a b}$
Now we prove it is the lowest.
That is:
:$a \divides n \land b \divides n \implies \lcm \set {a, b} \divides n$
Let $a, b \in \Z: a b \ne 0, m = \lcm \set {a, b}$.
Let $n \in \Z: a \divides n \land b \divides n$.
We have:
:$n = x_1 a = y_1 b$
:$m = x_2 a = y_2 b$
As $m > 0$, we have:
{{begin-eqn}}
{{eqn | l = n
      | r = m q + r: 0 \le r < \size m = m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = r
      | r = n - m q
      | c =
}}
{{eqn | r = 1 \times n + \paren {-q} \times m
      | c =
}}
{{eqn | ll= \leadsto
      | l = r
      | r = x_1 a + \paren {-q} x_2 a
      | c =
}}
{{eqn | r = y_1 b + \paren {-q} y_2 b
      | c =
}}
{{eqn | ll= \leadsto
      | l = a
      | o = \divides
      | r = r
      | c =
}}
{{eqn | lo= \land
      | l = b
      | o = \divides
      | r = r
      | c = 
}}
{{end-eqn}}
Since $r < m$, and $m$ is the smallest ''positive'' common multiple of $a$ and $b$, it follows that $r = 0$.
So:
:$\forall n \in \Z: a \divides n \land b \divides n: \lcm \set {a, b} \divides n$
That is, $\lcm \set {a, b}$ divides any common multiple of $a$ and $b$.
{{qed}}
Theorem: Existence of Lowest Common Multiple

Let $a, b \in \Z: a b \ne 0$.
The lowest common multiple of $a$ and $b$, denoted $\lcm \set {a, b}$, always exists.

Proof:
Either $a$ and $b$ are coprime or they are not.
Let:
:$a \perp b$
where $a \perp b$ denotes that $a$ and $b$ are coprime.
Let $a b = c$.
Then:
:$a \divides c, b \divides c$
where $a \divides c$ denotes that $a$ is a divisor of $c$.
Suppose both $a \divides d, b \divides d$ for some $d \in \N_{> 0}: d < c$.
Then:
:$\exists e \in \N_{> 0}: a e = d$
:$\exists f \in \N_{> 0}: b f = d$
Therefore:
:$a e = b f$
and from {{EuclidPropLink|book = VII|prop = 19|title = Relation of Ratios to Products}}:
:$a : b = f : e$
But $a$ and $b$ are coprime.
From:
:{{EuclidPropLink|prop = 21|title = Coprime Numbers form Fraction in Lowest Terms}}
and:
:{{EuclidPropLink|prop = 20|title = Ratios of Fractions in Lowest Terms}}
it follows that $b \divides e$
Since:
:$a b = c$
and:
:$a e = d$
it follows from {{EuclidPropLink|prop = 17|title = Multiples of Ratios of Numbers}} that:
:$b : e = c : d$
But $b \divides e$ and therefore:
:$c \divides d$
But $c > d$ which is impossible.
Therefore $a$ and $b$ are both the divisor of no number less than $c$.
Now suppose $a$ and $b$ are not coprime.
Let $f$ and $e$ be the least numbers of those which have the same ratio with $a$ and $b$.
Then from {{EuclidPropLink|prop = 19|title = Relation of Ratios to Products}}:
:$a e = b f$
Let $a e = c$.
Then $b f = c$.
Hence:
:$a \divides c$
:$b \divides c$
Suppose $a$ and $b$ are both the divisor of some number $d$ which is less than $c$.
Let:
:$a g = d$
and:
:$b h = d$
Therefore:
:$a g = b h$
and so by {{EuclidPropLink|prop = 19|title = Relation of Ratios to Products}}:
:$a : b = f : e$
Also:
:$f : e = h : g$
But $f, e$ are the least such.
From {{EuclidPropLink|prop = 20|title = Ratios of Fractions in Lowest Terms}}:
:$e \divides g$
Since $a e = c$ and $a g = d$, from {{EuclidPropLink|prop = 17|title = Multiples of Ratios of Numbers}}:
:$e : g = c : d$
But:
:$e \divides g$
So $c \divides d$
But $c > d$ which is impossible.
Therefore $a$ and $b$ are both the divisor of no number less than $c$.
{{qed}}
Theorem: Existence of Lowest Common Multiple

Let $a, b \in \Z: a b \ne 0$.
The lowest common multiple of $a$ and $b$, denoted $\lcm \set {a, b}$, always exists.

Proof:
Note that as Integer Divides Zero, both $a$ and $b$ are divisors of zero.
Thus by definition $0$ is a common multiple of $a$ and $b$.
Non-trivial common multiples of $a$ and $b$ exist.
Indeed, $a b$ and $-\paren {a b}$ are common multiples of $a$ and $b$.
Either $a b$ or $-\paren {a b}$ is strictly positive.
Let $S$ denote the set of strictly positive common multiples of $a$ and $b$.
By the Well-Ordering Principle, $S$ contains a smallest element.
This can then be referred to as the lowest common multiple of $a$ and $b$.
{{qed}}
Theorem: Product of GCD and LCM

:$\lcm \set {a, b} \times \gcd \set {a, b} = \size {a b}$
where:
:$\lcm \set {a, b}$ denotes the lowest common multiple of $a$ and $b$
:$\gcd \set {a, b}$ denotes the greatest common divisor of $a$ and $b$.

Proof:
It is sufficient to prove that $\lcm \set {a, b} \times \gcd \set {a, b} = a b$, where $a, b \in \Z_{>0}$.
{{begin-eqn}}
{{eqn | l = d 
      | r = \gcd \set {a, b}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = d
      | o = \divides
      | r = a b
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists n \in \Z_{>0}
      | l = a b
      | r = d n
      | c=
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = d \divides a
      | o = \land
      | r = d \divides b
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists u, v \in \Z
      | l = a = d u
      | o = \land
      | r = b = d v
      | c = 
}}
{{eqn | ll= \leadsto
      | l = d u b = d n
      | o = \land
      | r = a d v = d n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = n = b u
      | o = \land
      | r = n = a v
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a \divides n
      | o = \land
      | r = b \divides n
      | c = 
}}
{{end-eqn}}
Now we have:
:$a \divides m \land b \divides m \implies m = a r = b s$
Also, by Bézout's Identity we have:
:$d = a x + b y$
So:
{{begin-eqn}}
{{eqn | l = m d
      | r = a x m + b y m
      | c = 
}}
{{eqn | r = b s a x + a r b y
      | c = 
}}
{{eqn | r = a b \paren {s x + r y}
      | c = 
}}
{{eqn | r = d n \paren {s x + r y}
      | c = 
}}
{{end-eqn}}
So:
:$m = n \paren {s x + r y}$
Thus:
:$n \divides m \implies n \le \size m$
while:
:$a b = d n = \gcd \set {a, b} \times \lcm \set {a, b}$
as required.
{{qed}}
Theorem: Product of GCD and LCM

:$\lcm \set {a, b} \times \gcd \set {a, b} = \size {a b}$
where:
:$\lcm \set {a, b}$ denotes the lowest common multiple of $a$ and $b$
:$\gcd \set {a, b}$ denotes the greatest common divisor of $a$ and $b$.

Proof:
Let $a = g m$ and $b = g n$, where $g = \gcd \set {a, b}$ and $m$ and $n$ are coprime.
The existence of $m$ and $n$ are proved by Integers Divided by GCD are Coprime.
It follows that:
:$a = g m \divides g m n$
and:
:$b = g n \divides g m n$
So $g m n$ is a common multiple of $a$ and $b$. 
Hence there exists an integer $g k \le g m n$ that is divisible by both $a$ and $b$.
Then:
{{begin-eqn}}
{{eqn | l = a
      | r = g m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = g m
      | o = \divides
      | r = g k
      | c = 
}}
{{eqn | ll= \leadsto
      | l = m
      | o = \divides
      | r = k
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = b
      | r = g n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = g n
      | o = \divides
      | r = g k
      | c = 
}}
{{eqn | ll= \leadsto
      | l = n
      | o = \divides
      | r = k
      | c = 
}}
{{end-eqn}}
As $g k \le g m n$, it follows that:
:$k \le m n$
But $m, n$ are coprime.
So:
{{begin-eqn}}
{{eqn | l = \map \lcm {m, n}
      | r = m n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = k
      | o = \not <
      | r = m n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = k
      | r = m n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = g k
      | r = g m n
      | c = 
}}
{{eqn | r = \map \lcm {a, b}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \lcm \set {a, b} \times \gcd \set {a, b}
      | r = g m n \times g
      | c = 
}}
{{eqn | r = g m \times g n
      | c = 
}}
{{eqn | r = \size {a b}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Product of GCD and LCM

:$\lcm \set {a, b} \times \gcd \set {a, b} = \size {a b}$
where:
:$\lcm \set {a, b}$ denotes the lowest common multiple of $a$ and $b$
:$\gcd \set {a, b}$ denotes the greatest common divisor of $a$ and $b$.

Proof:
Let $d := \gcd \set {a, b}$. 
Then by definition of the GCD, there exist $j_1, j_2 \in \Z$ such that $a = d j_1$ and $b = d j_2$.
Because $d$ divides both $a$ and $b$, it must divide their product:
:$\exists l \in \Z$ such that $a b = d l$
Then we have: 
{{begin-eqn}}
{{eqn | l = d l
      | m = \paren {d j_1} b
      | mo= =
      | r = a \paren {d j_2}
}}
{{eqn | ll= \leadsto
      | l = l
      | m = j_1 b
      | mo= =
      | r = a j_2
}}
{{end-eqn}}
showing that $a \divides l$ and $b \divides l$.
That is, $l$ is a common multiple of $a$ and $b$.
Now it must be shown that $l$ is the least such number.
Let $m$ be any common multiple of $a$ and $b$.
Then there exist $k_1, k_2 \in \Z$ such that $m = a k_1 = b k_2$.
By Bézout's Identity:
:$\exists x, y \in \Z: d = a x + b y$
So:
{{begin-eqn}}
{{eqn | l = m d
      | r = m a x + m b y
}}
{{eqn | r = \paren {b k_2} a x + \paren {a k_1} b y
}}
{{eqn | r = a b \paren {b k_2 + a k_1}
}}
{{eqn | r = d l \paren {b k_2 + a k_1}
}}
{{end-eqn}}
Thus:
:$m = l \paren {b k_2 + a k_1}$
that is, $l \divides m$.
Hence by definition of the LCM:
:$\lcm \set {a, b} = l$
In conclusion:
:$a b = d l = \gcd \set {a, b} \cdot \lcm \set {a, b}$
{{qed}}
Theorem: Product of GCD and LCM

:$\lcm \set {a, b} \times \gcd \set {a, b} = \size {a b}$
where:
:$\lcm \set {a, b}$ denotes the lowest common multiple of $a$ and $b$
:$\gcd \set {a, b}$ denotes the greatest common divisor of $a$ and $b$.

Proof:
From Fundamental Theorem of Arithmetic, let:
{{begin-eqn}}
{{eqn | l = m
      | r = {p_1}^{k_1} {p_2}^{k_2} \dotsm {p_r}^{k_r}
}}
{{eqn | l = n
      | r = {p_1}^{l_1} {p_2}^{l_2} \dotsm {p_r}r^{l_r}
      | c = 
}}
{{end-eqn}}
From LCM from Prime Decomposition:
:$\lcm \set {m, n} = p_1^{\max \set {k_1, l_1} } p_2^{\max \set {k_2, l_2} } \dotsm p_r^{\max \set {k_r, l_r} }$
From GCD from Prime Decomposition:
:$\gcd \set {m, n} = p_1^{\min \set {k_1, l_1} } p_2^{\min \set {k_2, l_2} } \dotsm p_r^{\min \set {k_r, l_r} }$
From Sum of Maximum and Minimum, for all $i \in \set {1, 2, \ldots, r}$:
:$\min \set {k_i, l_i} + \max \set {k_i, l_i} = k_i + l_i$
Hence:
{{begin-eqn}}
{{eqn | l = \gcd \set {m, n} \times \lcm \set {m, n}
      | r = p_1^{k_1 + l_1} p_2^{k_2 + l_2} \dotsm p_r^{k_r + l_r}
      | c = 
}}
{{eqn | r = p_1^{k_1} p_1^{l_1} p_2^{k_2} p_2^{l_2} \dotsm p_r^{k_r} p_r^{l_r}
      | c = 
}}
{{eqn | r = p_1^{k_1} p_2^{k_2} \dotsm p_r^{k_r} \times p_1^{l_1} p_2^{l_2} \dotsm p_r^{l_r}
      | c = 
}}
{{eqn | r = m n
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Product of GCD and LCM

:$\lcm \set {a, b} \times \gcd \set {a, b} = \size {a b}$
where:
:$\lcm \set {a, b}$ denotes the lowest common multiple of $a$ and $b$
:$\gcd \set {a, b}$ denotes the greatest common divisor of $a$ and $b$.

Proof:
Let $d := \gcd \set {a, b}$. 
Then by definition of the GCD, there exist $r, s\in \Z$ such that $a = d r$ and $b = d s$.
Let $m = \dfrac {a b} d$.
Then:
:$m = a s = r b$
which makes $m$ a common multiple of $a$ and $b$.
Let $c \in \Z_{>0}$ be a common multiple of $a$ and $b$.
Let us say that:
:$c = a u = b v$
From Bézout's Identity:
:$\exists x, y \in \Z: d = a x + b y$
Then:
{{begin-eqn}}
{{eqn | l = \dfrac c m
      | r = \dfrac {c d} {a b}
}}
{{eqn | r = \dfrac {c \paren {a x + b y} } {a b}
}}
{{eqn | r = \dfrac c b x + \dfrac c a y
}}
{{eqn | r = v x + n y
}}
{{end-eqn}}
That is:
:$m \divides c$
where $\divides$ denotes divisibility.
So by Absolute Value of Integer is not less than Divisors:
:$m \le c$
Hence by definition of the LCM:
:$\lcm \set {a, b} = m$
In conclusion:
:$\lcm \set {a, b} = \dfrac {a b} d = \dfrac {a b} {\gcd \set {a, b} }$
and the result follows.
{{qed}}
Theorem: Congruent to Zero iff Modulo is Divisor

Let $a, z \in \R$.
Then $a$ is congruent to $0$ modulo $z$ {{iff}} $a$ is an integer multiple of $z$.
:$\exists k \in \Z: k z = a \iff a \equiv 0 \pmod z$
If $z \in \Z$, then further:
:$z \divides a \iff a \equiv 0 \pmod z$

Proof:
{{begin-eqn}}
{{eqn | q = \exists k \in \Z
      | l = a
      | r = k z
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists k \in \Z
      | l = a
      | r = 0 + k z
      | c = 
}}
{{end-eqn}}
Thus by definition of congruence, $a \equiv 0 \pmod z$ and the result is proved.
If $z$ is an integer, then by definition of divisor:
:$z \divides a \iff \exists k \in \Z: a = k z$
Hence the result for integer $z$.
{{qed}}
Category:Modulo Arithmetic
j0ebzok84v7um3g66ui8uges9abgk8m
Theorem: Integer is Congruent Modulo Divisor to Remainder

Let $a \in \Z$.
Let $a$ have a remainder $r$ on division by $m$.
Then:
:$a \equiv r \pmod m$
where the notation denotes that $a$ and $r$ are congruent modulo $m$.

Proof:
Let $a$ have a remainder $r$ on division by $m$.
Then:
:$\exists q \in \Z: a = q m + r$
Hence by definition of congruence modulo $m$:
:$a \equiv r \pmod m$
{{qed}}
Theorem: Integer is Congruent to Integer less than Modulus

Let $m \in \Z$.
Then each integer is congruent (modulo $m$) to precisely one of the integers $0, 1, \ldots, m - 1$.

Proof:
=== Existence ===
Let $a \in \Z$.
Then from the Division Theorem: $\exists r \in \set {0, 1, \ldots, m - 1}: a \equiv r \pmod m$.
{{qed|lemma}}
Theorem: Modulo Addition is Well-Defined

Let $m \in \Z$ be an integer.
Let $\Z_m$ be the set of integers modulo $m$.
Let $\eqclass a m$ denote the equivalence class on $\Z_m$, for some $a \in \Z$.
The modulo addition operation on $\Z_m$, defined by the rule:
:$\eqclass a m +_m \eqclass b m = \eqclass {a + b} m$
is a well-defined operation.
That is:
:If $a \equiv b \pmod m$ and $x \equiv y \pmod m$, then $a + x \equiv b + y \pmod m$.

Proof:
We need to show that if:
:$\eqclass {x'} m = \eqclass x m$
:$\eqclass {y'} m = \eqclass y m$
then:
:$\eqclass {x' + y'} m = \eqclass {x + y} m$
Since:
:$\eqclass {x'} m = \eqclass x m$
and:
:$\eqclass {y'} m = \eqclass y m$
it follows from the definition of set of integers modulo $m$ that:
:$x \equiv x' \pmod m$
and:
:$y \equiv y' \pmod m$
By definition, we have:
:$x \equiv x' \pmod m \implies \exists k_1 \in \Z: x = x' + k_1 m$
:$y \equiv y' \pmod m \implies \exists k_2 \in \Z: y = y' + k_2 m$
which gives us:
:$x + y = x' + k_1 m + y' + k_2 m = x' + y' + \paren {k_1 + k_2} m$
As $k_1 + k_2$ is an integer, it follows that, by definition:
:$x + y \equiv \paren {x' + y'} \pmod m$
Therefore, by the definition of integers modulo $m$:
:$\eqclass {x' + y'} m = \eqclass {x + y} m$
{{qed}}
Theorem: Modulo Addition is Well-Defined

Let $m \in \Z$ be an integer.
Let $\Z_m$ be the set of integers modulo $m$.
Let $\eqclass a m$ denote the equivalence class on $\Z_m$, for some $a \in \Z$.
The modulo addition operation on $\Z_m$, defined by the rule:
:$\eqclass a m +_m \eqclass b m = \eqclass {a + b} m$
is a well-defined operation.
That is:
:If $a \equiv b \pmod m$ and $x \equiv y \pmod m$, then $a + x \equiv b + y \pmod m$.

Proof:
The equivalence class $\eqclass a m$ is defined as:
:$\eqclass a m = \set {x \in \Z: x = a + k m: k \in \Z}$
That is, the set of all integers which differ from $a$ by an integer multiple of $m$.
Thus the notation for addition of two set of integers modulo $m$ is not usually:
:$\eqclass a m +_m \eqclass b m$
What is more normally seen is:
:$a + b \pmod m$
Using this notation:
{{begin-eqn}}
{{eqn | l = a
      | o = \equiv
      | r = b
      | rr= \pmod m
      | c =
}}
{{eqn | lo= \land
      | l = c
      | o = \equiv
      | r = d
      | rr= \pmod m
      | c =
}}
{{eqn | ll= \leadsto
      | l = a \bmod m
      | r = b \bmod m
      | c = {{Defof|Congruence Modulo Integer}}
}}
{{eqn | lo= \land
      | l = c \bmod m
      | r = d \bmod m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a
      | r = b + k_1 m
      | c = for some $k_1 \in \Z$
}}
{{eqn | lo= \land
      | l = c
      | r = d + k_2 m
      | c = for some $k_2 \in \Z$
}}
{{eqn | ll= \leadsto
      | l = a + c
      | r = b + d + \paren {k_1 + k_2} m
      | c = {{Defof|Integer Addition}}
}}
{{eqn | ll= \leadsto
      | l = a + c
      | o = \equiv
      | r = b + d
      | rr= \pmod m
      | c = {{Defof|Modulo Addition}}
}}
{{end-eqn}}
{{qed}}
Theorem: Modulo Multiplication is Well-Defined

The multiplication modulo $m$ operation on $\Z_m$, the set of integers modulo $m$, defined by the rule:
:$\eqclass x m \times_m \eqclass y m = \eqclass {x y} m$
is a well-defined operation.
That is:
:If $a \equiv b \pmod m$ and $x \equiv y \pmod m$, then $a x \equiv b y \pmod m$.

Proof:
We need to show that if:
:$\eqclass {x'} m = \eqclass x m$
and:
:$\eqclass {y'} m = \eqclass y m$
then:
:$\eqclass {x' y'} m = \eqclass {x y} m$
We have that:
:$\eqclass {x'} m = \eqclass x m$
and:
:$\eqclass {y'} m = \eqclass y m$
It follows from the definition of residue class modulo $m$ that:
:$x \equiv x' \pmod m$
and:
:$y \equiv y' \pmod m$
By definition, we have:
:$x \equiv x' \pmod m \implies \exists k_1 \in \Z: x = x' + k_1 m$
:$y \equiv y' \pmod m \implies \exists k_2 \in \Z: y = y' + k_2 m$
which gives us:
:$x y = \paren {x' + k_1 m} \paren {y' + k_2 m} = x' y' + \paren {x' k_2 + y' k_1} m + k_1 k_2 m^2$
Thus by definition:
:$x y \equiv \paren {x' y'} \pmod m$
Therefore, by the definition of residue class modulo $m$:
:$\eqclass {x' y'} m = \eqclass {x y} m$
{{qed}}
Theorem: Modulo Multiplication is Well-Defined

The multiplication modulo $m$ operation on $\Z_m$, the set of integers modulo $m$, defined by the rule:
:$\eqclass x m \times_m \eqclass y m = \eqclass {x y} m$
is a well-defined operation.
That is:
:If $a \equiv b \pmod m$ and $x \equiv y \pmod m$, then $a x \equiv b y \pmod m$.

Proof:
The equivalence class $\eqclass a m$ is defined as:
:$\eqclass a m = \set {x \in \Z: x = a + k m: k \in \Z}$
that is, the set of all integers which differ from $a$ by an integer multiple of $m$.
Thus the notation for multiplication of two residue classes modulo $z$ is not usually $\eqclass a m \times_m \eqclass b m$.
What is more normally seen is:
:$a b \pmod m$
Using this notation:
{{begin-eqn}}
{{eqn | l = a
      | o = \equiv
      | r = b
      | rr= \pmod m
      | c = 
}}
{{eqn | lo= \land
      | l = c
      | o = \equiv
      | r = d
      | rr= \pmod m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a \bmod m
      | r = b \bmod m
      | c = {{Defof|Congruence Modulo Integer}}
}}
{{eqn | lo= \land
      | l = c \bmod m
      | r = d \bmod m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a
      | r = b + k_1 m
      | c = for some $k_1 \in \Z$
}}
{{eqn | lo= \land
      | l = c
      | r = d + k_2 m
      | c = for some $k_2 \in \Z$
}}
{{eqn | ll= \leadsto
      | l = a c
      | r = \paren {b + k_1 m} \paren {d + k_2 m}
      | c = {{Defof|Multiplication}}
}}
{{eqn | r = b d + b k_2 m + d k_1 m + k_1 k_2 m^2
      | c = Integer Multiplication Distributes over Addition
}}
{{eqn | r = b d + \paren {b k_2 + d k_1 + k_1 k_2 m} m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a c
      | o = \equiv
      | r = b d
      | rr= \pmod m
      | c = {{Defof|Modulo Multiplication}}
}}
{{end-eqn}}
{{qed}}
Theorem: Congruence of Product

Let $a, b, z \in \R$.
Let $a$ be congruent to $b$ modulo $z$, that is:
:$a \equiv b \pmod z$
Then:
:$\forall m \in \Z: m a \equiv m b \pmod z$

Proof:
Let $m \in \Z$ and $a \equiv b \pmod z$.
Suppose $m = 0$.
Then the {{RHS}} of the assertion degenerates to $0 \equiv 0 \pmod z$ which is trivially true.
Otherwise, from Congruence by Product of Moduli, we have:
:$a \equiv b \iff m a \equiv m b \pmod z$
As $m \in \Z$, it follows that $m z$ is an integer multiple of $z$.
Hence from Congruence by Divisor of Modulus, it follows that:
:$m a \equiv m b \implies m a \equiv m b \pmod z$
{{qed}}
Theorem: Congruence of Powers

Let $a, b \in \R$ and $m \in \Z$.
Let $a$ be congruent to $b$ modulo $m$, that is:
:$a \equiv b \pmod m$
Then:
:$\forall n \in \Z_{\ge 0}: a^n \equiv b^n \pmod m$

Proof:
Proof by induction:
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$a \equiv b \implies a^k \equiv b^k \pmod m$
$\map P 0$ is trivially true, as $a^0 = b^0 = 1$.
$\map P 1$ is true, as this just says:
:$a \equiv b \pmod m$
Theorem: Modulo Addition is Associative

Addition modulo $m$ is associative:
:$\forall \eqclass x m, \eqclass y m, \eqclass z m \in \Z_m: \paren {\eqclass x m +_m \eqclass y m} +_m \eqclass z m = \eqclass x m +_m \paren {\eqclass y m +_m \eqclass z m}$
where $\Z_m$ is the set of integers modulo $m$.
That is:
:$\forall x, y, z \in \Z: \paren {x + y} + z \equiv x + \paren {y + z} \pmod m$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {\eqclass x m +_m \eqclass y m} +_m \eqclass z m
      | r = \eqclass {x + y} m +_m \eqclass z m
      | c = {{Defof|Modulo Addition}}
}}
{{eqn | r = \eqclass {\paren {x + y} + z} m
      | c = {{Defof|Modulo Addition}}
}}
{{eqn | r = \eqclass {x + \paren {y + z} } m
      | c = Associative Law of Addition
}}
{{eqn | r = \eqclass x m +_m \eqclass {y + z} m
      | c = {{Defof|Modulo Addition}}
}}
{{eqn | r = \eqclass x m +_m \paren {\eqclass y m +_m \eqclass z m}
      | c = {{Defof|Modulo Addition}}
}}
{{end-eqn}}
{{qed}}
Theorem: Modulo Addition is Commutative

Modulo addition is commutative:
:$\forall x, y, z \in \Z: x + y \pmod m = y + x \pmod m$

Proof:
From the definition of modulo addition, this is also written:
:$\forall m \in \Z: \forall \eqclass x m, \eqclass y m \in \Z_m: \eqclass x m +_m \eqclass y m = \eqclass y m +_m \eqclass x m$
By Modulo Addition is Well-Defined, $+_m$ is well-defined.
Hence:
{{begin-eqn}}
{{eqn | l = \eqclass x m +_m \eqclass y m
      | r = \eqclass {x + y} m
      | c = {{Defof|Modulo Addition}}
}}
{{eqn | r = \eqclass {y + x} m
      | c = Commutative Law of Addition
}}
{{eqn | r = \eqclass y m +_m \eqclass x m
      | c = {{Defof|Modulo Addition}}
}}
{{end-eqn}}
{{qed}}
Theorem: Modulo Addition has Identity

Let $m \in \Z$ be an integer.
Then addition modulo $m$ has an identity:
:$\forall \eqclass x m \in \Z_m: \eqclass x m +_m \eqclass 0 m = \eqclass x m = \eqclass 0 m +_m \eqclass x m$
That is:
:$\forall a \in \Z: a + 0 \equiv a \equiv 0 + a \pmod m$

Proof:
{{begin-eqn}}
{{eqn | l = \eqclass x m +_m \eqclass 0 m
      | r = \eqclass {x + 0} m
      | c = {{Defof|Modulo Addition}}
}}
{{eqn | r = \eqclass x m
      | c = 
}}
{{eqn | r = \eqclass {0 + x} m
      | c = 
}}
{{eqn | r = \eqclass 0 m +_m \eqclass x m
      | c = {{Defof|Modulo Addition}}
}}
{{end-eqn}}
Thus $\eqclass 0 m$ is the identity for addition modulo $m$.
{{Qed}}
Theorem: Modulo Addition has Inverses

Let $m \in \Z$ be an integer.
Then addition modulo $m$ has inverses:
For each element $\eqclass x m \in \Z_m$, there exists the element $\eqclass {-x} m \in \Z_m$ with the property:
:$\eqclass x m +_m \eqclass {-x} m = \eqclass 0 m = \eqclass {-x} m +_m \eqclass x m$
where $\Z_m$ is the set of integers modulo $m$.
That is:
:$\forall a \in \Z: a + \paren {-a} \equiv 0 \equiv \paren {-a} + a \pmod m$

Proof:
Let $x \in \Z$ be arbitrary.
As $x \in \Z$ implies $-x \in \Z$, we have:
:$\eqclass {-x} m \in \Z_m$
Therefore:
{{begin-eqn}}
{{eqn | l = \eqclass x m +_m \eqclass {-x} m
      | r = \eqclass {x + \paren {-x} } m
      | c = {{Defof|Modulo Addition}}
}}
{{eqn | r = \eqclass 0 m
      | c = 
}}
{{eqn | r = \eqclass {\paren {-x} + x} m
      | c = 
}}
{{eqn | r = \eqclass {-x} m +_m \eqclass x m
      | c = {{Defof|Modulo Addition}}
}}
{{end-eqn}}
{{qed}}