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.
Statement with defined notation
∀ p. ∀ g. Prime(p) → Dvd(g,p) → g = 1 ∨ p = gEvery purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.
Definitions used by this theorem
In the theorem statement
2 occurrences
In local proof propositions
0 occurrences
Exact expanded native-PA statement
forall p g. (~(p = 1) /\ forall c d. p = c * d -> c = 1 \/ d = 1) -> (exists x. p = g * x) -> g = 1 \/ p = gProof neighborhood
Direct theorem prerequisites
Direct theorem dependents
Definition-aware tactic body
Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.
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 (1)
01Fix variables and assumptionsL1–4
02Separate the logical casesL5–6
03Use earlier factsL7–8
04Establish hfactorL9–11
05Separate the logical casesL12–13
06Use earlier factsL14–14
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L14
exact hfactor_left
07Separate the logical casesL15–15
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L15
right
08Calculate and transport equalitiesL16–16
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L16
trans g * x
09Use earlier factsL17–17
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L17
exact hdiv_witness
10Calculate and transport equalitiesL18–18
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L18
rewrite hfactor_right
11Use earlier factsL19–19
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L19
apply mul_one
Original defined command ledger · 19 lines
- 0001
intro p - 0002
intro g - 0003
intro hp - 0004
intro hdiv - 0005
cases hp - 0006
cases hdiv - 0007
specialize hp_right g - 0008
specialize hp_right x - 0009
have hfactor : g = 1 \/ x = 1 - 0010
apply hp_right - 0011
exact hdiv_witness - 0012
cases hfactor - 0013
left - 0014
exact hfactor_left - 0015
right - 0016
trans g * x - 0017
exact hdiv_witness - 0018
rewrite hfactor_right - 0019
apply mul_one