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 n1 be a natural number and let p be a prime. Then

vp(n!)=k1npk

and

vp(2nn)=k1(2npk2npk).

Consequently:

  1. if n<p2n, then vp(2nn)=1;
  2. in general, vp(2nn)log(2n)logp.

Facts & Assumptions

Proof

technique · direct
1.1

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 pkm. Summing over mn therefore counts, for each k1, how many multiples of pk lie in {1,,n}. That number is n/pk, so vp(n!)=k1npk.

L1L2givenalgebra
2.1

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)=k1(2npk2npk).

L1L2step 1.1algebra
3.1

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

step 2.1givenalgebra
3.2

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

step 2.1algebra
4.1

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

step 1.1step 2.1step 3.1step 3.2

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