4. Proofs with structure, II

In the course of Chapter 2, we studied the logical symbols $\vee$, $\wedge$ and $\mathrm{\exists }$, which allow complicated mathematical statements to be built up from simpler ones. For each such symbol, we learned its “grammar”: the rule for using it when it appears in a hypothesis and the rule for using it when it appears in the goal. This grammar is called natural deduction.

This chapter finishes the work started in Chapter 2. We learn the grammar of the remaining logical symbols: $\mathrm{\forall }$, $\to$, and $\mathrm{\neg }$. We also learn the grammar of two other logical symbols, $\leftrightarrow$ and $\mathrm{\exists }!$, which are less fundamental because they can be defined in terms of the other ones.

4.1. “For all” and implication

4.1.1. Example

Problem

Let $a$ be a real number and suppose that for all real numbers $x$, it is true that $a\le x^2-2x$. Show that $a\le -1$.

Fig. 4.1 The parabola $y=x^2-2x$.

Specifying that a formula or predicate is meant to be true for all values of a variable $x$, like we did with $a\le x^2-2x$ in the above problem, is called universally quantifying over the variable $x$. It is expressed symbolically as ∀.

To use a hypothesis with a universal quantifier, you may want to “specialize” its use to one particular variable. For example, in the solution below, we use the special case of the hypothesis in which $x$ is set to 1.

Solution

$$\begin{array}{rl}a& \le 1^2-2\cdot 1\\ & =-1.\end{array}$$

In Lean, perform this specialization using the apply tactic.

example {a : ℝ} (h : ∀ x, a ≤ x ^ 2 - 2 * x) : a ≤ -1 :=
  calc
    a ≤ 1 ^ 2 - 2 * 1 := by apply h
    _ = -1 := by numbers

4.1.2. Example

Problem

Let $n$ be a natural number which is a factor of every natural number $m$. Show that $n=1$.

Solution

Since $n$ is a factor of every natural number, it is a factor of $1$. Also notice that $1$ is positive. So we can invoke the size bounds on factors discussed in Example 3.2.7 and Example 3.2.8: $n\le 1$ and $1\le n$. Therefore $n=1$.

For the Lean proof, we recall that the bound from Example 3.2.7 is in Lean as Nat.le_of_dvd, and the bound from Example 3.2.8 is in Lean as Nat.pos_of_dvd_of_pos.

example {n : ℕ} (hn : ∀ m, n ∣ m) : n = 1 := by
  have h1 : n ∣ 1 := by apply hn
  have h2 : 0 < 1 := by numbers
  apply le_antisymm
  · apply Nat.le_of_dvd h2 h1
  · apply Nat.pos_of_dvd_of_pos h1 h2

4.1.3. Example

Problem

Let $a$ and $b$ be real numbers and suppose that every real number $x$ is either at least $a$ or at most $b$. Show that $a\le b$.

Solution

Consider the real number $\frac{a+b}{2}$. It is either at least $a$ or at most $b$.

Case 1: $\frac{a+b}{2}\ge a$. Then

$$\begin{array}{rl}b& =2\left(\frac{a+b}{2}\right)-a\\ & \ge 2\cdot a-a\\ & =a.\end{array}$$

Case 2: $\frac{a+b}{2}\le b$. Then

$$\begin{array}{rl}a& =2\left(\frac{a+b}{2}\right)-b\\ & \le 2\cdot b-b\\ & =b.\end{array}$$

example {a b : ℝ} (h : ∀ x, x ≥ a ∨ x ≤ b) : a ≤ b := by
  sorry

4.1.4. Example

Problem

Let $a$ be real number whose square is at most 2, and which is greater than or equal to any real number whose square is at most 2. 1 Let $b$ be another real number with the same two properties. Prove that $a=b$.

Consider the hypothesis in this problem that

$a$ is greater than or equal to any real number whose square is at most 2.

Implicitly, there is a universal quantification (“any real number”), and also an implication, so a more pedantic version of this hypothesis would be

for all real numbers $y$, if $y^2\le 2$ then $y\le a$.

We can specialize such a hypothesis to any particular choice of $y$ for which the antecedent $y^2\le 2$ is true.

Solution

Since $a^2\le 2$, and $b$ is greater than or equal to any real number whose square is at most 2, $a\le b$.

Since $b^2\le 2$, and $a$ is greater than or equal to any real number whose square is at most 2, $b\le a$.

Therefore $a=b$.

In Lean, an implication is expressed using the symbol →. The tactic apply works for hypotheses featuring implications. In the proof below, the goal state before apply hb2 is

a b: ℝ
ha1 : a ^ 2 ≤ 2
hb1 : b ^ 2 ≤ 2
ha2 : ∀ (y : ℝ), y ^ 2 ≤ 2 → y ≤ a
hb2 : ∀ (y : ℝ), y ^ 2 ≤ 2 → y ≤ b
⊢ a ≤ b

and the goal state after it is

a b : ℝ
ha1 : a ^ 2 ≤ 2
hb1 : b ^ 2 ≤ 2
ha2 : ∀ (y : ℝ), y ^ 2 ≤ 2 → y ≤ a
hb2 : ∀ (y : ℝ), y ^ 2 ≤ 2 → y ≤ b
⊢ a ^ 2 ≤ 2

The hypothesis ∀ (y : ℝ), y ^ 2 ≤ 2 → y ≤ b has been applied to the goal a ≤ b, leaving the hopefully-easier goal a ^ 2 ≤ 2: proving the antecedent of the implication.

Fill in the second part of the proof.

example {a b : ℝ} (ha1 : a ^ 2 ≤ 2) (hb1 : b ^ 2 ≤ 2) (ha2 : ∀ y, y ^ 2 ≤ 2 → y ≤ a)
    (hb2 : ∀ y, y ^ 2 ≤ 2 → y ≤ b) :
    a = b := by
  apply le_antisymm
  · apply hb2
    apply ha1
  · sorry

4.1.5. Example

Problem

Show that there exists a real number $b$ such that for every real number $x$, it is true that $b\le x^2-2x$.

Notice that in this problem a universally quantified statement appears in the goal: “for every real number $x$, ….”

Solution

We show that -1 has this property. Indeed, let $x$ be a real number; then

$$\begin{array}{rl}-1& \le -1+(x-1{)}^2\\ & =x^2-2x.\end{array}$$

We solve the problem by formally introducing a particular, arbitrary real number $x$ (“let $x$ be a real number”) and proving the desired statement for that $x$. In Lean this argument is performed by the tactic intro. Before the use of this tactic, the goal state is

⊢ ∀ (x : ℝ), -1 ≤ x ^ 2 - 2 * x

After the use of this tactic, the goal state is

x : ℝ
⊢ -1 ≤ x ^ 2 - 2 * x

example : ∃ b : ℝ, ∀ x : ℝ, b ≤ x ^ 2 - 2 * x := by
  use -1
  intro x
  calc
    -1 ≤ -1 + (x - 1) ^ 2 := by extra
    _ = x ^ 2 - 2 * x := by ring

4.1.6. Example

Problem

Show that there exists a real number $c$ such that for all real numbers $x$ and $y$, if $x^2+y^2\le 4$, then $x+y\ge c$.

