Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Theorem. (FermatsLastTheorem)
∀n ∈ int, 2 < n → ∀x y z ∈ int, x ^ n + y ^ n = z ^ n → x = 0 ∨ y = 0 ∨ z = 0
In Proofgold the corresponding term root is a3012f... and proposition id is 6637e9...
Proof:
The rest of the proof is missing.

Theorem. (FermatsLastTheorem3)
∀x y z ∈ int, x ^ 3 + y ^ 3 = z ^ 3 → x = 0 ∨ y = 0 ∨ z = 0
In Proofgold the corresponding term root is efad22... and proposition id is d8f105...
Proof:
The rest of the proof is missing.

Theorem. (FermatsLastTheorem4)
∀x y z ∈ int, x ^ 4 + y ^ 4 = z ^ 4 → x = 0 ∨ y = 0 ∨ z = 0
In Proofgold the corresponding term root is 210a91... and proposition id is e250d2...
Proof:
The rest of the proof is missing.

Theorem. (FermatsLastTheoremReduction)
(∀x y z ∈ int, x ^ 3 + y ^ 3 = z ^ 3 → x = 0 ∨ y = 0 ∨ z = 0) → (∀x y z ∈ int, x ^ 4 + y ^ 4 = z ^ 4 → x = 0 ∨ y = 0 ∨ z = 0) → (∀p, prime_nat p → 5 ≤ p → ∀x y z ∈ int, x ^ p + y ^ p = z ^ p → x = 0 ∨ y = 0 ∨ z = 0) → (∀n ∈ int, 2 < n → ∀x y z ∈ int, x ^ n + y ^ n = z ^ n → x = 0 ∨ y = 0 ∨ z = 0)
In Proofgold the corresponding term root is 96423c... and proposition id is 33f51c...
Proof:
The rest of the proof is missing.