Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-01
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Prime valuations in the central binomial coefficient

Statement

Let n≥1 be a natural number and let p be a prime. Then

vp(n!)=∑k≥1⌊npk⌋

and

vp(2nn)=∑k≥1(⌊2npk⌋−2⌊npk⌋).

Consequently:

  1. if n<p≤2n, then vp(2nn)=1;
  2. in general, vp(2nn)≤log⁡(2n)log⁡p.

Facts & Assumptions

Proof

technique · direct
1.1L1L2givenalgebra

By [L2] and repeated use of additivity from [L1], vp(n!)=∑m=1nvp(m). For a fixed integer m, [L1] says that vp(m) is exactly the number of positive integers k for which pk∣m. Summing over m≤n therefore counts, for each k≥1, how many multiples of pk lie in {1,…,n}. That number is ⌊n/pk⌋, so vp(n!)=∑k≥1⌊npk⌋.

2.1L1L2step 1.1algebra

Applying [L1] and [L2] to (2nn) n! n!=(2n)! gives vp(2nn)=vp((2n)!)−2vp(n!). Substituting the formula from step 1.1 twice yields vp(2nn)=∑k≥1(⌊2npk⌋−2⌊npk⌋).

3.1step 2.1givenalgebra

Suppose n<p≤2n. Then ⌊2n/p⌋=1 and ⌊n/p⌋=0. Also p2>2n, so every term with k≥2 vanishes in step 2.1. Hence vp(2nn)=1.

3.2step 2.1algebra

For arbitrary p, each summand in step 2.1 is either 0 or 1, because 2⌊n/pk⌋≤⌊2n/pk⌋≤2⌊n/pk⌋+1. Therefore vp(2nn) is at most the number of positive integers k with pk≤2n. If pk≤2n, then klog⁡p≤log⁡(2n), so k≤log⁡(2n)/log⁡p. This proves vp(2nn)≤log⁡(2n)log⁡p.

4.1step 1.1step 2.1step 3.1step 3.2∎

Steps 1.1, 2.1, 3.1, and 3.2 prove all claims.

Depends on

Used by

Dependency tree · two levels

57 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources