Metamath Proof Explorer

Theorem isprm6

Description: A number is prime iff it satisfies Euclid's lemma euclemma . (Contributed by Mario Carneiro, 6-Sep-2015)

Ref Expression
Assertion isprm6 
|- ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ A. x e. ZZ A. y e. ZZ ( P || ( x x. y ) -> ( P || x \/ P || y ) ) ) )

Proof

Step Hyp Ref Expression
1 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
2 euclemma 
 |-  ( ( P e. Prime /\ x e. ZZ /\ y e. ZZ ) -> ( P || ( x x. y ) <-> ( P || x \/ P || y ) ) )
3 2 3expb 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( P || ( x x. y ) <-> ( P || x \/ P || y ) ) )
4 3 biimpd 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( P || ( x x. y ) -> ( P || x \/ P || y ) ) )
5 4 ralrimivva 
 |-  ( P e. Prime -> A. x e. ZZ A. y e. ZZ ( P || ( x x. y ) -> ( P || x \/ P || y ) ) )
6 1 5 jca 
 |-  ( P e. Prime -> ( P e. ( ZZ>= ` 2 ) /\ A. x e. ZZ A. y e. ZZ ( P || ( x x. y ) -> ( P || x \/ P || y ) ) ) )
7 simpl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ A. x e. ZZ A. y e. ZZ ( P || ( x x. y ) -> ( P || x \/ P || y ) ) ) -> P e. ( ZZ>= ` 2 ) )
8 eluz2nn 
 |-  ( P e. ( ZZ>= ` 2 ) -> P e. NN )
9 8 adantr 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> P e. NN )
10 9 nnzd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> P e. ZZ )
11 iddvds 
 |-  ( P e. ZZ -> P || P )
12 10 11 syl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> P || P )
13 nncn 
 |-  ( P e. NN -> P e. CC )
14 9 13 syl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> P e. CC )
15 nncn 
 |-  ( z e. NN -> z e. CC )
16 15 ad2antrl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> z e. CC )
17 nnne0 
 |-  ( z e. NN -> z =/= 0 )
18 17 ad2antrl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> z =/= 0 )
19 14 16 18 divcan1d 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> ( ( P / z ) x. z ) = P )
20 12 19 breqtrrd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> P || ( ( P / z ) x. z ) )
21 20 adantr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) /\ A. x e. ZZ A. y e. ZZ ( P || ( x x. y ) -> ( P || x \/ P || y ) ) ) -> P || ( ( P / z ) x. z ) )
22 simprr 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> z || P )
23 simprl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> z e. NN )
24 nndivdvds 
 |-  ( ( P e. NN /\ z e. NN ) -> ( z || P <-> ( P / z ) e. NN ) )
25 9 23 24 syl2anc 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> ( z || P <-> ( P / z ) e. NN ) )
26 22 25 mpbid 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> ( P / z ) e. NN )
27 26 nnzd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> ( P / z ) e. ZZ )
28 nnz 
 |-  ( z e. NN -> z e. ZZ )
29 28 ad2antrl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> z e. ZZ )
30 27 29 jca 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> ( ( P / z ) e. ZZ /\ z e. ZZ ) )
31 oveq1 
 |-  ( x = ( P / z ) -> ( x x. y ) = ( ( P / z ) x. y ) )
32 31 breq2d 
 |-  ( x = ( P / z ) -> ( P || ( x x. y ) <-> P || ( ( P / z ) x. y ) ) )
33 breq2 
 |-  ( x = ( P / z ) -> ( P || x <-> P || ( P / z ) ) )
34 33 orbi1d 
 |-  ( x = ( P / z ) -> ( ( P || x \/ P || y ) <-> ( P || ( P / z ) \/ P || y ) ) )
35 32 34 imbi12d 
 |-  ( x = ( P / z ) -> ( ( P || ( x x. y ) -> ( P || x \/ P || y ) ) <-> ( P || ( ( P / z ) x. y ) -> ( P || ( P / z ) \/ P || y ) ) ) )
36 oveq2 
 |-  ( y = z -> ( ( P / z ) x. y ) = ( ( P / z ) x. z ) )
37 36 breq2d 
 |-  ( y = z -> ( P || ( ( P / z ) x. y ) <-> P || ( ( P / z ) x. z ) ) )
38 breq2 
 |-  ( y = z -> ( P || y <-> P || z ) )
39 38 orbi2d 
 |-  ( y = z -> ( ( P || ( P / z ) \/ P || y ) <-> ( P || ( P / z ) \/ P || z ) ) )
40 37 39 imbi12d 
 |-  ( y = z -> ( ( P || ( ( P / z ) x. y ) -> ( P || ( P / z ) \/ P || y ) ) <-> ( P || ( ( P / z ) x. z ) -> ( P || ( P / z ) \/ P || z ) ) ) )
41 35 40 rspc2va 
 |-  ( ( ( ( P / z ) e. ZZ /\ z e. ZZ ) /\ A. x e. ZZ A. y e. ZZ ( P || ( x x. y ) -> ( P || x \/ P || y ) ) ) -> ( P || ( ( P / z ) x. z ) -> ( P || ( P / z ) \/ P || z ) ) )
42 30 41 sylan 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) /\ A. x e. ZZ A. y e. ZZ ( P || ( x x. y ) -> ( P || x \/ P || y ) ) ) -> ( P || ( ( P / z ) x. z ) -> ( P || ( P / z ) \/ P || z ) ) )
43 21 42 mpd 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) /\ A. x e. ZZ A. y e. ZZ ( P || ( x x. y ) -> ( P || x \/ P || y ) ) ) -> ( P || ( P / z ) \/ P || z ) )
44 dvdsle 
 |-  ( ( P e. ZZ /\ ( P / z ) e. NN ) -> ( P || ( P / z ) -> P <_ ( P / z ) ) )
45 10 26 44 syl2anc 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> ( P || ( P / z ) -> P <_ ( P / z ) ) )
46 14 div1d 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> ( P / 1 ) = P )
47 46 breq1d 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> ( ( P / 1 ) <_ ( P / z ) <-> P <_ ( P / z ) ) )
48 45 47 sylibrd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> ( P || ( P / z ) -> ( P / 1 ) <_ ( P / z ) ) )
49 nnrp 
 |-  ( z e. NN -> z e. RR+ )
50 49 rpregt0d 
 |-  ( z e. NN -> ( z e. RR /\ 0 < z ) )
51 50 ad2antrl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> ( z e. RR /\ 0 < z ) )
52 1rp 
 |-  1 e. RR+
53 rpregt0 
 |-  ( 1 e. RR+ -> ( 1 e. RR /\ 0 < 1 ) )
54 52 53 mp1i 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> ( 1 e. RR /\ 0 < 1 ) )
55 nnrp 
 |-  ( P e. NN -> P e. RR+ )
56 9 55 syl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> P e. RR+ )
57 56 rpregt0d 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> ( P e. RR /\ 0 < P ) )
58 lediv2 
 |-  ( ( ( z e. RR /\ 0 < z ) /\ ( 1 e. RR /\ 0 < 1 ) /\ ( P e. RR /\ 0 < P ) ) -> ( z <_ 1 <-> ( P / 1 ) <_ ( P / z ) ) )
59 51 54 57 58 syl3anc 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> ( z <_ 1 <-> ( P / 1 ) <_ ( P / z ) ) )
60 48 59 sylibrd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> ( P || ( P / z ) -> z <_ 1 ) )
61 nnle1eq1 
 |-  ( z e. NN -> ( z <_ 1 <-> z = 1 ) )
62 61 ad2antrl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> ( z <_ 1 <-> z = 1 ) )
63 60 62 sylibd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> ( P || ( P / z ) -> z = 1 ) )
64 nnnn0 
 |-  ( z e. NN -> z e. NN0 )
65 64 ad2antrl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> z e. NN0 )
66 65 adantr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) /\ P || z ) -> z e. NN0 )
67 nnnn0 
 |-  ( P e. NN -> P e. NN0 )
68 9 67 syl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> P e. NN0 )
69 68 adantr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) /\ P || z ) -> P e. NN0 )
70 simplrr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) /\ P || z ) -> z || P )
71 simpr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) /\ P || z ) -> P || z )
72 dvdseq 
 |-  ( ( ( z e. NN0 /\ P e. NN0 ) /\ ( z || P /\ P || z ) ) -> z = P )
73 66 69 70 71 72 syl22anc 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) /\ P || z ) -> z = P )
74 73 ex 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> ( P || z -> z = P ) )
75 63 74 orim12d 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) -> ( ( P || ( P / z ) \/ P || z ) -> ( z = 1 \/ z = P ) ) )
76 75 imp 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) /\ ( P || ( P / z ) \/ P || z ) ) -> ( z = 1 \/ z = P ) )
77 43 76 syldan 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( z e. NN /\ z || P ) ) /\ A. x e. ZZ A. y e. ZZ ( P || ( x x. y ) -> ( P || x \/ P || y ) ) ) -> ( z = 1 \/ z = P ) )
78 77 an32s 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ A. x e. ZZ A. y e. ZZ ( P || ( x x. y ) -> ( P || x \/ P || y ) ) ) /\ ( z e. NN /\ z || P ) ) -> ( z = 1 \/ z = P ) )
79 78 expr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ A. x e. ZZ A. y e. ZZ ( P || ( x x. y ) -> ( P || x \/ P || y ) ) ) /\ z e. NN ) -> ( z || P -> ( z = 1 \/ z = P ) ) )
80 79 ralrimiva 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ A. x e. ZZ A. y e. ZZ ( P || ( x x. y ) -> ( P || x \/ P || y ) ) ) -> A. z e. NN ( z || P -> ( z = 1 \/ z = P ) ) )
81 isprm2 
 |-  ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. NN ( z || P -> ( z = 1 \/ z = P ) ) ) )
82 7 80 81 sylanbrc 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ A. x e. ZZ A. y e. ZZ ( P || ( x x. y ) -> ( P || x \/ P || y ) ) ) -> P e. Prime )
83 6 82 impbii 
 |-  ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ A. x e. ZZ A. y e. ZZ ( P || ( x x. y ) -> ( P || x \/ P || y ) ) ) )