Skip to content

Block-level reductions for the Sylvester-Schur theorem

LemmaBertrand's postulate in block form#✓fully proved

For every natural number \(n \ge 1\) there are \(i < n\) and a prime \(p > n\) such that \(p\) divides \(n + 1 + i\). Thus one of the \(n\) consecutive integers \(n + 1, \dots, 2n\) has a prime divisor greater than \(n\).

lemma bertrand_base {n : ℕ} (hn : 1 ≤ n) :
    ∃ i < n, ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ n + 1 + i
15 fully proved

From block divisibility to binomial divisibility

LemmaPrime divisors above \(n\) of a block term divide the binomial coefficient#✓fully proved

Let \(n\), \(k\) and \(j\) be natural numbers with \(j < n\), and let \(r\) be a prime with \(r > n\). If \(r\) divides \(k + j\), then \(r\) divides \(\binom{k+n-1}{n}\).

lemma prime_dvd_seq_implies_choose {n k r : ℕ} (hr : r.Prime) (hr_gt : n < r)
    (j : ℕ) (hj : j < n) (hdvd : r ∣ k + j) :
    r ∣ Nat.choose (k + n - 1) n
Uses 1 · Used by 8
Proof usesLarge prime divisors of a block term divide the binomial coefficient
Used bySylvester–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 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 · Large prime divisor of the block binomial coefficient from the square-root primorial bound · Erdős key lemma

LemmaPrimes above \(n\) in the block divide the block binomial coefficient#✓fully proved

Let \(n\) and \(k\) be natural numbers and let \(p\) be a prime with \(p > n\) and \(k \le p \le k + n - 1\). Then \(p\) divides \(\binom{k+n-1}{n}\).

lemma prime_dvd_choose_of_mem_interval {n k p : ℕ} (hp : p.Prime) (hp_gt : n < p)
    (hp_ge : k ≤ p) (hp_le : p ≤ k + n - 1) :
    p ∣ Nat.choose (k + n - 1) n
Used by 1
Used byErdős key lemma

LemmaLarge prime divisors pass from a block to its binomial coefficient#✓fully proved

Let \(n\) and \(k\) be natural numbers. If some prime \(p > n\) divides \(k + i\) for some \(i < n\), then some prime \(q > n\) divides \(\binom{k + n - 1}{n}\).

lemma exists_prime_dvd_choose_of_large_prime_dvd_block {n k : ℕ}
    (hblock : ∃ i < n, ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ k + i) :
    ∃ q : ℕ, q.Prime ∧ n < q ∧ q ∣ Nat.choose (k + n - 1) n
Uses 1 · Used by 2
Proof usesPrime divisors above \(n\) of a block term divide the binomial coefficient
Used byLarge prime divisor of the block binomial coefficient from the smooth-number count · Erdős key lemma

LemmaA block term divisible by the block length plus two#✓fully proved

Let \(n \ge 1\) and \(k\) be natural numbers and let \(s = n + 2\). If \(s\) divides neither \(k - 1\) nor \(k - 2\) (natural-number differences, truncated at \(0\)), then \(s\) divides \(k + i\) for some \(i < n\).

The number \(s\) is not assumed to be prime.

lemma exists_dvd_block_of_succ_succ_prime_not_dvd_pred {n k s : ℕ} (hn : 0 < n)
    (hsn : s = n + 2) (hnot_one : ¬ s ∣ k - 1) (hnot_two : ¬ s ∣ k - 2) :
    ∃ i < n, s ∣ k + i
Used by 1
Used byErdős key lemma

Binomial criteria from block estimates

LemmaSylvester–Schur criterion for blocks with a large start#✓fully proved

Let \(2 \le n < k\) be natural numbers with \(n! \cdot 2^{n-1} < k\). Then some prime \(p > n\) divides \(\binom{k + n - 1}{n}\).

lemma exists_prime_dvd_choose_of_large_start {n k : ℕ} (hn : 2 ≤ n) (hk : n < k)
    (hlarge : n ! * 2 ^ (n - 1) < k) :
    ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ Nat.choose (k + n - 1) n