Here the goal contains universal quantification over $x$ and $y$, as well as an implication: “if $x^2+y^2\le 4$, then ….” In solving the problem, we formally introduce the variables $x$ and $y$ and also the hypothesis $x^2+y^2\le 4$ which they are assumed to satisfy:

Solution

We show that -3 has this property. Indeed, let $x$ and $y$ be real numbers and suppose that $x^2+y^2\le 4$. Then

$$\begin{array}{rl}(x+y{)}^2& \le (x+y{)}^2+(x-y{)}^2\\ & =2(x^2+y^2)\\ & \le 2\cdot 4\\ & \le 3^2.\end{array}$$

So $x+y\ge -3$ (and also $x+y\le 3$).

In Lean, the introduction of both the variables $x$ and $y$ and the hypothesis $x^2+y^2\le 4$ is done using the intro tactic. To deduce from $(x+y{)}^2\le 3^2$ that $-3\le x+y$ and $x+y\le 3$, you will need to use the lemma

lemma abs_le_of_sq_le_sq' (h : x ^ 2 ≤ y ^ 2) (hy : 0 ≤ y) : -y ≤ x ∧ x ≤ y :=

which we previously saw in Example 2.4.2.

example : ∃ c : ℝ, ∀ x y, x ^ 2 + y ^ 2 ≤ 4 → x + y ≥ c := by
  sorry

4.1.7. Example

Definition

A property is true for all sufficiently large integers $n$, if there exists an integer $N$, such that that property is true for all integers $n\ge N$.

Likewise for rational numbers, real numbers, ….

Problem

Show that for all sufficiently large integers $n$, it is true that $n^3\ge 4n^2+7$.

In the solution that follows, “For all $n\ge 5$” is a shorter way of expressing, “Let $n$ be an integer and suppose that $n\ge 5$”.

Solution

For all $n\ge 5$,

$$\begin{array}{rl}{n}^3& =n\cdot n^2\\ & \ge 5n^2\\ & =4n^2+n^2\\ & \ge 4n^2+5^2\\ & =4n^2+7+18\\ & \ge 4n^2+7.\end{array}$$

I have provided the notation forall_sufficiently_large to express this and similar problems in Lean.

example : forall_sufficiently_large n : ℤ, n ^ 3 ≥ 4 * n ^ 2 + 7 := by
  dsimp
  use 5
  intro n hn
  calc
    n ^ 3 = n * n ^ 2 := by ring
    _ ≥ 5 * n ^ 2 := by rel [hn]
    _ = 4 * n ^ 2 + n ^ 2 := by ring
    _ ≥ 4 * n ^ 2 + 5 ^ 2 := by rel [hn]
    _ = 4 * n ^ 2 + 7 + 18 := by ring
    _ ≥ 4 * n ^ 2 + 7 := by extra

4.1.8. Example

Definition

A natural number $p$ is prime, if it is at least $2$, and the only factors of $p$ are $1$ and $p$.

def Prime (p : ℕ) : Prop :=
  2 ≤ p ∧ ∀ m : ℕ, m ∣ p → m = 1 ∨ m = p

Problem

Show that 2 is prime.

Solution

Clearly $2\le 2$. Let $m$ be a factor of $2$. Since $2$ is positive, by the size bounds on factors discussed in Example 3.2.7 and Example 3.2.8, we have that $m\le 2$ and $1\le m$. The only natural numbers $m$ satisfying $m\le 2$ and $1\le m$ are $1$ and $2$, so as required $m=1$ or $m=2$.

One new technique used in this solution is to observe from numeric bounds on a natural number (like $m\le 2$ and $1\le m$ here) that there are finitely many possibilities (here, $m=1$ or $m=2$.) In Lean, we use the tactic interval_cases for this kind of argument. It also works for integers, but it doesn’t work for rational numbers or real numbers – why?

example : Prime 2 := by
  constructor
  · numbers -- show `2 ≤ 2`
  intro m hmp
  have hp : 0 < 2 := by numbers
  have hmp_le : m ≤ 2 := Nat.le_of_dvd hp hmp
  have h1m : 1 ≤ m := Nat.pos_of_dvd_of_pos hmp hp
  interval_cases m
  · left
    numbers -- show `1 = 1`
  · right
    numbers -- show `2 = 2`

This lemma is available for future use in Lean under the name prime_two.

4.1.9. Example

You might be wondering how to prove that a natural number $p$ is not prime. The idea is to show that it can be expressed as a nontrivial product.

Problem

Show that 6 is not prime.

Solution

$6=2\cdot 3$, so $2\mid 6$. But $2\ne 1$ and $2\ne 6$.

We will prove this test carefully in Example 4.5.7. For now, feel free to use it. In Lean the lemma name is not_prime.

example : ¬ Prime 6 := by
  apply not_prime 2 3
  · numbers -- show `2 ≠ 1`
  · numbers -- show `2 ≠ 6`
  · numbers -- show `6 = 2 * 3`

4.1.10. Exercises

1. Let $a$ be a rational number and suppose that for all rational numbers $b$, $a\ge -3+4b-b^2$. Show that $a\ge 1$.

   example {a : ℚ} (h : ∀ b : ℚ, a ≥ -3 + 4 * b - b ^ 2) : a ≥ 1 :=
     sorry
   

2. Let $n$ be an integer and suppose that every integer $m$ between 1 and 5 is a factor of $n$. Show that 15 is a factor of $n$. (You may need to review Section 3.5.)

   example {n : ℤ} (hn : ∀ m, 1 ≤ m → m ≤ 5 → m ∣ n) : 15 ∣ n := by
     sorry
   

3. Show that there exists a natural number $n$ such that every natural number $m$ is at least $n$.

   example : ∃ n : ℕ, ∀ m : ℕ, n ≤ m := by
     sorry
   

4. Show that there exists a real number $a$, such that for all real numbers $b$, there exists a real number $c$, such that $a+b<c$.

   example : ∃ a : ℝ, ∀ b : ℝ, ∃ c : ℝ, a + b < c := by
     sorry
   

5. Show that for all sufficiently large real numbers $x$, $x^3+3x\ge 7x^2+12$.

   example : forall_sufficiently_large x : ℝ, x ^ 3 + 3 * x ≥ 7 * x ^ 2 + 12 := by
     sorry
   

6. Show that 45 is not prime.

   You may use the Lean lemma not_prime, as in Example 4.1.9.

   example : ¬(Prime 45) := by
     sorry
   

Footnotes

1

That is, $a$ is maximal in the set of real numbers whose square is at most 2.

4.2. “If and only if”

4.2.1. Example

Problem

Let $a$ be a rational number. Show that $3a+1\le 7$ if and only if $a\le 2$.

The phrase “if and only if” means exactly what it sounds like. In this problem we have to show (1) if $3a+1\le 7$ then $a\le 2$ and (2) if $a\le 2$ then $3a+1\le 7$.

Solution

First, suppose that $3a+1\le 7$. Then

$$\begin{array}{rl}a& =\frac{(3a+1)-1}{3}\\ & \le \frac{7-1}{3}\\ & =2.\end{array}$$

Conversely, suppose that $a\le 2$. Then

$$\begin{array}{rl}3a+1& \le 3\cdot 2+1\\ & =7.\end{array}$$

In handwritten work, it is quite common to annotate the two directions with the symbols $\Rightarrow$ and $\Leftarrow$ respectively:

