Squares as sums or differences of powers

TheoremPowers of three plus one that are perfect squares#✓fully proved

For natural numbers \(y\) and \(z\), if \(3^{y+1} + 1 = z^2\), then \(y = 0\).

theorem eq_zero_of_three_pow_succ_add_one_eq_sq {y z : ℕ}
    (h : 3 ^ (y + 1) + 1 = z ^ 2) : y = 0

Sources

• M. Buosi, G. S. Ferreira, and A. L. P. Porto, arXiv:2308.10043v1, Lemma 2.1 (main.tex, lines 128–131). The paper uses natural numbers including zero.

TheoremSolutions of \(p^x + (p + a)^y = z^2\) for odd primes \(p\) and \(p + a\)#●ready to prove

Let \(p\) be a prime with \(p \ne 2\) and \(p \ne 3\), and let \(a\) be a natural number such that \(p + a\) is prime, \(a \equiv 0 \pmod 4\) and \(p\) divides \(a + 1\). If natural numbers \(x\), \(y\) and \(z\) satisfy \(p^x + (p + a)^y = z^2\), then \(x = 0\), \(y = 1\) and \(z^2 = p + a + 1\).

theorem_wanted pow_add_pow_eq_sq (p a x y z : ℕ)
    (hp : p.Prime) (hp2 : p ≠ 2) (hp3 : p ≠ 3)
    (hpa : (p + a).Prime) (ha4 : a % 4 = 0)
    (hap : p ∣ a + 1) (h : p ^ x + (p + a) ^ y = z ^ 2) :
    x = 0 ∧ y = 1 ∧ z ^ 2 = p + a + 1

Sources

• Shalini Choudhury and Naba Kanta Sarma, "On the Diophantine Equations (p+a)^x + p^y = z^2 and (p+a)^x - p^y = z^2 where p and p+a Are Odd Primes", Theorem 6.

Theorem\(19^x + 151^y\) is never a perfect square#●ready to prove

For all natural numbers \(x\), \(y\) and \(z\), \(19^x + 151^y \ne z^2\).

theorem_wanted pow19_add_pow151_ne_sq (x y z : ℕ) :
    19 ^ x + 151 ^ y ≠ z ^ 2

Sources

• Shalini Choudhury and Naba Kanta Sarma, "On the Diophantine Equations (p+a)^x + p^y = z^2 and (p+a)^x - p^y = z^2 where p and p+a Are Odd Primes", Corollary 1.

TheoremSolutions of \(2^x + 1 = z^2\)#●ready to prove

For natural numbers \(x\) and \(z\), \(2^x + 1 = z^2\) holds if and only if \(x = 3\) and \(z = 3\).

theorem_wanted two_pow_add_one_eq_sq (x z : ℕ) :
    2 ^ x + 1 = z ^ 2 ↔ x = 3 ∧ z = 3

Sources

• Suton Tadee, "On the Diophantine Equation n^x + (5p)^y = z^2", Lemma 1.

TheoremSolutions of \(n^x + 1 = z^2\) for \(n \ne 2\)#●ready to prove

Let \(n \ge 1\) be a natural number with \(n \ne 2\). For natural numbers \(x\) and \(z\), \(n^x + 1 = z^2\) holds if and only if \(x = 1\) and \(z^2 = n + 1\).

theorem_wanted pow_add_one_eq_sq (n x z : ℕ) (hn : 1 ≤ n)
    (hn2 : n ≠ 2) :
    n ^ x + 1 = z ^ 2 ↔ x = 1 ∧ z ^ 2 = n + 1

Sources

• Suton Tadee, "On the Diophantine Equation n^x + (5p)^y = z^2", Lemma 1.

TheoremThe case \(x = 0\) of \(n^x + (5p)^y = z^2\)#●ready to prove

Let \(p\) be a prime with \(p \ne 2\). For natural numbers \(y\) and \(z\), \(1 + (5p)^y = z^2\) holds if and only if \(y = 1\) and \(z^2 = 5p + 1\).

