Pythagorean Triples

The main result is the classification of Pythagorean triples. The final result is for general Pythagorean triples. It follows from the more interesting relatively prime case. We use the "rational parametrization of the circle" method for the proof. The parametrization maps the point (x / z, y / z) to the slope of the line through (-1 , 0) and (x / z, y / z). This quickly shows that (x / z, y / z) = (2 * m * n / (m ^ 2 + n ^ 2), (m ^ 2 - n ^ 2) / (m ^ 2 + n ^ 2)) where m / n is the slope. In order to identify numerators and denominators we now need results showing that these are coprime. This is easy except for the prime 2. In order to deal with that we have to analyze the parity of x, y, m and n and eliminate all the impossible cases. This takes up the bulk of the proof below.

theorem sq_ne_two_fin_zmod_four (z : ZMod 4) : z * z ≠ 2

theorem Int.sq_ne_two_mod_four (z : ℤ) : z * z % 4 ≠ 2

def PythagoreanTriple (x : ℤ) (y : ℤ) (z : ℤ) : Prop

Three integers x, y, and z form a Pythagorean triple if x * x + y * y = z * z.

Equations

• PythagoreanTriple x y z = (x * x + y * y = z * z)

theorem pythagoreanTriple_comm {x : ℤ} {y : ℤ} {z : ℤ} : PythagoreanTriple x y z ↔ PythagoreanTriple y x z

Pythagorean triples are interchangeable, i.e x * x + y * y = y * y + x * x = z * z. This comes from additive commutativity.

theorem PythagoreanTriple.zero : PythagoreanTriple 0 0 0

The zeroth Pythagorean triple is all zeros.

theorem PythagoreanTriple.eq {x : ℤ} {y : ℤ} {z : ℤ} (h : PythagoreanTriple x y z) : x * x + y * y = z * z

theorem PythagoreanTriple.symm {x : ℤ} {y : ℤ} {z : ℤ} (h : PythagoreanTriple x y z) : PythagoreanTriple y x z

theorem PythagoreanTriple.mul {x : ℤ} {y : ℤ} {z : ℤ} (h : PythagoreanTriple x y z) (k : ℤ) : PythagoreanTriple (k * x) (k * y) (k * z)

A triple is still a triple if you multiply x, y and z by a constant k.

theorem PythagoreanTriple.mul_iff {x : ℤ} {y : ℤ} {z : ℤ} (k : ℤ) (hk : k ≠ 0) : PythagoreanTriple (k * x) (k * y) (k * z) ↔ PythagoreanTriple x y z

(k*x, k*y, k*z) is a Pythagorean triple if and only if (x, y, z) is also a triple.

def PythagoreanTriple.IsClassified {x : ℤ} {y : ℤ} {z : ℤ} : PythagoreanTriple x y z → Prop

A Pythagorean triple x, y, z is “classified” if there exist integers k, m, n such that either

• x = k * (m ^ 2 - n ^ 2) and y = k * (2 * m * n), or
• x = k * (2 * m * n) and y = k * (m ^ 2 - n ^ 2).

Equations