Solution

$\Rightarrow$ Suppose that $3a+1\le 7$. Then …

$\Leftarrow$ Suppose that $a\le 2$. Then …

This is recommended for homework, tests, writing on the blackboard, etc. In more formal writing (such as this book) we omit such symbols and instead use words like “First” and “Conversely” to signal the different parts of the proof.

In Lean, an “if and only if” is stated with the bi-implication symbol ↔. Since, under the hood, an “if and only if” is an “and” statement, we use the same tactic as for “and” goals: constructor.

example {a : ℚ} : 3 * a + 1 ≤ 7 ↔ a ≤ 2 := by
  constructor
  · intro h
    calc a = ((3 * a + 1) - 1) / 3 := by ring
      _ ≤ (7 - 1) / 3 := by rel [h]
      _ = 2 := by numbers
  · intro h
    calc 3 * a + 1 ≤ 3 * 2 + 1 := by rel [h]
      _ = 7 := by numbers

4.2.2. Example

Let’s modify Example 3.5.1 to be an if-and-only-if problem. Now there are two things to prove, one of which we did before.

Problem

Let $n$ be an integer. Show that $5n$ is a multiple of $8$ if and only if $n$ is.

Solution

Suppose that $8\mid 5n$. Then there exists an integer $a$ such that $5n=8a$. So

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

so $8\mid n$.

Conversely, suppose that $8\mid n$. Then there exists an integer $a$ such that $n=8a$. So

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

so $8\mid 5n$.

example {n : ℤ} : 8 ∣ 5 * n ↔ 8 ∣ n := by
  constructor
  · intro hn
    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
  · intro hn
    obtain ⟨a, ha⟩ := hn
    use 5 * a
    calc 5 * n = 5 * (8 * a) := by rw [ha]
      _ = 8 * (5 * a) := by ring

4.2.3. Example

Problem

Show that an integer $n$ is odd, if and only if it is congruent to 1 modulo 2.

Solution

First, suppose that $n$ is odd. Then there exists an integer $k$ such that $n=2k+1$. Therefore $n-1=2k$, so $n-1$ is divisible by 2, so $n\equiv 1\mathrm{mod}2$.

Conversely, suppose that $n\equiv 1\mathrm{mod}2$. Then $2\mid n-1$, so there exists an integer $k$ such $n-1=2k$. Thus $n=2k+1$ and so $n$ is odd.

We name this example Int.odd_iff_modEq for future use.

theorem odd_iff_modEq (n : ℤ) : Odd n ↔ n ≡ 1 [ZMOD 2] := by
  constructor
  · intro h
    obtain ⟨k, hk⟩ := h
    dsimp [Int.ModEq]
    dsimp [(· ∣ ·)]
    use k
    addarith [hk]
  · sorry

4.2.4. Example

Now do the same to characterise evenness.

Problem

Show that an integer $n$ is even, if and only if it is congruent to 0 modulo 2.

theorem even_iff_modEq (n : ℤ) : Even n ↔ n ≡ 0 [ZMOD 2] := by
  constructor
  · intro h
    obtain ⟨k, hk⟩ := h
    dsimp [Int.ModEq]
    dsimp [(· ∣ ·)]
    use k
    addarith [hk]
  · sorry

4.2.5. Example

The high school concept of “solving” equations represents an “if and only if” problem: to solve an equation, you state a list of numbers and prove that they satisfy the equation and no other numbers do.

Problem

Let $x$ be a real number. Show that $x^2+x-6=0$, if and only if $x=-3$ or $x=2$.

Solution

First, suppose that $x^2+x-6=0$. Then

$$\begin{array}{rl}(x+3)(x-2)& =x^2+x-6\\ & =0,\end{array}$$

so either $x+3=0$ or $x-2=0$. If the former, $x=-3$; if the latter, $x=2$.

Conversely, if $x=-3$ then

$$\begin{array}{rl}{x}^2+x-6& =(-3{)}^2+(-3)-6\\ & =0,\end{array}$$

and if $x=2$ then

$$\begin{array}{rl}{x}^2+x-6& =2^2+2-6\\ & =0.\end{array}$$

example {x : ℝ} : x ^ 2 + x - 6 = 0 ↔ x = -3 ∨ x = 2 := by
  sorry

4.2.6. Example

Problem

Let $a$ be an integer. Show that $a^2-5a+5\le -1$, if and only if $a$ is 2 or 3.

Solution

First, suppose that $a^2-5a+5\le -1$. Then

$$\begin{array}{rl}(2a-5{)}^2& =4(a^2-5a+5)+5\\ & \le 4\cdot -1+5\\ & =1^2,\end{array}$$

so $-1\le 2a-5\le 1$. Therefore $2\cdot 2\le 2a$, so $2\le a$, and similarly $2a\le 2\cdot 3$, so $a\le 3$. Since $2\le a\le 3$, $a$ is 2 or 3.

Conversely, if $a=2$ then

$$\begin{array}{rl}{a}^2-5a+5& =2^2-5\cdot 2+5\\ & \le -1,\end{array}$$

and if $a=3$ then

$$\begin{array}{rl}{a}^2-5a+5& =3^2-5\cdot 3+5\\ & \le -1.\end{array}$$

example {a : ℤ} : a ^ 2 - 5 * a + 5 ≤ -1 ↔ a = 2 ∨ a = 3 := by
  sorry

4.2.7. Example

Some library lemmas have the form of an “if and only if”. This is convenient because they take the place of two ordinary lemmas, one for each direction.

Problem

Let $n$ be an integer and suppose $n^2-10n+24=0$. Show that $n$ is even.

Solution

We have

$$\begin{array}{rl}(n-4)(n-6)& =n^2-10n+24\\ & =0,\end{array}$$

so either $n-4=0$ or $n-6=0$. If the former, then $n=2\cdot 2$ so $n$ is even; if the latter, then $n=2\cdot 3$ so $n$ is even.

In this problem we need to transform the fact $(n-4)(n-6)=0$ into the fact that “$n-4=0$ or $n-6=0$.” Previously (like in Example 2.3.4), we would have done this in Lean by inserting this fact directly into the lemma

theorem eq_zero_or_eq_zero_of_mul_eq_zero {a b : ℤ} (h : a * b = 0) : a = 0 ∨ b = 0 :=

resulting in a proof setup like this:

example {n : ℤ} (hn : n ^ 2 - 10 * n + 24 = 0) : Even n := by
  have hn1 :=
    calc (n - 4) * (n - 6) = n ^ 2 - 10 * n + 24 := by ring
      _ = 0 := hn
  have hn2 := eq_zero_or_eq_zero_of_mul_eq_zero hn1
  sorry

(Exercise: finish off the proof.)

But there is also a library lemma in ↔ form, which combines eq_zero_or_eq_zero_of_mul_eq_zero with the converse (other direction) of that statement:

theorem mul_eq_zero {a b : ℤ} : a * b = 0 ↔ a = 0 ∨ b = 0 :=

We can use an ↔ lemma in Lean with the rw tactic; it converts a hypothesis (or the goal) in the form of the left-hand side of the ↔ to one with the form of the right-hand side.