theorem_wanted one_add_pow_eq_sq (p y z : ℕ) (hp : p.Prime)
    (hp2 : p ≠ 2) :
    1 + (5 * p) ^ y = z ^ 2 ↔ y = 1 ∧ z ^ 2 = 5 * p + 1

Sources

• Suton Tadee, "On the Diophantine Equation n^x + (5p)^y = z^2", Corollary 1.

TheoremEvenness of \(x\) in \(n^x + (5p)^y = z^2\) when \(n \equiv 2, 3 \pmod 5\)#●ready to prove

Let \(p\) be a prime and \(n\) a natural number with \(n \equiv 2 \pmod 5\) or \(n \equiv 3 \pmod 5\). If natural numbers \(x\), \(y\), \(z\) with \(y > 0\) satisfy \(n^x + (5p)^y = z^2\), then \(x\) is even.

theorem_wanted even_of_pos_exp (n p x y z : ℕ) (hp : p.Prime)
    (hn : n % 5 = 2 ∨ n % 5 = 3) (hy : 0 < y)
    (h : n ^ x + (5 * p) ^ y = z ^ 2) :
    Even x

Sources

• Suton Tadee, "On the Diophantine Equation n^x + (5p)^y = z^2", Lemma 2.

TheoremOpposite parity of the exponents in \(n^x + (5p)^y = z^2\) when \(n \equiv p \equiv 3 \pmod 4\)#●ready to prove

Let \(p\) be a prime and \(n\) a natural number with \(n \equiv 3 \pmod 4\) and \(p \equiv 3 \pmod 4\). If natural numbers \(x\), \(y\), \(z\) satisfy \(n^x + (5p)^y = z^2\), then \(x\) and \(y\) have opposite parity.

theorem_wanted opposite_parity (n p x y z : ℕ) (hp : p.Prime)
    (hn : n % 4 = 3) (hp4 : p % 4 = 3)
    (h : n ^ x + (5 * p) ^ y = z ^ 2) :
    x % 2 ≠ y % 2

Sources

• Suton Tadee, "On the Diophantine Equation n^x + (5p)^y = z^2", Lemma 3.

TheoremNo solutions of \(n^x + (5p)^y = z^2\) when \(n \equiv p \equiv 1 \pmod 4\)#●ready to prove

Let \(p\) be a prime and \(n\) a natural number with \(n \equiv 1 \pmod 4\) and \(p \equiv 1 \pmod 4\). Then there are no natural numbers \(x\), \(y\), \(z\) with \(n^x + (5p)^y = z^2\).

theorem_wanted no_solution_mod_four_one (n p : ℕ) (hp : p.Prime)
    (hn : n % 4 = 1) (hp4 : p % 4 = 1) :
    ¬ ∃ x y z : ℕ, n ^ x + (5 * p) ^ y = z ^ 2

Sources

• Suton Tadee, "On the Diophantine Equation n^x + (5p)^y = z^2", Theorem 2.

TheoremSolutions of \(2^x + (5p)^y = z^2\) for \(p \equiv 3 \pmod 4\)#●ready to prove

Let \(p\) be a prime with \(p \equiv 3 \pmod 4\). For natural numbers \(x\), \(y\), \(z\), \(2^x + (5p)^y = z^2\) holds if and only if \((x, y, z) = (3, 0, 3)\), or \(p = 3\) and \((x, y, z) = (6, 2, 17)\), or \(x = 0\), \(y = 1\) and \(z^2 = 5p + 1\).

theorem_wanted two_pow_solutions (p x y z : ℕ) (hp : p.Prime)
    (hp4 : p % 4 = 3) :
    2 ^ x + (5 * p) ^ y = z ^ 2 ↔
      (x = 3 ∧ y = 0 ∧ z = 3) ∨
        (p = 3 ∧ x = 6 ∧ y = 2 ∧ z = 17) ∨
        (x = 0 ∧ y = 1 ∧ z ^ 2 = 5 * p + 1)

