Theorem prmrp

Description: Unequal prime numbers are relatively prime. (Contributed by Mario Carneiro, 23-Feb-2014)

	Ref	Expression
Assertion	prmrp	|- ( ( P e. Prime /\ Q e. Prime ) -> ( ( P gcd Q ) = 1 <-> P =/= Q ) )

Proof

Step	Hyp	Ref	Expression
1		prmz	|- ( Q e. Prime -> Q e. ZZ )
2		coprm	|- ( ( P e. Prime /\ Q e. ZZ ) -> ( -. P || Q <-> ( P gcd Q ) = 1 ) )
3	1 2	sylan2	|- ( ( P e. Prime /\ Q e. Prime ) -> ( -. P || Q <-> ( P gcd Q ) = 1 ) )
4		prmuz2	|- ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
5		dvdsprm	|- ( ( P e. ( ZZ>= ` 2 ) /\ Q e. Prime ) -> ( P || Q <-> P = Q ) )
6	4 5	sylan	|- ( ( P e. Prime /\ Q e. Prime ) -> ( P || Q <-> P = Q ) )
7	6	necon3bbid	|- ( ( P e. Prime /\ Q e. Prime ) -> ( -. P || Q <-> P =/= Q ) )
8	3 7	bitr3d	|- ( ( P e. Prime /\ Q e. Prime ) -> ( ( P gcd Q ) = 1 <-> P =/= Q ) )