Squares among Pell–Lucas numbers

TheoremSquare Pell–Lucas numbers#●ready to prove

For every natural number \(n\), the Pell–Lucas number \(Q_n\) is a perfect square if and only if \(n = 0\) or \(n = 1\); thus the only square terms of the sequence are \(Q_0 = Q_1 = 1\).

theorem_wanted pellLucasSequence_isSquare_iff (n : ℕ) :
    IsSquare (MetaMathlibExt.pellLucasSequence n) ↔
      n = 0 ∨ n = 1

Sources

• Sérgio Mendes, "The Diophantine Equation Q_n^x + Q_{n+1}^x = y^2", Lemma 2.

Uses 1

Statement usesPell–Lucas sequence

TheoremPell and Pell–Lucas numbers are coprime#●ready to prove

For every natural number \(n\), the Pell number \(P_n\) and the Pell–Lucas number \(Q_n\) satisfy \(\gcd(P_n, Q_n) = 1\).

theorem_wanted gcd_pellNumber_pellLucasSequence (n : ℕ) :
    Nat.gcd (MetaMathlibExt.pellNumber n)
      (MetaMathlibExt.pellLucasSequence n) = 1

Sources

• Sérgio Mendes, "The Diophantine Equation Q_n^x + Q_{n+1}^x = y^2", Lemma 3.

Uses 2

Statement usesPell–Lucas sequence · Pell numbers

TheoremConsecutive Pell–Lucas numbers are coprime#●ready to prove

For every natural number \(n\), the Pell–Lucas numbers \(Q_n\) and \(Q_{n+1}\) satisfy \(\gcd(Q_n, Q_{n+1}) = 1\).

theorem_wanted gcd_pellLucasSequence_succ (n : ℕ) :
    Nat.gcd (MetaMathlibExt.pellLucasSequence n)
      (MetaMathlibExt.pellLucasSequence (n + 1)) = 1

Sources

• Sérgio Mendes, "The Diophantine Equation Q_n^x + Q_{n+1}^x = y^2", Lemma 4.

Uses 1

Statement usesPell–Lucas sequence

TheoremSums of two coprime positive \(n\)-th powers are not squares for \(n \ge 4\)#●ready to prove

Let \(n \ge 4\) be a natural number and let \(x\) and \(y\) be coprime positive integers. Then \(x^n + y^n\) is not a perfect square: there is no natural number \(z\) with \(x^n + y^n = z^2\).

theorem_wanted pow_add_pow_ne_sq (n x y z : ℕ)
    (hn : 4 ≤ n) (hx : 0 < x) (hy : 0 < y)
    (hxy : Nat.Coprime x y) :
    x ^ n + y ^ n ≠ z ^ 2

Sources

• Sérgio Mendes, "The Diophantine Equation Q_n^x + Q_{n+1}^x = y^2", Theorem 1.

TheoremSums of powers of consecutive Pell–Lucas numbers that are squares#●ready to prove

Let \(Q_n\) denote the Pell–Lucas numbers. For natural numbers \(n\), \(x\) and \(y\), the equation \(Q_n^x + Q_{n+1}^x = y^2\) holds if and only if \(n = 1\), \(x = 1\) and \(y = 2\); that is, its only solution in natural numbers is \(Q_1 + Q_2 = 1 + 3 = 2^2\).

theorem_wanted pellLucasSequence_pow_add_pow_eq_sq
    (n x y : ℕ) :
    MetaMathlibExt.pellLucasSequence n ^ x +
        MetaMathlibExt.pellLucasSequence (n + 1) ^ x
        = y ^ 2 ↔
      n = 1 ∧ x = 1 ∧ y = 2

Sources

• Sérgio Mendes, "The Diophantine Equation Q_n^x + Q_{n+1}^x = y^2", Theorem 2.

Uses 1

Statement usesPell–Lucas sequence

5 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.