3. 奇偶性与整除性

本章的问题涉及自然数和整数的一些初等性质：奇偶性（一个数是偶数还是奇数）、整除性，以及模 \(n\) 同余。

本章没有像 \(\lor\) 或 \(\exists\) 这样的新逻辑符号，也不会对我们的推理工具箱作重大补充（例如使用中间步骤或引理）。因此，本章在 第 2 章和 第 4 章的艰苦工作之间起到喘息作用，让你有机会巩固已经学到的内容。

3.1. 定义；奇偶性

3.1.1. 例

当一个数学术语第一次引入时，它会被给出定义。

定义

整数 \(a\) 称为奇数，如果存在整数 \(k\)，使得 \(a=2k+1\)。

下面是在 Lean 中给出定义的方式。

def Odd (a : ℤ) : Prop := ∃ k, a = 2 * k + 1

在纸上，你需要记住每个定义；这是能够使用定义的关键。在 Lean 中，当你看到一个术语并想再次确认它的定义时，可以右键点击该术语，选择 “Go to Definition”。它会带你到源代码中定义该术语的位置。请在术语 Odd 上试一试。

问题

证明 \(7\) 是奇数。

解答

\(7=2\cdot 3+1\)，所以 \(7\) 是奇数。

下面是这个问题在 Lean 中的样子。

example : Odd (7:ℤ) := by
  sorry

起始目标状态是：

⊢ Odd 7

你可以在证明中使用 dsimp（“definitional-simplify”）策略来检查定义。这里可以在证明中输入 dsimp [Odd]，使“奇数”的定义在目标中展开。

example : Odd (7:ℤ) := by
  dsimp [Odd]

这样做之后，目标会用“奇数”的定义显示，而不是用“奇数”这个词显示：

⊢ ∃ (k : ℤ), 7 = 2 * k + 1

不过，这一步是可选的；删除 dsimp 这一行后，证明仍然有效。

下面是该解答的完整 Lean 翻译。

example : Odd (7 : ℤ) := by
  dsimp [Odd]
  use 3
  numbers

如果你还不太理解这个证明，无论是文字版本还是 Lean 版本，请重读 第 2.5 节 中的一些例子，例如 例 2.5.3。

3.1.2. 例

下面是一个类似例子。

问题

证明 \(-3\) 是奇数。

example : Odd (-3 : ℤ) := by
  sorry

你应当证明对某个整数 \(k\)，有 \(-3=2k+1\)。但哪个 \(k\) 可行呢？

3.1.3. 例

问题

证明：如果 \(n\) 是奇整数，则 \(3n+2\) 是奇数。

解答

设 \(n\) 为奇数。那么存在整数 \(k\)，使得 \(n=2k+1\)。因此

\[\begin{split}3 n + 2 &= 3 (2 k + 1) + 2 \\ & = 2 (3 k + 2) + 1,\end{split}\]

所以 \(3n+2\) 是奇数。

在该问题的 Lean 版本中，初始目标状态如下。

n : ℤ
hn : Odd n
⊢ Odd (3 * n + 2)

如果想在目标中展开定义 Odd，可以如 例 3.1.1 中所讨论，使用 dsimp [Odd]。如果想在所有地方（目标和假设）展开定义 Odd，可以使用 dsimp [Odd] at *。

n : ℤ
hn : ∃ (k : ℤ), n = 2 * k + 1
⊢ ∃ (k : ℤ), 3 * n + 2 = 2 * k + 1

这是我们第一次遇到一个可能令人困惑的事情。存在量词内部的变量是一个“临时”变量，只在其所在句子的持续期间存在。你可以在证明中选择任何名称来命名这个见证；不必与题目陈述中的变量名相同。

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

同样，你可以检查 dsimp 这一行在解答中实际上并非必需。

3.1.4. 例

问题

设 \(n\) 为整数。证明：如果 \(n\) 是奇数，则 \(7n-4\) 是奇数。

example {n : ℤ} (hn : Odd n) : Odd (7 * n - 4) := by
  sorry

3.1.5. 例

问题

证明：如果整数 \(x\) 和 \(y\) 都是奇数，则 \(x+y+1\) 是奇数。

解答