example {n : ℤ} (hn : n ^ 2 - 10 * n + 24 = 0) : Even n := by
  have hn1 :=
    calc (n - 4) * (n - 6) = n ^ 2 - 10 * n + 24 := by ring
      _ = 0 := hn
  rw [mul_eq_zero] at hn1 -- `hn1 : n - 4 = 0 ∨ n - 6 = 0`
  sorry

4.2.8. Example

Above, in Example 4.2.3, we proved that an integer is odd if and only if it is congruent to 1 modulo 2, recording this under the name Int.odd_iff_modEq. This is now also a convenient “if and only if” library lemma which we can use to solve problems about parity using modulo arithmetic. As an example, let’s re-do the problem from Example 3.1.5.

Problem

Prove that if the integers $x$ and $y$ are odd, then $x+y+1$ is odd.

Solution

We will prove that if $x\equiv 1\mathrm{mod}2$ and $y\equiv 1\mathrm{mod}2$ then $x+y+1\equiv 1\mathrm{mod}2$. Indeed,

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

example {x y : ℤ} (hx : Odd x) (hy : Odd y) : Odd (x + y + 1) := by
  rw [Int.odd_iff_modEq] at *
  calc x + y + 1 ≡ 1 + 1 + 1 [ZMOD 2] := by rel [hx, hy]
    _ = 2 * 1 + 1 := by ring
    _ ≡ 1 [ZMOD 2] := by extra

4.2.9. Example

Another way we can use the characterization of parity in terms of modular arithmetic is to prove the theorem from Example 3.1.9 whose proof we skipped.

Theorem

Every integer is either even or odd.

Proof

Let $n$ be an integer. We do a case division according to the residue of $n$ modulo 2.

If $n\equiv 0\mathrm{mod}2$, then $n$ is even, and we are done.

If $n\equiv 0\mathrm{mod}2$, then $n$ is odd, and we are done.

Write this in Lean using the lemmas Int.odd_iff_modEq and Int.even_iff_modEq from Example 4.2.3 and Example 4.2.4, together with the tactic mod_cases. I have written the beginning.

example (n : ℤ) : Even n ∨ Odd n := by
  mod_cases hn : n % 2
  · left
    rw [Int.even_iff_modEq]
    apply hn
  · sorry

4.2.10. Exercises

1. Let $x$ be a real number. Show that $2x-1=11$ if and only if $x=6$.

   example {x : ℝ} : 2 * x - 1 = 11 ↔ x = 6 := by
     sorry
   

2. Let $n$ be an integer. Show that 63 is a factor of $n$ if and only if both 7 and 9 are.

   example {n : ℤ} : 63 ∣ n ↔ 7 ∣ n ∧ 9 ∣ n := by
     sorry
   

3. Let $a$ and $n$ be integers. Show that $a$ is a multiple of $n$ if and only if $a\equiv 0\mathrm{mod}n$.

   theorem dvd_iff_modEq {a n : ℤ} : n ∣ a ↔ a ≡ 0 [ZMOD n] := by
     sorry
   

4. Let $a$ and $b$ be integers and suppose that $a\mid b$. Show that $a\mid 2b^3-b^2+3b$.

   Note that this appeared already as an exercise in Section 3.2. But now, using the lemma Int.dvd_iff_modEq proved in the previous exercise, this kind of problem is much easier.

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

5. Let $k$ be a natural number. Show that $k^2\le 6$, if and only if $k$ is 0, 1 or 2.

   example {k : ℕ} : k ^ 2 ≤ 6 ↔ k = 0 ∨ k = 1 ∨ k = 2 := by
     sorry
   

4.3. “There exists a unique”

4.3.1. Example

Problem

Show that there exists a unique real number $a$, such that $3a+1=7$.

Solution

We will show that 2 is the unique real number with this property.

First, we show that 2 has this property. Indeed, $3\cdot 2+1=7$.

Now, let $y$ be a real number for which $3y+1=7$. Then

$$\begin{array}{rl}y& =\frac{(3y+1)-1}{3}\\ & =\frac{7-1}{3}\\ & =2.\end{array}$$

example : ∃! a : ℝ, 3 * a + 1 = 7 := by
  use 2
  dsimp
  constructor
  · numbers
  intro y hy
  calc
    y = (3 * y + 1 - 1) / 3 := by ring
    _ = (7 - 1) / 3 := by rw [hy]
    _ = 2 := by numbers

4.3.2. Example

Problem

Show that there exists a unique rational number $x$, such that for every rational number $a$ between 1 and 3, $(a-x{)}^2\le 1$.

Solution

We will show that 2 is the unique rational number with this property.

Firstly, if $a$ is a rational number between 1 and 3, then $-1\le a-2\le 1$, so by Example 2.1.7,

$$\begin{array}{rl}(a-2{)}^2& \le 1^2\\ & =1.\end{array}$$

Now, let $y$ be a rational number for which, for every rational number $a$ between 1 and 3, $(a-y{)}^2\le 1$.

Since 1 is between 1 and 3, $(1-y{)}^2\le 1$, and since 3 is between 1 and 3, $(3-y{)}^2\le 1$.

So

$$\begin{array}{rl}(y-2{)}^2& =\frac{(1-y{)}^2+(3-y{)}^2-2}{2}\\ & \le \frac{1+1-2}{2}\\ & =0.\end{array}$$

Also $(y-2{)}^2\ge 0$, since squares are positive. Thus $(y-2{)}^2=0$, so $y-2=0$, and so $y=2$.

In Lean, the result of Example 2.1.7 is available as the lemma sq_le_sq'.

example : ∃! x : ℚ, ∀ a, a ≥ 1 → a ≤ 3 → (a - x) ^ 2 ≤ 1 := by
  sorry

4.3.3. Example

Problem

Let $x$ be a rational number, and suppose that there exists a unique rational number $a$ such that $a^2=x$. Show that $x=0$.

More colloquially: the only rational number with a unique square root is 0.

Solution

We first show that $-a=a$. Indeed,

$$\begin{array}{rl}(-a{)}^2& =a^2\\ & =x,\end{array}$$

and since $a$ is the unique rational number such that $a^2=x$, this means that $-a=a$.

It follows that

$$\begin{array}{rl}a& =\frac{a-(-a)}{2}\\ & =\frac{a-a}{2}\\ & =0.\end{array}$$

So $x=0$ also:

$$\begin{array}{rl}x& =a^2\\ & =0^2\\ & =0.\end{array}$$

example {x : ℚ} (hx : ∃! a : ℚ, a ^ 2 = x) : x = 0 := by
  obtain ⟨a, ha1, ha2⟩ := hx
  have h1 : -a = a
  · apply ha2
    calc
      (-a) ^ 2 = a ^ 2 := by ring
      _ = x := ha1
  have h2 :=
    calc
      a = (a - -a) / 2 := by ring
      _ = (a - a) / 2 := by rw [h1]
      _ = 0 := by ring
  calc
    x = a ^ 2 := by rw [ha1]
    _ = 0 ^ 2 := by rw [h2]
    _ = 0 := by ring

4.3.4. Example

The following is an important theorem about the integers, which we will prove later in the book, in the exercises to Section 6.6.

Theorem (the Division Algorithm)

Let $a$ and $b$ be integers, with $b$ positive. Then there exists a unique integer $r$ between 0 (inclusive) and $b$ (exclusive), such that $a\equiv r\mathrm{mod}b$.

