Consecutive powerful numbers

TheoremSplitting \(RS = p^2 C^3\) when \(R\) and \(S\) are coprime#●ready to prove

Let \(p\) be a prime and let \(R\), \(S\), \(C\) be integers with \(RS = p^2 C^3\) and \(\gcd(R, S) = 1\). Then there are integers \(C_1\), \(C_2\) such that either \(R = C_1^3\) and \(S = p^2 C_2^3\), or \(R = p^2 C_1^3\) and \(S = C_2^3\).

public theorem_wanted cube_split_of_mul_eq_prime_sq_mul_cube_of_gcd_eq_one
    {p : ℕ} (hp : p.Prime) {R S C : ℤ} (h : R * S = (p : ℤ) ^ 2 * C ^ 3)
    (hg : Int.gcd R S = 1) :
    ∃ C₁ C₂ : ℤ, (R = C₁ ^ 3 ∧ S = (p : ℤ) ^ 2 * C₂ ^ 3) ∨
      (R = (p : ℤ) ^ 2 * C₁ ^ 3 ∧ S = C₂ ^ 3)

Sources

• Jialai She, Nonexistence of Consecutive Powerful Triplets Around Cubes with Prime-Square Factors, INTEGERS 25 (2025), Article A103, Lemma 1.

TheoremSplitting \(RS = p^2 C^3\) when \(\gcd(R, S)\) is prime#●ready to prove

Let \(p\) be a prime and let \(R\), \(S\), \(C\) be integers with \(RS = p^2 C^3\) such that \(g = \gcd(R, S)\) is prime. Then there are integers \(C_1\), \(C_2\) such that one of the following holds: \(R = g C_1^3\) and \(S = g C_2^3\); or \(R = g C_1^3\) and \(S = g^2 p^2 C_2^3\); or \(S = g C_1^3\) and \(R = g^2 p^2 C_2^3\); or \(R = g p^2 C_1^3\) and \(S = g^2 C_2^3\); or \(S = g p^2 C_1^3\) and \(R = g^2 C_2^3\).

public theorem_wanted cube_split_of_mul_eq_prime_sq_mul_cube_of_gcd_prime
    {p : ℕ} (hp : p.Prime) {R S C : ℤ} (h : R * S = (p : ℤ) ^ 2 * C ^ 3)
    (hg : (Int.gcd R S).Prime) :
    ∃ C₁ C₂ : ℤ,
      (R = (Int.gcd R S : ℤ) * C₁ ^ 3 ∧ S = (Int.gcd R S : ℤ) * C₂ ^ 3) ∨
      (R = (Int.gcd R S : ℤ) * C₁ ^ 3 ∧
        S = (Int.gcd R S : ℤ) ^ 2 * (p : ℤ) ^ 2 * C₂ ^ 3) ∨
      (S = (Int.gcd R S : ℤ) * C₁ ^ 3 ∧
        R = (Int.gcd R S : ℤ) ^ 2 * (p : ℤ) ^ 2 * C₂ ^ 3) ∨
      (R = (Int.gcd R S : ℤ) * (p : ℤ) ^ 2 * C₁ ^ 3 ∧
        S = (Int.gcd R S : ℤ) ^ 2 * C₂ ^ 3) ∨
      (S = (Int.gcd R S : ℤ) * (p : ℤ) ^ 2 * C₁ ^ 3 ∧
        R = (Int.gcd R S : ℤ) ^ 2 * C₂ ^ 3)

Sources

• Jialai She, Nonexistence of Consecutive Powerful Triplets Around Cubes with Prime-Square Factors, INTEGERS 25 (2025), Article A103, Lemma 1.

TheoremInteger solutions of \(u^2 \pm u + 1 = 3v^3\)#●ready to prove

For all integers \(u\) and \(v\), \(u^2 + u + 1 = 3v^3\) if and only if \((u, v) = (-2, 1)\) or \((u, v) = (1, 1)\), and \(u^2 - u + 1 = 3v^3\) if and only if \((u, v) = (2, 1)\) or \((u, v) = (-1, 1)\).

