This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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