Divisibility, Euclid's algorithm and unique factorisation

Lens

MotivationH

Tiles, jugs and a suspicious certainty

A workshop floor in Nairobi measures $1071$ cm by $462$ cm. The carpenter wants to cover it with identical square tiles, as large as possible, without cutting any. How big can the tiles be?

A tile of side $s$ fits exactly when $s$ divides both $1071$ and $462$ . So we want the greatest common divisor of $1071$ and $462$ . Listing all the divisors of both numbers would work, but slowly. Euclid, about $2300$ years ago, described a far faster method — and we will see that the answer is $21$ cm.

A second puzzle: with a $5$ -litre jug and a $3$ -litre jug and a tap, can you measure exactly $1$ litre? (Yes: fill the $3$ -litre jug twice and pour it into the $5$ -litre jug; the second time, $1$ litre is left over. In symbols, $2 \cdot 3 - 1 \cdot 5 = 1$ .) Which amounts can be measured with jugs of $a$ and $b$ litres? The answer is the same greatest common divisor.

Finally, a certainty you have relied on since primary school: every whole number breaks into primes in only one way, $360 = 2^3 \cdot 3^2 \cdot 5$ . It feels obvious. This lesson proves it — and shows a number system in which it is false.

DefinitionsH

Divisors, remainders and the gcd

Definition— divides

For integers $a$ and $b$ , $a$ divides $b$ , written $a \mid b$ , if $b = ak$ for some integer $k$ . We also say $a$ is a divisor of $b$ and $b$ is a multiple of $a$ . If $a$ does not divide $b$ we write $a \nmid b$ .

So $3 \mid 12$ , $-3 \mid 12$ , $5 \nmid 12$ , and every integer divides $0$ (since $0 = a \cdot 0$ ).

Theorem— Lemma 1 (rules for divisibility)

For integers $a, b, c, d, x, y$ : (a) if $a \mid b$ and $b \mid c$ , then $a \mid c$ ; (b) if $d \mid a$ and $d \mid b$ , then $d \mid ax + by$ ; (c) if $a \mid b$ and $b \neq 0$ , then $|a| \le |b|$ .

Proof

(a) If $b = ak$ and $c = bl$ , then $c = a(kl)$ . (b) If $a = dk$ and $b = dl$ , then $ax + by = d(kx + ly)$ . (c) If $b = ak$ with $b \neq 0$ , then $k \neq 0$ , so $|k| \ge 1$ and $|b| = |a|\,|k| \ge |a|$ .

∎

Theorem— Theorem 2 (division with remainder)

Let $a$ and $b$ be integers with $b > 0$ . There are unique integers $q$ (the quotient) and $r$ (the remainder) with

a = bq + r \quad\text{and}\quad 0 \le r < b .

Proof

Existence. The set $S = \{a - bq : q \in \Z\} \cap \{0, 1, 2, \dots\}$ is non-empty (take $q = -|a|$ ; then $a - bq = a + b|a| \ge a + |a| \ge 0$ ). By the well-ordering principle it has a least element $r = a - bq$ . Then $r \ge 0$ , and $r < b$ : otherwise $r - b = a - b(q + 1)$ would be a smaller element of $S$ . Uniqueness. If $bq + r = bq' + r'$ with $0 \le r, r' < b$ , then $b(q - q') = r' - r$ , a multiple of $b$ strictly between $-b$ and $b$ . The only such multiple is $0$ , so $q = q'$ and $r = r'$ .

∎

Definition— greatest common divisor, coprime, least common multiple

For integers $a, b$ not both zero, the greatest common divisor $\gcd(a, b)$ is the largest integer that divides both. (It exists: $1$ is a common divisor, and by Lemma 1(c) common divisors are at most $\max(|a|, |b|)$ .) Integers with $\gcd(a, b) = 1$ are coprime. For non-zero $a, b$ the least common multiple $\operatorname{lcm}(a, b)$ is the smallest positive integer divisible by both.

Definition— prime

A prime is an integer $p > 1$ whose only positive divisors are $1$ and $p$ . An integer $n > 1$ that is not prime is composite. (We met primes in factors, multiples and primes.)

Example— gcd versus lcm

For $12$ and $18$ : the common divisors are $1, 2, 3, 6$ , so $\gcd(12, 18) = 6$ ; the common multiples are $36, 72, \dots$ , so $\operatorname{lcm}(12, 18) = 36$ . Notice $6 \cdot 36 = 216 = 12 \cdot 18$ — no accident, as we will prove. The gcd is at most the smaller number; the lcm is at least the larger one.

ProofH

Euclid's algorithm

The whole algorithm rests on one observation.

Theorem— Lemma 3

If $a = bq + r$ , then the common divisors of $a$ and $b$ are exactly the common divisors of $b$ and $r$ . In particular, if $b > 0$ , then $\gcd(a, b) = \gcd(b, r)$ .

Proof

If $d \mid a$ and $d \mid b$ , then $d \mid a - bq = r$ by Lemma 1(b). Conversely, if $d \mid b$ and $d \mid r$ , then $d \mid bq + r = a$ . The two pairs have the same set of common divisors, hence the same greatest one.

∎

