Definition D1
d | a means there exists a natural number k with a = dk.
Proof.
Take a and b to be natural numbers at least 1, and regard 1 as the product with all exponents 0.convention
∎
Definition D2
gcd(a, b) is the greatest of the common divisors; lcm(a, b) is the least of the common multiples.
Proof.
That a greatest common divisor and a least common multiple actually exist is shown in L3 and L4.convention
∎
Definition D3
min(x, y) is whichever of the two is not larger; max(x, y) is whichever is not smaller.
Proof.
(1)A3 guarantees the two can be compared, so both values are always determined.A3
(2)min ≤ x, min ≤ y, x ≤ max, y ≤ max follow immediately from the definition.(1)
(3)If z ≤ x and z ≤ y then z ≤ min; if x ≤ w and y ≤ w then max ≤ w(1)
∎
Lemma L1
With a = ∏ p^xₚ and d = ∏ p^zₚ, d | a holds if and only if zₚ ≤ xₚ for every p.
Proof.
(1)A1 fixes the prime factorization of each number uniquely.A1
(2)Suppose zₚ ≤ xₚ for every p.assumption
(3)There is wₚ with zₚ + wₚ = xₚ.(2), A5
(4)Setting k = ∏ p^wₚ gives dk = ∏ p^(zₚ+wₚ) = a(1), (3), A2, A7, A8, E
(5)Therefore d | a(4), D1
(6)Now suppose d | a.assumption
(7)There is k with a = dk, and it can be written k = ∏ p^wₚ.(6), D1, A1
(8)dk = ∏ p^(zₚ+wₚ)(7), A2, A7, A8
(9)The prime factorization is unique, so xₚ = zₚ + wₚ(8), A1
(10)Therefore zₚ ≤ xₚ(9), A5
∎
Lemma L2
For all x, y, min(x, y) + max(x, y) = x + y
Proof.
(1)x ≤ y or y ≤ x.A3
(2)If x ≤ y, then min = x and max = y, so the sum is x + y.(1), D3
(3)If y ≤ x, then min = y and max = x, so the sum is y + x.(1), D3
(4)y + x = x + yA4
(5)In both cases the sum is x + y.(2), (3), (4)
∎
Lemma L3
gcd(a, b) = ∏ p^min(xₚ, yₚ)
Proof.
(1)Set g = ∏ p^min(xₚ, yₚ).convention
(2)min ≤ xₚ and min ≤ yₚ, so g | a and g | bD3, L1
(3)Let d = ∏ p^zₚ be a common divisor.assumption, A1
(4)For every p, zₚ ≤ xₚ and zₚ ≤ yₚ(3), L1
(5)zₚ ≤ min(xₚ, yₚ)(4), D3
(6)Therefore d | g(5), L1
(7)g ≥ 1, so d ≤ g(6), A6
(8)g is a common divisor and is not smaller than any common divisor.(2), (7)
(9)Therefore gcd(a, b) = g(8), D2
∎
Lemma L4
lcm(a, b) = ∏ p^max(xₚ, yₚ)
Proof.
(1)Set ℓ = ∏ p^max(xₚ, yₚ).convention
(2)xₚ ≤ max and yₚ ≤ max, so a | ℓ and b | ℓD3, L1
(3)Let m = ∏ p^wₚ be a common multiple.assumption, A1
(4)For every p, xₚ ≤ wₚ and yₚ ≤ wₚ(3), L1
(5)max(xₚ, yₚ) ≤ wₚ(4), D3
(6)Therefore ℓ | m(5), L1
(7)m ≥ 1, so ℓ ≤ m(6), A6
(8)ℓ is a common multiple and is not larger than any common multiple.(2), (7)
(9)Therefore lcm(a, b) = ℓ(8), D2
∎
Theorem T
gcd(a, b) × lcm(a, b) = ab
Proof.
(1)gcd(a,b) × lcm(a,b) = (∏ p^min)(∏ p^max)L3, L4, E
(2) = ∏ p^(min + max)A2, A7, A8
(3) = ∏ p^(xₚ + yₚ)(2), L2
(4) = (∏ p^xₚ)(∏ p^yₚ)A2, A7, A8
(5) = ab(4), A1
∎