Sources

• Suton Tadee, "On the Diophantine Equation n^x + (5p)^y = z^2", Theorem 3.

TheoremSolutions of \(n^x + (5p)^y = z^2\) for \(n \equiv 3, 27 \pmod{60}\) and \(p \equiv 7 \pmod{12}\)#●ready to prove

Let \(p\) be a prime with \(p \equiv 7 \pmod{12}\), and let \(n\) be a natural number with \(n \equiv 3 \pmod{60}\) or \(n \equiv 27 \pmod{60}\) such that \(\gcd(n, p) = 1\) and \(\gcd(n, 5p - 1) = 1\). For natural numbers \(x\), \(y\), \(z\), \(n^x + (5p)^y = z^2\) holds if and only if either \(x = 0\), \(y = 1\) and \(z^2 = 5p + 1\), or \(x = 1\), \(y = 0\) and \(z^2 = n + 1\).

theorem_wanted solutions_mod_sixty (n p x y z : ℕ) (hp : p.Prime)
    (hn : n % 60 = 3 ∨ n % 60 = 27) (hp12 : p % 12 = 7)
    (h1 : Nat.Coprime n p) (h2 : Nat.Coprime n (5 * p - 1)) :
    n ^ x + (5 * p) ^ y = z ^ 2 ↔
      (x = 0 ∧ y = 1 ∧ z ^ 2 = 5 * p + 1) ∨
        (x = 1 ∧ y = 0 ∧ z ^ 2 = n + 1)

Sources

• Suton Tadee, "On the Diophantine Equation n^x + (5p)^y = z^2", Theorem 4.

TheoremSolutions of \(2^x + 15^y = z^2\)#●ready to prove

The natural numbers \(x\), \(y\), \(z\) with \(2^x + 15^y = z^2\) are exactly \((x, y, z) = (3, 0, 3)\), \((0, 1, 4)\) and \((6, 2, 17)\).

theorem_wanted two_pow_add_fifteen_pow (x y z : ℕ) :
    2 ^ x + 15 ^ y = z ^ 2 ↔
      (x = 3 ∧ y = 0 ∧ z = 3) ∨ (x = 0 ∧ y = 1 ∧ z = 4) ∨
        (x = 6 ∧ y = 2 ∧ z = 17)

Sources

• Suton Tadee, "On the Diophantine Equation n^x + (5p)^y = z^2", Corollary 3.

TheoremSolutions of \(3^x + 35^y = z^2\)#●ready to prove

The natural numbers \(x\), \(y\), \(z\) with \(3^x + 35^y = z^2\) are exactly \((x, y, z) = (1, 0, 2)\) and \((x, y, z) = (0, 1, 6)\).

theorem_wanted three_pow_add_thirtyfive_pow (x y z : ℕ) :
    3 ^ x + 35 ^ y = z ^ 2 ↔
      (x = 1 ∧ y = 0 ∧ z = 2) ∨ (x = 0 ∧ y = 1 ∧ z = 6)

Sources

• Suton Tadee, "On the Diophantine Equation n^x + (5p)^y = z^2", Corollary 4.

TheoremPrime powers one less than a square#●ready to prove

Let \(p\) be a prime. Then non-negative integers \(x\) and \(y\) satisfy \(p^x + 1 = y^2\) if and only if \((p, x, y) = (2, 3, 3)\) or \((p, x, y) = (3, 1, 2)\).

theorem_wanted prime_pow_add_one_eq_sq_iff {p : ℕ} (hp : p.Prime) (x y : ℕ) :
    p ^ x + 1 = y ^ 2 ↔ (p, x, y) = (2, 3, 3) ∨ (p, x, y) = (3, 1, 2)

Sources

