Sylvester-Schur: binomial and consecutive forms

TheoremLarge prime divisors of a block term divide the binomial coefficient#✓fully proved

Let \(n\), \(k\) and \(j\) be natural numbers with \(j < n\), and let \(p\) be a prime with \(p > n\). If \(p\) divides \(k + j\), one of the \(n\) consecutive integers \(k, \dots, k+n-1\), then \(p\) divides \(\binom{k+n-1}{n}\).

theorem prime_dvd_choose_of_dvd_consecutive {n k p j : ℕ} (hp : p.Prime) (hp_gt : n < p)
    (hj : j < n) (hdvd : p ∣ k + j) :
    p ∣ Nat.choose (k + n - 1) n

Used by 1

Used byPrime divisors above \(n\) of a block term divide the binomial coefficient

TheoremPrime divisors of the block binomial coefficient divide a block term#✓fully proved

Let \(n\) and \(k\) be natural numbers and let \(p\) be a prime. If \(p\) divides \(\binom{k+n-1}{n}\), then \(p\) divides \(k + i\) for some \(i\) with \(0 \le i < n\).

theorem exists_dvd_consecutive_of_prime_dvd_choose (n k p : ℕ) (hp : p.Prime)
    (hp_dvd : p ∣ Nat.choose (k + n - 1) n) :
    ∃ i < n, p ∣ k + i

Used by 2

Used bySylvester–Schur theorem · From a large prime divisor of the binomial coefficient to one in the block

TheoremFrom a large prime divisor of the binomial coefficient to one in the block#✓fully proved

Let \(n\) and \(k\) be natural numbers. If some prime \(p > n\) divides \(\binom{k+n-1}{n}\), then some prime \(p > n\) divides one of the integers \(k + i\) with \(0 \le i < n\).

theorem consecutive_of_exists_prime_dvd_choose {n k : ℕ}
    (hbin : ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ Nat.choose (k + n - 1) n) :
    ∃ i < n, ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ k + i

Uses 1 · Used by 7

Proof usesPrime divisors of the block binomial coefficient divide a block term

Used byErdős layer criterion for a large prime in a consecutive block · Erdős layer criterion with a one-third first layer for a large prime in a consecutive block · Half-exponent criterion for a large prime in a consecutive block · Prime-counting criterion for a large prime in a consecutive block · Square-root and primorial criterion for a large prime in a consecutive block · Large starts give a large prime in a consecutive block · Quadratic starts give a large prime in a consecutive block

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.