Uses 2 · Used by 1
Proof usesPrime divisors above \(n\) of a block term divide the binomial coefficient · Large starts give a large prime in a consecutive block
Used byErdős key lemma

LemmaSylvester–Schur criterion from the half-exponent bound#✓fully proved

Let \(1 \le n < k\) be natural numbers and put \(N = k + n - 1\). If \(n! \cdot N^{\lfloor n/2 \rfloor + 1} < k^n\), then some prime \(p > n\) divides \(\binom{N}{n}\).

lemma exists_prime_dvd_choose_of_half_bound {n k : ℕ} (hn : 1 ≤ n) (hk : n < k)
    (hbound : n ! * (k + n - 1) ^ (n / 2 + 1) < k ^ n) :
    ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ Nat.choose (k + n - 1) n
Uses 2 · Used by 1
Proof usesPrime divisors above \(n\) of a block term divide the binomial coefficient · Half-exponent criterion for a large prime in a consecutive block
Used byErdős key lemma

LemmaBlocks without large prime divisors start at most at \(n^2\)#✓fully proved

Let \(n \ge 38\) and \(k\) be natural numbers. If none of the \(n\) consecutive integers \(k, k+1, \dots, k+n-1\) has a prime divisor greater than \(n\), then \(k \le n^2\).

lemma start_le_quadratic_of_no_large_prime_dvd_block {n k : ℕ} (hn : 38 ≤ n)
    (hblock : ¬ ∃ i < n, ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ k + i) :
    k ≤ n ^ 2
Uses 1 · Used by 1
Proof usesQuadratic starts give a large prime in a consecutive block
Used byErdős key lemma

LemmaSylvester–Schur criterion from the prime-counting bound#✓fully proved

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

lemma exists_prime_dvd_choose_of_primeCounting_bound {n k : ℕ} (hn : 1 ≤ n)
    (hk : n < k) (hbound : n ! * (k + n - 1) ^ Nat.primeCounting n < k ^ n) :
    ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ Nat.choose (k + n - 1) n
Uses 2 · Used by 1
Proof usesPrime divisors above \(n\) of a block term divide the binomial coefficient · Prime-counting criterion for a large prime in a consecutive block
Used byErdős key lemma

LemmaLarge prime divisor of the block binomial coefficient from the square-root primorial bound#✓fully proved

Large prime divisor of the block binomial coefficient from the square-root primorial bound. Let \(n \ge 1\) and \(k > n\) be natural numbers, write \(N = k + n - 1\), let \(\lfloor\sqrt{N}\rfloor\) be the integer square root of \(N\) and let \(P\) be the product of all primes at most \(n\). If \(n! \cdot N^{\lfloor\sqrt{N}\rfloor + 1} \cdot P < k^n\), then some prime \(p > n\) divides \(\binom{N}{n}\).

lemma exists_prime_dvd_choose_of_sqrt_primorial_bound {n k : ℕ} (hn : 1 ≤ n)
    (hk : n < k)
    (hbound :
      n ! * ((k + n - 1) ^ (Nat.sqrt (k + n - 1) + 1) * primorial n) < k ^ n) :
    ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ Nat.choose (k + n - 1) n
Uses 2 · Used by 1
Proof usesPrime divisors above \(n\) of a block term divide the binomial coefficient · Square-root and primorial criterion for a large prime in a consecutive block
Used byErdős key lemma

LemmaSylvester–Schur criterion from the Erdős layer bound#✓fully proved