Theorem— Theorem 4 (Euclid's algorithm)

Let $a \ge b > 0$ . Divide repeatedly, each time dividing the previous divisor by the previous remainder:

\begin{aligned} a &= b q_1 + r_1, & 0 &\le r_1 < b,\\ b &= r_1 q_2 + r_2, & 0 &\le r_2 < r_1,\\ r_1 &= r_2 q_3 + r_3, & 0 &\le r_3 < r_2,\\ &\;\;\vdots \end{aligned}

The process stops with a remainder $0$ , and the last non-zero remainder is $\gcd(a, b)$ . (If $r_1 = 0$ , then $\gcd(a, b) = b$ .)

Proof

The remainders form a strictly decreasing sequence of natural numbers $b > r_1 > r_2 > \dots \ge 0$ . Such a sequence cannot go on for ever (its terms would form a non-empty set of natural numbers with no least element, contradicting well-ordering), so some remainder $r_{k+1}$ is $0$ . By Lemma 3,

\gcd(a, b) = \gcd(b, r_1) = \gcd(r_1, r_2) = \dots = \gcd(r_k, 0) = r_k ,

since the greatest divisor of $r_k > 0$ that also divides $0$ is $r_k$ itself.

∎

Example— The tiles: gcd(1071, 462)

\begin{aligned} 1071 &= 2 \cdot 462 + 147,\\ 462 &= 3 \cdot 147 + 21,\\ 147 &= 7 \cdot 21 + 0. \end{aligned}

The last non-zero remainder is $21$ , so $\gcd(1071, 462) = 21$ : the largest tile is $21$ cm, and the floor takes $51 \times 22$ tiles. Three divisions instead of listing dozens of divisors.

How fast is it? Each remainder is less than half of the number two steps before it ( $r_{i+2} < r_i / 2$ ), so the number of steps grows only like the number of digits. Lamé's theorem (Gabriel Lamé, 1844) makes this precise: the number of division steps is at most five times the number of decimal digits of the smaller number, with consecutive Fibonacci numbers as the worst cases. The computation section tests this.

Explore

Explore: Euclid's algorithm as cutting squares

Here is the algorithm as geometry. From a $252 \times 105$ rectangle, cut the largest possible squares; then do the same to the leftover strip, and so on. A square tile that fits both sides of the rectangle also fits the leftover — that is Lemma 3 — so the last square is the largest tile that fits exactly.

Euclid's algorithm: cutting squares

Step through the cuts. How many squares of each size do you cut, and how does that match the quotients 2, 2, 2?

Width252Height105

252 × 105

Step 1 of 4

A 252 by 105 rectangle. Press “Next step” to cut off the biggest squares that fit.

Things to try: change the sides to two consecutive Fibonacci numbers such as $89$ and $55$ (every cut removes just one square — the slowest case), and to two coprime numbers such as $100$ and $63$ (the last square has side $1$ ).

ProofH

Bézout's identity and Euclid's lemma

Running Euclid's algorithm backwards writes the gcd in terms of $a$ and $b$ . From the tiles example:

21 = 462 - 3 \cdot 147 = 462 - 3\,(1071 - 2 \cdot 462) = 7 \cdot 462 - 3 \cdot 1071 .

Check: $7 \cdot 462 = 3234$ and $3 \cdot 1071 = 3213$ , which differ by $21$ . This always works.

Theorem— Theorem 5 (Bézout's identity)

If $a$ and $b$ are integers, not both zero, there are integers $x$ and $y$ with

ax + by = \gcd(a, b).

Moreover, $\gcd(a, b)$ is the smallest positive integer of the form $ax + by$ , and every common divisor of $a$ and $b$ divides $\gcd(a, b)$ .

Proof

Let $S$ be the set of positive integers of the form $ax + by$ with $x, y \in \Z$ . It is non-empty ( $a^2 + b^2 > 0$ is in it), so by well-ordering it has a least element $d = ax_0 + by_0$ .

$d$ divides $a$ . Divide: $a = dq + r$ with $0 \le r < d$ . Then $r = a - dq = a(1 - qx_0) + b(-qy_0)$ has the form $ax + by$ . If $r$ were positive it would be an element of $S$ smaller than $d$ , which is impossible; so $r = 0$ and $d \mid a$ . In the same way $d \mid b$ .

Every common divisor divides $d$ . If $c \mid a$ and $c \mid b$ , then $c \mid ax_0 + by_0 = d$ by Lemma 1(b). In particular $c \le |c| \le d$ .

So $d$ is a common divisor and is at least as large as every common divisor: $d = \gcd(a, b)$ .

∎

The jug puzzle is now solved completely: with jugs of $a$ and $b$ litres one can measure exactly the multiples of $\gcd(a, b)$ (up to the size of the larger jug). And Bézout gives a useful test: $a$ and $b$ are coprime exactly when $ax + by = 1$ has an integer solution.

Theorem— Theorem 6 (Euclid's lemma)

Let $p$ be a prime. If $p \mid ab$ , then $p \mid a$ or $p \mid b$ .

Proof

Suppose $p \mid ab$ and $p \nmid a$ . The only positive divisors of $p$ are $1$ and $p$ , and $p$ does not divide $a$ , so $\gcd(p, a) = 1$ . By Bézout there are integers $x, y$ with $px + ay = 1$ . Multiplying by $b$ :

b = p(bx) + (ab)\,y .

Both terms on the right are divisible by $p$ (the second because $p \mid ab$ ), so $p \mid b$ by Lemma 1(b).

∎

The same proof shows more generally: if $d \mid ab$ and $\gcd(d, a) = 1$ , then $d \mid b$ . But the hypothesis matters: $4 \mid 2 \cdot 2$ , yet $4 \nmid 2$ . And by induction on the number of factors, if a prime divides a product $a_1 a_2 \cdots a_k$ , it divides at least one $a_i$ .

ProofH

The fundamental theorem of arithmetic

Theorem— Theorem 7 (fundamental theorem of arithmetic)

Every integer $n > 1$ can be written as a product of primes, $n = p_1 p_2 \cdots p_k$ , and this factorisation is unique apart from the order of the factors.

Proof

Existence, by strong induction on $n$ . If $n$ is prime, it is a product of one prime. Otherwise $n = ab$ with $1 < a, b < n$ ; by the induction hypothesis $a$ and $b$ are products of primes, and so is $n$ .

Uniqueness, by strong induction on $n$ . Suppose

n = p_1 p_2 \cdots p_k = q_1 q_2 \cdots q_l

with all $p_i$ and $q_j$ prime. Then $p_1$ divides $q_1 q_2 \cdots q_l$ , so by Euclid's lemma (for several factors) $p_1 \mid q_j$ for some $j$ . Since $q_j$ is prime and $p_1 > 1$ , $p_1 = q_j$ . Reorder the $q$ 's so that $j = 1$ and cancel: $p_2 \cdots p_k = q_2 \cdots q_l$ . If this number is $1$ , both sides are empty products ( $k = l = 1$ ). Otherwise it is smaller than $n$ and bigger than $1$ , and by the induction hypothesis the remaining primes agree apart from order. So the two factorisations agree apart from order.

∎

Collecting equal primes gives the familiar form $n = p_1^{e_1} p_2^{e_2} \cdots p_r^{e_r}$ with distinct primes $p_i$ and exponents $e_i \ge 1$ . Uniqueness lets us read off divisors: the divisors of $n$ are exactly the numbers $p_1^{f_1} \cdots p_r^{f_r}$ with $0 \le f_i \le e_i$ . Consequently, for $a = \prod p_i^{e_i}$ and $b = \prod p_i^{f_i}$ (allowing exponents $0$ ),

\gcd(a, b) = \prod p_i^{\min(e_i, f_i)}, \qquad \operatorname{lcm}(a, b) = \prod p_i^{\max(e_i, f_i)},

and since $\min(e, f) + \max(e, f) = e + f$ , we get $\gcd(a, b) \cdot \operatorname{lcm}(a, b) = ab$ for positive $a, b$ . For $12 = 2^2 \cdot 3$ and $18 = 2 \cdot 3^2$ : $\gcd = 2 \cdot 3 = 6$ and $\operatorname{lcm} = 2^2 \cdot 3^2 = 36$ .

A second consequence answers a question from primary school: why do $\tfrac{7}{40} = 0.175$ and $\tfrac{3}{8} = 0.375$ stop, while $\tfrac{1}{3} = 0.333\ldots$ and $\tfrac{1}{12} = 0.08333\ldots$ go on for ever?

Theorem— Theorem 8 (terminating decimals)

Let $a/b$ be a fraction in lowest terms, with $b > 0$ . Its decimal expansion terminates if and only if $b$ has no prime factors other than $2$ and $5$ , that is, $b = 2^s 5^t$ for some $s, t \ge 0$ .

Proof

A decimal with $k$ digits after the point is a fraction $m/10^k$ with $m$ an integer. So $a/b$ terminates exactly when $a \cdot 10^k / b$ is an integer for some $k$ , that is, when $b \mid a \cdot 10^k$ for some $k \ge 0$ .

If $b = 2^s 5^t$ : let $k = \max(s, t)$ . Then $10^k = 2^k 5^k = b \cdot 2^{k-s} 5^{k-t}$ , so $b \mid 10^k$ , and $a/b = a\,2^{k-s}5^{k-t}/10^k$ terminates after at most $k$ digits.

Conversely, suppose $b \mid a \cdot 10^k$ and let $p$ be a prime factor of $b$ . Then $p \mid a \cdot 10^k$ . Since the fraction is in lowest terms, $p \nmid a$ (otherwise $p$ would divide $\gcd(a, b) = 1$ ). By Euclid's lemma (for several factors) $p$ divides one of the factors of $10^k = 10 \cdot 10 \cdots 10$ , so $p \mid 10 = 2 \cdot 5$ , and by Euclid's lemma once more $p \mid 2$ or $p \mid 5$ , so $p = 2$ or $p = 5$ . By unique factorisation, $b = 2^s 5^t$ .

∎

For example $\tfrac{7}{40}$ terminates because $40 = 2^3 \cdot 5$ (indeed $\tfrac{7}{40} = \tfrac{175}{1000}$ ); $\tfrac{1}{12}$ does not, because $12 = 2^2 \cdot 3$ ; and "lowest terms" matters: $\tfrac{3}{12} = \tfrac14 = 0.25$ terminates, although the denominator $12$ as written has the prime factor $3$ . (The lesson on fractions and decimals uses this rule.)

ExplanationH

Why uniqueness needs a proof

Imagine the only numbers you knew were the Hilbert numbers $1, 5, 9, 13, 17, 21, \dots$ — the numbers of the form $4k + 1$ . The product of two of them is again one of them, since $(4k + 1)(4l + 1) = 4(4kl + k + l) + 1$ . Call a Hilbert number bigger than $1$ irreducible if it is not a product of two smaller Hilbert numbers bigger than $1$ . Then $9$ , $21$ and $49$ are irreducible ( $9 = 3 \cdot 3$ , but $3$ is not a Hilbert number), and

441 = 9 \cdot 49 = 21 \cdot 21 .

Two different factorisations into irreducibles! Existence still holds (the same strong-induction proof works), but uniqueness fails. What breaks is Euclid's lemma: $9$ divides $21 \cdot 21$ but does not divide $21$ (in the Hilbert numbers). There is no Bézout identity to rescue it, because the Hilbert numbers are not closed under subtraction.

So the proof of unique factorisation in $\Z$ really depends on Euclid's algorithm, through Bézout and Euclid's lemma. The same phenomenon appears in more serious number systems — see the algebraist's viewpoint below — and it shaped the history of number theory.

Formal mathematicsF

Euclid, Bézout and unique factorisation in Lean

Divisibility and division. Lemma 1(b), division with remainder from the library, and the uniqueness half proved here (nlinarith handles the inequalities).

dvd_linear_combinationLean 4Proved here from basic factsFormally verified

/-- If `d ∣ a` and `d ∣ b`, then `d` divides every integer combination `a·x + b·y`:
from `a = d·k` and `b = d·l` we get `a·x + b·y = d·(k·x + l·y)`. -/
theorem dvd_linear_combination {d a b : ℤ} (ha : d ∣ a) (hb : d ∣ b) (x y : ℤ) :
    d ∣ a * x + b * y := by
  obtain ⟨k, rfl⟩ := ha
  obtain ⟨l, rfl⟩ := hb
  exact ⟨k * x + l * y, by ring⟩

Axioms used: propextformal/Lumenary/DivisibilityGcd.leanTry it in the Lean web editor

division_algorithmLean 4Applies a library theoremFormally verified

/-- **Division with remainder** (existence): for `b > 0`, every integer `a` is `b·q + r` with
`0 ≤ r < b`. This assembles core Lean's `Int.mul_ediv_add_emod`, `Int.emod_nonneg` and
`Int.emod_lt_of_pos`, with `q = a / b` and `r = a % b`. -/
theorem division_algorithm (a b : ℤ) (hb : 0 < b) :
    ∃ q r : ℤ, a = b * q + r ∧ 0 ≤ r ∧ r < b :=
  ⟨a / b, a % b, (Int.mul_ediv_add_emod a b).symm, Int.emod_nonneg a hb.ne', Int.emod_lt_of_pos a hb⟩

Axioms used: propextformal/Lumenary/DivisibilityGcd.leanTry it in the Lean web editor

division_uniqueLean 4Proved here from basic factsFormally verified

/-- **Division with remainder** (uniqueness): if `b·q + r = b·q' + r'` with both remainders in
`[0, b)`, then `q = q'` and `r = r'`. Indeed `b·(q − q') = r' − r` lies strictly between `−b` and
`b`, and the only multiple of `b` there is `0`. -/
theorem division_unique {b q r q' r' : ℤ} (hb : 0 < b)
    (h : b * q + r = b * q' + r') (hr : 0 ≤ r) (hrb : r < b) (hr' : 0 ≤ r') (hrb' : r' < b) :
    q = q' ∧ r = r' := by
  have hq : q = q' := by
    by_contra hne
    rcases lt_or_gt_of_ne hne with hlt | hgt
    · have : b * q + b ≤ b * q' := by nlinarith
      linarith
    · have : b * q' + b ≤ b * q := by nlinarith
      linarith
  subst hq
  exact ⟨rfl, by linarith⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/DivisibilityGcd.leanTry it in the Lean web editor

Our own Euclid. Lemma 3, then the algorithm as a recursive function. Lean only accepts the definition because it can check that the recursion terminates: the second argument decreases, $a \bmod (b + 1) < b + 1$ . The correctness proof follows the recursion, using Lemma 3 at each step.

common_divisors_modLean 4Proved here from basic factsFormally verified

/-- **The key step of Euclid's algorithm**: `a, b` and `b, a mod b` have exactly the same common
divisors, because `a = b·(a / b) + (a mod b)`. -/
theorem common_divisors_mod (a b d : ℕ) : (d ∣ a ∧ d ∣ b) ↔ (d ∣ b ∧ d ∣ a % b) := by
  have e : b * (a / b) + a % b = a := Nat.div_add_mod a b
  constructor
  · rintro ⟨ha, hb⟩
    refine ⟨hb, ?_⟩
    rw [← e] at ha
    exact (Nat.dvd_add_right (Dvd.dvd.mul_right hb _)).mp ha
  · rintro ⟨hb, hr⟩
    refine ⟨?_, hb⟩
    rw [← e]
    exact Nat.dvd_add (Dvd.dvd.mul_right hb _) hr

Axioms used: propextformal/Lumenary/DivisibilityGcd.leanTry it in the Lean web editor

euclidLean 4Formally verified

/-- **Euclid's algorithm**: `euclid a 0 = a`, and otherwise `euclid a b = euclid b (a mod b)`.
It terminates because the second argument strictly decreases (`a mod b < b`), and a decreasing
sequence of natural numbers cannot go on for ever. Lean checks this (`termination_by`). -/
def euclid : ℕ → ℕ → ℕ
  | a, 0 => a
  | a, b + 1 => euclid (b + 1) (a % (b + 1))
termination_by _ b => b
decreasing_by exact Nat.mod_lt _ (Nat.succ_pos _)

Axioms used: No axiomsformal/Lumenary/DivisibilityGcd.leanTry it in the Lean web editor

euclid_specLean 4Proved here from basic factsFormally verified

/-- **Euclid's algorithm computes a greatest common divisor**: its output divides both inputs,
and every common divisor of the inputs divides the output. Proof by induction following the
recursion: when `b = 0` the output is `a`; otherwise apply `common_divisors_mod`. -/
theorem euclid_spec (a b : ℕ) :
    (euclid a b ∣ a ∧ euclid a b ∣ b) ∧ ∀ d, d ∣ a → d ∣ b → d ∣ euclid a b := by
  induction a, b using euclid.induct with
  | case1 a =>
    rw [euclid]
    exact ⟨⟨dvd_refl a, dvd_zero a⟩, fun d ha _ => ha⟩
  | case2 a b ih =>
    rw [euclid]
    obtain ⟨⟨h1, h2⟩, h3⟩ := ih
    refine ⟨(common_divisors_mod a (b + 1) _).mpr ⟨h1, h2⟩, fun d ha hdb => ?_⟩
    exact h3 d hdb ((common_divisors_mod a (b + 1) d).mp ⟨ha, hdb⟩).2

Axioms used: propext, Quot.soundformal/Lumenary/DivisibilityGcd.leanTry it in the Lean web editor

euclid_eq_gcdLean 4Proved here from basic factsFormally verified

/-- Our `euclid` agrees with Lean's `Nat.gcd`: two numbers that divide each other are equal. -/
theorem euclid_eq_gcd (a b : ℕ) : euclid a b = Nat.gcd a b := by
  obtain ⟨⟨h1, h2⟩, h3⟩ := euclid_spec a b
  exact Nat.dvd_antisymm (Nat.dvd_gcd h1 h2) (h3 _ (Nat.gcd_dvd_left a b) (Nat.gcd_dvd_right a b))

Axioms used: propext, Quot.soundformal/Lumenary/DivisibilityGcd.leanTry it in the Lean web editor

gcd_1071_462Lean 4Proved here from basic factsFormally verified

/-- The lesson's worked example: `gcd(1071, 462) = 21` (`1071 = 2·462 + 147`, `462 = 3·147 + 21`,
`147 = 7·21`), computed by Lean's kernel. -/
theorem gcd_1071_462 : euclid 1071 462 = 21 := by
  rw [euclid_eq_gcd]
  rfl

Axioms used: propext, Quot.soundformal/Lumenary/DivisibilityGcd.leanTry it in the Lean web editor

Bézout. The extended algorithm keeps track of the coefficients, and the proof is the back-substitution of the text, checked by linear_combination. Mathlib has its own extended algorithm, Nat.gcdA and Nat.gcdB.

xgcdLean 4Formally verified

/-- The **extended Euclidean algorithm**: integers `(x, y)` with `a·x + b·y = gcd(a, b)`.
If `b = 0` take `(1, 0)`. Otherwise, from `b·x' + (a mod b)·y' = g` and
`a mod b = a − b·(a / b)` we get `a·y' + b·(x' − (a / b)·y') = g`. -/
def xgcd : ℕ → ℕ → ℤ × ℤ
  | _, 0 => (1, 0)
  | a, b + 1 =>
    let p := xgcd (b + 1) (a % (b + 1))
    (p.2, p.1 - ((a / (b + 1) : ℕ) : ℤ) * p.2)
termination_by _ b => b
decreasing_by exact Nat.mod_lt _ (Nat.succ_pos _)

Axioms used: No axiomsformal/Lumenary/DivisibilityGcd.leanTry it in the Lean web editor

bezoutLean 4Proved here from basic factsFormally verified

/-- **Bézout's identity**, with the coefficients produced by `xgcd`:
`a·x + b·y = gcd(a, b)`. Proof by induction following the recursion, using the back-substitution
described in `xgcd`. -/
theorem bezout (a b : ℕ) :
    (a : ℤ) * (xgcd a b).1 + (b : ℤ) * (xgcd a b).2 = (Nat.gcd a b : ℤ) := by
  rw [← euclid_eq_gcd]
  induction a, b using xgcd.induct with
  | case1 a =>
    rw [xgcd, euclid]
    simp
  | case2 a b ih =>
    rw [xgcd, euclid]
    have hcast : ((a % (b + 1) : ℕ) : ℤ) + ((b + 1 : ℕ) : ℤ) * ((a / (b + 1) : ℕ) : ℤ) = (a : ℤ) := by
      exact_mod_cast Nat.mod_add_div a (b + 1)
    simp only
    linear_combination ih - (xgcd (b + 1) (a % (b + 1))).2 * hcast

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/DivisibilityGcd.leanTry it in the Lean web editor

bezout_libraryLean 4Applies a library theoremFormally verified

/-- Bézout's identity in Mathlib: `Nat.gcd_eq_gcd_ab`, with Mathlib's extended Euclidean algorithm
`Nat.gcdA`, `Nat.gcdB`. -/
theorem bezout_library (a b : ℕ) :
    (Nat.gcd a b : ℤ) = a * Nat.gcdA a b + b * Nat.gcdB a b :=
  Nat.gcd_eq_gcd_ab a b

Axioms used: propext, Quot.soundformal/Lumenary/DivisibilityGcd.leanTry it in the Lean web editor

euclid_lemmaLean 4Proved here from basic factsFormally verified

/-- **Euclid's lemma**: if a prime `p` divides `a·b`, then `p ∣ a` or `p ∣ b`.
If `p ∤ a` then `gcd(p, a) = 1` (the only positive divisors of `p` are `1` and `p`), so by Bézout
`p·x + a·y = 1`. Multiplying by `b`: `b = p·(b·x) + (a·b)·y`, and `p` divides both terms. -/
theorem euclid_lemma {p a b : ℕ} (hp : p.Prime) (h : p ∣ a * b) : p ∣ a ∨ p ∣ b := by
  by_cases hpa : p ∣ a
  · exact Or.inl hpa
  · right
    have hcop : Nat.gcd p a = 1 := (Nat.Prime.coprime_iff_not_dvd hp).mpr hpa
    have hbez := bezout p a
    rw [hcop, Nat.cast_one] at hbez
    have hZ : (p : ℤ) ∣ (a : ℤ) * (b : ℤ) := by exact_mod_cast h
    have key : (b : ℤ) = (p : ℤ) * ((b : ℤ) * (xgcd p a).1) + ((a : ℤ) * (b : ℤ)) * (xgcd p a).2 := by
      linear_combination (-(b : ℤ)) * hbez
    have : (p : ℤ) ∣ (b : ℤ) := by
      rw [key]
      exact dvd_add (dvd_mul_right _ _) (Dvd.dvd.mul_right hZ _)
    exact_mod_cast this

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/DivisibilityGcd.leanTry it in the Lean web editor

euclid_lemma_libraryLean 4Applies a library theoremFormally verified

/-- Euclid's lemma in Mathlib: `Nat.Prime.dvd_mul`. -/
theorem euclid_lemma_library {p a b : ℕ} (hp : p.Prime) : p ∣ a * b ↔ p ∣ a ∨ p ∣ b :=
  hp.dvd_mul

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/DivisibilityGcd.leanTry it in the Lean web editor

four_counterexampleLean 4Proved here from basic factsFormally verified

/-- **Primality matters in Euclid's lemma**: `4 ∣ 2·2`, but `4 ∤ 2`. -/
theorem four_counterexample : 4 ∣ 2 * 2 ∧ ¬ 4 ∣ 2 := by decide

Axioms used: propextformal/Lumenary/DivisibilityGcd.leanTry it in the Lean web editor

The fundamental theorem. Factorisations are lists of primes; "unique apart from order" means the two lists are permutations of each other (List.Perm, written ~).

exists_prime_factorizationLean 4Proved here from basic factsFormally verified

/-- **Existence of prime factorisations**, by strong induction: every `n ≥ 1` is the product of a
list of primes (`1` is the empty product). For `n > 1`, let `p` be its smallest factor bigger
than `1` — a prime — and factorise the smaller number `n / p`. -/
theorem exists_prime_factorization (n : ℕ) (hn : n ≠ 0) :
    ∃ l : List ℕ, (∀ p ∈ l, p.Prime) ∧ l.prod = n := by
  induction n using Nat.strong_induction_on with
  | _ n ih =>
    by_cases h1 : n = 1
    · exact ⟨[], by simp, by simp [h1]⟩
    · have hp : (Nat.minFac n).Prime := Nat.minFac_prime h1
      have hdiv : Nat.minFac n * (n / Nat.minFac n) = n := Nat.mul_div_cancel' (Nat.minFac_dvd n)
      have hlt : n / Nat.minFac n < n := Nat.div_lt_self (Nat.pos_of_ne_zero hn) hp.one_lt
      have hne : n / Nat.minFac n ≠ 0 := by
        intro h0
        rw [h0, Nat.mul_zero] at hdiv
        exact hn hdiv.symm
      obtain ⟨l, hl, hprod⟩ := ih (n / Nat.minFac n) hlt hne
      refine ⟨Nat.minFac n :: l, ?_, ?_⟩
      · intro q hq
        rcases List.mem_cons.mp hq with rfl | hq
        · exact hp
        · exact hl q hq
      · rw [List.prod_cons, hprod, hdiv]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/DivisibilityGcd.leanTry it in the Lean web editor

prime_dvd_prodLean 4Proved here from basic factsFormally verified

/-- Euclid's lemma for several factors: if a prime divides a product of a list of numbers, it
divides one of them. Induction on the list, using `euclid_lemma` at each step. -/
theorem prime_dvd_prod {p : ℕ} (hp : p.Prime) :
    ∀ l : List ℕ, p ∣ l.prod → ∃ q ∈ l, p ∣ q
  | [], h => absurd (Nat.dvd_one.mp h) hp.one_lt.ne'
  | q :: t, h => by
    rw [List.prod_cons] at h
    rcases euclid_lemma hp h with hq | ht
    · exact ⟨q, List.mem_cons_self, hq⟩
    · obtain ⟨r, hr, hpr⟩ := prime_dvd_prod hp t ht
      exact ⟨r, List.mem_cons_of_mem q hr, hpr⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/DivisibilityGcd.leanTry it in the Lean web editor

factorization_uniqueLean 4Proved here from basic factsFormally verified

/-- **Uniqueness of prime factorisations**: two lists of primes with the same product are
rearrangements of each other (`List.Perm`, written `~`). Induction on the first list: its head `p`
divides the product of the second, so (Euclid's lemma) it divides — hence equals — one of its
primes `q`; remove `p` from both sides and cancel. -/
theorem factorization_unique :
    ∀ l₁ l₂ : List ℕ, (∀ p ∈ l₁, p.Prime) → (∀ p ∈ l₂, p.Prime) → l₁.prod = l₂.prod → l₁.Perm l₂
  | [], l₂, _, h₂, h => by
    cases l₂ with
    | nil => exact List.Perm.refl []
    | cons q t =>
      exfalso
      have hq : q ∣ (q :: t).prod := by rw [List.prod_cons]; exact dvd_mul_right q _
      rw [← h, List.prod_nil] at hq
      exact (h₂ q List.mem_cons_self).one_lt.ne' (Nat.dvd_one.mp hq)
  | p :: t, l₂, h₁, h₂, h => by
    have hp : p.Prime := h₁ p List.mem_cons_self
    have hdvd : p ∣ l₂.prod := by rw [← h, List.prod_cons]; exact dvd_mul_right p _
    obtain ⟨q, hq, hpq⟩ := prime_dvd_prod hp l₂ hdvd
    have hpq' : p = q := (Nat.prime_dvd_prime_iff_eq hp (h₂ q hq)).mp hpq
    subst hpq'
    have hperm : l₂.Perm (p :: l₂.erase p) := List.perm_cons_erase hq
    have hprod : t.prod = (l₂.erase p).prod := by
      have e : p * t.prod = p * (l₂.erase p).prod := by
        rw [← List.prod_cons, h, hperm.prod_eq, List.prod_cons]
      exact Nat.eq_of_mul_eq_mul_left hp.pos e
    have ht : t.Perm (l₂.erase p) :=
      factorization_unique t (l₂.erase p) (fun r hr => h₁ r (List.mem_cons_of_mem p hr))
        (fun r hr => h₂ r (List.mem_of_mem_erase hr)) hprod
    exact (ht.cons p).trans hperm.symm

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/DivisibilityGcd.leanTry it in the Lean web editor

factorization_unique_libraryLean 4Applies a library theoremFormally verified

/-- Unique factorisation in Mathlib: `Nat.primeFactorsList_unique` — any list of primes with
product `n` is a rearrangement of Mathlib's list `n.primeFactorsList`. -/
theorem factorization_unique_library {n : ℕ} {l : List ℕ} (h₁ : l.prod = n)
    (h₂ : ∀ p ∈ l, p.Prime) : l.Perm n.primeFactorsList :=
  Nat.primeFactorsList_unique h₁ h₂

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/DivisibilityGcd.leanTry it in the Lean web editor

Terminating decimals (Theorem 8). A fraction $a/b$ terminates when $b \mid a \cdot 10^k$ for some $k$ ; both directions of Theorem 8 are proved in that form.

prime_dvd_powLean 4Proved here from basic factsFormally verified

/-- If a prime divides a power `n ^ k`, it divides `n`: Euclid's lemma applied `k` times
(induction on `k`; for `k = 0`, no prime divides `1`). -/
theorem prime_dvd_pow {p n : ℕ} (hp : p.Prime) : ∀ k : ℕ, p ∣ n ^ k → p ∣ n
  | 0, h => absurd (Nat.dvd_one.mp (by simpa using h)) hp.one_lt.ne'
  | k + 1, h => by
    rw [pow_succ] at h
    rcases euclid_lemma hp h with h1 | h2
    · exact prime_dvd_pow hp k h1
    · exact h2

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/DivisibilityGcd.leanTry it in the Lean web editor

terminating_prime_factorsLean 4Proved here from basic factsFormally verified

/-- **Terminating decimals, one direction.** A fraction `a / b` has a terminating decimal exactly
when `a · 10ᵏ / b` is a whole number for some `k`, i.e. `b ∣ a · 10ᵏ`. If moreover `a / b` is in
lowest terms (`gcd(a, b) = 1`), then every prime factor `p` of `b` is `2` or `5`: `p` divides
`a · 10ᵏ` but not `a`, so (Euclid's lemma) it divides `10ᵏ`, hence `10 = 2 · 5`, hence `2` or `5`. -/
theorem terminating_prime_factors {a b k p : ℕ} (hcop : Nat.gcd a b = 1) (h : b ∣ a * 10 ^ k)
    (hp : p.Prime) (hpb : p ∣ b) : p = 2 ∨ p = 5 := by
  have hpa10 : p ∣ a * 10 ^ k := Nat.dvd_trans hpb h
  rcases euclid_lemma hp hpa10 with hpa | hp10
  · have : p ∣ Nat.gcd a b := Nat.dvd_gcd hpa hpb
    rw [hcop] at this
    exact absurd (Nat.dvd_one.mp this) hp.one_lt.ne'
  · have h10 : p ∣ 2 * 5 := prime_dvd_pow hp k hp10
    rcases euclid_lemma hp h10 with h2 | h5
    · exact Or.inl ((Nat.prime_dvd_prime_iff_eq hp Nat.prime_two).mp h2)
    · exact Or.inr ((Nat.prime_dvd_prime_iff_eq hp Nat.prime_five).mp h5)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/DivisibilityGcd.leanTry it in the Lean web editor

two_five_dvd_ten_powLean 4Proved here from basic factsFormally verified

/-- **Terminating decimals, the other direction.** If `b = 2ˢ · 5ᵗ`, then `b ∣ 10^(s + t)`, so
`a / b = a · c / 10^(s + t)` for a whole number `c`: the decimal terminates after `s + t` digits
(in fact after `max(s, t)`). Proof: `10^(s+t) = 2^(s+t) · 5^(s+t)`. -/
theorem two_five_dvd_ten_pow (s t : ℕ) : 2 ^ s * 5 ^ t ∣ 10 ^ (s + t) := by
  have e : (10 : ℕ) ^ (s + t) = 2 ^ (s + t) * 5 ^ (s + t) := by
    rw [← mul_pow]
    rfl
  rw [e]
  exact Nat.mul_dvd_mul (Nat.pow_dvd_pow 2 (Nat.le_add_right s t))
    (Nat.pow_dvd_pow 5 (Nat.le_add_left t s))

Axioms used: propextformal/Lumenary/DivisibilityGcd.leanTry it in the Lean web editor

Hilbert numbers. Irreducibility is defined with an unbounded "for all", proved equivalent to a finite check, and the finite check is run by Lean's kernel.

HilbertIrreducibleLean 4Formally verified

/-- In the **Hilbert numbers** `1, 5, 9, 13, …` (those leaving remainder `1` on division by `4`,
which are closed under multiplication), `n > 1` is *irreducible* if it is not a product of two
smaller Hilbert numbers bigger than `1`. -/
def HilbertIrreducible (n : ℕ) : Prop :=
  n % 4 = 1 ∧ 1 < n ∧ ∀ a b : ℕ, (a % 4 = 1 ∧ b % 4 = 1 ∧ a * b = n) → a = 1 ∨ b = 1

Axioms used: No axiomsformal/Lumenary/DivisibilityGcd.leanTry it in the Lean web editor

hilbertIrreducible_iffLean 4Proved here from basic factsFormally verified

/-- Irreducibility is a **finite check**: if `a · b = n` with `n > 0`, both factors are at most `n`,
so only `a, b ≤ n` need to be tried. -/
theorem hilbertIrreducible_iff (n : ℕ) :
    HilbertIrreducible n ↔ n % 4 = 1 ∧ 1 < n ∧
      ∀ a < n + 1, ∀ b < n + 1, (a % 4 = 1 ∧ b % 4 = 1 ∧ a * b = n) → a = 1 ∨ b = 1 := by
  constructor
  · rintro ⟨h4, h1, h⟩
    exact ⟨h4, h1, fun a _ b _ hab => h a b hab⟩
  · rintro ⟨h4, h1, h⟩
    refine ⟨h4, h1, fun a b hab => ?_⟩
    have hn : 0 < n := by omega
    have ha : a ≤ n := Nat.le_of_dvd hn ⟨b, hab.2.2.symm⟩
    have hb : b ≤ n := Nat.le_of_dvd hn ⟨a, by rw [Nat.mul_comm]; exact hab.2.2.symm⟩
    exact h a (by omega) b (by omega) hab

Axioms used: propext, Quot.soundformal/Lumenary/DivisibilityGcd.leanTry it in the Lean web editor

hilbert_non_uniqueLean 4Proved here from basic factsFormally verified

/-- **Unique factorisation needs proof**: among Hilbert numbers, `9`, `21` and `49` are irreducible,
yet `441 = 9 · 49 = 21 · 21` — two genuinely different factorisations into irreducibles. Checked
by the finite search of `hilbertIrreducible_iff` (`decide`). -/
theorem hilbert_non_unique :
    HilbertIrreducible 9 ∧ HilbertIrreducible 21 ∧ HilbertIrreducible 49 ∧
      9 * 49 = 441 ∧ 21 * 21 = 441 := by
  refine ⟨?_, ?_, ?_, rfl, rfl⟩ <;> rw [hilbertIrreducible_iff] <;> decide

Axioms used: propext, Quot.soundformal/Lumenary/DivisibilityGcd.leanTry it in the Lean web editor

What is formalised: every theorem of the lesson except Lamé's theorem and the gcd–lcm formula. Mathlib also has these facts in great generality — for instance unique factorisation in every unique factorisation domain (UniqueFactorizationMonoid), which includes every Euclidean domain.

ComputationC

Euclid by machine

Euclid's algorithm: steps, Bezout and Lame's boundPythonExact computationExhaustive finite checkComputationally tested

"""Euclid's algorithm: the steps, Bezout's coefficients, and how fast it is.

1. The extended Euclidean algorithm on (1071, 462): each division step
   a = q*b + r, and the integers x, y with 1071x + 462y = gcd(1071, 462).
2. Lame's theorem (1844): the number of division steps is at most five times
   the number of decimal digits of the smaller number. We find the slowest
   pair below each power of 10 by exhaustive search and compare: consecutive
   Fibonacci numbers are the worst cases.

Runs unchanged in the browser (Pyodide) using only the standard library.
"""

def euclid_steps(a, b):
    """The division steps (a, q, b, r) with a = q*b + r of Euclid's algorithm."""
    if a < 0 or b < 0:
        raise ValueError("a and b must be non-negative")
    steps = []
    while b:
        q, r = divmod(a, b)
        steps.append((a, q, b, r))
        a, b = b, r
    return steps

def extended_gcd(a, b):
    """Return (g, x, y) with a*x + b*y = g = gcd(a, b), by back-substitution
    through Euclid's algorithm (iterative version)."""
    x0, y0, x1, y1 = 1, 0, 0, 1
    while b:
        q, r = divmod(a, b)
        a, b = b, r
        x0, x1 = x1, x0 - q * x1
        y0, y1 = y1, y0 - q * y1
    return a, x0, y0

def fibonacci(k):
    """F_0 = 0, F_1 = 1, F_(k+1) = F_k + F_(k-1)."""
    a, b = 0, 1
    for _ in range(k):
        a, b = b, a + b
    return a

def slowest_pair(b_limit, a_limit):
    """Among 1 <= b < a < a_limit with b < b_limit, a pair with the most
    division steps (the first found), and that number of steps."""
    best, best_pair = -1, None
    for b in range(1, b_limit):
        for a in range(b + 1, a_limit):
            n = len(euclid_steps(a, b))
            if n > best:
                best, best_pair = n, (a, b)
    return best_pair, best

def main():
    print("1. Euclid's algorithm on 1071 and 462:")
    for a, q, b, r in euclid_steps(1071, 462):
        print(f"   {a:5d} = {q} * {b:4d} + {r}")
    g, x, y = extended_gcd(1071, 462)
    print(f"   gcd = {g} = 1071 * ({x}) + 462 * {y}"
          f"   [check: {1071 * x + 462 * y}]")
    print()
    print("2. Slowest pairs (exhaustive search) and Lame's bound:")
    print("   b <    a <    slowest pair (a, b)   steps   5 x digits of b")
    for b_limit, a_limit in [(10, 60), (100, 300), (1000, 1000)]:
        (a, b), n = slowest_pair(b_limit, a_limit)
        print(f"   {b_limit:4d}   {a_limit:4d}   {str((a, b)):19}   {n:5d}"
              f"   {5 * len(str(b)):15d}")
    fib = [fibonacci(k) for k in range(8, 18)]
    print("   Fibonacci numbers:", ", ".join(map(str, fib)))
    print("   steps for (F_(k+1), F_k), k = 2..16:", " ".join(
        str(len(euclid_steps(fibonacci(k + 1), fibonacci(k)))) for k in range(2, 17)))
    print()
    print("Epistemic status: exact integer arithmetic; part 2 is an exhaustive")
    print("search over the stated finite ranges. It agrees with Lame's theorem")
    print("but proves it only there; the general proof compares the remainders")
    print("with Fibonacci numbers.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

The slowest pairs are consecutive Fibonacci numbers, where every quotient is $1$ — exactly the squares-widget picture in which each cut removes a single square.

Hilbert numbers and the chance of being coprimePythonExact computationExhaustive finite checkNumerical approximationComputationally tested

"""When factorisation is not unique - and how often numbers are coprime.

1. The Hilbert numbers 1, 5, 9, 13, ... (those of the form 4k + 1) are closed
   under multiplication. Call one irreducible if it is bigger than 1 and not a
   product of two smaller Hilbert numbers bigger than 1. Every Hilbert number
   is a product of irreducibles, but not uniquely: 441 = 9 * 49 = 21 * 21.
   We list all factorisations into irreducibles up to 1500.
2. For contrast, we check that among ordinary integers 2..1500 every number has
   exactly one factorisation into primes (as the fundamental theorem says).
3. Two numbers picked "at random" are coprime with probability 6/pi^2. We
   count exactly the coprime pairs in {1, ..., N}^2 using Euler's totient
   function, for N up to 100 000.

Runs unchanged in the browser (Pyodide) using only the standard library.
"""

import math

def factorizations(n, atoms):
    """All factorisations of n as non-decreasing products of numbers in the
    sorted list ``atoms``, as tuples."""
    if n == 1:
        return [()]
    out = []

    def go(m, start, acc):
        if m == 1:
            out.append(tuple(acc))
            return
        for i in range(start, len(atoms)):
            a = atoms[i]
            if a > m:
                break
            if m % a == 0:
                go(m // a, i, acc + [a])
    go(n, 0, [])
    return out

def hilbert_irreducibles(limit):
    """Hilbert numbers 5 <= n <= limit that are not a product of two smaller
    Hilbert numbers greater than 1."""
    irr = []
    for n in range(5, limit + 1, 4):
        if not any(n % a == 0 and (n // a) % 4 == 1 for a in irr if a * a <= n):
            irr.append(n)
    return irr

def primes_up_to(limit):
    """Sieve of Eratosthenes."""
    sieve = bytearray([1]) * (limit + 1)
    sieve[0:2] = b"\x00\x00"
    for p in range(2, int(limit ** 0.5) + 1):
        if sieve[p]:
            sieve[p * p::p] = bytearray(len(range(p * p, limit + 1, p)))
    return [i for i in range(limit + 1) if sieve[i]]

def totients(limit):
    """phi(0..limit) by a sieve."""
    phi = list(range(limit + 1))
    for p in range(2, limit + 1):
        if phi[p] == p:                     # p is prime
            for k in range(p, limit + 1, p):
                phi[k] -= phi[k] // p
    return phi

def coprime_pairs(n, phi):
    """Number of ordered pairs (a, b) in {1..n}^2 with gcd(a, b) = 1:
    2 * (phi(1) + ... + phi(n)) - 1."""
    return 2 * sum(phi[1:n + 1]) - 1

def main():
    limit = 1500
    irr = hilbert_irreducibles(limit)
    print("1. Hilbert irreducibles start:", ", ".join(map(str, irr[:12])), "...")
    print("   Hilbert numbers <= 1500 with more than one factorisation:")
    for n in range(1, limit + 1, 4):
        fs = factorizations(n, irr)
        if len(fs) > 1:
            print(f"   {n:5d} = " + " = ".join(" * ".join(map(str, f)) for f in fs))
    primes = primes_up_to(limit)
    counts = [len(factorizations(n, primes)) for n in range(2, limit + 1)]
    print(f"2. Integers 2..{limit}: every one has exactly one prime factorisation:"
          f" {all(c == 1 for c in counts)}")
    phi = totients(100_000)
    print("3. Proportion of coprime pairs in {1..N}^2 (6/pi^2 = "
          f"{6 / math.pi ** 2:.6f}):")
    for n in (10, 100, 1000, 10_000, 100_000):
        print(f"   N = {n:6d}: {coprime_pairs(n, phi) / n ** 2:.6f}")
    print()
    print("Epistemic status: parts 1 and 2 are exhaustive searches up to 1500;")
    print("part 3 is an exact count turned into decimals. They illustrate the")
    print("theorems - unique factorisation in Z, its failure for Hilbert numbers,")
    print("and the limit 6/pi^2, a classical theorem - but a finite range proves")
    print("none of them.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Part 3 counts, among all pairs of whole numbers up to $N$ , the fraction that are coprime. It approaches $6/\pi^2 \approx 0.6079$ — a classical theorem, and a first meeting between number theory and $\pi$ . The computation is exact counting, but a finite range can only illustrate the limit.

Exercises

1. Divisibility, Euclid's algorithm and unique factorisation

Warm-upHuman

Use Euclid's algorithm to compute $\gcd(252, 198)$ .

2. Divisibility, Euclid's algorithm and unique factorisation

Warm-upHuman

Which pairs $(x, y)$ satisfy $5x + 3y = 1$ ? (Choose all that apply.)

Choose all that apply

3. Divisibility, Euclid's algorithm and unique factorisation

CoreHuman

For which of these numbers $d$ is it true that for all integers $a, b$ : if $d \mid ab$ then $d \mid a$ or $d \mid b$ ? (Choose all that apply.)

Choose all that apply

4. Divisibility, Euclid's algorithm and unique factorisation

CoreHuman

Compute $\operatorname{lcm}(84, 90)$ .

5. Divisibility, Euclid's algorithm and unique factorisation

CoreHuman

Which of these fractions have a terminating decimal expansion? (Choose all that apply.)

Choose all that apply

6. Divisibility, Euclid's algorithm and unique factorisation

CoreHuman

In the proof of Euclid's lemma we assume $p \mid ab$ and $p \nmid a$ , and then say $\gcd(p, a) = 1$ . Why?

Choose one

The positive divisors of

p

are only

1

and

p

, and

p

does not divide

a

, so the only positive common divisor is

1

.By Bézout's identity.Because

a < p

.Any two different numbers are coprime.

7. Divisibility, Euclid's algorithm and unique factorisation

CoreHuman

With a $6$ -litre jug, a $15$ -litre jug and a tap, what is the smallest positive amount of water you can measure exactly (by filling, emptying and pouring between the jugs)?

8. Divisibility, Euclid's algorithm and unique factorisation

StretchHuman

In the Hilbert numbers $1, 5, 9, 13, 17, 21, \dots$ (numbers of the form $4k + 1$ ), which statement is true?

Choose one

441 = 9 \cdot 49 = 21 \cdot 21

are two different factorisations into irreducibles, so unique factorisation fails.

9

is not irreducible, because

9 = 3 \cdot 3

.Euclid's lemma still holds: if an irreducible divides a product, it divides a factor.Some Hilbert numbers have no factorisation into irreducibles at all.

9. Divisibility, Euclid's algorithm and unique factorisation

CoreFormal

Which Lean statement correctly formalises Euclid's lemma for natural numbers?

Choose one

∀ p a b : ℕ, p.Prime → p ∣ a * b → p ∣ a ∨ p ∣ b∀ p a b : ℕ, p ∣ a * b → p ∣ a ∨ p ∣ b∀ p a b : ℕ, p.Prime → p ∣ a ∨ p ∣ b → p ∣ a * b∀ p a b : ℕ, p.Prime → p ∣ a * b → p ∣ a ∧ p ∣ b

10. Divisibility, Euclid's algorithm and unique factorisation

StretchComputational

Write extended_gcd(a, b) for natural numbers a, b (not both zero), returning a triple (g, x, y) with g == gcd(a, b) and a * x + b * y == g. Use the recursion: if b == 0 return (a, 1, 0); otherwise get (g, x, y) for (b, a % b) and back-substitute using a % b == a - (a // b) * b.

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

"Unique factorisation is obvious." It feels obvious because we have used it for years, but it is a theorem whose proof needs Euclid's lemma, and so Bézout's identity and Euclid's algorithm. In the Hilbert numbers $1, 5, 9, 13, \dots$ it fails: $441 = 9 \cdot 49 = 21 \cdot 21$ .

Misconception

"If $d \mid ab$ , then $d \mid a$ or $d \mid b$ ." True when $d$ is prime (Euclid's lemma), false in general: $4 \mid 2 \cdot 2$ but $4 \nmid 2$ ; $6 \mid 4 \cdot 9$ but $6$ divides neither.

Misconception

Confusing gcd and lcm. The greatest common divisor is the biggest number that goes into both ( $\gcd(12, 18) = 6$ ); the least common multiple is the smallest number that both go into ( $\operatorname{lcm}(12, 18) = 36$ ). A quick check: the gcd is never bigger than the smaller number, and the lcm never smaller than the larger.

Misconception

"Coprime means at least one of the numbers is prime." $8$ and $15$ are coprime, and neither is prime. Coprime means the two numbers share no prime factor.

Misconception

"To find a gcd you must factorise first." Euclid's algorithm needs no factorisation at all — which matters, because factorising large numbers is believed to be very hard, while Euclid's algorithm is fast even for numbers with hundreds of digits.

ViewpointsH

Many ways of seeing

Algebra— ideals and unique factorisation domains

The set of all combinations $\{ax + by : x, y \in \Z\}$ , written $a\Z + b\Z$ , is closed under addition, subtraction and multiplication by integers — an ideal of $\Z$ . Bézout's theorem says it equals $d\Z$ with $d = \gcd(a, b)$ : every ideal of $\Z$ consists of the multiples of one number ( $\Z$ is a principal ideal domain). The same proof works wherever there is division with a remainder that gets smaller — in a Euclidean domain, such as polynomials over $\Q$ or the Gaussian integers $\Z[i] = \{m + ni : m, n \in \Z\}$ — so these too have unique factorisation. But in $\Z[\sqrt{-5}] = \{m + n\sqrt{-5}\}$ ,

6 = 2 \cdot 3 = (1 + \sqrt{-5})(1 - \sqrt{-5}),

with all four factors irreducible: unique factorisation fails. Ernst Kummer's "ideal numbers" and Richard Dedekind's ideals were invented in the 19th century to repair this; see rings, ideals and fields.

Geometry— lattice points and cutting squares

Draw the integer grid. The line $ax + by = c$ passes through a grid point exactly when $\gcd(a, b) \mid c$ — Bézout in geometric form. The segment from $(0, 0)$ to $(a, b)$ , with $a, b > 0$ , passes through exactly $\gcd(a, b) + 1$ grid points (counting both ends), because the points on it are $\big(ka/d, kb/d\big)$ for $k = 0, 1, \dots, d$ with $d = \gcd(a, b)$ . And Euclid's algorithm is literally geometric: the Greeks thought of it as repeatedly subtracting the smaller length from the larger (anthyphairesis), the squares-cutting picture of the explorer. Applied to a diagonal and side of a square, the process never ends — one route to the irrationality of $\sqrt{2}$ .

Probability— the chance of being coprime

Pick two whole numbers "at random". The chance that both are even is about $\frac14$ , that both are multiples of $3$ about $\frac19$ , and so on for each prime. If these events behaved independently, the chance of sharing no prime factor would be $\prod_p \big(1 - \frac{1}{p^2}\big)$ , and Euler showed this product equals $1/\zeta(2) = 6/\pi^2$ , where $\zeta(2) = 1 + \frac14 + \frac19 + \dots = \pi^2/6$ . The heuristic can be made rigorous (the limit statement is a classical theorem), and the computation section shows the proportions creeping towards $0.6079\ldots$

Computation— an algorithm for the ages

Euclid's algorithm is among the oldest algorithms still in everyday use. By Lamé's theorem it needs a number of steps proportional to the number of digits, so it handles numbers with hundreds of digits instantly. The extended version computes inverses in clock arithmetic: if $\gcd(a, n) = 1$ then $ax + ny = 1$ gives $ax \equiv 1 \pmod n$ . That is how the RSA cryptosystem, which protects much of the world's online communication, computes its secret key. See algorithms and efficiency and congruences.

Wonder Trails

Remainders lead to the arithmetic of clocks — where Bézout's identity decides which numbers can be "divided by".

Wonder Trail · Optional · never gradedRemainder familiesSort every integer — positive, negative and zero — into families by its remainder after dividing by 3. If you add a member of one family to a member of another, does the family of the answer depend on which members you chose?Follow the trail Wonder Trail · Optional · never gradedClock arithmeticIt's 9 o'clock. What time will it be in 5 hours — and in 29 hours? Can a clock teach us a whole new kind of arithmetic?Follow the trail

History & global context

History and global context

Euclid's Elements (around 300 BCE), Book VII, opens with the algorithm (Propositions 1–2), phrased as repeatedly subtracting the smaller number from the larger, and proves Euclid's lemma as Proposition 30. Book IX, Proposition 14, comes close to the uniqueness of factorisation.
China. The Nine Chapters on the Mathematical Art (compiled by about the 1st century CE) reduces fractions using the "mutual subtraction" method (gēng xiāng jiǎn sǔn), which is Euclid's algorithm by repeated subtraction.
India. Āryabhaṭa (499 CE) gave the kuṭṭaka ("pulveriser") method for solving $ax + by = c$ in integers, essentially the extended Euclidean algorithm; Brahmagupta (628 CE) and later Indian mathematicians developed it further, including applications to astronomy and calendars.
Bézout's identity for integers appears in the work of Claude-Gaspard Bachet de Méziriac (1624); Étienne Bézout (1779) proved the analogous result for polynomials, and his name stuck.
Unique factorisation. Kamāl al-Dīn al-Fārisī (Persia, around 1300) proved the existence of prime factorisations and took steps towards uniqueness. The first clear statement and proof of uniqueness is in Carl Friedrich Gauss's Disquisitiones Arithmeticae (1801).
Algorithms and ideals. Gabriel Lamé's 1844 bound on Euclid's algorithm is often called the first analysis of the running time of an algorithm. In the 1840s Ernst Kummer discovered that unique factorisation fails in some number systems arising from Fermat's Last Theorem, and invented "ideal numbers" to restore it.

Tiles, jugs and a suspicious certainty

Divisors, remainders and the gcd

Euclid's algorithm

Explore: Euclid's algorithm as cutting squares

Bézout's identity and Euclid's lemma

The fundamental theorem of arithmetic

Why uniqueness needs a proof

Euclid, Bézout and unique factorisation in Lean

Euclid by machine

Exercises

Common misconceptions

Many ways of seeing

Wonder Trails

History and global context

Further reading