• PythagoreanTriple.IsClassified x = ∃ (k : ℤ) (m : ℤ) (n : ℤ), (x✝ = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x✝ = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧ Int.gcd m n = 1

def PythagoreanTriple.IsPrimitiveClassified {x : ℤ} {y : ℤ} {z : ℤ} : PythagoreanTriple x y z → Prop

A primitive Pythagorean triple x, y, z is a Pythagorean triple with x and y coprime. Such a triple is “primitively classified” if there exist coprime integers m, n such that either

• x = m ^ 2 - n ^ 2 and y = 2 * m * n, or
• x = 2 * m * n and y = m ^ 2 - n ^ 2.

Equations

• One or more equations did not get rendered due to their size.

theorem PythagoreanTriple.mul_isClassified {x : ℤ} {y : ℤ} {z : ℤ} (h : PythagoreanTriple x y z) (k : ℤ) (hc : PythagoreanTriple.IsClassified h) : PythagoreanTriple.IsClassified ⋯

theorem PythagoreanTriple.even_odd_of_coprime {x : ℤ} {y : ℤ} {z : ℤ} (h : PythagoreanTriple x y z) (hc : Int.gcd x y = 1) : x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0

theorem PythagoreanTriple.gcd_dvd {x : ℤ} {y : ℤ} {z : ℤ} (h : PythagoreanTriple x y z) : ↑(Int.gcd x y) ∣ z

theorem PythagoreanTriple.normalize {x : ℤ} {y : ℤ} {z : ℤ} (h : PythagoreanTriple x y z) : PythagoreanTriple (x / ↑(Int.gcd x y)) (y / ↑(Int.gcd x y)) (z / ↑(Int.gcd x y))

theorem PythagoreanTriple.isClassified_of_isPrimitiveClassified {x : ℤ} {y : ℤ} {z : ℤ} (h : PythagoreanTriple x y z) (hp : PythagoreanTriple.IsPrimitiveClassified h) : PythagoreanTriple.IsClassified h

theorem PythagoreanTriple.isClassified_of_normalize_isPrimitiveClassified {x : ℤ} {y : ℤ} {z : ℤ} (h : PythagoreanTriple x y z) (hc : PythagoreanTriple.IsPrimitiveClassified ⋯) : PythagoreanTriple.IsClassified h

theorem PythagoreanTriple.ne_zero_of_coprime {x : ℤ} {y : ℤ} {z : ℤ} (h : PythagoreanTriple x y z) (hc : Int.gcd x y = 1) : z ≠ 0

theorem PythagoreanTriple.isPrimitiveClassified_of_coprime_of_zero_left {x : ℤ} {y : ℤ} {z : ℤ} (h : PythagoreanTriple x y z) (hc : Int.gcd x y = 1) (hx : x = 0) : PythagoreanTriple.IsPrimitiveClassified h

theorem PythagoreanTriple.coprime_of_coprime {x : ℤ} {y : ℤ} {z : ℤ} (h : PythagoreanTriple x y z) (hc : Int.gcd x y = 1) : Int.gcd y z = 1

A parametrization of the unit circle

For the classification of Pythagorean triples, we will use a parametrization of the unit circle.

def circleEquivGen {K : Type u_1} [Field K] (hk : ∀ (x : K), 1 + x ^ 2 ≠ 0) : K ≃ { p : K × K // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }

A parameterization of the unit circle that is useful for classifying Pythagorean triples. (To be applied in the case where K = ℚ.)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem circleEquivGen_apply {K : Type u_1} [Field K] (hk : ∀ (x : K), 1 + x ^ 2 ≠ 0) (x : K) : ↑((circleEquivGen hk) x) = (2 * x / (1 + x ^ 2), (1 - x ^ 2) / (1 + x ^ 2))

@[simp]

theorem circleEquivGen_symm_apply {K : Type u_1} [Field K] (hk : ∀ (x : K), 1 + x ^ 2 ≠ 0) (v : { p : K × K // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }) : (circleEquivGen hk).symm v = (↑v).1 / ((↑v).2 + 1)

theorem PythagoreanTriple.isPrimitiveClassified_aux {x : ℤ} {y : ℤ} {z : ℤ} (h : PythagoreanTriple x y z) (hc : Int.gcd x y = 1) (hzpos : 0 < z) {m : ℤ} {n : ℤ} (hm2n2 : 0 < m ^ 2 + n ^ 2) (hv2 : ↑x / ↑z = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)) (hw2 : ↑y / ↑z = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)) (H : Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1) (co : Int.gcd m n = 1) (pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) : PythagoreanTriple.IsPrimitiveClassified h

theorem PythagoreanTriple.isPrimitiveClassified_of_coprime_of_odd_of_pos {x : ℤ} {y : ℤ} {z : ℤ} (h : PythagoreanTriple x y z) (hc : Int.gcd x y = 1) (hyo : y % 2 = 1) (hzpos : 0 < z) : PythagoreanTriple.IsPrimitiveClassified h

theorem PythagoreanTriple.isPrimitiveClassified_of_coprime_of_pos {x : ℤ} {y : ℤ} {z : ℤ} (h : PythagoreanTriple x y z) (hc : Int.gcd x y = 1) (hzpos : 0 < z) : PythagoreanTriple.IsPrimitiveClassified h

theorem PythagoreanTriple.isPrimitiveClassified_of_coprime {x : ℤ} {y : ℤ} {z : ℤ} (h : PythagoreanTriple x y z) (hc : Int.gcd x y = 1) : PythagoreanTriple.IsPrimitiveClassified h

theorem PythagoreanTriple.classified {x : ℤ} {y : ℤ} {z : ℤ} (h : PythagoreanTriple x y z) : PythagoreanTriple.IsClassified h

theorem PythagoreanTriple.coprime_classification {x : ℤ} {y : ℤ} {z : ℤ} : PythagoreanTriple x y z ∧ Int.gcd x y = 1 ↔ ∃ (m : ℤ) (n : ℤ), (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧ (z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)) ∧ Int.gcd m n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)

theorem PythagoreanTriple.coprime_classification' {x : ℤ} {y : ℤ} {z : ℤ} (h : PythagoreanTriple x y z) (h_coprime : Int.gcd x y = 1) (h_parity : x % 2 = 1) (h_pos : 0 < z) : ∃ (m : ℤ) (n : ℤ), x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∧ z = m ^ 2 + n ^ 2 ∧ Int.gcd m n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m

by assuming x is odd and z is positive we get a slightly more precise classification of the Pythagorean triple x ^ 2 + y ^ 2 = z ^ 2

theorem PythagoreanTriple.classification {x : ℤ} {y : ℤ} {z : ℤ} : PythagoreanTriple x y z ↔ ∃ (k : ℤ) (m : ℤ) (n : ℤ), (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧ (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

Formula for Pythagorean Triples