Finite residual checks for the Sylvester-Schur theorem

LemmaA numerical criterion for a prime divisor of \(\binom{N}{r}\) above \(r\) when \(N \ge 3r\)#✓fully proved

Let \(N\) and \(r\) be natural numbers with \(r \ge 4\) and \(3r \le N\), and let \(e = r + \lfloor \sqrt{N} \rfloor + \lfloor N^{1/3} \rfloor \cdot \lfloor \log_2 N \rfloor\). If \(r \cdot 2^r \cdot (3r)^r \cdot 4^e < 3^r \cdot 4^r \cdot N^r\), then some prime \(p\) with \(r < p\) divides \(\binom{N}{r}\).

lemma exists_prime_dvd_choose_of_scaled_ternary_erdos_layers_bound {N r : ℕ}
    (hr : 4 ≤ r) (hrN : 3 * r ≤ N)
    (hbound :
      r * (2 ^ r * ((3 * r) ^ r *
        4 ^ (r + Nat.sqrt N + Nat.nthRoot 3 N * Nat.log 2 N))) <
        3 ^ r * 4 ^ r * N ^ r) :
    ∃ p : ℕ, p.Prime ∧ r < p ∧ p ∣ Nat.choose N r

Uses 4 · Used by 1

Proof usesErdős layer bound for binomial coefficients without large prime factors · Three-layer power-of-four bound for the Erdős layer product · Negating the no-large-prime condition for \(\binom{N}{r}\) · Scaled monotonicity of binomial coefficients

Used byErdős key lemma

LemmaA numerical criterion for a prime divisor of \(\binom{N}{r}\) above \(r\) when \(N = 2r + i\)#✓fully proved

Let \(r\), \(i\) and \(N\) be natural numbers with \(r \ge 4\), \(i \le r\), \(N = 2r + i\) and \(N \ge 6\). For a natural number \(n\) write \(n\#\) for the product of the primes \(p \le n\). Let \(L = \lfloor \log_2 N \rfloor\), let \(a_0 = \lfloor N/3 \rfloor\#\) and \(a_j = \lfloor N^{1/(j+1)} \rfloor\#\) for \(j \ge 1\), and put \(P = \prod_{j=0}^{L-1} a_j\). If \(r \cdot 2^i \cdot P < 3^i \cdot 4^r\), then some prime \(p\) with \(r < p\) divides \(\binom{N}{r}\).

lemma exists_prime_dvd_choose_of_central_offset_erdos_div_three_layers_bound
    {N r i : ℕ} (hr : 4 ≤ r) (hi : i ≤ r) (hN : N = 2 * r + i) (hN6 : 6 ≤ N)
    (hbound :
      r * (2 ^ i *
        (∏ j ∈ Finset.range (Nat.log 2 N),
          if j = 0 then primorial (N / 3) else primorial (Nat.nthRoot (j + 1) N))) <
        3 ^ i * 4 ^ r) :
    ∃ p : ℕ, p.Prime ∧ r < p ∧ p ∣ Nat.choose N r

Uses 2 · Used by 1

Proof usesErdős layer bound with a one-third first layer · Negating the no-large-prime condition for \(\binom{N}{r}\)

Used byErdős key lemma

LemmaA prime divisor of \(\binom{2n+2}{n}\) above \(n\) for small \(n\)#✓fully proved

For every natural number \(n\) with \(7 \le n < 512\), some prime \(p\) with \(n < p\) divides \(\binom{2n+2}{n}\).

These cases are handled by an explicit short prime-gap certificate.

lemma exists_prime_dvd_choose_two_mul_add_two_small {n : ℕ} (hn7 : 7 ≤ n)
    (hnlt : n < 512) :
    ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ Nat.choose (2 * n + 2) n

Used by 1

Used byErdős key lemma

LemmaA block term with a large prime factor, small range#✓fully proved

Let \(n\) and \(k\) be natural numbers with \(7 \le n < 38\) and \(n + 3 \le k < 100\). Then there are a natural number \(i < n\) and a prime \(p > n\) such that \(p\) divides \(k + i\).

The witness comes from a table of prime gaps.

lemma second_residual_tiny_has_large_prime_factor {n k : ℕ}
    (hn7 : 7 ≤ n) (hnlt : n < 38) (hklo : n + 3 ≤ k) (hklt : k < 100) :
    ∃ i < n, ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ k + i

Used by 1

Used byErdős key lemma

LemmaA block term with a large prime factor, middle range#✓fully proved

Let \(n\) and \(k\) be natural numbers with \(38 \le n < 945\) and \(n + 3 \le k < 1291\). Then there are a natural number \(i < n\) and a prime \(p > n\) such that \(p\) divides \(k + i\).

The witness comes from a table of prime gaps.

lemma second_residual_mid_has_large_prime_factor {n k : ℕ}
    (hn38 : 38 ≤ n) (hnlt : n < 945) (hklo : n + 3 ≤ k) (hklt : k < 1291) :
    ∃ i < n, ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ k + i

Used by 1

Used byErdős key lemma

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.