Beal conjecture

Reference: Wikipedia

def BealConjecture.bealConjecture : Prop

Equations

• BealConjecture.bealConjecture = ∀ {A B C x y z : ℕ}, A ≠ 0 → B ≠ 0 → C ≠ 0 → 2 < x → 2 < y → 2 < z → A ^ x + B ^ y = C ^ z → 1 < {A, B, C}.gcd id

theorem BealConjecture.beal_conjecture : bealConjecture

The Beal Conjecture: if we are given positive integers $A, B, C, x, y, z$ such that $x, y, z > 2$ and $A^x + B^y = C^z$ then $A, B, C$ have a common divisor.

theorem BealConjecture.flt_of_beal_conjecture (H : bealConjecture) : FermatLastTheorem

The Beal Conjecture implies Fermat's last theorem