由于 \(x\) 和 \(y\) 都是奇数，存在整数 \(a\) 使得 \(x=2a+1\)，并且存在整数 \(b\) 使得 \(y=2b+1\)。于是

\[\begin{split}x + y + 1 &= (2 a + 1) + (2 b + 1) + 1 \\ &= 2 (a + b + 1) + 1,\end{split}\]

所以 \(x+y+1\) 是奇数。

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. 例

问题

证明：如果整数 \(x\) 和 \(y\) 都是奇数，则 \(xy+2y\) 是奇数。

解答

由于 \(x\) 和 \(y\) 都是奇数，存在整数 \(a\) 使得 \(x=2a+1\)，并且存在整数 \(b\) 使得 \(y=2b+1\)。于是

\[\begin{split}x y + 2 y &= (2 a + 1) (2 b + 1) + 2 (2 b + 1) \\ &= 2 (2 a b + 3 b + a + 1) + 1,\end{split}\]

所以 \(xy+2y\) 是奇数。

example {x y : ℤ} (hx : Odd x) (hy : Odd y) : Odd (x * y + 2 * y) := by
  sorry

3.1.7. 例

你大概可以猜到“偶数”的定义。

定义

整数 \(a\) 称为偶数，如果存在整数 \(k\)，使得 \(a=2k\)。

def Even (a : ℤ) : Prop := ∃ k, a = 2 * k

问题

设 \(m\) 为整数。证明：如果 \(m\) 是奇数，则 \(3m-5\) 是偶数。

解答

由于 \(m\) 是奇数，存在整数 \(t\)，使得 \(m = 2t+1\)。因此

\[\begin{split}3 m-5 &= 3 (2 t + 1) - 5 \\ & = 2 (3 t - 1),\end{split}\]

所以 \(3m-5\) 是偶数。

example {m : ℤ} (hm : Odd m) : Even (3 * m - 5) := by
  sorry

3.1.8. 例

问题

设 \(n\) 为偶整数。证明 \(n ^ 2 + 2n - 5\) 是奇数。

example {n : ℤ} (hn : Even n) : Odd (n ^ 2 + 2 * n - 5) := by
  sorry

3.1.9. 例

事实上，每个整数不是偶数就是奇数；稍后我们会在 例 4.2.9 中讨论如何证明这一点。

在 Lean 中，这个事实可以作为引理 Int.even_or_odd 调用：

lemma Int.even_or_odd (n : ℤ) : Even n ∨ Odd n :=

问题

设 \(n\) 为整数。证明 \(n ^ 2 + n + 4\) 是偶数。

解答

我们根据 \(n\) 是偶数还是奇数分类讨论。

如果 \(n\) 是偶数，那么存在整数 \(x\)，使得 \(n=2x\)。于是

\[\begin{split}n ^ 2 + n + 4 &= (2 x) ^ 2 + 2 x + 4\\ &= 2 (2 x ^ 2 + x + 2),\end{split}\]

所以 \(n ^ 2 + n + 4\) 是偶数。

如果 \(n\) 是奇数，那么存在整数 \(x\)，使得 \(n=2x+1\)。于是

\[\begin{split}n ^ 2 + n + 4 &= (2 x + 1) ^ 2 + (2 x + 1) + 4 \\ &= 2 (2 x ^ 2 + 3 x + 3),\end{split}\]

所以 \(n ^ 2 + n + 4\) 仍然是偶数。

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. 练习

1. 证明 -9 是奇数。

   example : Odd (-9 : ℤ) := by
     sorry
   

2. 证明 26 是偶数。

   example : Even (26 : ℤ) := by
     sorry
   

3. 设 \(m\) 为奇整数，\(n\) 为偶整数。证明 \(n+m\) 是奇数。

   example {m n : ℤ} (hm : Odd m) (hn : Even n) : Odd (n + m) := by
     sorry
   

4. 设 \(p\) 为奇整数，\(q\) 为偶整数。证明 \(p-q-4\) 是奇数。

   example {p q : ℤ} (hp : Odd p) (hq : Even q) : Odd (p - q - 4) := by
     sorry
   

5. 设 \(a\) 为偶整数，\(b\) 为奇整数。证明 \(3a+b-3\) 是偶数。

   example {a b : ℤ} (ha : Even a) (hb : Odd b) : Even (3 * a + b - 3) := by
     sorry
   

