Metamath Proof Explorer

Theorem coprm

Description: A prime number either divides an integer or is coprime to it, but not both. Theorem 1.8 in ApostolNT p. 17. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion coprm 
|- ( ( P e. Prime /\ N e. ZZ ) -> ( -. P || N <-> ( P gcd N ) = 1 ) )

Proof

Step Hyp Ref Expression
1 prmz 
 |-  ( P e. Prime -> P e. ZZ )
2 gcddvds 
 |-  ( ( P e. ZZ /\ N e. ZZ ) -> ( ( P gcd N ) || P /\ ( P gcd N ) || N ) )
3 1 2 sylan 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( ( P gcd N ) || P /\ ( P gcd N ) || N ) )
4 3 simprd 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( P gcd N ) || N )
5 breq1 
 |-  ( ( P gcd N ) = P -> ( ( P gcd N ) || N <-> P || N ) )
6 4 5 syl5ibcom 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( ( P gcd N ) = P -> P || N ) )
7 6 con3d 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( -. P || N -> -. ( P gcd N ) = P ) )
8 0nnn 
 |-  -. 0 e. NN
9 prmnn 
 |-  ( P e. Prime -> P e. NN )
10 eleq1 
 |-  ( P = 0 -> ( P e. NN <-> 0 e. NN ) )
11 9 10 syl5ibcom 
 |-  ( P e. Prime -> ( P = 0 -> 0 e. NN ) )
12 8 11 mtoi 
 |-  ( P e. Prime -> -. P = 0 )
13 12 intnanrd 
 |-  ( P e. Prime -> -. ( P = 0 /\ N = 0 ) )
14 13 adantr 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> -. ( P = 0 /\ N = 0 ) )
15 gcdn0cl 
 |-  ( ( ( P e. ZZ /\ N e. ZZ ) /\ -. ( P = 0 /\ N = 0 ) ) -> ( P gcd N ) e. NN )
16 15 ex 
 |-  ( ( P e. ZZ /\ N e. ZZ ) -> ( -. ( P = 0 /\ N = 0 ) -> ( P gcd N ) e. NN ) )
17 1 16 sylan 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( -. ( P = 0 /\ N = 0 ) -> ( P gcd N ) e. NN ) )
18 14 17 mpd 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( P gcd N ) e. NN )
19 3 simpld 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( P gcd N ) || P )
20 isprm2 
 |-  ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. NN ( z || P -> ( z = 1 \/ z = P ) ) ) )
21 20 simprbi 
 |-  ( P e. Prime -> A. z e. NN ( z || P -> ( z = 1 \/ z = P ) ) )
22 breq1 
 |-  ( z = ( P gcd N ) -> ( z || P <-> ( P gcd N ) || P ) )
23 eqeq1 
 |-  ( z = ( P gcd N ) -> ( z = 1 <-> ( P gcd N ) = 1 ) )
24 eqeq1 
 |-  ( z = ( P gcd N ) -> ( z = P <-> ( P gcd N ) = P ) )
25 23 24 orbi12d 
 |-  ( z = ( P gcd N ) -> ( ( z = 1 \/ z = P ) <-> ( ( P gcd N ) = 1 \/ ( P gcd N ) = P ) ) )
26 22 25 imbi12d 
 |-  ( z = ( P gcd N ) -> ( ( z || P -> ( z = 1 \/ z = P ) ) <-> ( ( P gcd N ) || P -> ( ( P gcd N ) = 1 \/ ( P gcd N ) = P ) ) ) )
27 26 rspcv 
 |-  ( ( P gcd N ) e. NN -> ( A. z e. NN ( z || P -> ( z = 1 \/ z = P ) ) -> ( ( P gcd N ) || P -> ( ( P gcd N ) = 1 \/ ( P gcd N ) = P ) ) ) )
28 21 27 syl5com 
 |-  ( P e. Prime -> ( ( P gcd N ) e. NN -> ( ( P gcd N ) || P -> ( ( P gcd N ) = 1 \/ ( P gcd N ) = P ) ) ) )
