fermatLastTheoremFour
theorem fermatLastTheoremFour : FermatLastTheoremFor 4
This theorem is a specific case of Fermat's Last Theorem for n=4 over natural numbers. It states that if `a`, `b`, and `c` are non-zero natural numbers, then the equation `a ^ 4 + b ^ 4` is not equal to `c ^ 4`, implying that there are no three natural numbers `a`, `b`, and `c` that satisfy this equation. In mathematical terms, it asserts that $a^4 + b^4 \neq c^4$ for all non-zero natural numbers `a`, `b`, and `c`.
More concisely: For all non-zero natural numbers `a`, `b`, and `c`, `a^4 + b^4 ≠ c^4`.
|
Fermat42.neg_of_minimal
theorem Fermat42.neg_of_minimal : ∀ {a b c : ℤ}, Fermat42.Minimal a b c → Fermat42.Minimal a b (-c)
The theorem `Fermat42.neg_of_minimal` states that if we have a minimal solution to the equation `a ^ 4 + b ^ 4 = c ^ 2`, denoted as `Fermat42.Minimal a b c`, where `a`, `b`, and `c` are integers and minimal refers to no other solution exists with a smaller `c` (in absolute value), then we can assume that the same minimal solution holds if `c` is negated, i.e., `Fermat42.Minimal a b (-c)`. In other words, the sign of `c` doesn't affect the minimality of the solution.
More concisely: If `(a, b, c)` is a minimal solution to `a^4 + b^4 = c^2`, then `(a, b, -c)` is also a minimal solution.
|
Fermat42.exists_odd_minimal
theorem Fermat42.exists_odd_minimal :
∀ {a b c : ℤ}, Fermat42 a b c → ∃ a0 b0 c0, Fermat42.Minimal a0 b0 c0 ∧ a0 % 2 = 1
The theorem states that for any three non-zero integers `a`, `b`, and `c` that satisfy the equation `a ^ 4 + b ^ 4 = c ^ 2`, there exists a minimal solution involving another set of integers `a0`, `b0`, and `c0`, where `a0` is odd. A minimal solution here means that there are no other solutions with a smaller `c` (in terms of absolute value).
More concisely: Given three non-zero integers `a`, `b`, and `c` satisfying `a ^ 4 +b ^ 4 = c ^ 2`, there exists an odd `a0` with minimal `|c0|` such that `a0 ^ 4 + b ^ 4 = c0 ^ 2`.
|
FermatLastTheorem.of_odd_primes
theorem FermatLastTheorem.of_odd_primes : (∀ (p : ℕ), p.Prime → Odd p → FermatLastTheoremFor p) → FermatLastTheorem
The theorem `FermatLastTheorem.of_odd_primes` states that to prove Fermat's Last Theorem, it is sufficient to prove it for odd prime exponents. In more detail, if for every natural number `p` that is both a prime number and odd, the statement of Fermat's Last Theorem holds for `p`, then the general statement of Fermat's Last Theorem, which asserts that there are no nontrivial natural solutions for `a ^ n + b ^ n = c ^ n` when `n` is greater than or equal to 3, is true.
More concisely: If Fermat's Last Theorem holds for all odd prime exponents, then it holds for all natural numbers greater than 2.
|
Fermat42.exists_minimal
theorem Fermat42.exists_minimal : ∀ {a b c : ℤ}, Fermat42 a b c → ∃ a0 b0 c0, Fermat42.Minimal a0 b0 c0
The theorem `Fermat42.exists_minimal` states that if there exists a solution to the equation `a^4 + b^4 = c^2` for three non-zero integers `a`, `b`, and `c`, then there is a minimal solution. A solution is said to be minimal if there's no other solution with a `c` that has a smaller absolute value.
More concisely: Given non-zero integers `a`, `b`, and `c` satisfying `a^4 + b^4 = c^2`, there exists a minimal solution with the smallest absolute value for `c`.
|
Fermat42.exists_pos_odd_minimal
theorem Fermat42.exists_pos_odd_minimal :
∀ {a b c : ℤ}, Fermat42 a b c → ∃ a0 b0 c0, Fermat42.Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
The theorem `Fermat42.exists_pos_odd_minimal` asserts that for every three non-zero integers `a`, `b`, and `c` that satisfy the equation `a ^ 4 + b ^ 4 = c ^ 2`, there exists three other integers `a0`, `b0`, `c0` that not only satisfy this equation but also form a minimal solution - meaning there is no other solution with a smaller `c` (in absolute value) - with the additional properties that `a0` is odd and `c0` is positive.
More concisely: Given three non-zero integers a, b, and c satisfying a^4 +b^4 = c^2, there exist odd a' and positive c' such that a'^4 + b^4 = c'^2 and c' is smaller in absolute value than any other solution.
|
Fermat42.coprime_of_minimal
theorem Fermat42.coprime_of_minimal : ∀ {a b c : ℤ}, Fermat42.Minimal a b c → IsCoprime a b
The theorem `Fermat42.coprime_of_minimal` states that for any integers `a`, `b`, and `c`, if the tuple `(a, b, c)` is a minimal solution to the equation `a ^ 4 + b ^ 4 = c ^ 2` (meaning that there is no other solution with a smaller `c` in absolute value), then `a` and `b` must be coprime. In terms of number theory, two integers `a` and `b` are said to be coprime if there exist two other integers `x` and `y` such that `a * x + b * y = 1`.
More concisely: If `(a, b, c)` is a minimal solution to the equation `a ^ 4 + b ^ 4 = c ^ 2` in integers `a`, `b`, and `c`, then `a` and `b` are coprime.
|
Fermat42.minimal_comm
theorem Fermat42.minimal_comm : ∀ {a b c : ℤ}, Fermat42.Minimal a b c → Fermat42.Minimal b a c
This theorem states that if we have a minimal solution to the equation `a ^ 4 + b ^ 4 = c ^ 2` (where 'minimal' means that there is no other solution with a smaller absolute value of `c`), then we can interchange `a` and `b` without affecting the minimality of the solution. In other words, if `(a, b, c)` is a minimal solution, then `(b, a, c)` is also a minimal solution.
More concisely: If `(a, b, c)` is a minimal solution to the equation `a ^ 4 + b ^ 4 = c ^ 2`, then interchanging `a` and `b` results in another minimal solution `(b, a, c)`.
|