Let \(1 \le n < k\) be natural numbers, put \(N = k + n - 1\) and \(L = \lfloor \log_2 N \rfloor\), and write \(m\#\) for the product of the primes at most \(m\). If

\[n! \cdot n\# \cdot \prod_{i=2}^{L} \lfloor N^{1/i} \rfloor\# < k^n,\]

then some prime \(p > n\) divides \(\binom{N}{n}\).

lemma exists_prime_dvd_choose_of_erdos_layers_bound {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) :
    ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ Nat.choose (k + n - 1) n
Uses 2 · Used by 3
Proof usesPrime divisors above \(n\) of a block term divide the binomial coefficient · Erdős layer criterion for a large prime in a consecutive block
Used bySylvester–Schur criterion from the coarse power-of-four Erdős bound · Sylvester–Schur criterion from the three-layer power-of-four Erdős bound · Erdős key lemma

LemmaSylvester–Schur criterion from the Erdős layer bound with a one-third first layer#✓fully proved

Let \(n < k\) be natural numbers, put \(N = k + n - 1\) and \(L = \lfloor \log_2 N \rfloor\), and assume \(N \ge 6\). Write \(m\#\) for the product of the primes at most \(m\). If

\[n! \cdot \lfloor N/3 \rfloor\# \cdot \prod_{i=2}^{L} \lfloor N^{1/i} \rfloor\# < k^n,\]

then some prime \(p > n\) divides \(\binom{N}{n}\).

lemma exists_prime_dvd_choose_of_erdos_div_three_layers_bound {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) :
    ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ Nat.choose (k + n - 1) n
Uses 2 · Used by 1
Proof usesPrime divisors above \(n\) of a block term divide the binomial coefficient · Erdős layer criterion with a one-third first layer for a large prime in a consecutive block
Used byErdős key lemma

LemmaSylvester–Schur criterion from the coarse power-of-four Erdős bound#✓fully proved

Let \(1 \le n < k\) be natural numbers and put \(N = k + n - 1\). If

\[n! \cdot 4^{n + \lfloor \sqrt N \rfloor \lfloor \log_2 N \rfloor} < k^n,\]

then some prime \(p > n\) divides \(\binom{N}{n}\).

lemma exists_prime_dvd_choose_of_erdos_layers_four_pow_bound {n k : ℕ}
    (hn : 1 ≤ n) (hk : n < k)
    (hbound :
      n ! *
          4 ^ (n + Nat.sqrt (k + n - 1) * Nat.log 2 (k + n - 1)) <
        k ^ n) :
    ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ Nat.choose (k + n - 1) n
Uses 2 · Used by 1
Proof usesSylvester–Schur criterion from the Erdős layer bound · Power-of-four bound for the Erdős layer product
Used byErdős key lemma

LemmaSylvester–Schur criterion from the three-layer power-of-four Erdős bound#✓fully proved

Let \(1 \le n < k\) be natural numbers and put \(N = k + n - 1\). If

\[n! \cdot 4^{n+\lfloor\sqrt N\rfloor+\lfloor N^{1/3}\rfloor\lfloor\log_2 N\rfloor} < k^n,\]

then some prime \(p > n\) divides \(\binom{N}{n}\).

lemma exists_prime_dvd_choose_of_erdos_layers_three_layers_bound {n k : ℕ}
    (hn : 1 ≤ n) (hk : n < k)
    (hbound :
      n ! *
          4 ^ (n + Nat.sqrt (k + n - 1) +
            Nat.nthRoot 3 (k + n - 1) * Nat.log 2 (k + n - 1)) <
        k ^ n) :
    ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ Nat.choose (k + n - 1) n
Uses 2 · Used by 1
Proof usesSylvester–Schur criterion from the Erdős layer bound · Three-layer power-of-four bound for the Erdős layer product
Used byErdős key lemma

LemmaLarge prime divisor of the block binomial coefficient from the smooth-number count#✓fully proved

Let \(n\) and \(k\) be natural numbers, let \(\pi(n)\) be the number of primes at most \(n\), and let \(\lfloor\sqrt{k+n-1}\rfloor\) be the integer square root. If \(2^{\pi(n)} \lfloor\sqrt{k+n-1}\rfloor < n\), then some prime \(p > n\) divides \(\binom{k+n-1}{n}\).

Otherwise all \(n\) integers \(k, \dots, k+n-1\) would be positive, at most \(k+n-1\) and free of prime factors greater than \(n\), and there are at most \(2^{\pi(n)} \lfloor\sqrt{k+n-1}\rfloor\) such integers.

lemma exists_prime_dvd_choose_of_smooth_count_bound {n k : ℕ}
    (hbound : 2 ^ Nat.primeCounting n * Nat.sqrt (k + n - 1) < n) :
    ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ Nat.choose (k + n - 1) n
Uses 1 · Used by 1
Proof usesLarge prime divisors pass from a block to its binomial coefficient
Used byErdős key lemma

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.