This lemma is what allows us to do case divisions according to congruence class modulo $b$ (the Lean tactic mod_cases). But it’s actually a bit more powerful, since the “uniqueness” part of the statement provides extra information.

In the Lean library it is available in the following form:

lemma Int.existsUnique_modEq_lt (a b : ℤ) (h : 0 < b) :
  ∃! r : ℤ, 0 ≤ r ∧ r < b ∧ a ≡ r [ZMOD b] :=

To understand this theorem better, let’s prove just one of the infinitely many cases of this theorem.

Problem

Show that there exists a unique integer $r$, such that $0\le r<5$ and $14\equiv r\mathrm{mod}5$.

Solution

We will show that the unique integer with this property is 4.

First, we show that 4 has this property. It is true that $0\le 4<5$, and since $14-4=5\cdot 2$ it is true that $14\equiv r\mathrm{mod}5$.

Now, let $r$ be an integer for which $0\le r<5$ and $14\equiv r\mathrm{mod}5$. Then there exists an integer $q$ such that $14-r=5q$.

We have,

$$\begin{array}{rl}5& \cdot 1<14-r\\ & =5q,\end{array}$$

so since $5$ is positive, $1<q$. Similarly, we have

$$\begin{array}{rl}5q& =14-r\\ & <5\cdot 3\end{array}$$

and so since $5$ is positive, $q<3$.

Therefore $q$ must be 2, the only integer strictly between 1 and 3. So $r=14-5\cdot 2=4$.

example : ∃! r : ℤ, 0 ≤ r ∧ r < 5 ∧ 14 ≡ r [ZMOD 5] := by
  use 4
  dsimp
  constructor
  · constructor
    · numbers
    constructor
    · numbers
    use 2
    numbers
  intro r hr
  obtain ⟨hr1, hr2, q, hr3⟩ := hr
  have :=
    calc
      5 * 1 < 14 - r := by addarith [hr2]
      _ = 5 * q := by rw [hr3]
  cancel 5 at this
  have :=
    calc
      5 * q = 14 - r := by rw [hr3]
      _ < 5 * 3 := by addarith [hr1]
  cancel 5 at this
  interval_cases q
  addarith [hr3]

4.3.5. Exercises

1. Show that there exists a unique rational number $x$, such that $4x-3=9$.

   example : ∃! x : ℚ, 4 * x - 3 = 9 := by
     sorry
   

2. Show that there exists a unique natural number $n$, such that for all natural numbers $a$, we have $n\le a$.

   example : ∃! n : ℕ, ∀ a, n ≤ a := by
     sorry
   

3. Show that there exists a unique integer $r$, such that $0\le r<3$ and $11\equiv r\mathrm{mod}3$.

   example : ∃! r : ℤ, 0 ≤ r ∧ r < 3 ∧ 11 ≡ r [ZMOD 3] := by
     sorry
   

4.4. Contradictory hypotheses

4.4.1. Example

Sometimes, we encounter a situation with two contradictory hypotheses. At this point, there is no need to prove anything more. Two contradictory hypotheses mean that the situation we had hypothesized can’t actually happen.

It is quite common to encounter this when giving a proof by cases. You might reduce the problem to some list of cases, prove your goal in some of those cases, and prove that the other cases are impossible.

Here is an example of this kind of reasoning. I have written the solution very pedantically, to make the point clearer.

Lemma

Let $x$ and $y$ be real numbers, and suppose that $0<xy$ and $0\le x$. Show that $0<y$.

We have used this fact many times before – it is one of the facts which underlie the cancel tactic.

Proof

We consider two cases, depending on whether or not $y$ is positive.

Case 1 ($y\le 0$): Since $0\le x$, we have that

$$\begin{array}{rl}0& =x\cdot 0\\ & \ge xy,\end{array}$$

and so it is false that $0<xy$. This contradicts the hypothesis that $0<xy$, so this case can’t happen.

Case 2 ($0<y$): This is what we needed to prove, so we are done.

In Lean, the tactic contradiction concludes a (part of a) proof by pointing out two contradictory hypotheses. In the Lean translation of this example, notice that right before it’s used, the goal state is

y x : ℝ
h : 0 < x * y
hx : 0 ≤ x
hneg : y ≤ 0
this : ¬0 < x * y
⊢ 0 < y

which contains the contradictory hypotheses h : 0 < x * y and this : ¬0 < x * y. (Remember that ¬ is the logical symbol for “not”. If you don’t name a hypothesis, Lean labels it this.)

example {y : ℝ} (x : ℝ) (h : 0 < x * y) (hx : 0 ≤ x) : 0 < y := by
  obtain hneg | hpos : y ≤ 0 ∨ 0 < y := le_or_lt y 0
  · -- the case `y ≤ 0`
    have : ¬0 < x * y
    · apply not_lt_of_ge
      calc
        0 = x * 0 := by ring
        _ ≥ x * y := by rel [hneg]
    contradiction
  · -- the case `0 < y`
    apply hpos

4.4.2. Example

One very common way to get a contradiction is by proving that the hypotheses imply some “obviously false” numeric fact, whose falseness can be checked with numbers.

Problem

Let $t$ be an integer which is less than 3, and suppose that $t-1=6$. Show that $t=13$.

Solution

We have,

$$\begin{array}{rl}7& =t\\ & <3.\end{array}$$

But clearly it’s false that $7<3$, contradiction. So any conclusion (including $t=13$) is true.

You can write this proof up in Lean directly using the contradiction tactic, as in the previous examples:

example {t : ℤ} (h2 : t < 3) (h : t - 1 = 6) : t = 13 := by
  have H :=
  calc
    7 = t := by addarith [h]
    _ < 3 := h2
  have : ¬(7 : ℤ) < 3 := by numbers
  contradiction

But the pattern is also sufficiently common that there is a shorthand in Lean. If H is a hypothesis whose negation can be proved by numbers, then writing numbers at H will close the goal.

example {t : ℤ} (h2 : t < 3) (h : t - 1 = 6) : t = 13 := by
  have H :=
  calc
    7 = t := by addarith [h]
    _ < 3 := h2
  numbers at H -- this is a contradiction!

4.4.3. Example

Problem

Show that if $n^2+n+1\equiv 1\mathrm{mod}3$ then $n\equiv 0\mathrm{mod}3$ or $n\equiv 2\mathrm{mod}3$.

Solution

We consider cases according to the residue of $n$ modulo 3. If $n\equiv 0\mathrm{mod}3$ or $n\equiv 2\mathrm{mod}3$, then we are done. Otherwise, $n\equiv 1\mathrm{mod}3$, so

$$\begin{array}{rl}0& \equiv 0+3\cdot 1\mathrm{mod}3\\ & =1^2+1+1\\ & \equiv n^2+n+1\mathrm{mod}3\\ & \equiv 1\mathrm{mod}3,\end{array}$$

contradiction.

Notice that in the above proof we did some extra work to get $0\equiv 1\mathrm{mod}3$ for the contradiction, rather than $3\equiv 1\mathrm{mod}3$, which could have been obtained more easily:

$$\begin{array}{rl}3& =1^2+1+1\\ & \equiv \dots \end{array}$$

