Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Exact expanded PA statement
forall n. ~(n = 0) -> exists p. ((~(p = 1) /\ forall a b. p = a * b -> a = 1 \/ b = 1) /\ ((exists u. u + S n = p) /\ (exists v. v + p = n + n)))Structural proof guide
Every nonzero natural has a prime in its open-closed Bertrand interval.
Direct prerequisites: le_or_lt, bertrand_eventually_closed_upper, bertrand_small_closed_upper. The authored body proceeds by case analysis (1).
Proof neighborhood
Direct dependencies
Direct dependents
Formal native tactic body
Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (3)
01Fix variables and assumptionsL1–2
02Use earlier factsL3–4
03Separate the logical casesL5–5
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L5
cases le_or_lt
04Use earlier factsL6–12
Instantiate or apply named facts and discharge the corresponding proof obligations.
Original exact command ledger · 12 lines
- 0001
intro n - 0002
intro hnonzero - 0003
specialize le_or_lt (16 * 32) - 0004
specialize le_or_lt n - 0005
cases le_or_lt - 0006
specialize bertrand_eventually_closed_upper n - 0007
apply bertrand_eventually_closed_upper - 0008
exact le_or_lt_left - 0009
specialize bertrand_small_closed_upper n - 0010
apply bertrand_small_closed_upper - 0011
exact hnonzero - 0012
exact le_or_lt_right