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 $\vee$ or $\mathrm{\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

$$\begin{array}{rl}3n+2& =3(2k+1)+2\\ & =2(3k+2)+1,\end{array}$$

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

$$\begin{array}{rl}x+y+1& =(2a+1)+(2b+1)+1\\ & =2(a+b+1)+1,\end{array}$$

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

$$\begin{array}{rl}xy+2y& =(2a+1)(2b+1)+2(2b+1)\\ & =2(2ab+3b+a+1)+1,\end{array}$$

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

$$\begin{array}{rl}3m-5& =3(2t+1)-5\\ & =2(3t-1),\end{array}$$

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+2n-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

$$\begin{array}{rl}{n}^2+n+4& =(2x{)}^2+2x+4\\ & =2(2x^2+x+2),\end{array}$$

so $n^2+n+4$ is even.

If $n$ is odd, then there exists an integer $x$ such that $n=2x+1$. Then

$$\begin{array}{rl}{n}^2+n+4& =(2x+1{)}^2+(2x+1)+4\\ & =2(2x^2+3x+3),\end{array}$$

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

1. Prove that -9 is odd.

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

2. Prove that 26 is even.

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

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

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

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

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

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

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

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

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

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

12. Let $n$ be an integer. Show that $3n^2+3n-1$ is odd.

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

13. Let $n$ be an integer. Show that there exists an integer $m\ge n$ which is odd.

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

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

$$\begin{array}{rl}{b}^2+2b& =(ak{)}^2+2(ak)\\ & =a(k(ak+2)).\end{array}$$

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^{2}y$. Then

$$\begin{array}{rl}c& =b^{2}y\\ & =(ax{)}^{2}y\\ & =a^2(x^{2}y).\end{array}$$

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

$$\begin{array}{rl}z& =(xy)t\\ & =x(yt).\end{array}$$

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

$$0<b=ak$$

so $0<k$. Thus in fact $1\le k$.

Now, we have

$$\begin{array}{rl}a& =a\cdot 1\\ & \le ak\\ & =b.\end{array}$$

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

$$0<b=ak,$$

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

1. Show that 0 is divisible by every integer $t$.

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

2. Show that -10 is not divisible by 3.

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

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

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

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

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

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

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

9. 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\mathrm{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\mathrm{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\mathrm{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\mathrm{mod}n$ and $c\equiv d\mathrm{mod}n$. Then $a+c\equiv b+d\mathrm{mod}n$.

Proof

Since $a\equiv b\mathrm{mod}n$, there exists an integer $x$ such that $a-b=nx$. Since $c\equiv d\mathrm{mod}n$, there exists an integer $y$ such that $c-d=ny$. Then

$$\begin{array}{rl}a+c-(b+d)& =(a-b)+(c-d)\\ & =nx+ny\\ & =n(x+y),\end{array}$$

so $a+c\equiv b+d\mathrm{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\mathrm{mod}n$ and $c\equiv d\mathrm{mod}n$. Then $a-c\equiv b-d\mathrm{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\mathrm{mod}n$. Then $-a\equiv -b\mathrm{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\mathrm{mod}n$ and $c\equiv d\mathrm{mod}n$. Then $ac\equiv bd\mathrm{mod}n$.

Proof

Since $a\equiv b\mathrm{mod}n$, there exists an integer $x$ such that $a-b=nx$. Since $c\equiv d\mathrm{mod}n$, there exists an integer $y$ such that $c-d=ny$. Then

$$\begin{array}{rl}ac-bd& =(a-b)c+b(c-d)\\ & =(nx)c+b(ny)\\ & =n(xc+by),\end{array}$$

so $ac\equiv bd\mathrm{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\mathrm{mod}n$ and $c\equiv d\mathrm{mod}n$, but $\frac{a}{c}\not\equiv \frac{b}{d}\mathrm{mod}n$.

Solution

We can take $a=10$, $b=18$, $c=2$, $d=6$. Indeed,

• $10-18=4\cdot -2$, so $10\equiv 18\mathrm{mod}4$;

• $2-6=4\cdot -1$, so $2\equiv 6\mathrm{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}\mathrm{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\mathrm{mod}n$. Then $a^2\equiv b^2\mathrm{mod}n$.

Proof

Since $a\equiv b\mathrm{mod}n$, there exists an integer $x$ such that $a-b=nx$. Then

$$\begin{array}{rl}{a}^2-b^2& =(a-b)(a+b)\\ & =(nx)(a+b)\\ & =n(x(a+b)).\end{array}$$

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\mathrm{mod}n$. Then $a^3\equiv b^3\mathrm{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\mathrm{mod}n$. Then $a^k\equiv b^k\mathrm{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\mathrm{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\mathrm{mod}4$. Show that $a{b}^2+a^{2}b+3a\equiv 2b^2+2^2\cdot b+3\cdot 2\mathrm{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

1. Show that $34\equiv 104\mathrm{mod}5$.

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

2. (symmetry rule for modular arithmetic) Let $a$, $b$ and $n$ be integers, and suppose that $a\equiv b\mathrm{mod}n$. Show that $b\equiv a\mathrm{mod}n$.

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

3. (transitivity rule for modular arithmetic) Let $a$, $b$, $c$ and $n$ be integers, and suppose that $a\equiv b\mathrm{mod}n$ and $b\equiv c\mathrm{mod}n$. Show that $a\equiv c\mathrm{mod}n$.

   theorem Int.ModEq.trans (h1 : a ≡ b [ZMOD n]) (h2 : b ≡ c [ZMOD n]) :
       a ≡ c [ZMOD n] := by
     sorry
   

4. Let $a$, $c$ and $n$ be integers. Show that $a+nc\equiv a\mathrm{mod}n$.

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

5. Give an alternative solution (i.e., with different numbers) to Example 3.3.7.

6. Let $a$ and $b$ be integers, and suppose that $a\equiv b\mathrm{mod}5$. Show that $2a+3\equiv 2b+3\mathrm{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
   

7. Let $m$ and $n$ be integers, and suppose that $m\equiv n\mathrm{mod}4$. Show that $3m-1\equiv 3n-1\mathrm{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
   

8. Let $k$ be an integer, and suppose that $k\equiv 3\mathrm{mod}5$. Show that $4k+k^3+3\equiv 4\cdot 3+3^3+3\mathrm{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\mathrm{mod}4$. Show that $a{b}^2+a^{2}b+3a\equiv 2b^2+2^2\cdot b+3\cdot 2\mathrm{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\mathrm{mod}5$ and $b\equiv 3\mathrm{mod}5$. Show that $ab+b^3+3\equiv 2\mathrm{mod}5$.

Solution

$$\begin{array}{rl}ab+b^3+3& \equiv 4b+b^3+3\mathrm{mod}5\\ & \equiv 4\cdot 3+3^3+3\mathrm{mod}5\\ & =2+5\cdot 8\\ & \equiv 2\mathrm{mod}5.\end{array}$$

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\mathrm{mod}11$.

Solution

The integer 8 has this property. Indeed,

$$\begin{array}{rl}6\cdot 8& =4+4\cdot 11\\ & \equiv 4\mathrm{mod}11.\end{array}$$

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\mathrm{mod}3$.

Solution

We consider cases according to the residue of $x$ modulo 3.

Case 1 ($x\equiv 0\mathrm{mod}3$):

$$\begin{array}{rl}{x}^3& \equiv 0^3\mathrm{mod}3\\ & =0\\ & \equiv x\mathrm{mod}3.\end{array}$$

Case 2 ($x\equiv 1\mathrm{mod}3$):

$$\begin{array}{rl}{x}^3& \equiv 1^3\mathrm{mod}3\\ & =1\\ & \equiv x\mathrm{mod}3.\end{array}$$

Case 3 ($x\equiv 2\mathrm{mod}3$):

$$\begin{array}{rl}{x}^3& \equiv 2^3\mathrm{mod}3\\ & =2+3\cdot 2\\ & \equiv 2\mathrm{mod}3\\ & \equiv x\mathrm{mod}3.\end{array}$$

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

1. Let $n$ be an integer for which $n\equiv 1\mathrm{mod}3$. Show that $n^3+7n\equiv 2\mathrm{mod}3$.

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

2. Let $a$ be an integer for which $a\equiv 3\mathrm{mod}4$. Show that $a^3+4a^2+2\equiv 1\mathrm{mod}4$.

   example {a : ℤ} (ha : a ≡ 3 [ZMOD 4]) :
       a ^ 3 + 4 * a ^ 2 + 2 ≡ 1 [ZMOD 4] :=
     sorry
   

3. Let $a$ and $b$ be integers. Show that $(a+b{)}^3\equiv a^3+b^3\mathrm{mod}3$.

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

4. Show that there exists an integer $a$, such that $4a\equiv 1\mathrm{mod}7$.

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

5. Show that there exists an integer $k$, such that $5k\equiv 6\mathrm{mod}8$.

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

6. Let $n$ be an integer. Show that $5n^2+3n+7\equiv 1\mathrm{mod}2$.

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

7. Let $x$ be an integer. Show that $x^5\equiv x\mathrm{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

$$\begin{array}{rl}n& =-3(5n)+16n\\ & =-3(8a)+16n\\ & =8(-3a+2n),\end{array}$$

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

$$\begin{array}{rl}n& =5(5n)-24n\\ & =5(8a)-24n\\ & =8(5a-3n),\end{array}$$

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

$$\begin{array}{rl}n& =2(3n)-5n\\ & =2(5x)-5n\\ & =5(2x-n),\end{array}$$

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

$$\begin{array}{rl}m& =-15m+16m\\ & =-15(8a)+16m\\ & =-15(8a)+16(5b)\\ & =40(-3a+2b),\end{array}$$

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

1. Show that if 6 divides $11n$, then it divides $n$.

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

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

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

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