Sylvester–Schur theorem

LemmaPrime-counting estimate for Sylvester–Schur when \(38 \le n < 945\)#✓fully proved

For all natural numbers \(n\) and \(k\) with \(38 \le n < 945\) and \(k \ge 1291\), we have \(n! \cdot (k + n - 1)^{\pi(n)} < k^n\), where \(\pi(n)\) denotes the number of primes at most \(n\).

The proof checks finitely many explicit numerical certificates.

lemma second_residual_mid_primeCounting_lt_start_pow {n k : ℕ}
    (hn38 : 38 ≤ n) (hnlt945 : n < 945) (hk1291 : 1291 ≤ k) :
    Nat.factorial n * (k + n - 1) ^ Nat.primeCounting n < k ^ n

Used by 1

Used byErdős key lemma

LemmaErdős key lemma#✓fully proved

For all natural numbers \(n\) and \(k\) with \(1 \le n < k\), the binomial coefficient \(\binom{k + n - 1}{n}\) has a prime factor \(p > n\).

This is the binomial form of the Sylvester–Schur theorem, as in Erdős's 1934 proof. The case \(n = 1\) is immediate, and the cases \(k = n + 1\) and \(k = n + 2\) follow directly from Bertrand's postulate.

lemma erdos_choose_prime_factor_gt (n : ℕ) (hn : 1 ≤ n) (k : ℕ) (hk : n < k) :
    ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ Nat.choose (k + n - 1) n

Uses 30 · Used by 1

Proof usesA block term divisible by the block length plus two · A numerical criterion for a prime divisor of \(\binom{N}{r}\) above \(r\) when \(N = 2r + i\) · Sylvester–Schur criterion from the Erdős layer bound with a one-third first layer · Sylvester–Schur criterion from the Erdős layer bound · Sylvester–Schur criterion from the coarse power-of-four Erdős bound · Sylvester–Schur criterion from the three-layer power-of-four Erdős bound · Sylvester–Schur criterion from the half-exponent bound · Large prime divisors pass from a block to its binomial coefficient · Sylvester–Schur criterion for blocks with a large start · Sylvester–Schur criterion from the prime-counting bound · A numerical criterion for a prime divisor of \(\binom{N}{r}\) above \(r\) when \(N \ge 3r\) · Large prime divisor of the block binomial coefficient from the smooth-number count · Large prime divisor of the block binomial coefficient from the square-root primorial bound · A prime divisor of \(\binom{2n+2}{n}\) above \(n\) for small \(n\) · Scaled ternary bound for the first residual estimate · Primes above \(n\) in the block divide the block binomial coefficient · Prime divisors above \(n\) of a block term divide the binomial coefficient · Central-offset residual bound · A block term with a large prime factor, middle range · Prime-counting estimate for Sylvester–Schur when \(38 \le n < 945\) · A block term with a large prime factor, small range · Tiny-range prime-counting bound · Blocks without large prime divisors start at most at \(n^2\) · Central Erdős layer estimate · Five consecutive integers above five have a prime factor above five · Four consecutive integers above four have a prime factor above four · Six consecutive integers above six have a prime factor above six · Sylvester–Schur theorem for three consecutive integers · Sylvester–Schur theorem for two consecutive integers · Erdős layer criterion, power-of-four form

Used bySylvester–Schur theorem

TheoremSylvester–Schur theorem#✓fully proved

Let \(n\) and \(k\) be natural numbers with \(0 < k < n\). Then some prime \(p > k\) divides the product \(n(n+1)\cdots(n+k-1)\) of the \(k\) consecutive integers starting at \(n\).

theorem exists_prime_gt_and_dvd_ascFactorial {n k : ℕ} (hk : 0 < k) (hkn : k < n) :
    ∃ p : ℕ, p.Prime ∧ k < p ∧ p ∣ n.ascFactorial k

Uses 2

Proof usesErdős key lemma · Prime divisors of the block binomial coefficient divide a block term

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.