• Jing Zhang and Yuan Li, On the Equation (-1)^α p^x + (-1)^β (2^k(2p - 1))^y = z^2 for Prime Pairs (p, 2p - 1), INTEGERS 24 (2024), Article A64, Lemma 2.

TheoremSquares of the form \(1 + (2^k(2p - 1))^y\) for prime pairs#●ready to prove

Let \(p\) be an odd prime such that \(2p - 1\) is prime, and let \(k \ge 1\) be an integer. Then non-negative integers \(y\) and \(z\) satisfy \(1 + (2^k(2p - 1))^y = z^2\) if and only if \(k = 4\), \(p = 3\), \(y = 1\) and \(z = 9\).

theorem_wanted one_add_two_pow_mul_pow_eq_sq_iff {p k : ℕ} (hp : p.Prime) (hp2 : p ≠ 2)
    (hq : (2 * p - 1).Prime) (hk : 1 ≤ k) (y z : ℕ) :
    1 + (2 ^ k * (2 * p - 1)) ^ y = z ^ 2 ↔ (k, p, y, z) = (4, 3, 1, 9)

Sources

• Jing Zhang and Yuan Li, On the Equation (-1)^α p^x + (-1)^β (2^k(2p - 1))^y = z^2 for Prime Pairs (p, 2p - 1), INTEGERS 24 (2024), Article A64, Lemma 4.

TheoremTerai's conjecture when \(c\) is prime and \(b \equiv \pm 5 \pmod 8\)#●ready to prove

Let \(a, b, c\) be natural numbers with \(a^2 + b^2 = c^2\), \(\gcd(a, b, c) = 1\), \(b \equiv \pm 5 \pmod 8\) (that is, \(b\) is \(3\) or \(5\) modulo \(8\)) and \(c\) prime. Then for all positive integers \(x, y, z\), the equation \(x^2 + b^y = c^z\) holds if and only if \((x, y, z) = (a, 2, 2)\).

This case of the conjecture is due to Yuan and Wang. Terai's conjecture (the paper's Conjecture 1) also assumes \(a\) even, which follows here since \(b\) is odd.

theorem_wanted terai_pythagorean_of_prime_of_mod_eight {a b c : ℕ} (habc : a ^ 2 + b ^ 2 = c ^ 2)
    (hgcd : Nat.gcd (Nat.gcd a b) c = 1) (hb : b % 8 = 3 ∨ b % 8 = 5) (hc : c.Prime)
    {x y z : ℕ} (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) :
    x ^ 2 + b ^ y = c ^ z ↔ (x, y, z) = (a, 2, 2)

Sources

• Jing Zhang and Yuan Li, On the Equation (-1)^α p^x + (-1)^β (2^k(2p - 1))^y = z^2 for Prime Pairs (p, 2p - 1), INTEGERS 24 (2024), Article A64, Lemma 6 and Conjecture 1.

TheoremInteger points on three Mordell curves#●ready to prove

The integer solutions of \(y^2 = x^3 - 2\) are exactly \((x, y) = (3, 5)\) and \((3, -5)\), the integer solutions of \(y^2 = x^3 - 18\) are exactly \((x, y) = (3, 3)\) and \((3, -3)\), and \(y^2 = x^3 - 162\) has no integer solutions.

theorem_wanted mordell_curves_two_eighteen_one_six_two_integer_points :
    (∀ x y : ℤ, y ^ 2 = x ^ 3 - 2 ↔ x = 3 ∧ (y = 5 ∨ y = -5)) ∧
      (∀ x y : ℤ, y ^ 2 = x ^ 3 - 18 ↔ x = 3 ∧ (y = 3 ∨ y = -3)) ∧
      ∀ x y : ℤ, y ^ 2 ≠ x ^ 3 - 162

Sources

• Jing Zhang and Yuan Li, On the Equation (-1)^α p^x + (-1)^β (2^k(2p - 1))^y = z^2 for Prime Pairs (p, 2p - 1), INTEGERS 24 (2024), Article A64, Lemma 7 (quoted from the LMFDB).

