Metamath Proof Explorer

Theorem isprm3

Description: The predicate "is a prime number". A prime number is an integer greater than or equal to 2 with no divisors strictly between 1 and itself. (Contributed by Paul Chapman, 26-Oct-2012)

Ref Expression
Assertion isprm3 
|- ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. ( 2 ... ( P - 1 ) ) -. z || P ) )

Proof

Step Hyp Ref Expression
1 isprm2 
 |-  ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. NN ( z || P -> ( z = 1 \/ z = P ) ) ) )
2 iman 
 |-  ( ( z e. NN -> ( z = 1 \/ z = P ) ) <-> -. ( z e. NN /\ -. ( z = 1 \/ z = P ) ) )
3 eluz2nn 
 |-  ( P e. ( ZZ>= ` 2 ) -> P e. NN )
4 nnz 
 |-  ( z e. NN -> z e. ZZ )
5 dvdsle 
 |-  ( ( z e. ZZ /\ P e. NN ) -> ( z || P -> z <_ P ) )
6 4 5 sylan 
 |-  ( ( z e. NN /\ P e. NN ) -> ( z || P -> z <_ P ) )
7 nnge1 
 |-  ( z e. NN -> 1 <_ z )
8 7 adantr 
 |-  ( ( z e. NN /\ P e. NN ) -> 1 <_ z )
9 6 8 jctild 
 |-  ( ( z e. NN /\ P e. NN ) -> ( z || P -> ( 1 <_ z /\ z <_ P ) ) )
10 3 9 sylan2 
 |-  ( ( z e. NN /\ P e. ( ZZ>= ` 2 ) ) -> ( z || P -> ( 1 <_ z /\ z <_ P ) ) )
11 zre 
 |-  ( z e. ZZ -> z e. RR )
12 nnre 
 |-  ( P e. NN -> P e. RR )
13 1re 
 |-  1 e. RR
14 leltne 
 |-  ( ( 1 e. RR /\ z e. RR /\ 1 <_ z ) -> ( 1 < z <-> z =/= 1 ) )
15 13 14 mp3an1 
 |-  ( ( z e. RR /\ 1 <_ z ) -> ( 1 < z <-> z =/= 1 ) )
16 15 3adant2 
 |-  ( ( z e. RR /\ P e. RR /\ 1 <_ z ) -> ( 1 < z <-> z =/= 1 ) )
17 16 3expia 
 |-  ( ( z e. RR /\ P e. RR ) -> ( 1 <_ z -> ( 1 < z <-> z =/= 1 ) ) )
18 leltne 
 |-  ( ( z e. RR /\ P e. RR /\ z <_ P ) -> ( z < P <-> P =/= z ) )
19 18 3expia 
 |-  ( ( z e. RR /\ P e. RR ) -> ( z <_ P -> ( z < P <-> P =/= z ) ) )
20 17 19 anim12d 
 |-  ( ( z e. RR /\ P e. RR ) -> ( ( 1 <_ z /\ z <_ P ) -> ( ( 1 < z <-> z =/= 1 ) /\ ( z < P <-> P =/= z ) ) ) )
21 11 12 20 syl2an 
 |-  ( ( z e. ZZ /\ P e. NN ) -> ( ( 1 <_ z /\ z <_ P ) -> ( ( 1 < z <-> z =/= 1 ) /\ ( z < P <-> P =/= z ) ) ) )
22 pm4.38 
 |-  ( ( ( 1 < z <-> z =/= 1 ) /\ ( z < P <-> P =/= z ) ) -> ( ( 1 < z /\ z < P ) <-> ( z =/= 1 /\ P =/= z ) ) )
23 df-ne 
 |-  ( z =/= 1 <-> -. z = 1 )
24 nesym 
 |-  ( P =/= z <-> -. z = P )
25 23 24 anbi12i 
 |-  ( ( z =/= 1 /\ P =/= z ) <-> ( -. z = 1 /\ -. z = P ) )
26 ioran 
 |-  ( -. ( z = 1 \/ z = P ) <-> ( -. z = 1 /\ -. z = P ) )
27 25 26 bitr4i 
 |-  ( ( z =/= 1 /\ P =/= z ) <-> -. ( z = 1 \/ z = P ) )