6. 证明：如果整数 \(r\) 和 \(s\) 都是奇数，则 \(3r-5s\) 是偶数。

   example {r s : ℤ} (hr : Odd r) (hs : Odd s) : Even (3 * r - 5 * s) := by
     sorry
   

7. 设 \(x\) 为整数。证明：如果 \(x\) 是奇数，则 \(x^3\) 也是奇数。

   example {x : ℤ} (hx : Odd x) : Odd (x ^ 3) := by
     sorry
   

8. 设 \(n\) 为奇整数。证明 \(n^2-3n+2\) 是偶数。

   example {n : ℤ} (hn : Odd n) : Even (n ^ 2 - 3 * n + 2) := by
     sorry
   

9. 设 \(a\) 为整数，并假设 \(a\) 是奇数。证明 \(a^2+2a-4\) 是奇数。

   example {a : ℤ} (ha : Odd a) : Odd (a ^ 2 + 2 * a - 4) := by
     sorry
   

10. 设 \(p\) 为奇整数。证明 \(p^2+3p-5\) 是奇数。

    example {p : ℤ} (hp : Odd p) : Odd (p ^ 2 + 3 * p - 5) := by
      sorry
    

11. 设 \(x\) 和 \(y\) 为奇整数。证明 \(xy\) 是奇数。

    example {x y : ℤ} (hx : Odd x) (hy : Odd y) : Odd (x * y) := by
      sorry
    

12. 设 \(n\) 为整数。证明 \(3n^2+3n-1\) 是奇数。

    example (n : ℤ) : Odd (3 * n ^ 2 + 3 * n - 1) := by
      sorry
    

13. 设 \(n\) 为整数。证明存在整数 \(m\geq n\)，使得 \(m\) 为奇数。

    example (n : ℤ) : ∃ m ≥ n, Odd m := by
      sorry
    

14. 设 \(a\)、\(b\) 和 \(c\) 为整数。证明 \(a-b\)、\(a+c\) 或 \(b-c\) 中至少有一个是偶数。1

    example (a b c : ℤ) : Even (a - b) ∨ Even (a + c) ∨ Even (b - c) := by
      sorry
    

脚注

1

练习取自 Hammack，《Book of Proof》，第 9 章。

3.2. 整除性

3.2.1. 例

另一个你也许以前见过的数学定义是整除性的定义。

定义

自然数 \(b\) 能被另一个自然数 \(a\) 整除，如果存在自然数 \(c\)，使得 \(b=ac\)。

例如，

问题

证明自然数 88 能被 11 整除。

解答

\(88 = 11 \cdot 8\)。

整除性是一个非常重要的概念，并且有几种不同说法。下面这些说法含义相同：

• \(b\) 能被 \(a\) 整除
• \(b\) 是 \(a\) 的倍数
• \(a\) 是 \(b\) 的约数
• \(a\) 是 \(b\) 的因子
• \(a\) 整除 \(b\)

我们最常使用最后一种“\(a\) 整除 \(b\)”，因为它最简洁。还有一个标准记号 \(a \mid b\)，我们也会经常使用。

在 Lean 中，整除性的定义已经在库中，同时还有许多关于它的定理。我们通常用记号 ∣ 在 Lean 中处理这个定义，它的写法与纸上记号相同。

与 第 3.1 节 中的 dsimp [Odd] 类似，可以在 Lean 证明中途展开整除性的定义，以提醒自己它在当前语境中的含义。命令是 dsimp [(· ∣ ·)]。

example : (11 : ℕ) ∣ 88 := by
  dsimp [(· ∣ ·)]
  use 8
  numbers

3.2.2. 例

这个定义的另一个特点是，虽然我们上面是对自然数陈述的，但我们也经常希望考虑整数的整除性。下面是相应定义。

定义

整数 \(b\) 能被另一个整数 \(a\) 整除，如果存在整数 \(c\)，使得 \(b=ac\)。

对于整数整除性，我们也使用所有相同的变体术语，以及相同的记号 \(a \mid b\)。

问题

证明整数 6 能被 -2 整除。

解答

\(6 = -2 \cdot -3\)。

example : (-2 : ℤ) ∣ 6 := by
  sorry

3.2.3. 例

问题