TheoremSolutions of \(3^x = y^2 + 2\)#●ready to prove

For natural numbers \(x, y\), we have \(3^x = y^2 + 2\) if and only if \((x, y)\) is \((1, 1)\) or \((3, 5)\).

theorem_wanted three_pow_eq_sq_add_two_iff (x y : ℕ) :
    3 ^ x = y ^ 2 + 2 ↔ (x, y) = (1, 1) ∨ (x, y) = (3, 5)

Sources

• Jing Zhang and Yuan Li, On the Equation (-1)^α p^x + (-1)^β (2^k(2p - 1))^y = z^2 for Prime Pairs (p, 2p - 1), INTEGERS 24 (2024), Article A64, Lemma 8.

TheoremSolutions of \(2x^2 + 1 = 3^y\)#●ready to prove

For natural numbers \(x, y\), we have \(2x^2 + 1 = 3^y\) if and only if \((x, y)\) is \((0, 0)\), \((1, 1)\), \((2, 2)\) or \((11, 5)\).

theorem_wanted two_mul_sq_add_one_eq_three_pow_iff (x y : ℕ) :
    2 * x ^ 2 + 1 = 3 ^ y ↔
      (x, y) = (0, 0) ∨ (x, y) = (1, 1) ∨ (x, y) = (2, 2) ∨ (x, y) = (11, 5)

Sources

• Jing Zhang and Yuan Li, On the Equation (-1)^α p^x + (-1)^β (2^k(2p - 1))^y = z^2 for Prime Pairs (p, 2p - 1), INTEGERS 24 (2024), Article A64, Lemma 9.

TheoremSquares of the form \(p^x + (2p - 1)^y\) for prime pairs#●ready to prove

Let \(p\) be an odd prime such that \(2p - 1\) is prime. Then non-negative integers \(x\), \(y\) and \(z\) satisfy \(p^x + (2p - 1)^y = z^2\) if and only if \(p = 3\) and \((x, y, z) = (1, 0, 2)\).

theorem_wanted prime_pair_pow_add_pow_eq_sq_iff {p : ℕ} (hp : p.Prime) (hp2 : p ≠ 2)
    (hq : (2 * p - 1).Prime) (x y z : ℕ) :
    p ^ x + (2 * p - 1) ^ y = z ^ 2 ↔ (p, x, y, z) = (3, 1, 0, 2)

Sources

• Jing Zhang and Yuan Li, On the Equation (-1)^α p^x + (-1)^β (2^k(2p - 1))^y = z^2 for Prime Pairs (p, 2p - 1), INTEGERS 24 (2024), Article A64, Theorem 1.

TheoremNo squares of the form \(p^x + (2^{2k+1}(2p - 1))^y\) for prime pairs with \(p \equiv 5, 7 \pmod 8\)#●ready to prove

No squares of the form \(p^x + (2^{2k+1}(2p - 1))^y\) for prime pairs with \(p \equiv 5, 7 \pmod 8\). Let \(p\) be a prime with \(p \equiv 5 \pmod 8\) or \(p \equiv 7 \pmod 8\) such that \(2p - 1\) is prime. Then for all non-negative integers \(k\), \(x\), \(y\) and \(z\), \(p^x + (2^{2k+1}(2p - 1))^y \ne z^2\).

theorem_wanted prime_pair_pow_add_two_pow_odd_mul_pow_ne_sq {p : ℕ} (hp : p.Prime)
    (hq : (2 * p - 1).Prime) (hp8 : p % 8 = 5 ∨ p % 8 = 7) (k x y z : ℕ) :
    p ^ x + (2 ^ (2 * k + 1) * (2 * p - 1)) ^ y ≠ z ^ 2

Sources

• Jing Zhang and Yuan Li, On the Equation (-1)^α p^x + (-1)^β (2^k(2p - 1))^y = z^2 for Prime Pairs (p, 2p - 1), INTEGERS 24 (2024), Article A64, Theorem 2.

