7. Number theory
This chapter is different in style from the other chapters of the book. The facts here are famous theorems, and their proofs require one-off, clever ideas. These particular ideas will not turn up again on homework or exams. Think of this chapter instead as a capstone: we explore what kinds of mathematical statements are in reach with the reasoning tools and theory we have developed so far in the book.
7.1. Infinitely many primes
Theorem
There are infinitely many prime numbers.
This is a an extremely old theorem, with the first known proof written in Euclid’s Elements in about 300 BC.
Proof
We show that for a given natural number \(N\), there exists a prime number \(p \geq N\).
Consider \(N!\), the factorial of \(N\). By one of the exercises to Section 6.2, \(0<N!\), so \(2 \le N! + 1\). Therefore, by Example 6.4.2, there exists a prime number \(p\) which is a factor of \(N! + 1\).
Let \(k\) be a natural number such that \(N! + 1=pk\). This number \(k\) cannot be zero, since if it were, we would have
contradiction. Thus \(k>0\), so \(k\) is of the form \(l+1\) for some natural number \(l\), and \(N! + 1=p(l+1)\).
We now show that \(p\) is not a factor of \(N!\), by showing that \(N!\) lies between the consecutive multiples \(pl\) and \(p(l+1)\) of \(p\). (This is the test from Example 4.5.8.) Indeed,
so \(pl< N!\), and
If \(p\le N\), then by Example 6.2.5, \(p\) would be a factor of \(N!\), which contradicts what we just proved. Therefore \(p > N\). This gives the required prime number greater than or equal to \(N\).
In Lean, the exercise to Section 6.2 has the name factorial_pos,
Example 6.4.2 has the name exists_prime_factor,
Example 4.5.8 has the name Nat.not_dvd_of_exists_lt_and_lt, and
Example 6.2.5 has the name dvd_factorial.
example (N : ℕ) : ∃ p ≥ N, Prime p := by
have hN0 : 0 < N ! := by apply factorial_pos
have hN2 : 2 ≤ N ! + 1 := by addarith [hN0]
-- `N! + 1` has a prime factor, `p`
obtain ⟨p, hp, hpN⟩ : ∃ p : ℕ, Prime p ∧ p ∣ N ! + 1 := exists_prime_factor hN2
have hp2 : 2 ≤ p
· obtain ⟨hp', hp''⟩ := hp
apply hp'
obtain ⟨k, hk⟩ := hpN
match k with
| 0 => -- if `k` is zero, contradiction
have k_contra :=
calc 0 < N ! + 1 := by extra
_ = p * 0 := hk
_ = 0 := by ring
numbers at k_contra
| l + 1 => -- so `k = l + 1` for some `l`
-- the key fact: `p` is not a factor of `N!`
have key : ¬ p ∣ (N !)
· apply Nat.not_dvd_of_exists_lt_and_lt (N !)
use l
constructor
· have :=
calc p * l + p = p * (l + 1) := by ring
_ = N ! + 1 := by rw [hk]
_ < N ! + p := by addarith [hp2]
addarith [this]
· calc N ! < N ! + 1 := by extra
_ = p * (l + 1) := by rw [hk]
-- so `p` is a prime number greater than or equal to `N`, as we sought
use p
constructor
· obtain h_le | h_gt : p ≤ N ∨ N < p := le_or_lt p N
· have : p ∣ (N !)
· apply dvd_factorial
· extra
· addarith [h_le]
contradiction
· addarith [h_gt]
· apply hp
7.2. Gauss’ and Euclid’s lemmas
Theorem (Gauss’ lemma)
Let \(a\), \(b\) and \(d\) be integers. Suppose that \(ab\) is a multiple of \(d\) and \(\operatorname{gcd}(a,d)=1\). Then \(b\) is a multiple of \(d\).
This lemma is the “final form” of the argument we have carried out in special cases in Example 3.5.1, Example 3.5.2, etc. Like in those special cases, the trick is to find a “Bézout identity” relating \(a\) and \(d\): multiples of \(a\) and \(d\) which differ by 1. In the special cases we could find such multiples explicitly. In the general situation the existence of such multiples is guaranteed by Example 6.7.6.
Proof
By Example 6.7.6 (Bézout’s identity) there exist integers \(x\) and \(y\) such that \(xa + yd = \operatorname{gcd}(a, d)\). Since \(ab\) is a multiple of \(d\), there exists an integer \(z\) such that \(ab=dz\). We then have that
so \(b\) is a multiple of \(d\).
theorem gauss_lemma {d a b : ℤ} (h1 : d ∣ a * b) (h2 : gcd a d = 1) : d ∣ b := by
obtain ⟨x, y, h⟩ := bezout a d
obtain ⟨z, hz⟩ := h1
use x * z + b * y
calc b = b * 1 := by ring
_ = b * gcd a d := by rw [h2]
_ = b * (x * a + y * d) := by rw [h]
_ = x * (a * b) + b * y * d := by ring
_ = x * (d * z) + b * y * d := by rw [hz]
_ = d * (x * z + b * y) := by ring
Theorem (Euclid’s lemma)
Let \(a\), \(b\) and \(p\) be natural numbers, with \(p\) prime. Suppose that \(ab\) is a multiple of \(p\). Then either \(a\) or \(b\) is a multiple of \(p\).
This lemma also dates back to Euclid’s Elements.
Proof
By Example 6.7.2, \(\operatorname{gcd}(a,p)\geq 0\), so \(\operatorname{gcd}(a,p)\) (a priori an integer) can be considered as a natural number. Let us call that natural number \(d\). Then
by Example 6.7.3, \(d\mid a\) and \(d\mid p\);
(\(\star\)) by Gauss’ lemma, if \(p\mid ab\) and \(d=1\) then \(p \mid b\).
A priori these divisibility statements are all statements about \(a\), \(b\), \(p\) and \(d\) considered as integers, but these are equivalent to the corresponding divisibility statements about natural numbers.
We now begin the proof proper. Since \(p\) is prime and \(d\mid p\), either \(d=1\) or \(d=p\).
Case 1 (\(d=1\)): Then by (\(\star\)), \(p \mid b\).
Case 2 (\(d=p\)): Then since \(d\mid a\), \(p\mid a\).
To write this proof in Lean, we need some tricks to handle the interaction between integers and natural numbers. These will not be used again and it’s fine not to read them very closely.
When invoking lemmas about integers (
gcd_dvd_left,gcd_dvd_right,gauss_lemma,gcd_nonneg) on natural number inputs, we cast the natural number inputs to integers, like(a:ℤ)– this is not always necessary but it avoids ambiguity. (The casts then display in the infoview with arrows, as↑a, etc.)Once we have the hypothesis
0 ≤ gcd (a:ℤ) (p:ℤ), we can use the Lean tacticliftto introduce a natural numberdwhose cast to the integers isgcd (a:ℤ) (p:ℤ).Finally, we can run the tactic
norm_caston all our hypotheses, which converts statements about natural-numbers-cast-to-integers into the corresponding statements about natural numbers, if this is mathematically valid. For example,↑d ∣ ↑ais converted tod ∣ a.
theorem euclid_lemma {a b p : ℕ} (hp : Prime p) (H : p ∣ a * b) : p ∣ a ∨ p ∣ b := by
-- write down everything we know about `gcd (a:ℤ) (p:ℤ)`
have hap1 : gcd (a:ℤ) (p:ℤ) ∣ (a:ℤ) := gcd_dvd_left (a:ℤ) (p:ℤ)
have hap2 : gcd (a:ℤ) (p:ℤ) ∣ (p:ℤ) := gcd_dvd_right (a:ℤ) (p:ℤ)
have h_gauss : (p:ℤ) ∣ (a:ℤ) * (b:ℤ) → gcd (a:ℤ) (p:ℤ) = 1 → (p:ℤ) ∣ (b:ℤ) :=
gauss_lemma
have hgcd : 0 ≤ gcd (a:ℤ) (p:ℤ) := gcd_nonneg (a:ℤ) (p:ℤ)
-- convert to `ℕ` facts
lift gcd a p to ℕ using hgcd with d hd
norm_cast at hap1 hap2 h_gauss
-- actually prove the theorem
dsimp [Prime] at hp
obtain ⟨hp1, hp2⟩ := hp
obtain hgcd_1 | hgcd_p : d = 1 ∨ d = p := hp2 d hap2
· right
apply h_gauss H hgcd_1
· left
rw [← hgcd_p]
apply hap1
Corollary
Let \(a\), \(p\) and \(k\) be natural numbers, with \(p\) prime and \(k\geq 1\). If \(a^k\) is a multiple of \(p\), then \(a\) is a multiple of \(p\).
Proof
We prove this by induction on \(k\), starting at 1.
Base case: If \(a^1\) is a multiple of \(p\), then since \(a^1=a\), we conclude that \(a\) is a multiple of \(p\).
Inductive step: Let \(t\) be a natural number and suppose that if \(a^t\) is a multiple of \(p\) then \(a\) is. (\(\star\))
Now suppose that \(a^{t+1}\) is a multiple of \(p\). Since \(a^{t+1}=a\cdot a^t\), this means that \(a \cdot a^t\) is a multiple of \(p\).
Therefore, by Euclid’s lemma, either \(a\) is a multiple of \(p\), in which case we are done, or \(a^t\) is a multiple of \(p\), in which case by the inductive hypothesis (\(\star\)) we are done.
theorem euclid_lemma_pow (a k p : ℕ) (hp : Prime p) (hk : 1 ≤ k) (H : p ∣ a ^ k) :
p ∣ a := by
induction_from_starting_point k, hk with t ht IH
· have ha : a ^ 1 = a := by ring
rw [ha] at H
apply H
have ha : a ^ (t + 1) = a * a ^ t := by ring
rw [ha] at H
have key : p ∣ a ∨ p ∣ a ^ t := euclid_lemma hp H
obtain h1 | h2 := key
· apply h1
· apply IH
apply h2
7.3. The square root of two
Theorem
There do not exist natural numbers \(a\) and \(b\) with \(b\ne 0\), for which \(a^2=2b^2\).
This is another theorem which dates back to the ancient Greeks, in this case to the followers of Pythagoras, c. 450 BC.
This theorem constitutes most of the work of proving that the square root of two is irrational, that is, not a rational number (\(\mathbb{Q}\)). We can’t draw that conclusion here since we haven’t yet defined rational numbers precisely, but we will circle back to it later in the book.
Proof
We will show a logically equivalent fact: that for all natural numbers \(a\) and \(b\) with \(b\ne 0\), it holds that \(a^2\ne 2b^2\). We prove this by strong induction on \(b\).
Let \(a\) and \(b\) be natural numbers and suppose that for all natural numbers \(r\), \(s\) with \(s<b\) and \(s\ne 0\), it holds that \(r^2\ne 2s^2\).
Suppose that \(a^2= 2b^2\). Then \(a^2\) is even, so by one of the exercises to Section 6.1, \(a\) is even. Let \(k\) be a natural number such that \(a=2k\). Then
so \(b^2=2k^2\). Then
so \(k>0\), so \(k\ne 0\).
We therefore invoke the inductive hypothesis with \(r=b\), \(s=k\). (Note that
so \(k<b\), so the induction is well-founded.) The inductive hypothesis gives that \(b^2\ne 2k^2\), contradiction. So it cannot be that \(a^2\ne 2b^2\).
In Lean we break this argument into three pieces. The lemma irrat_aux_wf is the
justification for the well-foundedness of the strong induction. Like in
Example 6.7.1, we tag the well-foundedness lemma with
@[decreasing] to make it available later for the strong induction.
@[decreasing] theorem irrat_aux_wf (b k : ℕ) (hb : k ≠ 0) (hab : b ^ 2 = 2 * k ^ 2) :
k < b := by
have h :=
calc k ^ 2 < k ^ 2 + k ^ 2 := by extra
_ = 2 * k ^ 2 := by ring
_ = b ^ 2 := by rw [hab]
cancel 2 at h
The lemma irrat_aux is the claim which is proved by strong induction. It contains the central
argument of the proof. In Lean, the exercise to Section 6.1 which is used
in this step has the name Nat.even_of_pow_even.
theorem irrat_aux (a b : ℕ) (hb : b ≠ 0) : a ^ 2 ≠ 2 * b ^ 2 := by
intro hab
have H : Nat.Even a
· apply Nat.even_of_pow_even (n := 2)
use b ^ 2
apply hab
obtain ⟨k, hk⟩ := H
have hbk :=
calc 2 * b ^ 2 = a ^ 2 := by rw [hab]
_ = (2 * k) ^ 2 := by rw [hk]
_ = 2 * (2 * k ^ 2) := by ring
cancel 2 at hbk
have hk' :=
calc 0 < b ^ 2 := by extra
_ = 2 * k ^ 2 := by rw [hbk]
_ = k * (2 * k) := by ring
cancel 2 * k at hk'
have hk'' : k ≠ 0 := ne_of_gt hk'
have IH := irrat_aux b k -- inductive hypothesis
have : b ^ 2 ≠ 2 * k ^ 2 := IH hk''
contradiction
termination_by _ => b
Finally, the main theorem is actually logically equivalent to irrat_aux, and its proof consists
of establishing this logical equivalence.
example : ¬ ∃ a b : ℕ, b ≠ 0 ∧ a ^ 2 = 2 * b ^ 2 := by
intro h
obtain ⟨a, b, hb, hab⟩ := h
have := irrat_aux a b hb
contradiction
That was fun … let’s do it again! Here is a different proof of the same theorem. Or, nearly the same theorem – this proof works better for integers. (It would be fiddly but not fundamentally difficult to convert the integer version to the natural number version or vice versa, using the techniques from Section 7.2.)
Theorem
There do not exist integers \(a\) and \(b\) with \(b\ne 0\), for which \(a^2=2b^2\).
Proof
Suppose that \(a\) and \(b\) were integers with \(b\ne 0\) and \(a^2=2b^2\).
Denote by \(d\) the greatest common divisor of \(a\) and \(b\). By Example 6.7.3, \(d\mid a\) and \(d\mid b\). Let \(k\) and \(l\) be integers such that \(a=dk\) and \(b=dl\).
Also by Example 6.7.6 (Bézout’s identity) there exist integers \(x\) and \(y\) such that \(xa+yb=d\).
The key calculation is the following (\(\dagger\)).:
We have that \(d\ne 0\), since if not,
contradiction. Hence by (\(\dagger\)),
But by Example 2.3.5, no integer squares to 2, so this is impossible.
Note the use of Brahmagupta’s identity (Example 1.1.3) above in the middle of the key calculation.
example : ¬ ∃ a b : ℤ, b ≠ 0 ∧ b ^ 2 = 2 * a ^ 2 := by
intro h
obtain ⟨a, b, hb, hab⟩ := h
have Ha : gcd a b ∣ a := gcd_dvd_left a b
have Hb : gcd a b ∣ b := gcd_dvd_right a b
obtain ⟨k, hk⟩ := Ha
obtain ⟨l, hl⟩ := Hb
obtain ⟨x, y, h⟩ := bezout a b
set d := gcd a b
have key :=
calc (2 * k * y + l * x) ^ 2 * d ^ 2
= (2 * (d * k) * y + (d * l) * x) ^ 2 := by ring
_ = (2 * a * y + b * x) ^ 2 := by rw [hk, hl]
_ = 2 * (x * a + y * b) ^ 2 + (x ^ 2 - 2 * y ^ 2) * (b ^ 2 - 2 * a ^ 2) := by ring
_ = 2 * d ^ 2 + (x ^ 2 - 2 * y ^ 2) * (b ^ 2 - b ^ 2) := by rw [h, hab]
_ = 2 * d ^ 2 := by ring
have hd : d ≠ 0
· intro hd
have :=
calc b = d * l := hl
_ = 0 * l := by rw [hd]
_ = 0 := by ring
contradiction
cancel d ^ 2 at key
have := sq_ne_two (2 * k * y + l * x)
contradiction