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))Structural proof guide
Generated structural guide
A prime cannot divide a distinct prime.
Use the direct prerequisites prime_divisor_eq_one_or_self as previously established PA formulas.
The proof proceeds by case analysis (2), intermediate claims (1).
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-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.
- 0001
intro p - 0002
intro q - 0003
intro hp - 0004
intro hq - 0005
intro hpq - 0006
intro hdiv - 0007
have hfactor : p = 1 \/ q = p - 0008
specialize prime_divisor_eq_one_or_self q - 0009
specialize prime_divisor_eq_one_or_self p - 0010
apply prime_divisor_eq_one_or_self - 0011
exact hq - 0012
exact hdiv - 0013
cases hfactor - 0014
cases hp - 0015
apply hp_left - 0016
exact hfactor_left - 0017
apply hpq - 0018
symm - 0019
exact hfactor_right