TheoremSquares of the form \(p^x + (2^{2k}(2p - 1))^y\) for prime pairs#●ready to prove

Let \(p\) be a prime with \(p \equiv 3 \pmod 4\) such that \(2p - 1\) is prime, and let \(k \ge 1\) be an integer. Then non-negative integers \(x\), \(y\) and \(z\) satisfy \(p^x + (2^{2k}(2p - 1))^y = z^2\) if and only if either \(p = 3\) and \((x, y, z) = (1, 0, 2)\), or \(p = 3\), \(k = 2\) and \((x, y, z) = (0, 1, 9)\).

theorem_wanted prime_pair_pow_add_two_pow_even_mul_pow_eq_sq_iff {p k : ℕ} (hp : p.Prime)
    (hq : (2 * p - 1).Prime) (hp4 : p % 4 = 3) (hk : 1 ≤ k) (x y z : ℕ) :
    p ^ x + (2 ^ (2 * k) * (2 * p - 1)) ^ y = z ^ 2 ↔
      (p, x, y, z) = (3, 1, 0, 2) ∨ (p, k, x, y, z) = (3, 2, 0, 1, 9)

Sources

• Jing Zhang and Yuan Li, On the Equation (-1)^α p^x + (-1)^β (2^k(2p - 1))^y = z^2 for Prime Pairs (p, 2p - 1), INTEGERS 24 (2024), Article A64, Theorem 3.

TheoremSquares of the form \((2p - 1)^x - p^y\) for prime pairs#●ready to prove

Let \(p\) be a prime with \(p \equiv 3 \pmod 4\) such that \(2p - 1\) is prime. Then non-negative integers \(x\), \(y\) and \(z\) satisfy \((2p - 1)^x - p^y = z^2\) if and only if \((x, y, z) = (0, 0, 0)\), or \(p = 3\) and \((x, y, z) = (2, 2, 4)\), or \(p = 2t^2 + 1\) for some non-negative integer \(t\) and \((x, y, z) = (1, 0, 2t)\).

In the last family the two primes are \(p = 2t^2 + 1\) and \(2p - 1 = 4t^2 + 1\).

theorem_wanted prime_pair_pow_sub_pow_eq_sq_iff {p : ℕ} (hp : p.Prime) (hq : (2 * p - 1).Prime)
    (hp4 : p % 4 = 3) (x y z : ℕ) :
    (2 * (p : ℤ) - 1) ^ x - (p : ℤ) ^ y = (z : ℤ) ^ 2 ↔
      (x, y, z) = (0, 0, 0) ∨ (p, x, y, z) = (3, 2, 2, 4) ∨
        ∃ t : ℕ, p = 2 * t ^ 2 + 1 ∧ x = 1 ∧ y = 0 ∧ z = 2 * t

Sources

• Jing Zhang and Yuan Li, On the Equation (-1)^α p^x + (-1)^β (2^k(2p - 1))^y = z^2 for Prime Pairs (p, 2p - 1), INTEGERS 24 (2024), Article A64, Theorem 4.

TheoremSquares of the form \((2^{2k}(2p - 1))^x - p^y\) for prime pairs#●ready to prove

Let \(p\) be a prime with \(p \equiv 3 \pmod 4\) such that \(2p - 1\) is prime, and let \(k \ge 1\) be an integer. Then non-negative integers \(x\), \(y\) and \(z\) satisfy \((2^{2k}(2p - 1))^x - p^y = z^2\) if and only if \((x, y, z) = (0, 0, 0)\).

theorem_wanted prime_pair_two_pow_even_mul_pow_sub_pow_eq_sq_iff {p k : ℕ} (hp : p.Prime)
    (hq : (2 * p - 1).Prime) (hp4 : p % 4 = 3) (hk : 1 ≤ k) (x y z : ℕ) :
    ((2 : ℤ) ^ (2 * k) * (2 * p - 1)) ^ x - (p : ℤ) ^ y = (z : ℤ) ^ 2 ↔ (x, y, z) = (0, 0, 0)

