Beal's Conjecture

-- If aˣ + bʸ = cᶜ with x, y, z > 2, then a, b, c share a common prime factor.
theorem beal (a b c x y z : ℕ)
    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
    (hx : 2 < x) (hy : 2 < y) (hz : 2 < z)
    (h : a ^ x + b ^ y = c ^ z) :
    ∃ p : ℕ, Nat.Prime p ∧ p ∣ a ∧ p ∣ b ∧ p ∣ c :=