public theorem_wanted sq_add_add_one_eq_three_mul_cube_iff (u v : ℤ) :
    (u ^ 2 + u + 1 = 3 * v ^ 3 ↔ (u, v) = (-2, 1) ∨ (u, v) = (1, 1)) ∧
      (u ^ 2 - u + 1 = 3 * v ^ 3 ↔ (u, v) = (2, 1) ∨ (u, v) = (-1, 1))

Sources

• Jialai She, Nonexistence of Consecutive Powerful Triplets Around Cubes with Prime-Square Factors, INTEGERS 25 (2025), Article A103, Lemma 2.

TheoremWhen \(u^2 \pm u + 1\) is a cube#●ready to prove

For every integer \(u\), \(u^2 + u + 1\) is the cube of an integer if and only if \(u \in \{-19, -1, 0, 18\}\), and \(u^2 - u + 1\) is the cube of an integer if and only if \(u \in \{-18, 0, 1, 19\}\).

public theorem_wanted sq_add_add_one_eq_cube_iff (u : ℤ) :
    ((∃ v : ℤ, u ^ 2 + u + 1 = v ^ 3) ↔ u = -19 ∨ u = -1 ∨ u = 0 ∨ u = 18) ∧
      ((∃ v : ℤ, u ^ 2 - u + 1 = v ^ 3) ↔ u = -18 ∨ u = 0 ∨ u = 1 ∨ u = 19)

Sources

• Jialai She, Nonexistence of Consecutive Powerful Triplets Around Cubes with Prime-Square Factors, INTEGERS 25 (2025), Article A103, Lemma 3.

TheoremThe gcd of \(x \mp 1\) and \(x^2 \pm x + 1\)#●ready to prove

For every integer \(x\), \(\gcd(x - 1, x^2 + x + 1) = \gcd(x - 1, 3)\) and \(\gcd(x + 1, x^2 - x + 1) = \gcd(x + 1, 3)\).

public theorem_wanted gcd_sub_one_sq_add_add_one (x : ℤ) :
    Int.gcd (x - 1) (x ^ 2 + x + 1) = Int.gcd (x - 1) 3 ∧
      Int.gcd (x + 1) (x ^ 2 - x + 1) = Int.gcd (x + 1) 3

Sources

• Jialai She, Nonexistence of Consecutive Powerful Triplets Around Cubes with Prime-Square Factors, INTEGERS 25 (2025), Article A103, Lemma 4.

TheoremInteger solutions of \(u^3 - v^3 = 2\) and \(u^3 - v^3 = 1\)#●ready to prove

For all integers \(u\) and \(v\), \(u^3 - v^3 = 2\) if and only if \((u, v) = (1, -1)\), and \(u^3 - v^3 = 1\) if and only if \((u, v) = (1, 0)\) or \((u, v) = (0, -1)\).

public theorem_wanted cube_sub_cube_eq_two_or_one_iff (u v : ℤ) :
    (u ^ 3 - v ^ 3 = 2 ↔ (u, v) = (1, -1)) ∧
      (u ^ 3 - v ^ 3 = 1 ↔ (u, v) = (1, 0) ∨ (u, v) = (0, -1))

Sources

• Jialai She, Nonexistence of Consecutive Powerful Triplets Around Cubes with Prime-Square Factors, INTEGERS 25 (2025), Article A103, Lemma 5.

TheoremInteger solutions of \(u^3 - 2v^3 = 1\)#●ready to prove

For all integers \(u\) and \(v\), \(u^3 - 2v^3 = 1\) if and only if \((u, v) = (1, 0)\) or \((u, v) = (-1, -1)\).

public theorem_wanted cube_sub_two_mul_cube_eq_one_iff (u v : ℤ) :
    u ^ 3 - 2 * v ^ 3 = 1 ↔ (u, v) = (1, 0) ∨ (u, v) = (-1, -1)

Sources

• Jialai She, Nonexistence of Consecutive Powerful Triplets Around Cubes with Prime-Square Factors, INTEGERS 25 (2025), Article A103, Lemma 7.

