Conditional Sylvester-Schur consequences

TheoremSylvester–Schur theorem for two consecutive integers#✓fully proved

For every natural number \(k > 2\), one of the two integers \(k\), \(k + 1\) is divisible by a prime \(p > 2\).

theorem consecutive_two {k : ℕ} (hk : 2 < k) :
    ∃ i : ℕ, i < 2 ∧ ∃ p : ℕ, p.Prime ∧ 2 < p ∧ p ∣ k + i

Used by 1

Used byErdős key lemma

TheoremSylvester–Schur theorem for three consecutive integers#✓fully proved

For every natural number \(k > 3\), one of the three integers \(k\), \(k + 1\), \(k + 2\) is divisible by a prime \(p > 3\).

theorem consecutive_three {k : ℕ} (hk : 3 < k) :
    ∃ i : ℕ, i < 3 ∧ ∃ p : ℕ, p.Prime ∧ 3 < p ∧ p ∣ k + i

Used by 2

Used byFour consecutive integers above four have a prime factor above four · Erdős key lemma

TheoremFour consecutive integers above four have a prime factor above four#✓fully proved

For every natural number \(k > 4\), some prime \(p > 4\) divides one of \(k\), \(k+1\), \(k+2\), \(k+3\).

theorem consecutive_four {k : ℕ} (hk : 4 < k) :
    ∃ i : ℕ, i < 4 ∧ ∃ p : ℕ, p.Prime ∧ 4 < p ∧ p ∣ k + i

Uses 1 · Used by 1

Proof usesSylvester–Schur theorem for three consecutive integers

Used byErdős key lemma

TheoremFive consecutive integers above five have a prime factor above five#✓fully proved

For every natural number \(k > 5\), some prime \(p > 5\) divides one of \(k\), \(k+1\), \(k+2\), \(k+3\), \(k+4\).

theorem consecutive_five {k : ℕ} (hk : 5 < k) :
    ∃ i : ℕ, i < 5 ∧ ∃ p : ℕ, p.Prime ∧ 5 < p ∧ p ∣ k + i

Used by 2

Used bySix consecutive integers above six have a prime factor above six · Erdős key lemma

TheoremSix consecutive integers above six have a prime factor above six#✓fully proved

For every natural number \(k > 6\), some prime \(p > 6\) divides one of \(k\), \(k+1\), \(k+2\), \(k+3\), \(k+4\), \(k+5\).

theorem consecutive_six {k : ℕ} (hk : 6 < k) :
    ∃ i : ℕ, i < 6 ∧ ∃ p : ℕ, p.Prime ∧ 6 < p ∧ p ∣ k + i

Uses 1 · Used by 1

Proof usesFive consecutive integers above five have a prime factor above five

Used byErdős key lemma

TheoremPrime-counting criterion for a large prime in a consecutive block#✓fully proved

Let \(1 \le n < k\) be natural numbers and let \(\pi(n)\) be the number of primes at most \(n\). If \(n! \cdot (k+n-1)^{\pi(n)} < k^n\), then some prime \(p > n\) divides one of the integers \(k, k+1, \dots, k+n-1\).

theorem consecutive_of_factorial_mul_top_pow_primeCounting_lt_start_pow {n k : ℕ}
    (hn : 1 ≤ n) (hk : n < k)
    (hbound : n ! * (k + n - 1) ^ Nat.primeCounting n < k ^ n) :
    ∃ i < n, ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ k + i

Uses 2 · Used by 1

Proof usesFrom a large prime divisor of the binomial coefficient to one in the block · Large-prime criterion from the prime-counting bound

Used bySylvester–Schur criterion from the prime-counting bound

TheoremHalf-exponent criterion for a large prime in a consecutive block#✓fully proved

Let \(1 \le n < k\) be natural numbers. If \(n! \cdot (k+n-1)^{\lfloor n/2 \rfloor + 1} < k^n\), then some prime \(p > n\) divides one of the integers \(k, k+1, \dots, k+n-1\).

The exponent comes from the bound \(\pi(n) \le \lfloor n/2 \rfloor + 1\) on the prime-counting function \(\pi\).

theorem consecutive_of_factorial_mul_top_pow_half_add_one_lt_start_pow {n k : ℕ}
    (hn : 1 ≤ n) (hk : n < k)
    (hbound : n ! * (k + n - 1) ^ (n / 2 + 1) < k ^ n) :
    ∃ i < n, ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ k + i

Uses 2 · Used by 1

Proof usesFrom a large prime divisor of the binomial coefficient to one in the block · Large-prime criterion from the half-plus-one exponent bound

Used bySylvester–Schur criterion from the half-exponent bound

TheoremQuadratic starts give a large prime in a consecutive block#✓fully proved

Let \(n \ge 38\) and \(k > n^2\) be natural numbers. Then some prime \(p > n\) divides one of the integers \(k, k+1, \dots, k+n-1\).

