Generalized Fermat equation

DefinitionSolvable generalized Fermat equation#✓fully proved

For natural numbers \(m\), \(n\), \(r\), the equation \(x^m + y^n = z^r\) is called solvable when there are nonzero integers \(x\), \(y\), \(z\) with \(x^m + y^n = z^r\).

def GeneralizedFermatSolvable (m n r : ℕ) : Prop :=
  ∃ x y z : ℤ, x ≠ 0 ∧ y ≠ 0 ∧ z ≠ 0 ∧ x ^ m + y ^ n = z ^ r
Sources
  • Richard F. Ryan, Under What Conditions on the Exponents Does x^m + y^n = z^r Have Solutions?, INTEGERS 24 (2024), Article A48, Section 1, equation (1).
Used by 5
Used byGeneralized Fermat equations with exponents u, uv and v · A solution of x³ + y⁶ = z² · Generalized Fermat equations with exponents 3s, 6t and 2w · Generalized Fermat equations with two non-coprime pairs of exponents · Swapping the first two exponents of a generalized Fermat equation

TheoremA solution of x³ + y⁶ = z²#✓fully proved

The equation \(x^3 + y^6 = z^2\) has a solution in nonzero integers, namely \(2^3 + 1^6 = 3^2\).

theorem generalizedFermatSolvable_three_six_two : GeneralizedFermatSolvable 3 6 2
Sources
  • Richard F. Ryan, Under What Conditions on the Exponents Does x^m + y^n = z^r Have Solutions?, INTEGERS 24 (2024), Article A48, Lemma 1 (the case s = t = w = 1).
Uses 1
Statement usesSolvable generalized Fermat equation

TheoremSwapping the first two exponents of a generalized Fermat equation#✓fully proved

For natural numbers \(m\), \(n\), \(r\), if \(x^m + y^n = z^r\) has a solution in nonzero integers, then so does \(x^n + y^m = z^r\).

theorem GeneralizedFermatSolvable.swap {m n r : ℕ} (h : GeneralizedFermatSolvable m n r) :
    GeneralizedFermatSolvable n m r
Sources
  • Richard F. Ryan, Under What Conditions on the Exponents Does x^m + y^n = z^r Have Solutions?, INTEGERS 24 (2024), Article A48, Section 1, equation (1).
Uses 1
Statement usesSolvable generalized Fermat equation

TheoremGeneralized Fermat equations with two non-coprime pairs of exponents#●ready to prove

Let \(m, n, r \ge 2\) be integers with \(\gcd(m, n, r) = 1\) such that at least two of \(\gcd(m, n)\), \(\gcd(m, r)\) and \(\gcd(n, r)\) are greater than \(1\). Suppose there are no natural numbers \(s, t, w\) that are pairwise coprime, with \(s\) odd and \(3 \nmid w\), such that \((m, n, r)\) is one of \((3s, 6t, 2w)\), \((6t, 3s, 2w)\), \((2w, 3s, 6t)\) and \((3s, 2w, 6t)\). Then the equation \(x^m + y^n = z^r\) has no solution in nonzero integers \(x, y, z\).

Positivity of \(s, t, w\) is automatic from \(m, n, r \ge 2\).

public theorem_wanted not_generalizedFermatSolvable_of_two_gcd_gt_one {m n r : ℕ}
    (hm : 2 ≤ m) (hn : 2 ≤ n) (hr : 2 ≤ r) (hgcd : Nat.gcd (Nat.gcd m n) r = 1)
    (htwo : (1 < Nat.gcd m n ∧ 1 < Nat.gcd m r) ∨ (1 < Nat.gcd m n ∧ 1 < Nat.gcd n r) ∨
      (1 < Nat.gcd m r ∧ 1 < Nat.gcd n r))
    (hexc : ¬ ∃ s t w : ℕ, Nat.Coprime s t ∧ Nat.Coprime s w ∧ Nat.Coprime t w ∧ Odd s ∧
      ¬ 3 ∣ w ∧ ((m, n, r) = (3 * s, 6 * t, 2 * w) ∨ (m, n, r) = (6 * t, 3 * s, 2 * w) ∨
        (m, n, r) = (2 * w, 3 * s, 6 * t) ∨ (m, n, r) = (3 * s, 2 * w, 6 * t))) :
    ¬ GeneralizedFermatSolvable m n r
Sources
  • Richard F. Ryan, Under What Conditions on the Exponents Does x^m + y^n = z^r Have Solutions?, INTEGERS 24 (2024), Article A48, Theorem 1.
