# 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 \(\lor\) or \(\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

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

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

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

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

so \(n ^ 2 + n + 4\) is even.

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

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

Prove that -9 is odd.

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

Prove that 26 is even.

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

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

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

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

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

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

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

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

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

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

Let \(n\) be an integer. Show that \(3n^2+3n- 1\) is odd.

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

Let \(n\) be an integer. Show that there exists an integer \(m\geq n\) which is odd.

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

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

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^2y\). Then

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

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

so \(0<k\). Thus in fact \(1 \le k\).

Now, we have

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

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

Show that 0 is divisible by every integer \(t\).

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

Show that -10 is not divisible by 3.

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

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

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

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

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

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

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

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 \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 \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 \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 \mod n\) and \(c\equiv d \mod n\). Then \(a+c\equiv b+d \mod n\).

Proof

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

so \(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. Exercise

Lemma (subtraction rule for modular arithmetic)

Let \(a\), \(b\), \(c\), \(d\) and \(n\) be integers, and suppose that \(a\equiv b \mod n\) and \(c\equiv d \mod n\). Then \(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. Exercise

Lemma (negation rule for modular arithmetic)

Let \(a\), \(b\) and \(n\) be integers, and suppose that \(a\equiv b \mod n\). Then \(-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. Example

Lemma (multiplication rule for modular arithmetic)

Let \(a\), \(b\), \(c\), \(d\) and \(n\) be integers, and suppose that \(a\equiv b \mod n\) and \(c\equiv d \mod n\). Then \(ac\equiv bd \mod n\).

Proof

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

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

Solution

We can take \(a=10\), \(b=18\), \(c=2\), \(d=6\). Indeed,

\(10-18=4\cdot -2\), so \(10\equiv 18 \mod 4\);

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

Proof

Since \(a\equiv b \mod n\), there exists an integer \(x\) such that \(a-b=nx\). Then

```
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 \mod n\). Then \(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
```

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 \mod n\). Then \(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. Example

Lemma (reflexivity rule for modular arithmetic)

Let \(a\) and \(n\) be integers. Then \(a\equiv a \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 \mod 4\). Show that \(a b ^ 2 + a ^ 2 b + 3 a \equiv 2 b ^ 2 + 2 ^ 2 \cdot b + 3 \cdot 2 \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

Show that \(34\equiv 104 \mod 5\).

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

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

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

(transitivity rule for modular arithmetic) Let \(a\), \(b\), \(c\) and \(n\) be integers, and suppose that \(a\equiv b \mod n\) and \(b\equiv c \mod n\). Show that \(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

Let \(a\), \(c\) and \(n\) be integers. Show that \(a+nc\equiv a \mod n\).

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

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

Let \(a\) and \(b\) be integers, and suppose that \(a \equiv b \mod 5\). Show that \(2a+3 \equiv 2b+3 \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

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

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

Solution

```
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\mod 11\).

Solution

The integer 8 has this property. Indeed,

```
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\mod 3\).

Solution

We consider cases according to the residue of \(x\) modulo 3.

**Case 1** (\(x\equiv 0\mod 3\)):

**Case 2** (\(x\equiv 1\mod 3\)):

**Case 3** (\(x\equiv 2\mod 3\)):

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

Let \(n\) be an integer for which \(n\equiv 1\mod 3\). Show that \(n^3+7n\equiv 2\mod 3\).

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

Let \(a\) be an integer for which \(a\equiv 3\mod 4\). Show that \(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

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

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

Show that there exists an integer \(a\), such that \(4a\equiv 1\mod 7\).

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

Show that there exists an integer \(k\), such that \(5k\equiv 6\mod 8\).

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

Let \(n\) be an integer. Show that \(5n^2+3n+7\equiv 1\mod 2\).

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

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

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

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

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

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

Show that if 6 divides \(11n\), then it divides \(n\).

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

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

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

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