Sources

• Jing Zhang and Yuan Li, On the Equation (-1)^α p^x + (-1)^β (2^k(2p - 1))^y = z^2 for Prime Pairs (p, 2p - 1), INTEGERS 24 (2024), Article A64, Theorem 6.

TheoremSquares of the form \((2^{2k+1}(2p - 1))^x - p^y\) for prime pairs#●ready to prove

Let \(p\) be a prime with \(p \equiv 5 \pmod 8\) such that \(2p - 1\) is prime, and let \(k\) be a non-negative integer. Then non-negative integers \(x\), \(y\) and \(z\) satisfy \((2^{2k+1}(2p - 1))^x - p^y = z^2\) if and only if \((x, y, z) = (0, 0, 0)\), or \(k = 0\), \(x = 1\), \(y = 0\) and \(4p = z^2 + 3\).

In the last case the two primes are \(p = (z^2 + 3)/4\) and \(2p - 1 = (z^2 + 1)/2\).

theorem_wanted prime_pair_two_pow_odd_mul_pow_sub_pow_eq_sq_iff {p : ℕ} (hp : p.Prime)
    (hq : (2 * p - 1).Prime) (hp8 : p % 8 = 5) (k x y z : ℕ) :
    ((2 : ℤ) ^ (2 * k + 1) * (2 * p - 1)) ^ x - (p : ℤ) ^ y = (z : ℤ) ^ 2 ↔
      (x, y, z) = (0, 0, 0) ∨ (4 * p = z ^ 2 + 3 ∧ k = 0 ∧ x = 1 ∧ y = 0)

Sources

• Jing Zhang and Yuan Li, On the Equation (-1)^α p^x + (-1)^β (2^k(2p - 1))^y = z^2 for Prime Pairs (p, 2p - 1), INTEGERS 24 (2024), Article A64, Theorem 7.

TheoremSquares of the form \(p^x - (2^{2k+1}(2p - 1))^y\) for prime pairs#●ready to prove

Let \(p\) be a prime with \(p \equiv 3 \pmod 8\) such that \(2p - 1\) is prime, and let \(k\) be a non-negative integer. Then non-negative integers \(x\), \(y\) and \(z\) satisfy \(p^x - (2^{2k+1}(2p - 1))^y = z^2\) if and only if \((x, y, z) = (0, 0, 0)\).

theorem_wanted prime_pair_pow_sub_two_pow_odd_mul_pow_eq_sq_iff {p : ℕ} (hp : p.Prime)
    (hq : (2 * p - 1).Prime) (hp8 : p % 8 = 3) (k x y z : ℕ) :
    (p : ℤ) ^ x - ((2 : ℤ) ^ (2 * k + 1) * (2 * p - 1)) ^ y = (z : ℤ) ^ 2 ↔ (x, y, z) = (0, 0, 0)

Sources

• Jing Zhang and Yuan Li, On the Equation (-1)^α p^x + (-1)^β (2^k(2p - 1))^y = z^2 for Prime Pairs (p, 2p - 1), INTEGERS 24 (2024), Article A64, Theorem 9.

TheoremThe exponential equations for the prime pair (2, 3)#●ready to prove