Uses 1
Statement usesSolvable generalized Fermat equation

TheoremThe Bartolomé–Mihăilescu theorem for prime exponents#●ready to prove

Let \(p \le q\) be primes with \(p \ge 5\), and let \(x, y, z\) be pairwise coprime nonzero integers. Then \(x^p + y^p \ne z^q\).

The source quotes this result from Bartolomé and Mihăilescu, arXiv:2108.08572.

public theorem_wanted pow_add_pow_ne_pow_of_prime_five_le {p q : ℕ} (hp : p.Prime) (hq : q.Prime)
    (h5 : 5 ≤ p) (hpq : p ≤ q) {x y z : ℤ} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0)
    (hxy : IsCoprime x y) (hyz : IsCoprime y z) (hxz : IsCoprime x z) :
    x ^ p + y ^ p ≠ z ^ q
Sources
  • Richard F. Ryan, Under What Conditions on the Exponents Does x^m + y^n = z^r Have Solutions?, INTEGERS 24 (2024), Article A48, Corollary 1.

TheoremGeneralized Fermat equations with exponents 3s, 6t and 2w#●ready to prove

Let \(s, t, w\) be positive integers. If \(s, t, w\) are pairwise coprime, \(s\) is odd and \(3 \nmid w\), then the equation \(x^{3s} + y^{6t} = z^{2w}\) has infinitely many solutions \((x, y, z)\) in nonzero integers; otherwise it has no solution in nonzero integers.

public theorem_wanted generalizedFermat_three_six_two_mul {s t w : ℕ} (hs : 0 < s) (ht : 0 < t)
    (hw : 0 < w) :
    (Nat.Coprime s t ∧ Nat.Coprime s w ∧ Nat.Coprime t w ∧ Odd s ∧ ¬ 3 ∣ w →
      {xyz : ℤ × ℤ × ℤ | xyz.1 ≠ 0 ∧ xyz.2.1 ≠ 0 ∧ xyz.2.2 ≠ 0 ∧
        xyz.1 ^ (3 * s) + xyz.2.1 ^ (6 * t) = xyz.2.2 ^ (2 * w)}.Infinite) ∧
    (¬ (Nat.Coprime s t ∧ Nat.Coprime s w ∧ Nat.Coprime t w ∧ Odd s ∧ ¬ 3 ∣ w) →
      ¬ GeneralizedFermatSolvable (3 * s) (6 * t) (2 * w))
Sources
  • Richard F. Ryan, Under What Conditions on the Exponents Does x^m + y^n = z^r Have Solutions?, INTEGERS 24 (2024), Article A48, Lemma 1.
Uses 1
Statement usesSolvable generalized Fermat equation

TheoremGeneralized Fermat equations with exponents u, uv and v#●ready to prove

Let \(u, v \ge 2\) be integers. (A) The equation \(x^u + y^{uv} = z^v\) has a solution in nonzero integers \(x, y, z\) if and only if it has one with \(\gcd(x, y, z) = 1\). (B) If \(u\) or \(v\) is even, \((u, v) \ne (2, 2)\) and \((u, v) \ne (3, 2)\), the equation has no solution in nonzero integers. (C) If \(3 \mid u\) or \(3 \mid v\), and \((u, v) \ne (3, 2)\), the equation has no solution in nonzero integers.

public theorem_wanted generalizedFermat_mul_exponent {u v : ℕ} (hu : 2 ≤ u) (hv : 2 ≤ v) :
    (GeneralizedFermatSolvable u (u * v) v ↔
      ∃ x y z : ℤ, x ≠ 0 ∧ y ≠ 0 ∧ z ≠ 0 ∧ Nat.gcd (Int.gcd x y) z.natAbs = 1 ∧
        x ^ u + y ^ (u * v) = z ^ v) ∧
    ((Even u ∨ Even v) → (u, v) ≠ (2, 2) → (u, v) ≠ (3, 2) →
      ¬ GeneralizedFermatSolvable u (u * v) v) ∧
    ((3 ∣ u ∨ 3 ∣ v) → (u, v) ≠ (3, 2) → ¬ GeneralizedFermatSolvable u (u * v) v)
Sources
  • Richard F. Ryan, Under What Conditions on the Exponents Does x^m + y^n = z^r Have Solutions?, INTEGERS 24 (2024), Article A48, Lemma 2.
Uses 1
Statement usesSolvable generalized Fermat equation
3 fully proved4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.