Sylvester's sequence
DefinitionGeneralized Sylvester sequence#✓fully proved
For a natural number \(n\), the generalized Sylvester sequence \((s_k(n))_{k \ge 0}\) is the sequence of natural numbers defined by \(s_0(n) = n + 1\) and \(s_{k+1}(n) = s_k(n)^2 - s_k(n) + 1\) for \(k \ge 0\).
The source indexes the sequence from one: its \(s_1(n)\) is \(s_0(n)\) here.
def generalizedSylvester (n : ℕ) : ℕ → ℕ
| 0 => n + 1
| k + 1 => generalizedSylvester n k ^ 2 - generalizedSylvester n k + 1TheoremInitial term of the generalized Sylvester sequence#✓fully proved
For every natural number \(n\), the generalized Sylvester sequence \((s_k(n))_{k \ge 0}\) satisfies \(s_0(n) = n + 1\).
@[simp]
theorem generalizedSylvester_zero (n : ℕ) :
generalizedSylvester n 0 = n + 1def generalizedSylvester (n : ℕ) : ℕ → ℕ
| 0 => n + 1
| k + 1 => generalizedSylvester n k ^ 2 - generalizedSylvester n k + 1MathlibExt/NumberTheory/GeneralizedSylvester.lean:33
Uses 1
TheoremRecurrence for the generalized Sylvester sequence#✓fully proved
For all natural numbers \(n\) and \(k\), the generalized Sylvester sequence \((s_k(n))_{k \ge 0}\) satisfies \(s_{k+1}(n) = s_k(n)^2 - s_k(n) + 1\).
@[simp]
theorem generalizedSylvester_succ (n k : ℕ) :
generalizedSylvester n (k + 1) =
generalizedSylvester n k ^ 2 - generalizedSylvester n k + 1def generalizedSylvester (n : ℕ) : ℕ → ℕ
| 0 => n + 1
| k + 1 => generalizedSylvester n k ^ 2 - generalizedSylvester n k + 1MathlibExt/NumberTheory/GeneralizedSylvester.lean:33
Uses 1
TheoremPositivity of the generalized Sylvester sequence#✓fully proved
For all natural numbers \(n\) and \(k\), the term \(s_k(n)\) of the generalized Sylvester sequence is positive.
theorem generalizedSylvester_pos (n k : ℕ) : 0 < generalizedSylvester n kdef generalizedSylvester (n : ℕ) : ℕ → ℕ
| 0 => n + 1
| k + 1 => generalizedSylvester n k ^ 2 - generalizedSylvester n k + 1MathlibExt/NumberTheory/GeneralizedSylvester.lean:33
Uses 1
AbbreviationSylvester numbers#✓fully proved
The Sylvester numbers \(S_0, S_1, S_2, \dots\) are the natural numbers given by \(S_0 = 2\) and \(S_{n+1} = S_n^2 - S_n + 1\) for \(n \ge 0\), so the sequence begins \(2, 3, 7, 43, 1807, \dots\). It is the generalized Sylvester sequence with parameter \(1\).
abbrev sylvesterNumber (n : ℕ) : ℕ :=
Nat.generalizedSylvester 1 ndef generalizedSylvester (n : ℕ) : ℕ → ℕ
| 0 => n + 1
| k + 1 => generalizedSylvester n k ^ 2 - generalizedSylvester n k + 1MathlibExt/NumberTheory/GeneralizedSylvester.lean:33
Uses 1 · Used by 13
TheoremDivisibility of differences of Sylvester numbers#●ready to prove
Let \((S_n)_{n \ge 0}\) be the Sylvester sequence, \(S_0 = 2\) and \(S_{n+1} = S_n^2 - S_n + 1\). For all natural numbers \(k\), \(m\) and \(n\) with \(k \ge 1\), \(m \ge k\) and \(n \ge k\), the integer \((S_k - 1)^2\) divides \(S_n - S_m\).
theorem_wanted sylvester_sub_dvd
(k m n : ℕ) (hk : 1 ≤ k) (hm : k ≤ m) (hn : k ≤ n) :
((sylvesterNumber k : ℤ) - 1) ^ 2 ∣
(sylvesterNumber n : ℤ) - (sylvesterNumber m : ℤ)abbrev sylvesterNumber (n : ℕ) : ℕ :=
Nat.generalizedSylvester 1 nWantedExt/NumberTheory/Recurrences/SylvesterSequenceWanted.lean:45
Sources
- Abderrahim Makki Naciri, "A Note on Sylvester's Sequence", Proposition 1, divisibility (4).
Uses 1
TheoremSylvester numbers modulo 4#●ready to prove
Let \((S_n)_{n \ge 0}\) be the Sylvester sequence, \(S_0 = 2\) and \(S_{n+1} = S_n^2 - S_n + 1\). For every \(n \ge 1\), \(S_n \equiv 3 \pmod 4\).
theorem_wanted sylvester_modEq_three_mod_four
(n : ℕ) (hn : 1 ≤ n) :
sylvesterNumber n % 4 = 3abbrev sylvesterNumber (n : ℕ) : ℕ :=
Nat.generalizedSylvester 1 nWantedExt/NumberTheory/Recurrences/SylvesterSequenceWanted.lean:45
Sources
- Abderrahim Makki Naciri, "A Note on Sylvester's Sequence", Proposition 1, congruence (5).
Uses 1
TheoremSylvester numbers modulo 36#●ready to prove
Let \((S_n)_{n \ge 0}\) be the Sylvester sequence, \(S_0 = 2\) and \(S_{n+1} = S_n^2 - S_n + 1\). For every \(n \ge 2\), \(S_n \equiv 7 \pmod{36}\).
theorem_wanted sylvester_modEq_seven_mod_thirty_six
(n : ℕ) (hn : 2 ≤ n) :
sylvesterNumber n % 36 = 7abbrev sylvesterNumber (n : ℕ) : ℕ :=
Nat.generalizedSylvester 1 nWantedExt/NumberTheory/Recurrences/SylvesterSequenceWanted.lean:45
Sources
- Abderrahim Makki Naciri, "A Note on Sylvester's Sequence", Proposition 1, congruence (6).
Uses 1
TheoremSylvester numbers modulo 1764#●ready to prove
Let \((S_n)_{n \ge 0}\) be the Sylvester sequence, \(S_0 = 2\) and \(S_{n+1} = S_n^2 - S_n + 1\). For every \(n \ge 3\), \(S_n \equiv 43 \pmod{1764}\).
theorem_wanted sylvester_modEq_forty_three_mod_1764
(n : ℕ) (hn : 3 ≤ n) :
sylvesterNumber n % 1764 = 43abbrev sylvesterNumber (n : ℕ) : ℕ :=
Nat.generalizedSylvester 1 nWantedExt/NumberTheory/Recurrences/SylvesterSequenceWanted.lean:45
Sources
- Abderrahim Makki Naciri, "A Note on Sylvester's Sequence", Proposition 1, congruence (7).
Uses 1
TheoremAlternating divisibility for Sylvester numbers#●ready to prove
Let \((S_n)_{n \ge 0}\) be the Sylvester sequence, \(S_0 = 2\) and \(S_{n+1} = S_n^2 - S_n + 1\). For all natural numbers \(k\) and \(n\) with \(1 \le k \le n\), the integer \(S_k^2 + 1\) divides the integer \(S_n - (-1)^{n-k} S_k\).
theorem_wanted sylvester_sq_add_one_dvd_sub
(k n : ℕ) (hk : 1 ≤ k) (hn : k ≤ n) :
(sylvesterNumber k : ℤ) ^ 2 + 1 ∣
(sylvesterNumber n : ℤ) -
(-1 : ℤ) ^ (n - k) * (sylvesterNumber k : ℤ)abbrev sylvesterNumber (n : ℕ) : ℕ :=
Nat.generalizedSylvester 1 nWantedExt/NumberTheory/Recurrences/SylvesterSequenceWanted.lean:45
Sources
- Abderrahim Makki Naciri, "A Note on Sylvester's Sequence", Proposition 2, divisibility (8).
Uses 1
TheoremSylvester numbers of even index modulo 10#●ready to prove
Let \((S_n)_{n \ge 0}\) be the Sylvester sequence, \(S_0 = 2\) and \(S_{n+1} = S_n^2 - S_n + 1\). For every \(i \ge 1\), \(S_{2i} \equiv 7 \pmod{10}\).
theorem_wanted sylvester_even_index_mod_ten
(i : ℕ) (hi : 1 ≤ i) :
sylvesterNumber (2 * i) % 10 = 7abbrev sylvesterNumber (n : ℕ) : ℕ :=
Nat.generalizedSylvester 1 nWantedExt/NumberTheory/Recurrences/SylvesterSequenceWanted.lean:45
Sources
- Abderrahim Makki Naciri, "A Note on Sylvester's Sequence", Proposition 2, congruence (9), even indices.
Uses 1
TheoremSylvester numbers of odd index modulo 10#●ready to prove
Let \((S_n)_{n \ge 0}\) be the Sylvester sequence, \(S_0 = 2\) and \(S_{n+1} = S_n^2 - S_n + 1\). For every \(i \ge 1\), \(S_{2i+1} \equiv 3 \pmod{10}\).
theorem_wanted sylvester_odd_index_mod_ten
(i : ℕ) (hi : 1 ≤ i) :
sylvesterNumber (2 * i + 1) % 10 = 3abbrev sylvesterNumber (n : ℕ) : ℕ :=
Nat.generalizedSylvester 1 nWantedExt/NumberTheory/Recurrences/SylvesterSequenceWanted.lean:45
Sources
- Abderrahim Makki Naciri, "A Note on Sylvester's Sequence", Proposition 2, congruence (9), odd indices.
Uses 1
TheoremMersenne numbers in the Sylvester sequence#●ready to prove
Let \((S_n)_{n \ge 0}\) be the Sylvester sequence, \(S_0 = 2\) and \(S_{n+1} = S_n^2 - S_n + 1\). The natural numbers \(x\) such that \(x = S_n\) for some \(n\) and \(x = 2^r - 1\) for some \(r \ge 1\) are exactly \(3\) and \(7\).
theorem_wanted mersenne_sylvester_values_eq :
{x : ℕ | ∃ n r : ℕ, 1 ≤ r ∧ x = sylvesterNumber n ∧
x = 2 ^ r - 1} = {3, 7}abbrev sylvesterNumber (n : ℕ) : ℕ :=
Nat.generalizedSylvester 1 nWantedExt/NumberTheory/Recurrences/SylvesterSequenceWanted.lean:45
Sources
- Abderrahim Makki Naciri, "A Note on Sylvester's Sequence", Corollary 1(a).
Uses 1
TheoremThe only triangular Sylvester number is \(3\)#●ready to prove
Let \(S_n\) denote the \(n\)-th Sylvester number. A natural number \(x\) equals \(S_n\) for some \(n\) and satisfies \(2x = m(m + 1)\) for some natural number \(m \ge 1\) if and only if \(x = 3\).
theorem_wanted triangular_sylvester_values_eq :
{x : ℕ | ∃ n m : ℕ, 1 ≤ m ∧ x = sylvesterNumber n ∧
2 * x = m * (m + 1)} = {3}abbrev sylvesterNumber (n : ℕ) : ℕ :=
Nat.generalizedSylvester 1 nWantedExt/NumberTheory/Recurrences/SylvesterSequenceWanted.lean:45
Sources
- Abderrahim Makki Naciri, "A Note on Sylvester's Sequence", Corollary 1(b).
Uses 1
TheoremNo Sylvester number is perfect#●ready to prove
For every natural number \(n\), the \(n\)-th Sylvester number \(S_n\) is not a perfect number.
theorem_wanted sylvester_not_perfect
(n : ℕ) :
¬ (sylvesterNumber n).Perfectabbrev sylvesterNumber (n : ℕ) : ℕ :=
Nat.generalizedSylvester 1 nWantedExt/NumberTheory/Recurrences/SylvesterSequenceWanted.lean:45
Sources
- Abderrahim Makki Naciri, "A Note on Sylvester's Sequence", Corollary 1(c).
Uses 1
TheoremPrime divisors congruent to 3 modulo 4 of Sylvester numbers#●ready to prove
Let \((S_n)_{n \ge 0}\) be the Sylvester sequence, \(S_0 = 2\) and \(S_{n+1} = S_n^2 - S_n + 1\). For every \(n \ge 1\), \(S_n\) has a prime divisor \(p\) with \(p \equiv 3 \pmod 4\).
theorem_wanted sylvester_exists_prime_divisor_mod_four_eq_three
(n : ℕ) (hn : 1 ≤ n) :
∃ p : ℕ, p.Prime ∧ p ∣ sylvesterNumber n ∧ p % 4 = 3abbrev sylvesterNumber (n : ℕ) : ℕ :=
Nat.generalizedSylvester 1 nWantedExt/NumberTheory/Recurrences/SylvesterSequenceWanted.lean:45
Sources
- Abderrahim Makki Naciri, "A Note on Sylvester's Sequence", Corollary 1(d).
Uses 1
TheoremSylvester numbers are not perfect powers#●ready to prove
Let \((S_n)_{n \ge 0}\) be the Sylvester sequence, \(S_0 = 2\) and \(S_{n+1} = S_n^2 - S_n + 1\). For every \(n\) there are no natural numbers \(a \ge 2\) and \(m \ge 2\) with \(S_n = a^m\).
theorem_wanted sylvester_not_perfect_power
(n : ℕ) :
¬ ∃ a m : ℕ, 2 ≤ a ∧ 2 ≤ m ∧ sylvesterNumber n = a ^ mabbrev sylvesterNumber (n : ℕ) : ℕ :=
Nat.generalizedSylvester 1 nWantedExt/NumberTheory/Recurrences/SylvesterSequenceWanted.lean:45
Sources
- Abderrahim Makki Naciri, "A Note on Sylvester's Sequence", Proposition 3(a).
Uses 1
TheoremSylvester numbers next to perfect powers#●ready to prove
Let \((S_n)_{n \ge 0}\) be the Sylvester sequence, \(S_0 = 2\) and \(S_{n+1} = S_n^2 - S_n + 1\). For every \(n\) other than \(1\) and \(2\) there are no natural numbers \(a \ge 2\) and \(m \ge 2\) with \(S_n = a^m + 1\) or \(S_n = a^m - 1\).
theorem_wanted sylvester_ne_pow_add_or_sub_one
(n : ℕ) (hn1 : n ≠ 1) (hn2 : n ≠ 2) :
¬ ∃ a m : ℕ, 2 ≤ a ∧ 2 ≤ m ∧
((sylvesterNumber n : ℤ) = (a : ℤ) ^ m + 1 ∨
(sylvesterNumber n : ℤ) = (a : ℤ) ^ m - 1)abbrev sylvesterNumber (n : ℕ) : ℕ :=
Nat.generalizedSylvester 1 nWantedExt/NumberTheory/Recurrences/SylvesterSequenceWanted.lean:45
Sources
- Abderrahim Makki Naciri, "A Note on Sylvester's Sequence", Proposition 3(b).
Uses 1
TheoremCoprime solutions of \(x^2 + 3 = 4y^n\)#●ready to prove
For natural numbers \(n\), \(x\) and \(y\), the conditions \(n \ge 3\), \(x \ge 1\), \(y \ge 1\), \(\gcd(x, y) = 1\) and \(x^2 + 3 = 4y^n\) hold if and only if \(n \ge 3\) and either \(x = y = 1\) or \((n, x, y) = (3, 37, 7)\) (Luca–Tengely–Togbé).
theorem_wanted lebesgue_nagell_three_solutions_iff
(n x y : ℕ) :
(3 ≤ n ∧ 1 ≤ x ∧ 1 ≤ y ∧ Nat.Coprime x y ∧
x ^ 2 + 3 = 4 * y ^ n) ↔
(3 ≤ n ∧ ((x = 1 ∧ y = 1) ∨ (n = 3 ∧ x = 37 ∧ y = 7)))Sources
- F. Luca, Sz. Tengely, and A. Togbé, "On the Diophantine equation x² + C = 4yⁿ", Theorem 1.1, as quoted in Abderrahim Makki Naciri, "A Note on Sylvester's Sequence", Theorem 1, equation with C = 3.
TheoremCoprime solutions of \(x^2 + 7 = 4y^n\)#●ready to prove
For natural numbers \(n\), \(x\) and \(y\), the conditions \(n \ge 3\), \(x \ge 1\), \(y \ge 1\), \(\gcd(x, y) = 1\) and \(x^2 + 7 = 4y^n\) hold if and only if \((n, x, y)\) is \((3, 5, 2)\), \((5, 11, 2)\) or \((13, 181, 2)\) (Luca–Tengely–Togbé).
theorem_wanted lebesgue_nagell_seven_solutions_iff
(n x y : ℕ) :
(3 ≤ n ∧ 1 ≤ x ∧ 1 ≤ y ∧ Nat.Coprime x y ∧
x ^ 2 + 7 = 4 * y ^ n) ↔
((n = 3 ∧ x = 5 ∧ y = 2) ∨ (n = 5 ∧ x = 11 ∧ y = 2) ∨
(n = 13 ∧ x = 181 ∧ y = 2))Sources
- F. Luca, Sz. Tengely, and A. Togbé, "On the Diophantine equation x² + C = 4yⁿ", Theorem 1.1, as quoted in Abderrahim Makki Naciri, "A Note on Sylvester's Sequence", Theorem 1, equation with C = 7.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.