设 \(a\) 和 \(b\) 为整数，并且假设 \(a \mid b\)。证明 \(a \mid b^2+2b\)。

解答

由于 \(a \mid b\)，存在整数 \(k\)，使得 \(b=ak\)。于是

\[\begin{split}b ^ 2 + 2 b &= (a k) ^ 2 + 2 (a k) \\ & = a (k (a k + 2)).\end{split}\]

所以 \(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. 例

问题

设 \(a\)、\(b\) 和 \(c\) 为自然数，并且假设 \(a \mid b\) 且 \(b^2\mid c\)。证明 \(a^2 \mid c\)。

解答

由于 \(a \mid b\)，存在自然数 \(x\) 使得 \(b=ax\)。由于 \(b^2 \mid c\)，存在自然数 \(y\) 使得 \(c=b^2y\)。于是

\[\begin{split}c &= b ^ 2 y \\ & = (a x) ^ 2 y\\ & = a ^ 2 (x ^ 2 y).\end{split}\]

所以 \(a^2 \mid c\)。

把这个解答翻译成 Lean。照常，如果愿意，你可以使用命令 dsimp [(· ∣ ·)] at * 在目标状态中的所有地方把 \(\mid\) 展开为定义，不过这不是必需的。

example {a b c : ℕ} (hab : a ∣ b) (hbc : b ^ 2 ∣ c) : a ^ 2 ∣ c := by
  sorry

3.2.5. 例

问题

设 \(x\)、\(y\) 和 \(z\) 为自然数，并且假设 \(xy \mid z\)。证明 \(x \mid z\)。

解答

由于 \(xy \mid z\)，存在自然数 \(t\)，使得 \(z=(xy)t\)。于是

\[\begin{split}z &= (xy)t \\ & = x(yt).\end{split}\]

所以 \(x \mid z\)。

example {x y z : ℕ} (h : x * y ∣ z) : x ∣ z := by
  sorry

3.2.6. 例

你可能会问，怎样证明一个数不能被另一个数整除。这里有一个方便的判据，它是本书后面将在 例 4.5.8 中证明的定理：如果整数 \(b\) 位于整数 \(a\) 的两个相邻倍数之间，则 \(a\) 不整除 \(b\)。

问题

证明 12 不能被 5 整除。

解答

\(5 \cdot 2 < 12 < 5 \cdot (2 + 1)\)。

在 Lean 中，这个判据可作为引理 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 :=

下面是在 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. 例

问题

设 \(a\) 和 \(b\) 为自然数，其中 \(b\) 为正，并且假设 \(a\) 整除 \(b\)。证明 \(a \le b\)。

解答

由于 \(a \mid b\)，存在自然数 \(k\)，使得 \(b=ak\)。

我们先注意到

\[0 < b =ak\]

所以 \(0<k\)。因此实际上 \(1 \le k\)。

现在，我们有

\[\begin{split}a &= a \cdot 1 \\ &≤ a k \\ &= b.\end{split}\]

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]

这个引理在 Lean 主库中可用，名称为 Nat.le_of_dvd。

3.2.8. 例

问题

设 \(a\) 和 \(b\) 为自然数，其中 \(b\) 为正，并且假设 \(a\) 整除 \(b\)。证明 \(a\) 为正。

解答

由于 \(a \mid b\)，存在自然数 \(k\)，使得 \(b=ak\)。

我们有

\[0 < b = a k,\]

所以 \(0<a\)。

example {a b : ℕ} (hab : a ∣ b) (hb : 0 < b) : 0 < a := by
  sorry

这个引理也在 Lean 主库中可用，名称为 Nat.pos_of_dvd_of_pos。

3.2.9. 练习

1. 证明 0 能被每个整数 \(t\) 整除。

   example (t : ℤ) : t ∣ 0 := by
     sorry
   

2. 证明 -10 不能被 3 整除。

   example : ¬(3 : ℤ) ∣ -10 := by
     sorry
   

3. 设 \(x\) 和 \(y\) 为整数，并且假设 \(x \mid y\)。证明 \(x \mid 3y-4y^2\)。

   example {x y : ℤ} (h : x ∣ y) : x ∣ 3 * y - 4 * y ^ 2 := by
     sorry
   

