7. 数论
本章的风格不同于本书其他章节。这里的事实是著名定理，其证明需要一次性的巧妙想法。这些特定想法不会再次出现在作业或考试中。请把本章看作一个总结性章节：我们探索到目前为止在本书中发展出的推理工具和理论能够达到怎样的数学陈述。
7.1. 素数有无穷多个
定理
素数有无穷多个。
这是一个极其古老的定理，最早已知证明写在约公元前 300 年 Euclid 的《几何原本》中。
证明
我们证明：给定自然数 \(N\)，存在素数 \(p \geq N\)。
考虑 \(N!\)，即 \(N\) 的阶乘。由第 6.2 节的一道练习，\(0<N!\)，所以 \(2 \le N! + 1\)。因此由例 6.4.2，存在一个素数 \(p\) 是 \(N! + 1\) 的因子。
设 \(k\) 为自然数，满足 \(N! + 1=pk\)。这个数 \(k\) 不可能为零，因为若它为零，则有
矛盾。因此 \(k>0\)，所以 \(k\) 形如 \(l+1\)，其中 \(l\) 为某个自然数，并且 \(N! + 1=p(l+1)\)。
现在我们证明 \(p\) 不是 \(N!\) 的因子：只需说明 \(N!\) 位于 \(p\) 的相邻倍数 \(pl\) 与 \(p(l+1)\) 之间。（这是例 4.5.8 中的判据。）确实，
所以 \(pl< N!\)，并且
如果 \(p\le N\)，那么由例 6.2.5，\(p\) 将是 \(N!\) 的因子，这与我们刚才证明的结论矛盾。因此 \(p > N\)。这就给出了所需的大于等于 \(N\) 的素数。
在 Lean 中，第 6.2 节的练习名为 factorial_pos，例 6.4.2 名为 exists_prime_factor，例 4.5.8 名为 Nat.not_dvd_of_exists_lt_and_lt，例 6.2.5 名为 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. 高斯引理与欧几里得引理
定理（高斯引理）
设 \(a\)、\(b\) 和 \(d\) 为整数。假设 \(ab\) 是 \(d\) 的倍数，并且 \(\operatorname{gcd}(a,d)=1\)。则 \(b\) 是 \(d\) 的倍数。
这个引理是我们在例 3.5.1、例 3.5.2 等特殊情形中所作论证的“最终形态”。和那些特殊情形一样，技巧是找到一个联系 \(a\) 与 \(d\) 的“贝祖等式”：即相差 1 的 \(a\) 的倍数和 \(d\) 的倍数。在特殊情形中，我们可以显式找到这样的倍数；在一般情形中，这种倍数的存在性由例 6.7.6 保证。
证明
由例 6.7.6（贝祖等式），存在整数 \(x\) 和 \(y\)，使得 \(xa + yd = \operatorname{gcd}(a, d)\)。由于 \(ab\) 是 \(d\) 的倍数，存在整数 \(z\)，使得 \(ab=dz\)。于是有
所以 \(b\) 是 \(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
定理（欧几里得引理）
设 \(a\)、\(b\) 和 \(p\) 为自然数，其中 \(p\) 为素数。假设 \(ab\) 是 \(p\) 的倍数。则 \(a\) 或 \(b\) 是 \(p\) 的倍数。
这个引理也可追溯到 Euclid 的《几何原本》。
证明
由例 6.7.2，\(\operatorname{gcd}(a,p)\geq 0\)，所以 \(\operatorname{gcd}(a,p)\)（先验上是整数）可以看作自然数。把这个自然数称为 \(d\)。那么
- 由例 6.7.3，\(d\mid a\) 且 \(d\mid p\)；
- （\(\star\)）由高斯引理，若 \(p\mid ab\) 且 \(d=1\)，则 \(p \mid b\)。
先验上，这些整除陈述都是把 \(a\)、\(b\)、\(p\) 和 \(d\) 看作整数时的陈述；但它们等价于相应的自然数整除陈述。
现在开始正式证明。因为 \(p\) 是素数且 \(d\mid p\)，所以 \(d=1\) 或 \(d=p\)。
情形 1（\(d=1\)）：由（\(\star\)），\(p \mid b\)。
情形 2（\(d=p\)）：由于 \(d\mid a\)，有 \(p\mid a\)。
为了把这个证明写成 Lean，我们需要一些技巧来处理整数与自然数之间的相互作用。这些技巧以后不会再使用；不仔细阅读也没关系。
- 在对自然数输入调用关于整数的引理（
gcd_dvd_left、gcd_dvd_right、gauss_lemma、gcd_nonneg）时，我们把自然数输入强制转换为整数，例如(a:ℤ)；这并不总是必要的，但可以避免歧义。（这些强制转换随后会在 infoview 中显示为箭头，如 ↑a 等。） - 一旦有了假设
0 ≤ gcd (a:ℤ) (p:ℤ)，我们就可以使用 Lean 策略lift引入一个自然数 \(d\)，它到整数的强制转换等于gcd (a:ℤ) (p:ℤ)。 - 最后，我们可以在所有假设上运行策略
norm_cast；若数学上有效，它会把关于“强制转换成整数的自然数”的陈述转换为相应的自然数陈述。例如，↑d ∣ ↑a 会被转换为 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
设 \(a\)、\(p\) 和 \(k\) 为自然数，其中 \(p\) 为素数且 \(k\geq 1\)。若 \(a^k\) 是 \(p\) 的倍数，则 \(a\) 是 \(p\) 的倍数。
证明
我们从 1 开始对 \(k\) 归纳证明。
基例：若 \(a^1\) 是 \(p\) 的倍数，则由于 \(a^1=a\)，可得 \(a\) 是 \(p\) 的倍数。
归纳步：设 \(t\) 为自然数，并假设若 \(a^t\) 是 \(p\) 的倍数，则 \(a\) 也是 \(p\) 的倍数。（\(\star\)）
现在假设 \(a^{t+1}\) 是 \(p\) 的倍数。由于 \(a^{t+1}=a\cdot a^t\)，这意味着 \(a \cdot a^t\) 是 \(p\) 的倍数。
因此由欧几里得引理，要么 \(a\) 是 \(p\) 的倍数，此时证明完成；要么 \(a^t\) 是 \(p\) 的倍数，此时由归纳假设（\(\star\)）证明完成。
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. 二的平方根
定理
不存在自然数 \(a\) 和 \(b\) 满足 \(b\ne 0\) 且 \(a^2=2b^2\)。
这也是一个可追溯到古希腊的定理，在这个情形中可追溯到 Pythagoras 学派，约公元前 450 年。
这个定理构成了证明二的平方根为无理数的大部分工作，即证明它不是有理数（\(\mathbb{Q}\)）。由于我们还没有精确定义有理数，所以这里还不能得出这个结论；但本书稍后会回到这一点。
证明
我们将证明一个逻辑等价的事实：对所有自然数 \(a\) 和 \(b\)，若 \(b\ne 0\)，则 \(a^2\ne 2b^2\)。我们对 \(b\) 作强归纳证明。
设 \(a\) 和 \(b\) 为自然数，并假设对所有自然数 \(r\)、\(s\)，若 \(s<b\) 且 \(s\ne 0\)，则 \(r^2\ne 2s^2\)。
假设 \(a^2= 2b^2\)。那么 \(a^2\) 为偶数，所以由第 6.1 节的一道练习，\(a\) 为偶数。设 \(k\) 为自然数，使得 \(a=2k\)。于是
所以 \(b^2=2k^2\)。于是
所以 \(k>0\)，从而 \(k\ne 0\)。
因此我们以 \(r=b\)、\(s=k\) 调用归纳假设。（注意
所以 \(k<b\)，因此归纳是良基的。）归纳假设给出 \(b^2\ne 2k^2\)，矛盾。所以不可能有 \(a^2=2b^2\)。
在 Lean 中，我们把这个论证分成三部分。引理 irrat_aux_wf 是强归纳良基性的说明。和例 6.7.1 一样，我们用 @[decreasing] 标记这个良基性引理，使它稍后可用于强归纳。
@[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
引理 irrat_aux 是通过强归纳证明的命题。它包含证明的核心论证。在 Lean 中，此步骤使用的第 6.1 节练习名为 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
最后，主定理实际上与 irrat_aux 逻辑等价，其证明就是建立这种逻辑等价。
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
这很有趣……我们再来一次！下面是同一个定理的另一个证明。或者说，几乎是同一个定理：这个证明更适合整数。（使用第 7.2 节中的技巧，把整数版本转化为自然数版本或反过来，并不本质困难，只是会很繁琐且不太有趣。）
定理
不存在整数 \(a\) 和 \(b\) 满足 \(b\ne 0\) 且 \(a^2=2b^2\)。
证明
假设存在整数 \(a\) 和 \(b\)，满足 \(b\ne 0\) 且 \(a^2=2b^2\)。
记 \(d\) 为 \(a\) 与 \(b\) 的最大公因子。由例 6.7.3，\(d\mid a\) 且 \(d\mid b\)。设 \(k\) 和 \(l\) 为整数，使得 \(a=dk\) 且 \(b=dl\)。
又由例 6.7.6（贝祖等式），存在整数 \(x\) 和 \(y\)，使得 \(xa+yb=d\)。
关键计算如下（\(\dagger\)）：
我们有 \(d\ne 0\)，因为若不然，
矛盾。因此由（\(\dagger\)），
但由例 2.3.5，不存在平方等于 2 的整数，所以这是不可能的。
注意，上面的关键计算中间使用了 Brahmagupta 恒等式（例 1.1.3）。
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