For the purposes of this book, we will treat as “obviously true/false” only congruences $i\equiv j\mathrm{mod}n$ for which $0\le i<n$ and $0\le j<n$. We will ask that congruences involving larger numbers be explicitly reduced modulo $n$, as we did here in reducing $3=1^2+1+1$ to $0+3\cdot 1$ modulo 3 and thus to $0$.

The mathematical justification for this is the uniqueness lemma Int.existsUnique_modEq_lt, discussed in Example 4.3.4.

example (n : ℤ) (hn : n ^ 2 + n + 1 ≡ 1 [ZMOD 3]) :
    n ≡ 0 [ZMOD 3] ∨ n ≡ 2 [ZMOD 3] := by
  mod_cases h : n % 3
  · -- case 1: `n ≡ 0 [ZMOD 3]`
    left
    apply h
  · -- case 2: `n ≡ 1 [ZMOD 3]`
    have H :=
      calc 0 ≡ 0 + 3 * 1 [ZMOD 3] := by extra
      _ = 1 ^ 2 + 1 + 1 := by numbers
      _ ≡ n ^ 2 + n + 1 [ZMOD 3] := by rel [h]
      _ ≡ 1 [ZMOD 3] := hn
    numbers at H -- contradiction!
  · -- case 3: `n ≡ 2 [ZMOD 3]`
    right
    apply h

4.4.4. Example

We defined prime numbers in Example 4.1.8, and proved that 2 was prime. Let’s now prove a slight reformulation of the definition, which will be convenient in showing that other numbers are prime.

Lemma

Let $p$ be a natural number greater than or equal to 2. Suppose that for all natural numbers $m$ for which $1<m<p$, it is not true that $m$ is a factor of $p$. Show that $p$ is prime.

Proof

Since we are given that $2\le p$, what’s left is to prove the second part of the definition “prime”: let $m$ be a factor of $p$ ($\star$); we must show that $m=1$ or $m=p$.

Since $m$ is a factor of $p$, we have that $1\le m$. So either $m=1$ or $1<m$; we consider cases accordingly.

Case 1 ($m=1$): This immediately gives our goal that $m=1$ or $m=p$.

Case 2 ($1<m$): Since $m$ is a factor of $p$, we have that $m\le p$. So either $m=p$ or $m<p$; we consider cases accordingly.

Case 2(i) ($m=p$): This immediately gives our goal that $m=1$ or $m=p$.

Case 2(ii) ($m<p$): We have now established that $1<m<p$, and by one of the facts given in the problem statement, this means that $m$ is not a factor of $p$. This contradicts the earlier statement ($\star$).

I’ve filled in about half of this proof in Lean; fill in the rest, including the final contradiction. If you need to look up the Lean names for the size bounds on factors, they were proved in Example 3.2.7 and Example 3.2.8.

example {p : ℕ} (hp : 2 ≤ p) (H : ∀ m : ℕ, 1 < m → m < p → ¬m ∣ p) : Prime p := by
  constructor
  · apply hp -- show that `2 ≤ p`
  intro m hmp
  have hp' : 0 < p := by extra
  have h1m : 1 ≤ m := Nat.pos_of_dvd_of_pos hmp hp'
  obtain hm | hm_left : 1 = m ∨ 1 < m := eq_or_lt_of_le h1m
  · -- the case `m = 1`
    left
    addarith [hm]
  -- the case `1 < m`
  sorry

We record this for future use under the Lean name prime_test.

Here’s an example of how this prime-testing lemma is used.

Problem

Show that 5 is prime.

Solution

Clearly $2\le 5$. Let $m$ be a natural number with $1<m<5$. We must show that 5 is not a multiple of $m$. There are three cases to check:

Case 1 ($m=2$): Since 5 lies between the consecutive multiples $2\cdot 2$ and $2\cdot 3$ of 2, it is not a multiple of 2.

Case 2 ($m=3$): Since 5 lies between the consecutive multiples $3\cdot 1$ and $3\cdot 2$ of 3, it is not a multiple of 3.

Case 3 ($m=4$): Since 5 lies between the consecutive multiples $4\cdot 1$ and $4\cdot 2$ of 4, it is not a multiple of 4.

example : Prime 5 := by
  apply prime_test
  · numbers
  intro m hm_left hm_right
  apply Nat.not_dvd_of_exists_lt_and_lt
  interval_cases m
  · use 2
    constructor <;> numbers
  · use 1
    constructor <;> numbers
  · use 1
    constructor <;> numbers

Here constructor <;> numbers is a shorthand for

constructor
· numbers
· numbers

More generally, <;> connects two tactics, performing the second one on every goal created by the first one.

4.4.5. Example

Here’s a harder example, with many cases.

Problem

Let $a$, $b$ and $c$ be positive natural numbers satisfying $a^2+b^2=c^2$. Show that $3\le a$.

Three numbers satisfying this equation are called a Pythagorean triple, since by Pythagoras’ theorem this means that they form the three sides of a right-angled triangle. The natural numbers 3, 4, 5 satisfy this equation: $3^2+4^2=5^2$. There are other solutions, like 5, 12, 13, but we are showing in this problem that 3, 4, 5 is the smallest solution.

Solution

Either $a\le 2$ or $3\le a$. If $3\le a$ then we are done. We will derive a contradiction if $a\le 2$.

Either $b\le 1$ or $2\le b$. We will consider these two cases separately.

Case 1 ($b\le 1$):

We have that

$$\begin{array}{rl}{c}^2& =a^2+b^2\\ & \le 2^2+1^2\\ & <3^2.\end{array}$$

This implies that $c<3$. We now have upper bounds $a\le 2$, $b\le 1$, $c<3$, so $a$ is 1 or 2, $b$ is 1, and $c$ is 1 or 2. We can analyze all these cases and check they don’t work:

$$\begin{array}{rl}{1}^2+1^2& \ne 1^2,\\ 2^2+1^2& \ne 1^2,\\ 1^2+1^2& \ne 2^2,\\ 2^2+1^2& \ne 2^2.\end{array}$$

Case 2 ($2\le b$):

We have that

$$\begin{array}{rl}{b}^2& <a^2+b^2\\ & =c^2,\end{array}$$

so $b<c$, so $b+1\le c$. But also

$$\begin{array}{rl}{c}^2& =a^2+b^2\\ & \le 2^2+b^2\\ & =b^2+2\cdot 2\\ & \le b^2+2b\\ & <b^2+2b+1\\ & =(b+1{)}^2,\end{array}$$

so $c<b+1$, so it is false that $b+1\le c$. These two facts contradict each other.

Write this proof up in Lean. It will be long; my version is 27 lines.