theorem consecutive_of_quadratic_start {n k : ℕ} (hn : 38 ≤ n)
    (hkquad : n ^ 2 < k) :
    ∃ i < n, ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ k + i

Uses 2 · Used by 1

Proof usesFrom a large prime divisor of the binomial coefficient to one in the block · Power-only large-prime criterion from the 3r/8 exponent bound

Used byBlocks without large prime divisors start at most at \(n^2\)

TheoremSquare-root and primorial criterion for a large prime in a consecutive block#✓fully proved

Let \(1 \le n < k\) be natural numbers, write \(N = k + n - 1\), and let \(P(n)\) denote the product of all primes at most \(n\). If \(n! \cdot N^{\lfloor \sqrt{N} \rfloor + 1} \cdot P(n) < k^n\), then some prime \(p > n\) divides one of the integers \(k, k+1, \dots, k+n-1\).

theorem consecutive_of_factorial_mul_top_pow_sqrt_mul_primorial_lt_start_pow {n k : ℕ}
    (hn : 1 ≤ n) (hk : n < k)
    (hbound :
      n ! * ((k + n - 1) ^ (Nat.sqrt (k + n - 1) + 1) * primorial n) < k ^ n) :
    ∃ i < n, ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ k + i

Uses 2 · Used by 1

Proof usesFrom a large prime divisor of the binomial coefficient to one in the block · Large-prime criterion from the square-root split bound

Used byLarge prime divisor of the block binomial coefficient from the square-root primorial bound

TheoremErdős layer criterion for a large prime in a consecutive block#✓fully proved

Let \(1 \le n < k\) be natural numbers, write \(N = k + n - 1\) and \(L = \lfloor \log_2 N \rfloor\), and for a natural number \(m\) let \(P(m)\) denote the product of all primes at most \(m\). If \(n! \cdot P(n) \cdot \prod_{i=2}^{L} P(\lfloor N^{1/i} \rfloor) < k^n\), then some prime \(p > n\) divides one of the integers \(k, k+1, \dots, k+n-1\).

theorem consecutive_of_factorial_mul_prod_erdos_layers_lt_start_pow {n k : ℕ}
    (hn : 1 ≤ n) (hk : n < k)
    (hbound :
      n ! *
          (∏ j ∈ Finset.range (Nat.log 2 (k + n - 1)),
            if j = 0 then primorial n else primorial (Nat.nthRoot (j + 1) (k + n - 1))) <
        k ^ n) :
    ∃ i < n, ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ k + i

Uses 2 · Used by 1

Proof usesFrom a large prime divisor of the binomial coefficient to one in the block · Large-prime criterion from the Erdős layer bound

Used bySylvester–Schur criterion from the Erdős layer bound

TheoremErdős layer criterion with a one-third first layer for a large prime in a consecutive block#✓fully proved

Let \(n < k\) be natural numbers, write \(N = k + n - 1\) and \(L = \lfloor \log_2 N \rfloor\), assume \(N \ge 6\), and for a natural number \(m\) let \(P(m)\) denote the product of all primes at most \(m\). If \(n! \cdot P(\lfloor N/3 \rfloor) \cdot \prod_{i=2}^{L} P(\lfloor N^{1/i} \rfloor) < k^n\), then some prime \(p > n\) divides one of the integers \(k, k+1, \dots, k+n-1\).

theorem consecutive_of_factorial_mul_prod_erdos_div_three_layers_lt_start_pow {n k : ℕ}
    (hk : n < k) (hN6 : 6 ≤ k + n - 1)
    (hbound :
      n ! *
          (∏ j ∈ Finset.range (Nat.log 2 (k + n - 1)),
            if j = 0 then primorial ((k + n - 1) / 3)
            else primorial (Nat.nthRoot (j + 1) (k + n - 1))) <
        k ^ n) :
    ∃ i < n, ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ k + i

Uses 2 · Used by 1

Proof usesFrom a large prime divisor of the binomial coefficient to one in the block · Erdős layer criterion, factorial form

Used bySylvester–Schur criterion from the Erdős layer bound with a one-third first layer

TheoremLarge starts give a large prime in a consecutive block#✓fully proved

Let \(n \ge 2\) and \(k > n\) be natural numbers with \(n! \cdot 2^{n-1} < k\). Then some prime \(p > n\) divides one of the integers \(k, k+1, \dots, k+n-1\).

theorem consecutive_of_large_start {n k : ℕ} (hn : 2 ≤ n) (hk : n < k)
    (hlarge : n ! * 2 ^ (n - 1) < k) :
    ∃ i < n, ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ k + i

Uses 2 · Used by 1

Proof usesFrom a large prime divisor of the binomial coefficient to one in the block · Large-prime criterion from the r − 1 exponent bound

Used bySylvester–Schur criterion for blocks with a large start

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.