29 28 adantr 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( ( P gcd N ) e. NN -> ( ( P gcd N ) || P -> ( ( P gcd N ) = 1 \/ ( P gcd N ) = P ) ) ) )
30 18 19 29 mp2d 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( ( P gcd N ) = 1 \/ ( P gcd N ) = P ) )
31 biorf 
 |-  ( -. ( P gcd N ) = P -> ( ( P gcd N ) = 1 <-> ( ( P gcd N ) = P \/ ( P gcd N ) = 1 ) ) )
32 orcom 
 |-  ( ( ( P gcd N ) = P \/ ( P gcd N ) = 1 ) <-> ( ( P gcd N ) = 1 \/ ( P gcd N ) = P ) )
33 31 32 bitrdi 
 |-  ( -. ( P gcd N ) = P -> ( ( P gcd N ) = 1 <-> ( ( P gcd N ) = 1 \/ ( P gcd N ) = P ) ) )
34 30 33 syl5ibrcom 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( -. ( P gcd N ) = P -> ( P gcd N ) = 1 ) )
35 7 34 syld 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( -. P || N -> ( P gcd N ) = 1 ) )
36 iddvds 
 |-  ( P e. ZZ -> P || P )
37 1 36 syl 
 |-  ( P e. Prime -> P || P )
38 37 adantr 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> P || P )
39 dvdslegcd 
 |-  ( ( ( P e. ZZ /\ P e. ZZ /\ N e. ZZ ) /\ -. ( P = 0 /\ N = 0 ) ) -> ( ( P || P /\ P || N ) -> P <_ ( P gcd N ) ) )
40 39 ex 
 |-  ( ( P e. ZZ /\ P e. ZZ /\ N e. ZZ ) -> ( -. ( P = 0 /\ N = 0 ) -> ( ( P || P /\ P || N ) -> P <_ ( P gcd N ) ) ) )
41 40 3anidm12 
 |-  ( ( P e. ZZ /\ N e. ZZ ) -> ( -. ( P = 0 /\ N = 0 ) -> ( ( P || P /\ P || N ) -> P <_ ( P gcd N ) ) ) )
42 1 41 sylan 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( -. ( P = 0 /\ N = 0 ) -> ( ( P || P /\ P || N ) -> P <_ ( P gcd N ) ) ) )
43 14 42 mpd 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( ( P || P /\ P || N ) -> P <_ ( P gcd N ) ) )
44 38 43 mpand 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( P || N -> P <_ ( P gcd N ) ) )
45 prmgt1 
 |-  ( P e. Prime -> 1 < P )
46 45 adantr 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> 1 < P )
47 1re 
 |-  1 e. RR
48 1 zred 
 |-  ( P e. Prime -> P e. RR )
49 18 nnred 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( P gcd N ) e. RR )
50 ltletr 
 |-  ( ( 1 e. RR /\ P e. RR /\ ( P gcd N ) e. RR ) -> ( ( 1 < P /\ P <_ ( P gcd N ) ) -> 1 < ( P gcd N ) ) )
51 47 48 49 50 mp3an2ani 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( ( 1 < P /\ P <_ ( P gcd N ) ) -> 1 < ( P gcd N ) ) )
52 46 51 mpand 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( P <_ ( P gcd N ) -> 1 < ( P gcd N ) ) )
53 ltne 
 |-  ( ( 1 e. RR /\ 1 < ( P gcd N ) ) -> ( P gcd N ) =/= 1 )
54 47 53 mpan 
 |-  ( 1 < ( P gcd N ) -> ( P gcd N ) =/= 1 )
55 54 a1i 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( 1 < ( P gcd N ) -> ( P gcd N ) =/= 1 ) )
56 44 52 55 3syld 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( P || N -> ( P gcd N ) =/= 1 ) )
57 56 necon2bd 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( ( P gcd N ) = 1 -> -. P || N ) )
58 35 57 impbid 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( -. P || N <-> ( P gcd N ) = 1 ) )