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-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
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