pythagoreanTriple_comm
theorem pythagoreanTriple_comm : ∀ {x y z : ℤ}, PythagoreanTriple x y z ↔ PythagoreanTriple y x z
The theorem `pythagoreanTriple_comm` asserts that the Pythagorean triples are interchangeable. In other words, given three integers `x`, `y`, and `z`, if `x`, `y`, and `z` form a Pythagorean triple in the sense that `x * x + y * y = z * z`, then `y`, `x`, and `z` also form a Pythagorean triple, i.e., `y * y + x * x = z * z`. This property arises due to the principle of additive commutativity in arithmetic.
More concisely: If `x`, `y`, and `z` form a Pythagorean triple `x*x + y*y = z*z`, then interchanging `x` and `y` results in another Pythagorean triple `y*y + x*x = z*z`.
|
PythagoreanTriple.coprime_classification'
theorem PythagoreanTriple.coprime_classification' :
∀ {x y z : ℤ},
PythagoreanTriple x y z →
x.gcd y = 1 →
x % 2 = 1 →
0 < z →
∃ m n,
x = m ^ 2 - n ^ 2 ∧
y = 2 * m * n ∧
z = m ^ 2 + n ^ 2 ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m
The theorem `PythagoreanTriple.coprime_classification'` provides a more specific classification of Pythagorean triples, which are defined as three integers `x`, `y`, and `z` such that `x * x + y * y = z * z`. The theorem states that for any Pythagorean triple in which `x` is odd, the greatest common divisor (gcd) of `x` and `y` is 1, and `z` is positive, there exist integers `m` and `n` such that `x` equals `m * m - n * n`, `y` equals `2 * m * n`, and `z` equals `m * m + n * n`. Moreover, `m` and `n` are coprime (their gcd is 1) and either `m` is even and `n` is odd, or `m` is odd and `n` is even, and `m` is nonnegative. This theorem is a formulation of the parameterization of primitive Pythagorean triples.
More concisely: For every odd, positive integer x in a Pythagorean triple x^2 + y^2 = z^2, there exist coprime integers m and n with m > 0 such that x = m^2 - n^2, y = 2*m*n, and z = m^2 + n^2.
|
PythagoreanTriple.zero
theorem PythagoreanTriple.zero : PythagoreanTriple 0 0 0
This theorem states that the zeroth Pythagorean triple consists of all zeros. In other words, when all three integers `x`, `y`, and `z` are zero, they form a Pythagorean triple as per the defined condition, i.e., $0^2 + 0^2 = 0^2$.
More concisely: The theorem asserts that the triplet (0, 0, 0) is a Pythagorean triple since 0^2 + 0^2 equals 0^2.
|
PythagoreanTriple.classification
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))
The "Formula for Pythagorean Triples" theorem states that for any three integers `x`, `y`, and `z`, they form a Pythagorean triple (i.e., $x^2 + y^2 = z^2$) if and only if there exist integers `k`, `m`, and `n` such that `x`, `y`, and `z` can be expressed in one of the following ways: either `x` is `k` times the difference of the squares of `m` and `n` and `y` is `k` times twice the product of `m` and `n`, or `x` is `k` times twice the product of `m` and `n` and `y` is `k` times the difference of the squares of `m` and `n`, and `z` is either `k` times the sum of the squares of `m` and `n` or negative `k` times the sum of the squares of `m` and `n`.
More concisely: A triple of integers `(x, y, z)` forms a Pythagorean triple if and only if there exist integers `k`, `m`, and `n` such that `x = k*(m^2 - n^2)`, `y = k*(2*m*n)`, and `z = k*(m^2 + n^2)` or `x = k*(2*m*n)`, `y = k*(m^2 - n^2)`, and `z = k*(m^2 + n^2)` (with the signs of `m` and `n` in the first expression adjusted if necessary to ensure `z > 0`).
|
PythagoreanTriple.eq
theorem PythagoreanTriple.eq : ∀ {x y z : ℤ}, PythagoreanTriple x y z → x * x + y * y = z * z
The theorem `PythagoreanTriple.eq` states that for any three integers `x`, `y`, and `z`, if `x`, `y` and `z` form a Pythagorean triple (which is defined to be true when the square of `x` plus the square of `y` equals the square of `z`), then the equation `x * x + y * y = z * z` holds true.
More concisely: If integers x, y, and z form a Pythagorean triple, then x² +y² = z² holds true. Equivalently, x, y, and z satisfy the equation x² +y² = z² if and only if there exist integers a and b such that x = a²+b², y = 2ab, and z = a²+b²².
|
PythagoreanTriple.mul_iff
theorem PythagoreanTriple.mul_iff :
∀ {x y z : ℤ} (k : ℤ), k ≠ 0 → (PythagoreanTriple (k * x) (k * y) (k * z) ↔ PythagoreanTriple x y z)
The theorem states that for any three integers `x`, `y`, and `z`, and an integer `k` that is not zero, the triple `(k*x, k*y, k*z)` forms a Pythagorean triple if and only if the original triple `(x, y, z)` is a Pythagorean triple. In other words, multiplying all elements of a Pythagorean triple by a non-zero integer results in another Pythagorean triple, and vice versa. A Pythagorean triple is defined as three integers `x`, `y`, and `z` where `x * x + y * y = z * z`.
More concisely: For any non-zero integer `k` and Pythagorean triple `(x, y, z)` with `x * x + y * y = z * z`, the triple `(k*x, k*y, k*z)` is also a Pythagorean triple.
|
PythagoreanTriple.mul
theorem PythagoreanTriple.mul :
∀ {x y z : ℤ}, PythagoreanTriple x y z → ∀ (k : ℤ), PythagoreanTriple (k * x) (k * y) (k * z)
This theorem states that if three integers `x`, `y`, and `z` form a Pythagorean triple (meaning that `x * x + y * y = z * z`), then multiplying all three numbers by a constant integer `k` will still result in a Pythagorean triple. In other words, if `(x, y, z)` is a Pythagorean triple, then so is `(k*x, k*y, k*z)` for any integer `k`. This matches the mathematical fact that scaling the sides of a right triangle by a constant factor preserves the Pythagorean relationship.
More concisely: If `(x, y, z)` is a Pythagorean triple of integers, then `(k*x, k*y, k*z)` is also a Pythagorean triple for any integer `k`.
|