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_q_not_p. p = q * frm_factor_dpn_q_not_p))Structural proof guide
Generated structural guide
The reverse orientation is nondivisible as well.
Use the direct prerequisites distinct_primes_left_not_divide_right as previously established PA formulas.
The proof proceeds by 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
have hqp : ~(q = p) - 0007
intro h - 0008
apply hpq - 0009
symm - 0010
exact h - 0011
specialize distinct_primes_left_not_divide_right q - 0012
specialize distinct_primes_left_not_divide_right p - 0013
intro hdiv - 0014
apply distinct_primes_left_not_divide_right - 0015
exact hq - 0016
exact hp - 0017
exact hqp - 0018
exact hdiv