TheoremInteger solutions of \(u^3 - d v^3 = 1\) for \(d \in \{4, 18, 36\}\)#●ready to prove

Let \(d\) be one of the integers \(4\), \(18\), \(36\). For all integers \(u\) and \(v\), \(u^3 - d v^3 = 1\) if and only if \((u, v) = (1, 0)\).

public theorem_wanted cube_sub_mul_cube_eq_one_iff_of_mem {d : ℤ}
    (hd : d = 4 ∨ d = 18 ∨ d = 36) (u v : ℤ) :
    u ^ 3 - d * v ^ 3 = 1 ↔ (u, v) = (1, 0)

Sources

• Jialai She, Nonexistence of Consecutive Powerful Triplets Around Cubes with Prime-Square Factors, INTEGERS 25 (2025), Article A103, Lemma 8.

Theorem\(x^3 - 1\) and \(x^3 + 1\) are not both a prime square times a cube#●ready to prove

There are no primes \(p\), \(q\) and integers \(x\), \(a\), \(b\) with \(x^3 - 1 = p^2 a^3\) and \(x^3 + 1 = q^2 b^3\).

As in the paper, \(x\), \(a\), \(b\) range over all integers, with no positivity assumption.

public theorem_wanted not_cube_sub_one_eq_prime_sq_mul_cube_and_cube_add_one
    {p q : ℕ} (hp : p.Prime) (hq : q.Prime) (x a b : ℤ) :
    ¬ (x ^ 3 - 1 = (p : ℤ) ^ 2 * a ^ 3 ∧ x ^ 3 + 1 = (q : ℤ) ^ 2 * b ^ 3)

Sources

• Jialai She, Nonexistence of Consecutive Powerful Triplets Around Cubes with Prime-Square Factors, INTEGERS 25 (2025), Article A103, Theorem 1.

Theorem\(x^6 - 1\) is not \(p^2 q^2\) times a nonzero cube#●ready to prove

For all primes \(p\), \(q\) and all integers \(x\) and \(a\) with \(a \ne 0\), \(x^6 - 1 \ne p^2 q^2 a^3\).

public theorem_wanted pow_six_sub_one_ne_prime_sq_mul_prime_sq_mul_cube
    {p q : ℕ} (hp : p.Prime) (hq : q.Prime) (x a : ℤ) (ha : a ≠ 0) :
    x ^ 6 - 1 ≠ (p : ℤ) ^ 2 * (q : ℤ) ^ 2 * a ^ 3

Sources

• Jialai She, Nonexistence of Consecutive Powerful Triplets Around Cubes with Prime-Square Factors, INTEGERS 25 (2025), Article A103, Corollary 1.

TheoremTwo is not a difference of two squares#●ready to prove

For all integers \(a\) and \(b\), \(a^2 - b^2 \neq 2\).

theorem_wanted int_sq_sub_int_sq_ne_two
    (a b : ℤ) :
    a ^ 2 - b ^ 2 ≠ 2

Sources

• Tsz Ho Chan, "A Note on Three Consecutive Powerful Numbers", Lemma 1.

TheoremExact divisibility of \(x^2 + x + 1\) by \(3\)#●ready to prove

If \(x\) is an integer with \(x \equiv 1 \pmod 3\), then \(3\) divides \(x^2 + x + 1\) but \(9\) does not.

theorem_wanted three_exact_dvd_sq_add_self_add_one
    (x : ℤ) (hx : x % 3 = 1) :
    3 ∣ x ^ 2 + x + 1 ∧ ¬ 9 ∣ x ^ 2 + x + 1

Sources

• Tsz Ho Chan, "A Note on Three Consecutive Powerful Numbers", Lemma 2.

TheoremExact divisibility of \(x^2 - x + 1\) by \(3\)#●ready to prove

If \(x\) is an integer with \(x \equiv 2 \pmod 3\), then \(3\) divides \(x^2 - x + 1\) but \(9\) does not.

theorem_wanted three_exact_dvd_sq_sub_self_add_one
    (x : ℤ) (hx : x % 3 = 2) :
    3 ∣ x ^ 2 - x + 1 ∧ ¬ 9 ∣ x ^ 2 - x + 1

