# 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 tactic`lift`

to introduce a natural number`d`

whose cast to the integers is`gcd (a:ℤ) (p:ℤ)`

.Finally, we can run the tactic

`norm_cast`

on 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 ∣ ↑a`

is converted to`d ∣ 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
```