4. 设 \(m\) 和 \(n\) 为整数，并且假设 \(m \mid n\)。证明 \(m \mid 2n^3+n\)。

   example {m n : ℤ} (h : m ∣ n) : m ∣ 2 * n ^ 3 + n := by
     sorry
   

5. 设 \(a\) 和 \(b\) 为整数，并且假设 \(a \mid b\)。证明 \(a \mid 2b^3-b^2+3b\)。

   example {a b : ℤ} (hab : a ∣ b) : a ∣ 2 * b ^ 3 - b ^ 2 + 3 * b := by
     sorry
   

6. 设 \(k\)、\(l\) 和 \(m\) 为整数，并且假设 \(k\) 整除 \(l\)，且 \(l^3\) 整除 \(m\)。证明 \(k^3\) 整除 \(m\)。

   example {k l m : ℤ} (h1 : k ∣ l) (h2 : l ^ 3 ∣ m) : k ^ 3 ∣ m := by
     sorry
   

7. 设 \(p\)、\(q\) 和 \(r\) 为整数，并且假设 \(p^3\) 整除 \(q\)，且 \(q^2\) 整除 \(r\)。证明 \(p^6\) 整除 \(r\)。

   example {p q r : ℤ} (hpq : p ^ 3 ∣ q) (hqr : q ^ 2 ∣ r) : p ^ 6 ∣ r := by
     sorry
   

8. 证明：存在自然数 \(n>0\)，使得 \(9\) 是 \(2^n-1\) 的因子。

   example : ∃ n : ℕ, 0 < n ∧ 9 ∣ 2 ^ n - 1 := by
     sorry
   

9. 证明：存在整数 \(a\) 和 \(b\)，且 \(0<b<a\)，使得 \(a-b \mid a+b\)。

   example : ∃ a b : ℤ, 0 < b ∧ b < a ∧ a - b ∣ a + b := by
     sorry
   

3.3. 模算术：理论

定义

整数 \(a\) 和 \(b\) 称为模 \(n\) 同余，如果 \(n\mid (a-b)\)。

