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:
Proof not loaded.

L12

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:
Proof not loaded.

L15

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:
Proof not loaded.

L18

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:
Proof not loaded.