28 22 27 bitrdi 
 |-  ( ( ( 1 < z <-> z =/= 1 ) /\ ( z < P <-> P =/= z ) ) -> ( ( 1 < z /\ z < P ) <-> -. ( z = 1 \/ z = P ) ) )
29 21 28 syl6 
 |-  ( ( z e. ZZ /\ P e. NN ) -> ( ( 1 <_ z /\ z <_ P ) -> ( ( 1 < z /\ z < P ) <-> -. ( z = 1 \/ z = P ) ) ) )
30 4 3 29 syl2an 
 |-  ( ( z e. NN /\ P e. ( ZZ>= ` 2 ) ) -> ( ( 1 <_ z /\ z <_ P ) -> ( ( 1 < z /\ z < P ) <-> -. ( z = 1 \/ z = P ) ) ) )
31 10 30 syld 
 |-  ( ( z e. NN /\ P e. ( ZZ>= ` 2 ) ) -> ( z || P -> ( ( 1 < z /\ z < P ) <-> -. ( z = 1 \/ z = P ) ) ) )
32 31 imp 
 |-  ( ( ( z e. NN /\ P e. ( ZZ>= ` 2 ) ) /\ z || P ) -> ( ( 1 < z /\ z < P ) <-> -. ( z = 1 \/ z = P ) ) )
33 eluzelz 
 |-  ( P e. ( ZZ>= ` 2 ) -> P e. ZZ )
34 1z 
 |-  1 e. ZZ
35 zltp1le 
 |-  ( ( 1 e. ZZ /\ z e. ZZ ) -> ( 1 < z <-> ( 1 + 1 ) <_ z ) )
36 34 35 mpan 
 |-  ( z e. ZZ -> ( 1 < z <-> ( 1 + 1 ) <_ z ) )
37 df-2 
 |-  2 = ( 1 + 1 )
38 37 breq1i 
 |-  ( 2 <_ z <-> ( 1 + 1 ) <_ z )
39 36 38 bitr4di 
 |-  ( z e. ZZ -> ( 1 < z <-> 2 <_ z ) )
40 39 adantr 
 |-  ( ( z e. ZZ /\ P e. ZZ ) -> ( 1 < z <-> 2 <_ z ) )
41 zltlem1 
 |-  ( ( z e. ZZ /\ P e. ZZ ) -> ( z < P <-> z <_ ( P - 1 ) ) )
42 40 41 anbi12d 
 |-  ( ( z e. ZZ /\ P e. ZZ ) -> ( ( 1 < z /\ z < P ) <-> ( 2 <_ z /\ z <_ ( P - 1 ) ) ) )
43 peano2zm 
 |-  ( P e. ZZ -> ( P - 1 ) e. ZZ )
44 2z 
 |-  2 e. ZZ
45 elfz 
 |-  ( ( z e. ZZ /\ 2 e. ZZ /\ ( P - 1 ) e. ZZ ) -> ( z e. ( 2 ... ( P - 1 ) ) <-> ( 2 <_ z /\ z <_ ( P - 1 ) ) ) )
46 44 45 mp3an2 
 |-  ( ( z e. ZZ /\ ( P - 1 ) e. ZZ ) -> ( z e. ( 2 ... ( P - 1 ) ) <-> ( 2 <_ z /\ z <_ ( P - 1 ) ) ) )
47 43 46 sylan2 
 |-  ( ( z e. ZZ /\ P e. ZZ ) -> ( z e. ( 2 ... ( P - 1 ) ) <-> ( 2 <_ z /\ z <_ ( P - 1 ) ) ) )
48 42 47 bitr4d 
 |-  ( ( z e. ZZ /\ P e. ZZ ) -> ( ( 1 < z /\ z < P ) <-> z e. ( 2 ... ( P - 1 ) ) ) )
49 4 33 48 syl2an 
 |-  ( ( z e. NN /\ P e. ( ZZ>= ` 2 ) ) -> ( ( 1 < z /\ z < P ) <-> z e. ( 2 ... ( P - 1 ) ) ) )
50 49 adantr 
 |-  ( ( ( z e. NN /\ P e. ( ZZ>= ` 2 ) ) /\ z || P ) -> ( ( 1 < z /\ z < P ) <-> z e. ( 2 ... ( P - 1 ) ) ) )
51 32 50 bitr3d 
 |-  ( ( ( z e. NN /\ P e. ( ZZ>= ` 2 ) ) /\ z || P ) -> ( -. ( z = 1 \/ z = P ) <-> z e. ( 2 ... ( P - 1 ) ) ) )
52 51 anasss 
 |-  ( ( z e. NN /\ ( P e. ( ZZ>= ` 2 ) /\ z || P ) ) -> ( -. ( z = 1 \/ z = P ) <-> z e. ( 2 ... ( P - 1 ) ) ) )
53 52 expcom 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ z || P ) -> ( z e. NN -> ( -. ( z = 1 \/ z = P ) <-> z e. ( 2 ... ( P - 1 ) ) ) ) )
54 53 pm5.32d 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ z || P ) -> ( ( z e. NN /\ -. ( z = 1 \/ z = P ) ) <-> ( z e. NN /\ z e. ( 2 ... ( P - 1 ) ) ) ) )
55 fzssuz 
 |-  ( 2 ... ( P - 1 ) ) C_ ( ZZ>= ` 2 )
56 2eluzge1 
 |-  2 e. ( ZZ>= ` 1 )