example {a b c : ℕ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
    (h_pyth : a ^ 2 + b ^ 2 = c ^ 2) : 3 ≤ a := by
  sorry

4.4.6. Exercises

1. Let $x$ and $y$ be real numbers, with $x$ nonnegative, and let $n$ be a positive natural number. Prove that if $y^n\le x^n$ then $y\le x$.

   We have used this fact before; it’s another of the lemmas which underlie the cancel tactic.

   example {x y : ℝ} (n : ℕ) (hx : 0 ≤ x) (hn : 0 < n) (h : y ^ n ≤ x ^ n) :
       y ≤ x := by
     sorry
   

2. Show that if $n^2\equiv 4\mathrm{mod}5$ then $n\equiv 2\mathrm{mod}5$ or $n\equiv 3\mathrm{mod}5$.

   example (n : ℤ) (hn : n ^ 2 ≡ 4 [ZMOD 5]) : n ≡ 2 [ZMOD 5] ∨ n ≡ 3 [ZMOD 5] := by
     sorry
   

3. Show that 7 is prime.

   example : Prime 7 := by
     sorry
   

4. Give a different proof of a problem from the exercises to Section 2.1: Let $x$ be a rational number whose square is 4, and which is greater than 1. Show that $x=2$.

   Instead of using the cancel tactic, give a direct proof using the ideas of this section: break into two cases, and then rule out one of them. (You may find it convenient to deduce a numeric contradiction.)

   example {x : ℚ} (h1 : x ^ 2 = 4) (h2 : 1 < x) : x = 2 := by
     have h3 :=
       calc
         (x + 2) * (x - 2) = x ^ 2 + 2 * x - 2 * x - 4 := by ring
         _ = 0 := by addarith [h1]
     rw [mul_eq_zero] at h3
     sorry
   

5. Show that a prime number is either 2 or odd.

   example (p : ℕ) (h : Prime p) : p = 2 ∨ Odd p := by
     sorry
   

4.5. Proof by contradiction

4.5.1. Example

Problem

Show that it is not true that for all real numbers $x$, we have $x^2\ge x$.

Solution

Suppose that for all real numbers $x$, we have $x^2\ge x$. Then in particular ${0.5}^2\ge 0.5$, but this is false, contradiction.

example : ¬ (∀ x : ℝ, x ^ 2 ≥ x) := by
  intro h
  have : 0.5 ^ 2 ≥ 0.5 := h 0.5
  numbers at this

4.5.2. Example

Problem

Show that 13 is not a multiple of 3.

In the past we have established non-divisibility facts using the theorem Nat.not_dvd_of_exists_lt_and_lt. But now we finally have the tools to do this from first principles.

Solution

Suppose that 13 were a multiple of 3. Then there would exist a natural number $k$ such that $13=3k$.

Case 1, $k\le 4$: Then

$$\begin{array}{rl}13& =3k\\ & \le 3\cdot 4,\end{array}$$

contradiction.

Case 2, $k\ge 5$: Then

$$\begin{array}{rl}13& =3k\\ & \ge 3\cdot 5,\end{array}$$

contradiction.

example : ¬ 3 ∣ 13 := by
  intro H
  obtain ⟨k, hk⟩ := H
  obtain h4 | h5 := le_or_succ_le k 4
  · have h :=
    calc 13 = 3 * k := hk
      _ ≤ 3 * 4 := by rel [h4]
    numbers at h
  · sorry

4.5.3. Example

Problem

Let $x$ and $y$ be real numbers and suppose that $x+y=0$. Show that it is not possible for both $x$ and $y$ to be positive.

Solution

Suppose that $x$ and $y$ were both positive. Then

$$\begin{array}{rl}0& =x+y\\ & >0,\end{array}$$

contradiction.

example {x y : ℝ} (h : x + y = 0) : ¬(x > 0 ∧ y > 0) := by
  intro h
  obtain ⟨hx, hy⟩ := h
  have H :=
  calc 0 = x + y := by rw [h]
    _ > 0 := by extra
  numbers at H

4.5.4. Example

Problem

Show that there does not exist a natural number $n$, such that $n^2=2$.

(Compare this with Example 2.3.2.)

Solution

Suppose that some integer $n$ satisfied $n^2=2$.

Case 1, $n\le 1$: Then

$$\begin{array}{rl}2& =n^2\\ & \le 1^2,\end{array}$$

contradiction.

Case 2, $n\ge 2$: Then

$$\begin{array}{rl}2& =n^2\\ & \ge 2^2,\end{array}$$

contradiction.

example : ¬ (∃ n : ℕ, n ^ 2 = 2) := by
  sorry

4.5.5. Example

Lemma

Show that an integer $n$ is even if and only if it is not odd.

Proof

First, let $n$ be even, and suppose that it were also odd. Then $n\equiv 0\mathrm{mod}2$ but also $n\equiv 1\mathrm{mod}2$. So

$$\begin{array}{rl}0& \equiv n\mathrm{mod}2\\ & \equiv 1\mathrm{mod}2,\end{array}$$

contradiction.

Now, suppose that $n$ is not odd. Since $n$ has to be either even or odd, it is even.

We record this for future use in Lean problems under the name Int.even_iff_not_odd.

example (n : ℤ) : Int.Even n ↔ ¬ Int.Odd n := by
  constructor
  · intro h1 h2
    rw [Int.even_iff_modEq] at h1
    rw [Int.odd_iff_modEq] at h2
    have h :=
    calc 0 ≡ n [ZMOD 2] := by rel [h1]
      _ ≡ 1 [ZMOD 2] := by rel [h2]
    numbers at h -- contradiction!
  · intro h
    obtain h1 | h2 := Int.even_or_odd n
    · apply h1
    · contradiction

Now repeat the process to characterise “not-even.”

Lemma

Show that an integer $n$ is odd if and only if it is not even.

example (n : ℤ) : Int.Odd n ↔ ¬ Int.Even n := by
  sorry

4.5.6. Example

Problem

Let $n$ be an integer. Show that $n^2\not\equiv 2\mathrm{mod}3$.

Solution

Suppose that $n^2\equiv 2\mathrm{mod}3$. We consider cases according to the residue of $n$ modulo 3.

If $n\equiv 0\mathrm{mod}3$, then

$$\begin{array}{rl}0& =0^2\\ & \equiv n^2\mathrm{mod}3\\ & \equiv 2\mathrm{mod}3,\end{array}$$

contradiction.

If $n\equiv 1\mathrm{mod}3$, then

$$\begin{array}{rl}1& =1^2\\ & \equiv n^2\mathrm{mod}3\\ & \equiv 2\mathrm{mod}3,\end{array}$$

contradiction.

Finally, if $n\equiv 2\mathrm{mod}3$, then

$$\begin{array}{rl}1& \equiv 1+3\cdot 1\mathrm{mod}3\\ & =2^2\\ & \equiv n^2\mathrm{mod}3\\ & \equiv 2\mathrm{mod}3,\end{array}$$

contradiction.

example (n : ℤ) : ¬(n ^ 2 ≡ 2 [ZMOD 3]) := by
  intro h
  mod_cases hn : n % 3
  · have h :=
    calc (0:ℤ) = 0 ^ 2 := by numbers
      _ ≡ n ^ 2 [ZMOD 3] := by rel [hn]
      _ ≡ 2 [ZMOD 3] := by rel [h]
    numbers at h -- contradiction!
  · sorry
  · sorry

4.5.7. Example

We can now pay a couple of debts. First, there is this theorem, first mentioned in Example 4.1.9:

Theorem

Let $p$, $k$ and $l$ be natural numbers, with $k\ne 1$, $k\ne p$, and $p=kl$. Then $p$ is not prime.

Proof

$k$ is a factor of $p$. If $p$ were prime, then by definition for any factor $x$ of $p$ either $x=1$ or $x=p$, so in particular $k=1$ or $k=p$. But either of these contradicts a hypothesis.

example {p : ℕ} (k l : ℕ) (hk1 : k ≠ 1) (hkp : k ≠ p) (hkl : p = k * l) :
    ¬(Prime p) := by
  have hk : k ∣ p
  · use l
    apply hkl
  intro h
  obtain ⟨h2, hfact⟩ := h
  have : k = 1 ∨ k = p := hfact k hk
  obtain hk1' | hkp' := this
  · contradiction
  · contradiction

4.5.8. Example

Secondly, there is this theorem, first mentioned in Example 3.2.6:

Theorem

Let $a$ and $b$ be integers. If there exists an integer $q$ such that $bq<a<b(q+1)$, then $a$ is not a multiple of $b$.

This is the lemma we have invoked in Lean as Int.not_dvd_of_exists_lt_and_lt.

Proof

Suppose for the sake of contradiction that $a$ is a multiple of $b$. Then there exists an integer $k$ such that $a=bk$. Also, let $q$ be an integer such that $bq<a<b(q+1)$.

We first note that

$$\begin{array}{rl}0& =a-a\\ & <b(q+1)-bq\\ & =b.\end{array}$$

Now let us reason from the two known inequalities separately. We first observe that

$$\begin{array}{rl}bk& =a\\ & <b(q+1),\end{array}$$

and so (since $b>0$) we have $k<q+1$.

We next observe that

$$\begin{array}{rl}bq& <a\\ & =bk,\end{array}$$

and so (since $b>0$) we have $q<k$, thus $q+1\le k$.

These two facts contradict each other, so $a$ must not be a multiple of $b$ after all.

example (a b : ℤ) (h : ∃ q, b * q < a ∧ a < b * (q + 1)) : ¬b ∣ a := by
  intro H
  obtain ⟨k, hk⟩ := H
  obtain ⟨q, hq₁, hq₂⟩ := h
  have hb :=
  calc 0 = a - a := by ring
    _ < b * (q + 1) - b * q := by rel [hq₁, hq₂]
    _ = b := by ring
  have h1 :=
  calc b * k = a := by rw [hk]
    _ < b * (q + 1) := hq₂
  cancel b at h1
  sorry

4.5.9. Example

We also establish a test for primality which will be more efficient than the test from Example 4.4.4.

Theorem

Let $p$ be a natural number which is at least 2. Let $T$ be another natural number, whose square is greater than $p$, and suppose that every natural number $m$ for which $1<m<T$ is not a factor of $p$. Then $p$ is prime.

(Notice that in the Example 4.4.4 test we had to check that every number up to $p$ was not a factor of $p$; with this test we only need to check the numbers up to approximately the square root of $p$.)

Proof

By the prime test from Example 4.4.4, it suffices to show that every natural number $m$ with $1<m<p$ is not a factor of $p$. Let $m$ be such a natural number. If $m<T$ then by hypothesis $m$ is not a factor of $p$.

So suppose that $T\le m$, and that $m$ is a factor of $p$. Then there exists a natural number $l$ such that $p=ml$. The natural number $l$ is a factor of $p$, too.

We claim that $1<l$. It will suffice to show that $m\cdot 1<ml$, and indeed,

$$\begin{array}{rl}m\cdot 1& =m\\ & <p\\ & =ml.\end{array}$$

We also claim that $l<T$. It will suffice to show that $Tl<T\cdot T$, and indeed,

$$\begin{array}{rl}Tl& \le ml\\ & =p\\ & <T^2\\ & =T\cdot T.\end{array}$$

Since we have established that $1<l<T$, by hypothesis $l$ is not a factor of $p$, contradiction. So $m$ must not be a factor of $p$ after all.

example {p : ℕ} (hp : 2 ≤ p)  (T : ℕ) (hTp : p < T ^ 2)
    (H : ∀ (m : ℕ), 1 < m → m < T → ¬ (m ∣ p)) :
    Prime p := by
  apply prime_test hp
  intro m hm1 hmp
  obtain hmT | hmT := lt_or_le m T
  · apply H m hm1 hmT
  intro h_div
  obtain ⟨l, hl⟩ := h_div
  have : l ∣ p
  · sorry
  have hl1 :=
    calc m * 1 = m := by ring
      _ < p := hmp
      _ = m * l := hl
  cancel m at hl1
  have hl2 : l < T
  · sorry
  have : ¬ l ∣ p := H l hl1 hl2
  contradiction

We record this for future use under the Lean name better_prime_test.

Here’s an example of how this prime-testing lemma is used. I have left some of the later cases for you to check.

Problem

Show that 79 is prime.

Solution

Clearly $2\le 79$. Also notice that $79<9^2$. Let $m$ be a natural number with $1<m<9$. We will show that 79 is not a multiple of $m$. There are seven cases to check:

Case 1 ($m=2$): Since 79 lies between the consecutive multiples $2\cdot 39$ and $2\cdot 40$ of 2, it is not a multiple of 2.

Case 2 ($m=3$): Since 79 lies between the consecutive multiples $3\cdot 26$ and $3\cdot 27$ of 3, it is not a multiple of 3.

Case 3 ($m=4$): Since 79 lies between the consecutive multiples $4\cdot 19$ and $4\cdot 20$ of 4, it is not a multiple of 4.

(etc. for 5, 6, 7 and 8)

example : Prime 79 := by
  apply better_prime_test (T := 9)
  · numbers
  · numbers
  intro m hm1 hm2
  apply Nat.not_dvd_of_exists_lt_and_lt
  interval_cases m
  · use 39
    constructor <;> numbers
  · use 26
    constructor <;> numbers
  · use 19
    constructor <;> numbers
  · sorry
  · sorry
  · sorry
  · sorry

4.5.10. Exercises

1. Show that there does not exist a real number $t$, such that $t\le 4$ and $t\ge 5$.

   example : ¬ (∃ t : ℝ, t ≤ 4 ∧ t ≥ 5) := by
     sorry
   

2. Show that there does not exist a real number $a$, such that $a^2\le 8$ and $a^3\ge 30$.

   example : ¬ (∃ a : ℝ, a ^ 2 ≤ 8 ∧ a ^ 3 ≥ 30) := by
     sorry
   

3. Show that 7 is not even.

   example : ¬ Int.Even 7 := by
     sorry
   

4. Let $n$ be an integer satisfying $n+3=7$. Show that $n$ cannot be both even and a solution to $n^2=10$.

   example {n : ℤ} (hn : n + 3 = 7) : ¬ (Int.Even n ∧ n ^ 2 = 10) := by
     sorry
   

5. Let $x$ be a real number satisfying $x^2<9$. Show that $x$ cannot be either less than or equal to -3, or greater than or equal to 3.

   example {x : ℝ} (hx : x ^ 2 < 9) : ¬ (x ≤ -3 ∨ x ≥ 3) := by
     sorry
   

6. Show that there does not exist a natural number $N$, such that every natural number greater than $N$ is even.

   example : ¬ (∃ N : ℕ, ∀ k > N, Nat.Even k) := by
     sorry
   

7. Let $n$ be an integer. Show that $n^2\not\equiv 2\mathrm{mod}4$.

   example (n : ℤ) : ¬(n ^ 2 ≡ 2 [ZMOD 4]) := by
     sorry
   

8. Show that 1 is not prime.

   We record this lemma for future use under the name not_prime_one.

   example : ¬ Prime 1 := by
     sorry
   

9. Show that 97 is prime.

   example : Prime 97 := by
     sorry