natural-prime

Entry	Value
Name	natural-prime_40
Conclusion	!p1 p2. prime p1 /\ prime p2 /\ divides p1 p2 ==> p1 = p2
Constructive Proof	Yes
Axiom	N\|A
Classical Lemmas	N\|A
Constructive Lemmas	T !t. F /\ t <=> F !t. (T <=> t) <=> t !t. T ==> t <=> t !t. t ==> F <=> ~t !t. t \/ t <=> t !p1 p2. prime p1 /\ prime p2 /\ divides p1 p2 ==> p1 = p2 F <=> (!p. p) T <=> (\p. p) = (\p. p) ~F <=> T ~T <=> F (~) = (\p. p ==> F) (/\) = (\p q. (\f. f p q) = (\f. f T T)) (==>) = (\p q. p /\ q <=> p) (\/) = (\p q. !r. (p ==> r) ==> (q ==> r) ==> r) (!) = (\p. p = (\x. T))
Contained Package	natural-prime
Comment	Natural-prime package from OpenTheory.