Sources

• Tsz Ho Chan, "A Note on Three Consecutive Powerful Numbers", Lemma 3.

TheoremInteger points on a quartic give integer points on a cubic#●ready to prove

Let \(a\), \(c\) and \(e\) be integers with \(a \neq 0\). If there are integers \(x \neq 0\) and \(y\) with \(y^2 = a x^4 + c x^2 + e\), then there are integers \(X \neq 0\) and \(Y\) with \(Y^2 = X^3 + c X^2 + a e X\).

theorem_wanted exists_int_point_elliptic_of_exists_int_point_quartic
    (a c e : ℤ) (ha : a ≠ 0)
    (h : ∃ x y : ℤ, x ≠ 0 ∧ y ^ 2 = a * x ^ 4 + c * x ^ 2 + e) :
    ∃ X Y : ℤ, X ≠ 0 ∧ Y ^ 2 = X ^ 3 + c * X ^ 2 + a * e * X

Sources

• Tsz Ho Chan, "A Note on Three Consecutive Powerful Numbers", Lemma 4.

TheoremPositive solutions of \(x^2 - 3y^2 = 1\)#●ready to prove

For integers \(x\) and \(y\), we have \(x > 0\), \(y > 0\) and \(x^2 - 3y^2 = 1\) if and only if \(x + y\sqrt{3} = (2 + \sqrt{3})^k\) in \(\mathbb{Z}[\sqrt{3}]\) for some natural number \(k \ge 1\). Writing \((2 + \sqrt{3})^k = u_k + v_k \sqrt{3}\) for \(k \ge 0\), we have \((u_1, v_1) = (2, 1)\), \((u_2, v_2) = (7, 4)\), and \(u_{k+2} = 4u_{k+1} - u_k\) and \(v_{k+2} = 4v_{k+1} - v_k\) for every \(k \ge 0\).

theorem_wanted pell_three_eq_one_positive_solutions_iff_and_recurrence :
    (∀ x y : ℤ,
      (0 < x ∧ 0 < y ∧ x ^ 2 - 3 * y ^ 2 = 1) ↔
        ∃ k : ℕ, 1 ≤ k ∧
          (⟨x, y⟩ : ℤ√3) = (⟨2, 1⟩ : ℤ√3) ^ k) ∧
      (((⟨2, 1⟩ : ℤ√3) ^ 1).re = 2 ∧ ((⟨2, 1⟩ : ℤ√3) ^ 1).im = 1 ∧
        ((⟨2, 1⟩ : ℤ√3) ^ 2).re = 7 ∧ ((⟨2, 1⟩ : ℤ√3) ^ 2).im = 4 ∧
        ∀ k : ℕ,
          ((⟨2, 1⟩ : ℤ√3) ^ (k + 2)).re =
              4 * ((⟨2, 1⟩ : ℤ√3) ^ (k + 1)).re -
                ((⟨2, 1⟩ : ℤ√3) ^ k).re ∧
            ((⟨2, 1⟩ : ℤ√3) ^ (k + 2)).im =
              4 * ((⟨2, 1⟩ : ℤ√3) ^ (k + 1)).im -
                ((⟨2, 1⟩ : ℤ√3) ^ k).im)

Sources

• Tsz Ho Chan, "A Note on Three Consecutive Powerful Numbers", Lemma 5.

TheoremPositive solutions of \(x^2 - 3y^2 = -2\)#●ready to prove

For integers \(x\) and \(y\), we have \(x > 0\), \(y > 0\) and \(x^2 - 3y^2 = -2\) if and only if \(x + y\sqrt{3} = (1 + \sqrt{3})(2 + \sqrt{3})^k\) in \(\mathbb{Z}[\sqrt{3}]\) for some integer \(k \ge 0\). Writing \((1 + \sqrt{3})(2 + \sqrt{3})^k = u_k + v_k \sqrt{3}\) for \(k \ge 0\), we have \((u_0, v_0) = (1, 1)\), \((u_1, v_1) = (5, 3)\), and \(u_{k+2} = 4u_{k+1} - u_k\) and \(v_{k+2} = 4v_{k+1} - v_k\) for every \(k \ge 0\).