The six equations \((-1)^\alpha 2^x + (-1)^\beta (2^k \cdot 3)^y = z^2\) with \(\alpha, \beta, k \in \{0, 1\}\) and \(\alpha\beta = 0\) have exactly the following solutions in natural numbers \(x, y, z\), where the equations are read in the integers. The equation \(2^x + 3^y = z^2\) holds if and only if \((x, y, z)\) is \((0, 1, 2)\), \((3, 0, 3)\) or \((4, 2, 5)\). The equation \(2^x - 3^y = z^2\) holds if and only if \((x, y, z)\) is \((0, 0, 0)\), \((1, 0, 1)\) or \((2, 1, 1)\). The equation \(-2^x + 3^y = z^2\) holds if and only if \((x, y, z)\) is \((0, 0, 0)\), \((1, 1, 1)\), \((1, 3, 5)\), \((3, 2, 1)\) or \((5, 4, 7)\). The equation \(2^x + 6^y = z^2\) holds if and only if \((x, y, z)\) is \((3, 0, 3)\) or \((6, 2, 10)\). The equation \(2^x - 6^y = z^2\) holds if and only if \((x, y, z)\) is \((0, 0, 0)\) or \((1, 0, 1)\). The equation \(-2^x + 6^y = z^2\) holds if and only if \((x, y, z)\) is \((0, 0, 0)\), \((1, 1, 2)\), \((5, 2, 2)\), \((9, 4, 28)\) or \((5, 5, 88)\).

MetaMathlibExt.two_pow_three_pow_six_pow_eq_sq_solutions · 15 lines

theorem_wanted two_pow_three_pow_six_pow_eq_sq_solutions :
    (∀ x y z : ℕ, (2 : ℤ) ^ x + 3 ^ y = (z : ℤ) ^ 2 ↔
      (x, y, z) = (0, 1, 2) ∨ (x, y, z) = (3, 0, 3) ∨ (x, y, z) = (4, 2, 5)) ∧
    (∀ x y z : ℕ, (2 : ℤ) ^ x - 3 ^ y = (z : ℤ) ^ 2 ↔
      (x, y, z) = (0, 0, 0) ∨ (x, y, z) = (1, 0, 1) ∨ (x, y, z) = (2, 1, 1)) ∧
    (∀ x y z : ℕ, -(2 : ℤ) ^ x + 3 ^ y = (z : ℤ) ^ 2 ↔
      (x, y, z) = (0, 0, 0) ∨ (x, y, z) = (1, 1, 1) ∨ (x, y, z) = (1, 3, 5) ∨
        (x, y, z) = (3, 2, 1) ∨ (x, y, z) = (5, 4, 7)) ∧
    (∀ x y z : ℕ, (2 : ℤ) ^ x + 6 ^ y = (z : ℤ) ^ 2 ↔
      (x, y, z) = (3, 0, 3) ∨ (x, y, z) = (6, 2, 10)) ∧
    (∀ x y z : ℕ, (2 : ℤ) ^ x - 6 ^ y = (z : ℤ) ^ 2 ↔
      (x, y, z) = (0, 0, 0) ∨ (x, y, z) = (1, 0, 1)) ∧
    (∀ x y z : ℕ, -(2 : ℤ) ^ x + 6 ^ y = (z : ℤ) ^ 2 ↔
      (x, y, z) = (0, 0, 0) ∨ (x, y, z) = (1, 1, 2) ∨ (x, y, z) = (5, 2, 2) ∨
        (x, y, z) = (9, 4, 28) ∨ (x, y, z) = (5, 5, 88))

Sources

• Jing Zhang and Yuan Li, On the Equation (-1)^α p^x + (-1)^β (2^k(2p - 1))^y = z^2 for Prime Pairs (p, 2p - 1), INTEGERS 24 (2024), Article A64, Theorem 10.

TheoremSolutions of \(2 + 7^y = z^2\)#●ready to prove

For natural numbers \(y, z\), we have \(2 + 7^y = z^2\) if and only if \((y, z) = (1, 3)\).

theorem_wanted two_add_seven_pow_eq_sq_iff (y z : ℕ) : 2 + 7 ^ y = z ^ 2 ↔ (y, z) = (1, 3)

Sources

• Jing Zhang and Yuan Li, On the Equation (-1)^α p^x + (-1)^β (2^k(2p - 1))^y = z^2 for Prime Pairs (p, 2p - 1), INTEGERS 24 (2024), Article A64, Theorem 11.

1 fully proved27 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.