3. Parity and divisibility
The problems in this chapter concern some elementary properties of natural numbers and integers: parity (whether a number is even or odd), divisibility, and congruence modulo \(n\).
There are no new logical symbols like \(\lor\) or \(\exists\) in this chapter, and no major additions (such as the use of intermediate steps or lemmas) to our reasoning toolkit. Thus this chapter functions as a breather between the hard work of Chapter 2 and Chapter 4, a chance to consolidate what you have learned.
3.1. Definitions; parity
3.1.1. Example
When a mathematical term is introduced for the first time, it is given a definition.
Definition
An integer \(a\) is odd, if there exists an integer \(k\), such that \(a=2k+1\).
Here’s how we make a definition in Lean.
def Odd (a : ℤ) : Prop := ∃ k, a = 2 * k + 1
On paper, you need to memorize every definition; this is crucial to be able to work with them.
In Lean, when you see a term whose definition you’d like to double-check, you can right-click
(Windows) / two-finger-click (Mac) to bring up an option “Go to Definition”. This will send you
to the place in the Lean code where the definition was introduced. (The keyboard shortcut
Ctrl
--
will bring you back from that definition to where you were working before.)
Problem
Show that \(7\) is odd.
Solution
\(7=2\cdot 3+1\), so \(7\) is odd.
Here’s how this problem looks in Lean.
example : Odd (7:ℤ) := by
sorry
The goal state at the start is:
⊢ Odd 7
You can check a definition within a proof using the dsimp
(“definitional-simplify”) tactic.
Here, you can type dsimp [Odd]
within the proof to have the definition of “odd” unfolded for
you:
example : Odd (7:ℤ) := by
dsimp [Odd]
After doing this, the goal is displayed using the definition of “odd” rather than with the word “odd”:
⊢ ∃ (k : ℤ), 7 = 2 * k + 1
This is optional, though; the proof will still work if you delete the dsimp
line.
Here is the full Lean translation of the solution.
example : Odd (7 : ℤ) := by
dsimp [Odd]
use 3
numbers
If you don’t quite follow the proof – either in its text version or its Lean version – then reread some of the examples in Section 2.5, such as Example 2.5.3.
3.1.2. Example
Here’s a similar example.
Problem
Show that \(-3\) is odd.
example : Odd (-3 : ℤ) := by
sorry
You should show that \(-3=2k+1\) for some integer \(k\). But what is the \(k\) that works?
3.1.3. Example
Problem
Prove that if \(n\) is an odd integer, then \(3n+2\) is odd.
Solution
Let n be odd. Then there exists an integer \(k\) such that \(n = 2k+1\). Thus
so \(3n+2\) is odd.
In the Lean version of the problem, the goal state initially looks like this.
n : ℤ
hn : Odd n
⊢ Odd (3 * n + 2)
If you want to unfold the definition Odd
in the goal, you can use dsimp [Odd]
, as
discussed in Example 3.1.1. If you want to unfold the definition Odd
everywhere
(goals and hypotheses), you can use dsimp [Odd] at *
. After that the goal state looks like
this:
n : ℤ
hn : ∃ (k : ℤ), n = 2 * k + 1
⊢ ∃ (k : ℤ), 3 * n + 2 = 2 * k + 1
This is our first encounter with something which might be confusing. The variable inside an
existential is a “throwaway” variable, which exists only for the duration of the sentence. So the
same variable might occur within the goal state repeatedly, without meaning the same thing. Here
the k
in the hypothesis hn
is different from the k
in the goal; it’s just the default
name when the definition “odd” is unfolded.
example {n : ℤ} (hn : Odd n) : Odd (3 * n + 2) := by
dsimp [Odd] at *
obtain ⟨k, hk⟩ := hn
use 3 * k + 2
calc
3 * n + 2 = 3 * (2 * k + 1) + 2 := by rw [hk]
_ = 2 * (3 * k + 2) + 1 := by ring
Again, you can check that the dsimp
line is not actually needed in the solution.
3.1.4. Example
Problem
Let \(n\) be an integer. Prove that if \(n\) is odd, then \(7n-4\) is odd.
example {n : ℤ} (hn : Odd n) : Odd (7 * n - 4) := by
sorry
3.1.5. Example
Problem
Prove that if the integers \(x\) and \(y\) are odd, then \(x+y+1\) is odd.
Solution
Since \(x\) and \(y\) are odd, there exists an integer \(a\) such that \(x=2a+1\), and there exists an integer \(b\) such that \(y=2b+1\). Then
so \(x+y+1\) is odd.
example {x y : ℤ} (hx : Odd x) (hy : Odd y) : Odd (x + y + 1) := by
obtain ⟨a, ha⟩ := hx
obtain ⟨b, hb⟩ := hy
use a + b + 1
calc
x + y + 1 = 2 * a + 1 + (2 * b + 1) + 1 := by rw [ha, hb]
_ = 2 * (a + b + 1) + 1 := by ring
3.1.6. Example
Problem
Prove that if the integers \(x\) and \(y\) are odd, then \(xy+2y\) is odd.
Solution
Since \(x\) and \(y\) are odd, there exists an integer \(a\) such that \(x=2a+1\), and there exists an integer \(b\) such that \(y=2b+1\). Then
so \(xy+2y\) is odd.
example {x y : ℤ} (hx : Odd x) (hy : Odd y) : Odd (x * y + 2 * y) := by
sorry
3.1.7. Example
You can probably guess the definition of “even”.
Definition
An integer \(a\) is even, if there exists an integer \(k\), such that \(a=2k\).
def Even (a : ℤ) : Prop := ∃ k, a = 2 * k
Problem
Let \(m\) be an integer. Prove that if \(m\) is odd, then \(3m-5\) is even.
Solution
Since m is odd, there exists an integer \(t\) such that \(m = 2t+1\). Thus
so \(3m-5\) is even.
example {m : ℤ} (hm : Odd m) : Even (3 * m - 5) := by
sorry
3.1.8. Example
Problem
Let \(n\) be an even integer. Prove that \(n ^ 2 + 2 n - 5\) is odd.
example {n : ℤ} (hn : Even n) : Odd (n ^ 2 + 2 * n - 5) := by
sorry
3.1.9. Example
In fact every integer is either even or odd; we will discuss how to prove this later, in Example 4.2.9.
In Lean this fact can be invoked as the lemma Int.even_or_odd
:
lemma Int.even_or_odd (n : ℤ) : Even n ∨ Odd n :=
Problem
Let \(n\) be an integer. Prove that \(n ^ 2 + n + 4\) is even.
Solution
We consider two cases, depending on whether \(n\) is even or odd.
If \(n\) is even, then there exists an integer \(x\) such that \(n=2x\). Then
so \(n ^ 2 + n + 4\) is even.
If \(n\) is odd, then there exists an integer \(x\) such that \(n=2x+1\). Then
so \(n ^ 2 + n + 4\) is again even.
example (n : ℤ) : Even (n ^ 2 + n + 4) := by
obtain hn | hn := Int.even_or_odd n
· obtain ⟨x, hx⟩ := hn
use 2 * x ^ 2 + x + 2
calc
n ^ 2 + n + 4 = (2 * x) ^ 2 + 2 * x + 4 := by rw [hx]
_ = 2 * (2 * x ^ 2 + x + 2) := by ring
· obtain ⟨x, hx⟩ := hn
use 2 * x ^ 2 + 3 * x + 3
calc
n ^ 2 + n + 4 = (2 * x + 1) ^ 2 + (2 * x + 1) + 4 := by rw [hx]
_ = 2 * (2 * x ^ 2 + 3 * x + 3) := by ring
3.1.10. Exercises
Prove that -9 is odd.
example : Odd (-9 : ℤ) := by sorry
Prove that 26 is even.
example : Even (26 : ℤ) := by sorry
Let \(m\) be an odd integer and \(n\) be an even integer. Prove that \(n + m\) is odd.
example {m n : ℤ} (hm : Odd m) (hn : Even n) : Odd (n + m) := by sorry
Let \(p\) be an odd integer and let \(q\) be an even integer. Show that \(p - q - 4\) is odd.
example {p q : ℤ} (hp : Odd p) (hq : Even q) : Odd (p - q - 4) := by sorry
Let \(a\) be an even integer and let \(b\) be an odd integer. Show that \(3a + b - 3\) is even.
example {a b : ℤ} (ha : Even a) (hb : Odd b) : Even (3 * a + b - 3) := by sorry
Prove that if the integers \(r\) and \(s\) are odd, then \(3r-5s\) is even.
example {r s : ℤ} (hr : Odd r) (hs : Odd s) : Even (3 * r - 5 * s) := by sorry
Let \(x\) be an integer. Show that if \(x\) is odd then so is \(x^3\).
example {x : ℤ} (hx : Odd x) : Odd (x ^ 3) := by sorry
Let \(n\) be an odd integer. Show that \(n^2-3n+2\) is even.
example {n : ℤ} (hn : Odd n) : Even (n ^ 2 - 3 * n + 2) := by sorry
Let \(a\) be an integer and suppose that \(a\) is odd. Show that \(a^2+2a-4\) is odd.
example {a : ℤ} (ha : Odd a) : Odd (a ^ 2 + 2 * a - 4) := by sorry
Let \(p\) be an odd integer. Show that \(p^2+3p-5\) is odd.
example {p : ℤ} (hp : Odd p) : Odd (p ^ 2 + 3 * p - 5) := by sorry
Let \(x\) and \(y\) be odd integers. Show that \(xy\) is odd.
example {x y : ℤ} (hx : Odd x) (hy : Odd y) : Odd (x * y) := by sorry
Let \(n\) be an integer. Show that \(3n^2+3n- 1\) is odd.
example (n : ℤ) : Odd (3 * n ^ 2 + 3 * n - 1) := by sorry
Let \(n\) be an integer. Show that there exists an integer \(m\geq n\) which is odd.
example (n : ℤ) : ∃ m ≥ n, Odd m := by sorry
Let \(a\), \(b\) and \(c\) be integers. Show that at least one of \(a-b\), \(a+c\) or \(b-c\) is even. 1
example (a b c : ℤ) : Even (a - b) ∨ Even (a + c) ∨ Even (b - c) := by sorry
Footnotes
- 1
Exercise taken from Hammack, Book of Proof, Chapter 9.
3.2. Divisibility
3.2.1. Example
Another mathematical definition you may have seen before is the definition of divisibility.
Definition
A natural number \(b\) is divisible by another natural number \(a\), if there exists a natural number \(c\), such that \(b=ac\).
For example,
Problem
Show that the natural number 88 is divisible by 11.
Solution
\(88 = 11 \cdot 8\).
Divisibility is a very important concept, and there are several different names for it. All the following mean the same thing:
\(b\) is divisible by \(a\)
\(b\) is a multiple of \(a\)
\(a\) is a divisor of \(b\)
\(a\) is a factor of \(b\)
\(a\) divides \(b\)
We will most frequently use the last of these, “\(a\) divides \(b\),” since it’s the most compact. There is also a standard notation, \(a \mid b\), which we will also use frequently.
In Lean, the definition of divisibility is already in the library,
together with many theorems about it. We will typically work with this definition in Lean using
the notation, ∣
, which you can type in Lean as \|
or \mid
. (In general, hover over a
symbol in VSCode with your mouse to find out how to type it.) Warning: this is different from the
visually similar symbol |
which appears on your keyboard and which we use in obtain
statements.
As in Section 3.1 with dsimp [Odd]
, it is possible to unfold the definition of
divisibility in the middle of a Lean proof to remind yourself of what it means in the current
context. You can write either dsimp [Dvd.dvd]
(this being the text name of the Lean notation
\(\mid\) for divisibility) or dsimp [(· ∣ ·)]
– unfortunately dsimp [∣]
without the
dots and parentheses does not work. As in the Section 3.1 examples, this unfolding
is optional – the proof still works without it.
example : (11 : ℕ) ∣ 88 := by
dsimp [(· ∣ ·)]
use 8
numbers
3.2.2. Example
Another feature of this definition is that, although we stated it above for natural numbers, we will also often want to consider divisibility of integers. Here is the corresponding definition for integers:
Definition
An integer \(b\) is divisible by another integer \(a\), if there exists an integer \(c\), such that \(b=ac\).
We also use all the same variant terminology and the same notation \(a \mid b\) for integer divisibility.
Problem
Show that the integer 6 is divisible by -2.
Solution
\(6 = -2 \cdot -3\).
example : (-2 : ℤ) ∣ 6 := by
sorry
3.2.3. Example
Problem
Let \(a\) and \(b\) be integers and suppose that \(a \mid b\). Show that \(a \mid b^2+2b\).
Solution
Since \(a \mid b\), there exists an integer \(k\) such that \(b=ak\). Then
So \(a \mid b^2+2b\).
example {a b : ℤ} (hab : a ∣ b) : a ∣ b ^ 2 + 2 * b := by
obtain ⟨k, hk⟩ := hab
use k * (a * k + 2)
calc
b ^ 2 + 2 * b = (a * k) ^ 2 + 2 * (a * k) := by rw [hk]
_ = a * (k * (a * k + 2)) := by ring
3.2.4. Example
Problem
Let \(a\), \(b\) and \(c\) be natural numbers and suppose that \(a \mid b\) and \(b ^2\mid c\). Show that \(a^2 \mid c\).
Solution
Since \(a \mid b\), there exists a natural number \(x\) such that \(b=ax\). Since \(b^2 \mid c\), there exists a natural number \(y\) such that \(c=b^2y\). Then
So \(a ^2 \mid c\).
Translate this solution into Lean.
As usual, if you wish, you can use the command dsimp [(· ∣ ·)] at *
to unfold \(\mid\) to
its definition everywhere in the goal state, though this will have no effect on the correctness of
the proof.
example {a b c : ℕ} (hab : a ∣ b) (hbc : b ^ 2 ∣ c) : a ^ 2 ∣ c := by
sorry
3.2.5. Example
Problem
Let \(x\), \(y\) and \(z\) be natural numbers and suppose that \(xy \mid z\). Show that \(x \mid z\).
Solution
Since \(xy \mid z\), there exists a natural number \(t\) such that \(z=(xy)t\). Then
So \(x \mid z\).
example {x y z : ℕ} (h : x * y ∣ z) : x ∣ z := by
sorry
3.2.6. Example
You might wonder how to show that a number is not divisible by another number. A convenient test here is a theorem which we will prove later in the book, in Example 4.5.8: if an integer \(a\) is strictly between two consecutive multiples of an integer \(b\), then it is not a multiple of \(b\). More formally, if there exists an integer \(q\) such that \(bq<a<b(q + 1)\), then \(a\) is not a multiple of \(b\). Here is an example applying this test:
Problem
Show that 12 is not divisible by 5.
Solution
\(5 \cdot 2 < 12 < 5 \cdot (2 + 1)\).
In Lean, this test is available as the lemma Int.not_dvd_of_exists_lt_and_lt
:
lemma Int.not_dvd_of_exists_lt_and_lt (a b : ℤ)
(h : ∃ q, b * q < a ∧ a < b * (q + 1)) :
¬b ∣ a :=
And here is the same solution written up in Lean.
example : ¬(5 : ℤ) ∣ 12 := by
apply Int.not_dvd_of_exists_lt_and_lt
use 2
constructor
· numbers -- show `5 * 2 < 12`
· numbers -- show `12 < 5 * (2 + 1)`
3.2.7. Example
Problem
Let \(a\) and \(b\) be natural numbers, with \(b\) positive, and suppose that \(a\) divides \(b\). Show that \(a \le b\).
Solution
Since \(a \mid b\), there exists a natural number \(k\) such that \(b=ak\).
We first note that
so \(0<k\). Thus in fact \(1 \le k\).
Now, we have
example {a b : ℕ} (hb : 0 < b) (hab : a ∣ b) : a ≤ b := by
obtain ⟨k, hk⟩ := hab
have H1 :=
calc
0 < b := hb
_ = a * k := hk
cancel a at H1
have H : 1 ≤ k := H1
calc
a = a * 1 := by ring
_ ≤ a * k := by rel [H]
_ = b := by rw [hk]
This lemma is available in the main Lean library under the name Nat.le_of_dvd
.
3.2.8. Example
Problem
Let \(a\) and \(b\) be natural numbers, with \(b\) positive, and suppose that \(a\) divides \(b\). Show that \(a\) is positive.
Solution
Since \(a \mid b\), there exists a natural number \(k\) such that \(b=ak\).
We have
so \(0<a\).
example {a b : ℕ} (hab : a ∣ b) (hb : 0 < b) : 0 < a := by
sorry
This lemma is also available in the main Lean library, under the name Nat.pos_of_dvd_of_pos
.
3.2.9. Exercises
Show that 0 is divisible by every integer \(t\).
example (t : ℤ) : t ∣ 0 := by sorry
Show that -10 is not divisible by 3.
example : ¬(3 : ℤ) ∣ -10 := by sorry
Let \(x\) and \(y\) be integers and suppose that \(x \mid y\). Show that \(x \mid 3y-4y^2\).
example {x y : ℤ} (h : x ∣ y) : x ∣ 3 * y - 4 * y ^ 2 := by sorry
Let \(m\) and \(n\) be integers and suppose that \(m \mid n\). Show that \(m \mid 2n^3+n\).
example {m n : ℤ} (h : m ∣ n) : m ∣ 2 * n ^ 3 + n := by sorry
Let \(a\) and \(b\) be integers and suppose that \(a \mid b\). Show that \(a \mid 2b^3-b^2+3b\).
example {a b : ℤ} (hab : a ∣ b) : a ∣ 2 * b ^ 3 - b ^ 2 + 3 * b := by sorry
Let \(k\), \(l\) and \(m\) be integers and suppose that \(k\) divides \(l\) and \(l^3\) divides \(m\). Show that \(k^3\) divides \(m\).
example {k l m : ℤ} (h1 : k ∣ l) (h2 : l ^ 3 ∣ m) : k ^ 3 ∣ m := by sorry
Let \(p\), \(q\) and \(r\) be integers and suppose that \(p^3\) divides \(q\) and \(q^2\) divides \(r\). Show that \(p^6\) divides \(r\).
example {p q r : ℤ} (hpq : p ^ 3 ∣ q) (hqr : q ^ 2 ∣ r) : p ^ 6 ∣ r := by sorry
Show that there exists a natural number \(n>0\), such that \(9\) is a factor of \(2^n-1\).
example : ∃ n : ℕ, 0 < n ∧ 9 ∣ 2 ^ n - 1 := by sorry
Show that there exists integers \(a\) and \(b\), with \(0<b<a\), such that \(a-b \mid a+b\).
example : ∃ a b : ℤ, 0 < b ∧ b < a ∧ a - b ∣ a + b := by sorry
3.3. Modular arithmetic: theory
Definition
The integers \(a\) and \(b\) are congruent modulo \(n\), if \(n\mid (a - b)\).
We use the notation \(a\equiv b \mod n\) to denote that \(a\) and \(b\) are congruent modulo \(n\).
def Int.ModEq (n a b : ℤ) : Prop := n ∣ a - b
notation:50 a " ≡ " b " [ZMOD " n "]" => Int.ModEq n a b
3.3.1. Example
Problem
Show that \(11\equiv 3 \mod 4\).
Solution
\(11-3=4\cdot 2\), so \(4\mid(11-3)\).
example : 11 ≡ 3 [ZMOD 4] := by
use 2
numbers
3.3.2. Example
Problem
Show that \(-5\equiv 1 \mod 3\).
Solution
\(-5-1=3\cdot -2\), so \(3\mid(-5-1)\).
example : -5 ≡ 1 [ZMOD 3] := by
sorry
3.3.3. Example
Lemma (addition rule for modular arithmetic)
Let \(a\), \(b\), \(c\), \(d\) and \(n\) be integers, and suppose that \(a\equiv b \mod n\) and \(c\equiv d \mod n\). Then \(a+c\equiv b+d \mod n\).
Proof
Since \(a\equiv b \mod n\), there exists an integer \(x\) such that \(a-b=nx\). Since \(c\equiv d \mod n\), there exists an integer \(y\) such that \(c-d=ny\). Then
so \(a+c\equiv b+d \mod n\).
theorem Int.ModEq.add {n a b c d : ℤ} (h1 : a ≡ b [ZMOD n]) (h2 : c ≡ d [ZMOD n]) :
a + c ≡ b + d [ZMOD n] := by
dsimp [Int.ModEq] at *
obtain ⟨x, hx⟩ := h1
obtain ⟨y, hy⟩ := h2
use x + y
calc
a + c - (b + d) = a - b + (c - d) := by ring
_ = n * x + n * y := by rw [hx, hy]
_ = n * (x + y) := by ring
3.3.4. Exercise
Lemma (subtraction rule for modular arithmetic)
Let \(a\), \(b\), \(c\), \(d\) and \(n\) be integers, and suppose that \(a\equiv b \mod n\) and \(c\equiv d \mod n\). Then \(a-c\equiv b-d \mod n\).
theorem Int.ModEq.sub {n a b c d : ℤ} (h1 : a ≡ b [ZMOD n]) (h2 : c ≡ d [ZMOD n]) :
a - c ≡ b - d [ZMOD n] := by
sorry
3.3.5. Exercise
Lemma (negation rule for modular arithmetic)
Let \(a\), \(b\) and \(n\) be integers, and suppose that \(a\equiv b \mod n\). Then \(-a\equiv -b \mod n\).
theorem Int.ModEq.neg {n a b : ℤ} (h1 : a ≡ b [ZMOD n]) : -a ≡ -b [ZMOD n] := by
sorry
3.3.6. Example
Lemma (multiplication rule for modular arithmetic)
Let \(a\), \(b\), \(c\), \(d\) and \(n\) be integers, and suppose that \(a\equiv b \mod n\) and \(c\equiv d \mod n\). Then \(ac\equiv bd \mod n\).
Proof
Since \(a\equiv b \mod n\), there exists an integer \(x\) such that \(a-b=nx\). Since \(c\equiv d \mod n\), there exists an integer \(y\) such that \(c-d=ny\). Then
so \(ac\equiv bd \mod n\).
theorem Int.ModEq.mul {n a b c d : ℤ} (h1 : a ≡ b [ZMOD n]) (h2 : c ≡ d [ZMOD n]) :
a * c ≡ b * d [ZMOD n] := by
obtain ⟨x, hx⟩ := h1
obtain ⟨y, hy⟩ := h2
use x * c + b * y
calc
a * c - b * d = (a - b) * c + b * (c - d) := by ring
_ = n * x * c + b * (n * y) := by rw [hx, hy]
_ = n * (x * c + b * y) := by ring
3.3.7. Example
Warning: There is no “division rule” for modular arithmetic!
Problem
It is possible to have integers \(a\), \(b\), \(c\), \(d\) and \(n\) with \(a\equiv b \mod n\) and \(c\equiv d \mod n\), but \(\frac{a}{c}\not\equiv \frac{b}{d} \mod n\).
Solution
We can take \(a=10\), \(b=18\), \(c=2\), \(d=6\). Indeed,
\(10-18=4\cdot -2\), so \(10\equiv 18 \mod 4\);
\(2-6=4\cdot -1\), so \(2\equiv 6 \mod 4\);
\(\frac{10}{2}-\frac{18}{6}=2\) lies between the consecutive multiples \(4 \cdot 0\) and \(4 \cdot (0 + 1)\) of 4, so \(\frac{10}{2}\not\equiv \frac{18}{6} \mod 4\).
Notice that here we’re using the test for non-divisibility from Example 3.2.6.
3.3.8. Example
Lemma (squaring rule for modular arithmetic)
Let \(a\), \(b\) and \(n\) be integers, and suppose that \(a\equiv b \mod n\). Then \(a^2\equiv b^2 \mod n\).
Proof
Since \(a\equiv b \mod n\), there exists an integer \(x\) such that \(a-b=nx\). Then
theorem Int.ModEq.pow_two (h : a ≡ b [ZMOD n]) : a ^ 2 ≡ b ^ 2 [ZMOD n] := by
obtain ⟨x, hx⟩ := h
use x * (a + b)
calc
a ^ 2 - b ^ 2 = (a - b) * (a + b) := by ring
_ = n * x * (a + b) := by rw [hx]
_ = n * (x * (a + b)) := by ring
3.3.9. Exercise
Lemma (cubing rule for modular arithmetic)
Let \(a\), \(b\) and \(n\) be integers, and suppose that \(a\equiv b \mod n\). Then \(a^3\equiv b^3 \mod n\).
theorem Int.ModEq.pow_three (h : a ≡ b [ZMOD n]) : a ^ 3 ≡ b ^ 3 [ZMOD n] := by
sorry
In fact the same is true for any power, although we don’t yet have the tools to prove it. We’ll come back to this later in the book, in Example 6.1.3.
Lemma (power rule for modular arithmetic)
Let \(k\) be a natural number and let \(a\), \(b\) and \(n\) be integers, and suppose that \(a\equiv b \mod n\). Then \(a^k\equiv b^k \mod n\).
theorem Int.ModEq.pow (k : ℕ) (h : a ≡ b [ZMOD n]) : a ^ k ≡ b ^ k [ZMOD n] :=
sorry -- we'll prove this later in the book
3.3.10. Example
Lemma (reflexivity rule for modular arithmetic)
Let \(a\) and \(n\) be integers. Then \(a\equiv a \mod n\).
Proof
\(a-a=n\cdot 0\), so \(n\mid a - a\).
theorem Int.ModEq.refl (a : ℤ) : a ≡ a [ZMOD n] := by
use 0
ring
3.3.11. Example
Whew! That was a lot of lemmas. But they pay off, as you will now see. Suppose we now encounter some very specific modular arithmetic problem of the same general type as we’ve seen before: the congruence modulo \(n\) of two expressions which differ in a kind of spot-the-difference way, like a “rewriting” by one congruence. For example,
Problem
Let \(a\) and \(b\) be integers, and suppose that \(a\equiv 2 \mod 4\). Show that \(a b ^ 2 + a ^ 2 b + 3 a \equiv 2 b ^ 2 + 2 ^ 2 \cdot b + 3 \cdot 2 \mod 4\).
We could solve this by working directly from the definition, which is rather painful:
example {a b : ℤ} (ha : a ≡ 2 [ZMOD 4]) :
a * b ^ 2 + a ^ 2 * b + 3 * a ≡ 2 * b ^ 2 + 2 ^ 2 * b + 3 * 2 [ZMOD 4] := by
obtain ⟨x, hx⟩ := ha
use x * (b ^ 2 + a * b + 2 * b + 3)
calc
a * b ^ 2 + a ^ 2 * b + 3 * a - (2 * b ^ 2 + 2 ^ 2 * b + 3 * 2) =
(a - 2) * (b ^ 2 + a * b + 2 * b + 3) :=
by ring
_ = 4 * x * (b ^ 2 + a * b + 2 * b + 3) := by rw [hx]
_ = 4 * (x * (b ^ 2 + a * b + 2 * b + 3)) := by ring
Or, better, we can solve this by applying the right combination of the lemmas we already proved, in the right order. This requires much less thinking:
example {a b : ℤ} (ha : a ≡ 2 [ZMOD 4]) :
a * b ^ 2 + a ^ 2 * b + 3 * a ≡ 2 * b ^ 2 + 2 ^ 2 * b + 3 * 2 [ZMOD 4] := by
apply Int.ModEq.add
apply Int.ModEq.add
apply Int.ModEq.mul
apply ha
apply Int.ModEq.refl
apply Int.ModEq.mul
apply Int.ModEq.pow
apply ha
apply Int.ModEq.refl
apply Int.ModEq.mul
apply Int.ModEq.refl
apply ha
3.3.12. Exercises
Show that \(34\equiv 104 \mod 5\).
example : 34 ≡ 104 [ZMOD 5] := by sorry
(symmetry rule for modular arithmetic) Let \(a\), \(b\) and \(n\) be integers, and suppose that \(a\equiv b \mod n\). Show that \(b\equiv a \mod n\).
theorem Int.ModEq.symm (h : a ≡ b [ZMOD n]) : b ≡ a [ZMOD n] := by sorry
(transitivity rule for modular arithmetic) Let \(a\), \(b\), \(c\) and \(n\) be integers, and suppose that \(a\equiv b \mod n\) and \(b\equiv c \mod n\). Show that \(a\equiv c \mod n\).
theorem Int.ModEq.trans (h1 : a ≡ b [ZMOD n]) (h2 : b ≡ c [ZMOD n]) : a ≡ c [ZMOD n] := by sorry
Let \(a\), \(c\) and \(n\) be integers. Show that \(a+nc\equiv a \mod n\).
example : a + n * c ≡ a [ZMOD n] := by sorry
Give an alternative solution (i.e., with different numbers) to Example 3.3.7.
Let \(a\) and \(b\) be integers, and suppose that \(a \equiv b \mod 5\). Show that \(2a+3 \equiv 2b+3 \mod 5\).
Give two solutions, following the style of the two solutions in Example 3.3.11.
example {a b : ℤ} (h : a ≡ b [ZMOD 5]) : 2 * a + 3 ≡ 2 * b + 3 [ZMOD 5] := by sorry
Let \(m\) and \(n\) be integers, and suppose that \(m \equiv n \mod 4\). Show that \(3m-1 \equiv 3n-1 \mod 4\).
Give two solutions, following the style of the two solutions in Example 3.3.11.
example {m n : ℤ} (h : m ≡ n [ZMOD 4]) : 3 * m - 1 ≡ 3 * n - 1 [ZMOD 4] := by sorry
Let \(k\) be an integer, and suppose that \(k\equiv 3 \mod 5\). Show that \(4 k + k ^ 3 + 3\equiv 4 \cdot 3 + 3 ^ 3 + 3 \mod 5\).
Give two solutions, following the style of the two solutions in Example 3.3.11.
example {k : ℤ} (hb : k ≡ 3 [ZMOD 5]) : 4 * k + k ^ 3 + 3 ≡ 4 * 3 + 3 ^ 3 + 3 [ZMOD 5] := by sorry
3.4. Modular arithmetic: calculations
3.4.1. Example
Recall the problem from Example 3.3.11.
Problem
Let \(a\) and \(b\) be integers, and suppose that \(a\equiv 2 \mod 4\). Show that \(a b ^ 2 + a ^ 2 b + 3 a \equiv 2 b ^ 2 + 2 ^ 2 \cdot b + 3 \cdot 2 \mod 4\).
After solving this and the many similar problems in Section 3.3, you probably feel like you can check the correctness of any statement of this style by sight. And that’s great! When we have built up enough theory that a particular class of statement can be checked by sight, we will stop requiring detailed proofs. So for now on we’ll take such statements for granted.
This is also usually the point at which it’s easy to write a Lean tactic which checks the
correctness of a class of statement. I’ve done exactly this, updating tactic rel
to cover this
kind of statement. We won’t discuss tactic-writing in this book, but effectively, the tactic
now throws the lemmas Int.ModEq.add
, Int.ModEq.neg
, Int.ModEq.sub
, Int.ModEq.mul
,
Int.ModEq.pow
, Int.ModEq.refl
and the provided hypotheses at the statement until (a) the
goal is solved or (b) none of these lemmas apply any more. And that’s exactly what we’re doing in
our heads when we check the paper statement of the problem.
example {a b : ℤ} (ha : a ≡ 2 [ZMOD 4]) :
a * b ^ 2 + a ^ 2 * b + 3 * a ≡ 2 * b ^ 2 + 2 ^ 2 * b + 3 * 2 [ZMOD 4] := by
rel [ha]
3.4.2. Example
From now on, we will solve more interesting modular arithmetic problems, dealing with steps like Example 3.3.11 in a single line.
Problem
Let \(a\) and \(b\) be integers, with \(a \equiv 4\mod 5\) and \(b \equiv 3\mod 5\). Show that \(ab+b^3+3 \equiv 2\mod 5\).
Solution
example {a b : ℤ} (ha : a ≡ 4 [ZMOD 5]) (hb : b ≡ 3 [ZMOD 5]) :
a * b + b ^ 3 + 3 ≡ 2 [ZMOD 5] :=
calc
a * b + b ^ 3 + 3 ≡ 4 * b + b ^ 3 + 3 [ZMOD 5] := by rel [ha]
_ ≡ 4 * 3 + 3 ^ 3 + 3 [ZMOD 5] := by rel [hb]
_ = 2 + 5 * 8 := by numbers
_ ≡ 2 [ZMOD 5] := by extra
3.4.3. Example
Problem
Show that there exists an integer \(a\), such that \(6a \equiv 4\mod 11\).
Solution
The integer 8 has this property. Indeed,
example : ∃ a : ℤ, 6 * a ≡ 4 [ZMOD 11] := by
use 8
calc
(6:ℤ) * 8 = 4 + 4 * 11 := by numbers
_ ≡ 4 [ZMOD 11] := by extra
3.4.4. Example
Problem
Let \(x\) be an integer. Show that \(x ^ 3 \equiv x\mod 3\).
Solution
We consider cases according to the residue of \(x\) modulo 3.
Case 1 (\(x\equiv 0\mod 3\)):
Case 2 (\(x\equiv 1\mod 3\)):
Case 3 (\(x\equiv 2\mod 3\)):
example {x : ℤ} : x ^ 3 ≡ x [ZMOD 3] := by
mod_cases hx : x % 3
calc
x ^ 3 ≡ 0 ^ 3 [ZMOD 3] := by rel [hx]
_ = 0 := by numbers
_ ≡ x [ZMOD 3] := by rel [hx]
calc
x ^ 3 ≡ 1 ^ 3 [ZMOD 3] := by rel [hx]
_ = 1 := by numbers
_ ≡ x [ZMOD 3] := by rel [hx]
calc
x ^ 3 ≡ 2 ^ 3 [ZMOD 3] := by rel [hx]
_ = 2 + 3 * 2 := by numbers
_ ≡ 2 [ZMOD 3] := by extra
_ ≡ x [ZMOD 3] := by rel [hx]
3.4.5. Exercises
Let \(n\) be an integer for which \(n\equiv 1\mod 3\). Show that \(n^3+7n\equiv 2\mod 3\).
example {n : ℤ} (hn : n ≡ 1 [ZMOD 3]) : n ^ 3 + 7 * n ≡ 2 [ZMOD 3] := sorry
Let \(a\) be an integer for which \(a\equiv 3\mod 4\). Show that \(a^3+4a^2+2\equiv 1\mod 4\).
example {a : ℤ} (ha : a ≡ 3 [ZMOD 4]) : a ^ 3 + 4 * a ^ 2 + 2 ≡ 1 [ZMOD 4] := sorry
Let \(a\) and \(b\) be integers. Show that \((a + b)^3\equiv a^3+b^3\mod 3\).
example (a b : ℤ) : (a + b) ^ 3 ≡ a ^ 3 + b ^ 3 [ZMOD 3] := sorry
Show that there exists an integer \(a\), such that \(4a\equiv 1\mod 7\).
example : ∃ a : ℤ, 4 * a ≡ 1 [ZMOD 7] := by sorry
Show that there exists an integer \(k\), such that \(5k\equiv 6\mod 8\).
example : ∃ k : ℤ, 5 * k ≡ 6 [ZMOD 8] := by sorry
Let \(n\) be an integer. Show that \(5n^2+3n+7\equiv 1\mod 2\).
example (n : ℤ) : 5 * n ^ 2 + 3 * n + 7 ≡ 1 [ZMOD 2] := by sorry
Let \(x\) be an integer. Show that \(x^5\equiv x\mod 5\).
example {x : ℤ} : x ^ 5 ≡ x [ZMOD 5] := by sorry
3.5. Bézout’s identity
3.5.1. Example
Problem
Let \(n\) be an integer and suppose that \(5n\) is a multiple of \(8\). Show that \(n\) is also a multiple of \(8\).
Solution
Since \(8\mid 5n\), there exists an integer \(a\) such that \(5n=8a\). Then
so \(8\mid n\).
example {n : ℤ} (hn : 8 ∣ 5 * n) : 8 ∣ n := by
obtain ⟨a, ha⟩ := hn
use -3 * a + 2 * n
calc
n = -3 * (5 * n) + 16 * n := by ring
_ = -3 * (8 * a) + 16 * n := by rw [ha]
_ = 8 * (-3 * a + 2 * n) := by ring
Such a problem will typically have many possible solutions. Here is another solution.
Solution
Since \(8\mid 5n\), there exists an integer \(a\) such that \(5n=8a\). Then
so \(8\mid n\).
Try typing the variant solution up in Lean.
example {n : ℤ} (hn : 8 ∣ 5 * n) : 8 ∣ n := by
sorry
3.5.2. Example
Problem
Show that if for some integer \(n\) we have that \(5\) divides \(3n\), then \(5\) also divides \(n\).
Solution
Since \(5\mid 3n\), there exists an integer \(x\) such that \(3n=5x\). Then
so \(5\mid n\).
example {n : ℤ} (h1 : 5 ∣ 3 * n) : 5 ∣ n := by
sorry
3.5.3. Example
Problem
Let \(m\) be an integer which is divisible by 8 and by 5. Show that it is also divisible by 40.
Solution
Since \(8\mid m\), there exists an integer \(a\) such that \(m=8a\). Since \(5\mid m\), there exists an integer \(b\) such that \(m=5b\). Then
so \(40\mid m\).
example {m : ℤ} (h1 : 8 ∣ m) (h2 : 5 ∣ m) : 40 ∣ m := by
obtain ⟨a, ha⟩ := h1
obtain ⟨b, hb⟩ := h2
use -3 * a + 2 * b
calc
m = -15 * m + 16 * m := by ring
_ = -15 * (8 * a) + 16 * m := by rw [ha]
_ = -15 * (8 * a) + 16 * (5 * b) := by rw [hb]
_ = 40 * (-3 * a + 2 * b) := by ring
3.5.4. Exercises
Show that if 6 divides \(11n\), then it divides \(n\).
example {n : ℤ} (hn : 6 ∣ 11 * n) : 6 ∣ n := by sorry
Let \(a\) be an integer and suppose that \(5a\) is a multiple of \(7\). Show that \(a\) is also a multiple of \(7\).
example {a : ℤ} (ha : 7 ∣ 5 * a) : 7 ∣ a := by sorry
Suppose that 7 and 9 are both factors of some integer \(n\). Show that 63 is also a factor of \(n\).
example {n : ℤ} (h1 : 7 ∣ n) (h2 : 9 ∣ n) : 63 ∣ n := by sorry
Let \(n\) be an integer which is divisible by 5 and by 13. Show that it is also divisible by 65.
example {n : ℤ} (h1 : 5 ∣ n) (h2 : 13 ∣ n) : 65 ∣ n := by sorry