MathlibExt.NumberTheory.PowerfulNumbersWanted.pell_three_eq_neg_two_positive_solutions_iff_and_recurrence · 16 lines

theorem_wanted pell_three_eq_neg_two_positive_solutions_iff_and_recurrence :
    (∀ x y : ℤ,
      (0 < x ∧ 0 < y ∧ x ^ 2 - 3 * y ^ 2 = -2) ↔
        ∃ k : ℕ,
          (⟨x, y⟩ : ℤ√3) = (⟨1, 1⟩ : ℤ√3) * (⟨2, 1⟩ : ℤ√3) ^ k) ∧
      ((((⟨1, 1⟩ : ℤ√3) * (⟨2, 1⟩ : ℤ√3) ^ 0).re = 1 ∧
          ((⟨1, 1⟩ : ℤ√3) * (⟨2, 1⟩ : ℤ√3) ^ 0).im = 1 ∧
          ((⟨1, 1⟩ : ℤ√3) * (⟨2, 1⟩ : ℤ√3) ^ 1).re = 5 ∧
          ((⟨1, 1⟩ : ℤ√3) * (⟨2, 1⟩ : ℤ√3) ^ 1).im = 3) ∧
        ∀ k : ℕ,
          ((⟨1, 1⟩ : ℤ√3) * (⟨2, 1⟩ : ℤ√3) ^ (k + 2)).re =
              4 * ((⟨1, 1⟩ : ℤ√3) * (⟨2, 1⟩ : ℤ√3) ^ (k + 1)).re -
                ((⟨1, 1⟩ : ℤ√3) * (⟨2, 1⟩ : ℤ√3) ^ k).re ∧
            ((⟨1, 1⟩ : ℤ√3) * (⟨2, 1⟩ : ℤ√3) ^ (k + 2)).im =
              4 * ((⟨1, 1⟩ : ℤ√3) * (⟨2, 1⟩ : ℤ√3) ^ (k + 1)).im -
                ((⟨1, 1⟩ : ℤ√3) * (⟨2, 1⟩ : ℤ√3) ^ k).im)

Sources

• Tsz Ho Chan, "A Note on Three Consecutive Powerful Numbers", Lemma 6.

TheoremNo cube whose neighbours are prime cubes times squares#●ready to prove

There are no primes \(p\), \(q\) and positive integers \(x\), \(y\), \(z\) with \(x^3 - 1 = p^3 y^2\) and \(x^3 + 1 = q^3 z^2\).

theorem_wanted not_exists_prime_cube_square_neighbors_of_cube :
    ¬ ∃ p q x y z : ℕ,
      p.Prime ∧ q.Prime ∧ 0 < x ∧ 0 < y ∧ 0 < z ∧
        (x : ℤ) ^ 3 - 1 = (p : ℤ) ^ 3 * (y : ℤ) ^ 2 ∧
          (x : ℤ) ^ 3 + 1 = (q : ℤ) ^ 3 * (z : ℤ) ^ 2

Sources

• Tsz Ho Chan, "A Note on Three Consecutive Powerful Numbers", Theorem 1.

TheoremNo integer solutions of \(64x^6 - 1 = p^3 q^3 y^2\) with \(p\), \(q\) prime#●ready to prove

There are no integers \(x\), \(y\) and primes \(p\), \(q\) with \(64 x^6 - 1 = p^3 q^3 y^2\).

theorem_wanted not_exists_sixty_four_mul_pow_six_sub_one_eq :
    ¬ ∃ (p q : ℕ) (x y : ℤ),
      p.Prime ∧ q.Prime ∧
        64 * x ^ 6 - 1 = (p : ℤ) ^ 3 * (q : ℤ) ^ 3 * y ^ 2

Sources

• Tsz Ho Chan, "A Note on Three Consecutive Powerful Numbers", Corollary 1.

18 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.