57 uzss 
 |-  ( 2 e. ( ZZ>= ` 1 ) -> ( ZZ>= ` 2 ) C_ ( ZZ>= ` 1 ) )
58 56 57 ax-mp 
 |-  ( ZZ>= ` 2 ) C_ ( ZZ>= ` 1 )
59 55 58 sstri 
 |-  ( 2 ... ( P - 1 ) ) C_ ( ZZ>= ` 1 )
60 nnuz 
 |-  NN = ( ZZ>= ` 1 )
61 59 60 sseqtrri 
 |-  ( 2 ... ( P - 1 ) ) C_ NN
62 61 sseli 
 |-  ( z e. ( 2 ... ( P - 1 ) ) -> z e. NN )
63 62 pm4.71ri 
 |-  ( z e. ( 2 ... ( P - 1 ) ) <-> ( z e. NN /\ z e. ( 2 ... ( P - 1 ) ) ) )
64 54 63 bitr4di 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ z || P ) -> ( ( z e. NN /\ -. ( z = 1 \/ z = P ) ) <-> z e. ( 2 ... ( P - 1 ) ) ) )
65 64 notbid 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ z || P ) -> ( -. ( z e. NN /\ -. ( z = 1 \/ z = P ) ) <-> -. z e. ( 2 ... ( P - 1 ) ) ) )
66 2 65 syl5bb 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ z || P ) -> ( ( z e. NN -> ( z = 1 \/ z = P ) ) <-> -. z e. ( 2 ... ( P - 1 ) ) ) )
67 66 pm5.74da 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( ( z || P -> ( z e. NN -> ( z = 1 \/ z = P ) ) ) <-> ( z || P -> -. z e. ( 2 ... ( P - 1 ) ) ) ) )
68 bi2.04 
 |-  ( ( z || P -> ( z e. NN -> ( z = 1 \/ z = P ) ) ) <-> ( z e. NN -> ( z || P -> ( z = 1 \/ z = P ) ) ) )
69 con2b 
 |-  ( ( z || P -> -. z e. ( 2 ... ( P - 1 ) ) ) <-> ( z e. ( 2 ... ( P - 1 ) ) -> -. z || P ) )
70 67 68 69 3bitr3g 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( ( z e. NN -> ( z || P -> ( z = 1 \/ z = P ) ) ) <-> ( z e. ( 2 ... ( P - 1 ) ) -> -. z || P ) ) )
71 70 ralbidv2 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( A. z e. NN ( z || P -> ( z = 1 \/ z = P ) ) <-> A. z e. ( 2 ... ( P - 1 ) ) -. z || P ) )
72 71 pm5.32i 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ A. z e. NN ( z || P -> ( z = 1 \/ z = P ) ) ) <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. ( 2 ... ( P - 1 ) ) -. z || P ) )
73 1 72 bitri 
 |-  ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. ( 2 ... ( P - 1 ) ) -. z || P ) )