我们用记号 \(a\equiv b \mod n\) 表示 \(a\) 与 \(b\) 模 \(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. 例

问题

证明 \(11\equiv 3 \mod 4\)。

解答

\(11-3=4\cdot 2\)，所以 \(4\mid(11-3)\)。

example : 11 ≡ 3 [ZMOD 4] := by
  use 2
  numbers

3.3.2. 例

问题

证明 \(-5\equiv 1 \mod 3\)。

解答

\(-5-1=3\cdot -2\)，所以 \(3\mid(-5-1)\)。

example : -5 ≡ 1 [ZMOD 3] := by
  sorry

3.3.3. 例

引理（模算术的加法规则）

设 \(a\)、\(b\)、\(c\)、\(d\) 和 \(n\) 为整数，并且假设 \(a\equiv b \mod n\)、\(c\equiv d \mod n\)。则 \(a+c\equiv b+d \mod n\)。

证明

由于 \(a\equiv b \mod n\)，存在整数 \(x\)，使得 \(a-b=nx\)。由于 \(c\equiv d \mod n\)，存在整数 \(y\)，使得 \(c-d=ny\)。于是

\[\begin{split}a + c - (b + d) &= (a - b) + (c - d) \\ &= n x + n y \\ &= n (x + y),\end{split}\]

所以 \(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. 练习

引理（模算术的减法规则）

设 \(a\)、\(b\)、\(c\)、\(d\) 和 \(n\) 为整数，并且假设 \(a\equiv b \mod n\)、\(c\equiv d \mod n\)。则 \(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. 练习

引理（模算术的取负规则）

设 \(a\)、\(b\) 和 \(n\) 为整数，并且假设 \(a\equiv b \mod n\)。则 \(-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. 例

引理（模算术的乘法规则）

设 \(a\)、\(b\)、\(c\)、\(d\) 和 \(n\) 为整数，并且假设 \(a\equiv b \mod n\)、\(c\equiv d \mod n\)。则 \(ac\equiv bd \mod n\)。

证明

由于 \(a\equiv b \mod n\)，存在整数 \(x\)，使得 \(a-b=nx\)。由于 \(c\equiv d \mod n\)，存在整数 \(y\)，使得 \(c-d=ny\)。于是

\[\begin{split}a c - b d &= (a - b) c + b (c - d) \\ &= (n x) c + b (n y) \\ & = n (x c + b y),\end{split}\]

所以 \(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. 例

警告：模算术中不存在“除法规则”！

问题

可能存在整数 \(a\)、\(b\)、\(c\)、\(d\) 和 \(n\)，使得 \(a\equiv b \mod n\)、\(c\equiv d \mod n\)，但 \(\frac{a}{c}\not\equiv \frac{b}{d} \mod n\)。

解答

可取 \(a=10\)、\(b=18\)、\(c=2\)、\(d=6\)。事实上，

• \(10-18=4\cdot -2\)，所以 \(10\equiv 18 \mod 4\)；
• \(2-6=4\cdot -1\)，所以 \(2\equiv 6 \mod 4\)；
• \(\frac{10}{2}-\frac{18}{6}=2\) 位于 4 的两个相邻倍数 \(4\cdot 0\) 与 \(4\cdot (0+1)\) 之间，所以 \(\frac{10}{2}\not\equiv \frac{18}{6} \mod 4\)。

注意，这里我们使用了 例 3.2.6 中的不整除判据。

3.3.8. 例

引理（模算术的平方规则）

设 \(a\)、\(b\) 和 \(n\) 为整数，并且假设 \(a\equiv b \mod n\)。则 \(a^2\equiv b^2 \mod n\)。

证明

由于 \(a\equiv b \mod n\)，存在整数 \(x\)，使得 \(a-b=nx\)。于是

\[\begin{split}a ^ 2 - b ^ 2 &= (a - b) (a + b) \\ &= (n x) (a + b) \\ &= n (x (a + b)).\end{split}\]

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. 练习

引理（模算术的立方规则）

设 \(a\)、\(b\) 和 \(n\) 为整数，并且假设 \(a\equiv b \mod n\)。则 \(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

事实上，对任意幂次同样成立，尽管我们现在还没有证明它的工具。本书稍后会在 例 6.1.3 中回到这一点。

引理（模算术的幂规则）

设 \(k\) 为自然数，设 \(a\)、\(b\) 和 \(n\) 为整数，并且假设 \(a\equiv b \mod n\)。则 \(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. 例

引理（模算术的自反性规则）

设 \(a\) 和 \(n\) 为整数。则 \(a\equiv a \mod n\)。

证明

\(a-a=n\cdot 0\)，所以 \(n\mid a-a\)。

theorem Int.ModEq.refl (a : ℤ) : a ≡ a [ZMOD n] := by
  use 0
  ring

3.3.11. 例

呼！刚才有很多引理。但你现在会看到，它们很值得。假设现在遇到一个非常具体的模算术问题，其一般类型与我们已见过的问题相同。

问题

设 \(a\) 和 \(b\) 为整数，并且假设 \(a\equiv 2 \mod 4\)。证明 \(a b ^ 2 + a ^ 2 b + 3a \equiv 2b ^ 2 + 2 ^ 2 \cdot b + 3 \cdot 2 \mod 4\)。

我们可以直接从定义出发解决它，但那相当痛苦：

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

或者，更好的是，我们可以按正确顺序应用已经证明过的引理的正确组合来解决它。这需要少得多的思考：

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. 练习

1. 证明 \(34\equiv 104 \mod 5\)。

   example : 34 ≡ 104 [ZMOD 5] := by
     sorry
   

2. （模算术的对称性规则）设 \(a\)、\(b\) 和 \(n\) 为整数，并且假设 \(a\equiv b \mod n\)。证明 \(b\equiv a \mod n\)。

   theorem Int.ModEq.symm (h : a ≡ b [ZMOD n]) : b ≡ a [ZMOD n] := by
     sorry
   

3. （模算术的传递性规则）设 \(a\)、\(b\)、\(c\) 和 \(n\) 为整数，并且假设 \(a\equiv b \mod n\) 且 \(b\equiv c \mod n\)。证明 \(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
   

4. 设 \(a\)、\(c\) 和 \(n\) 为整数。证明 \(a+nc\equiv a \mod n\)。

   example : a + n * c ≡ a [ZMOD n] := by
     sorry
   

5. 给出 例 3.3.7 的另一种解答（即使用不同的数）。

6. 设 \(a\) 和 \(b\) 为整数，并且假设 \(a \equiv b \mod 5\)。证明 \(2a+3 \equiv 2b+3 \mod 5\)。请给出两个解答，仿照 例 3.3.11 中两个解答的风格。

   example {a b : ℤ} (h : a ≡ b [ZMOD 5]) : 2 * a + 3 ≡ 2 * b + 3 [ZMOD 5] := by
     sorry
   

7. 设 \(m\) 和 \(n\) 为整数，并且假设 \(m \equiv n \mod 4\)。证明 \(3m-1 \equiv 3n-1 \mod 4\)。请给出两个解答，仿照 例 3.3.11 中两个解答的风格。

   example {m n : ℤ} (h : m ≡ n [ZMOD 4]) : 3 * m - 1 ≡ 3 * n - 1 [ZMOD 4] := by
     sorry
   

8. 设 \(k\) 为整数，并且假设 \(k\equiv 3 \mod 5\)。证明 \(4k+k^3+3\equiv 4\cdot 3 + 3^3 + 3 \mod 5\)。请给出两个解答，仿照 例 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. 模算术：计算

3.4.1. 例

回忆 例 3.3.11 的问题。

问题

设 \(a\) 和 \(b\) 为整数，并且假设 \(a\equiv 2 \mod 4\)。证明 \(a b ^ 2 + a ^ 2 b + 3a \equiv 2b ^ 2 + 2 ^ 2 \cdot b + 3 \cdot 2 \mod 4\)。

在解决这个问题以及 第 3.3 节 中许多类似问题之后，你大概觉得自己已经能一眼检查这种风格的任何陈述是否正确。这很好！当你可以一眼看出某个结论时，在文字证明中通常也可以省略细节。

这通常也是容易写出 Lean 策略来检查一类陈述正确性的时刻。我正是这样做的：更新了策略 rel，使其覆盖模算术的这类步骤。

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. 例

从现在起，我们会解决更有趣的模算术问题，把类似 例 3.3.11 的步骤压缩为一行。

问题

设 \(a\) 和 \(b\) 为整数，且 \(a \equiv 4\mod 5\)、\(b \equiv 3\mod 5\)。证明 \(ab+b^3+3 \equiv 2\mod 5\)。

解答

\[\begin{split}a b + b ^ 3 + 3 &\equiv 4 b + b ^ 3 + 3 \mod 5\\ &\equiv 4 \cdot 3 + 3 ^ 3 + 3 \mod 5\\ &=2+5 \cdot 8\\ &\equiv 2\mod 5.\end{split}\]

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. 例

问题

证明：存在整数 \(a\)，使得 \(6a \equiv 4\mod 11\)。

解答

整数 8 具有这个性质。事实上，

\[\begin{split}6 \cdot 8 &= 4 + 4 \cdot 11\\ &\equiv 4\mod 11.\end{split}\]

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. 例

问题

设 \(x\) 为整数。证明 \(x ^ 3 \equiv x\mod 3\)。

解答

我们按照 \(x\) 模 3 的余数分类讨论。

情形 1（\(x\equiv 0\mod 3\)）：

\[\begin{split}x^3 &\equiv 0^3\mod 3\\ & = 0\\ &\equiv x\mod 3.\end{split}\]

情形 2（\(x\equiv 1\mod 3\)）：

\[\begin{split}x^3 &\equiv 1^3\mod 3\\ & = 1\\ &\equiv x\mod 3.\end{split}\]

情形 3（\(x\equiv 2\mod 3\)）：

\[\begin{split}x^3 &\equiv 2^3\mod 3\\ & = 2 + 3 \cdot 2\\ &\equiv 2\mod 3\\ &\equiv x\mod 3.\end{split}\]

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. 练习

1. 设 \(n\) 为满足 \(n\equiv 1\mod 3\) 的整数。证明 \(n^3+7n\equiv 2\mod 3\)。

   example {n : ℤ} (hn : n ≡ 1 [ZMOD 3]) : n ^ 3 + 7 * n ≡ 2 [ZMOD 3] :=
     sorry
   

2. 设 \(a\) 为满足 \(a\equiv 3\mod 4\) 的整数。证明 \(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
   

3. 设 \(a\) 和 \(b\) 为整数。证明 \((a+b)^3\equiv a^3+b^3\mod 3\)。

   example (a b : ℤ) : (a + b) ^ 3 ≡ a ^ 3 + b ^ 3 [ZMOD 3] :=
     sorry
   

4. 证明：存在整数 \(a\)，使得 \(4a\equiv 1\mod 7\)。

   example : ∃ a : ℤ, 4 * a ≡ 1 [ZMOD 7] := by
     sorry
   

5. 证明：存在整数 \(k\)，使得 \(5k\equiv 6\mod 8\)。

   example : ∃ k : ℤ, 5 * k ≡ 6 [ZMOD 8] := by
     sorry
   

6. 设 \(n\) 为整数。证明 \(5n^2+3n+7\equiv 1\mod 2\)。

   example (n : ℤ) : 5 * n ^ 2 + 3 * n + 7 ≡ 1 [ZMOD 2] := by
     sorry
   

7. 设 \(x\) 为整数。证明 \(x^5\equiv x\mod 5\)。

   example {x : ℤ} : x ^ 5 ≡ x [ZMOD 5] := by
     sorry
   

3.5. 贝祖等式

3.5.1. 例

问题

设 \(n\) 为整数，并且假设 \(5n\) 是 \(8\) 的倍数。证明 \(n\) 也是 \(8\) 的倍数。

解答

由于 \(8\mid 5n\)，存在整数 \(a\)，使得 \(5n=8a\)。于是

\[\begin{split}n &= -3 (5 n) + 16 n \\ &= -3 (8 a) + 16 n \\ & = 8 (-3 a + 2 n),\end{split}\]

所以 \(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

这种问题通常会有许多可能的解法。下面是另一种解法。

解答

由于 \(8\mid 5n\)，存在整数 \(a\)，使得 \(5n=8a\)。于是

\[\begin{split}n &= 5 (5 n) - 24 n \\ &= 5 (8 a) -24 n \\ & = 8 (5 a - 3 n),\end{split}\]

所以 \(8\mid n\)。

请试着把这个变体解答输入 Lean。

example {n : ℤ} (hn : 8 ∣ 5 * n) : 8 ∣ n := by
  sorry

3.5.2. 例

问题

证明：如果对某个整数 \(n\) 有 \(5\) 整除 \(3n\)，则 \(5\) 也整除 \(n\)。

解答

由于 \(5\mid 3n\)，存在整数 \(x\)，使得 \(3n=5x\)。于是

\[\begin{split}n &= 2 (3 n) - 5 n \\ &= 2 (5 x) - 5 n \\ & = 5 (2x - n),\end{split}\]

所以 \(5\mid n\)。

example {n : ℤ} (h1 : 5 ∣ 3 * n) : 5 ∣ n := by
  sorry

3.5.3. 例

问题

设 \(m\) 为能被 8 和 5 整除的整数。证明它也能被 40 整除。

解答

由于 \(8\mid m\)，存在整数 \(a\)，使得 \(m=8a\)。由于 \(5\mid m\)，存在整数 \(b\)，使得 \(m=5b\)。于是

\[\begin{split}m &= -15 m + 16 m\\ &= -15 (8 a) + 16 m \\ &= -15 (8 a) + 16 (5 b) \\ & = 40 (-3 a + 2 b),\end{split}\]

所以 \(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. 练习

1. 证明：如果 6 整除 \(11n\)，则 6 整除 \(n\)。

   example {n : ℤ} (hn : 6 ∣ 11 * n) : 6 ∣ n := by
     sorry
   

2. 设 \(a\) 为整数，并假设 \(5a\) 是 \(7\) 的倍数。证明 \(a\) 也是 \(7\) 的倍数。

   example {a : ℤ} (ha : 7 ∣ 5 * a) : 7 ∣ a := by
     sorry
   

3. 假设 7 和 9 都是某个整数 \(n\) 的因子。证明 63 也是 \(n\) 的因子。

   example {n : ℤ} (h1 : 7 ∣ n) (h2 : 9 ∣ n) : 63 ∣ n := by
     sorry
   

4. 设 \(n\) 为能被 5 和 13 整除的整数。证明它也能被 65 整除。

   example {n : ℤ} (h1 : 5 ∣ n) (h2 : 13 ∣ n) : 65 ∣ n := by
     sorry