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 p q. ((~(p = 1) /\ forall frm_prime_left_dpn_prime_p frm_prime_right_dpn_prime_p. p = frm_prime_left_dpn_prime_p * frm_prime_right_dpn_prime_p -> frm_prime_left_dpn_prime_p = 1 \/ frm_prime_right_dpn_prime_p = 1)) -> ((~(q = 1) /\ forall frm_prime_left_dpn_prime_q frm_prime_right_dpn_prime_q. q = frm_prime_left_dpn_prime_q * frm_prime_right_dpn_prime_q -> frm_prime_left_dpn_prime_q = 1 \/ frm_prime_right_dpn_prime_q = 1)) -> ~(p = q) -> ((~(exists frm_factor_dpn_p_not_q. q = p * frm_factor_dpn_p_not_q)) /\ (~(exists frm_factor_dpn_q_not_p. p = q * frm_factor_dpn_q_not_p)))Structural proof guide
Generated structural guide
Distinct primes are mutually nondivisible.
Use the direct prerequisites distinct_primes_left_not_divide_right, distinct_primes_right_not_divide_left as previously established PA formulas.
The proof proceeds by direct introduction and elimination.
Referenced ingredients
Proof neighborhood
Direct dependencies
Direct dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.
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 (2)
01Fix variables and assumptionsL1–5
02Separate the logical casesL6–6
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L6
split
03Use earlier factsL7–8
04Fix variables and assumptionsL9–9
Work with arbitrary variables or the premises of the current implication.
- L9
intro hdiv
05Use earlier factsL10–16
06Fix variables and assumptionsL17–17
Work with arbitrary variables or the premises of the current implication.
- L17
intro hdiv
Original exact command ledger · 22 lines
- 0001
intro p - 0002
intro q - 0003
intro hp - 0004
intro hq - 0005
intro hpq - 0006
split - 0007
specialize distinct_primes_left_not_divide_right p - 0008
specialize distinct_primes_left_not_divide_right q - 0009
intro hdiv - 0010
apply distinct_primes_left_not_divide_right - 0011
exact hp - 0012
exact hq - 0013
exact hpq - 0014
exact hdiv - 0015
specialize distinct_primes_right_not_divide_left p - 0016
specialize distinct_primes_right_not_divide_left q - 0017
intro hdiv - 0018
apply distinct_primes_right_not_divide_left - 0019
exact hp - 0020
exact hq - 0021
exact hpq - 0022
exact hdiv