Metamath Proof Explorer

Theorem isprm5

Description: One need only check prime divisors of P up to sqrt P in order to ensure primality. (Contributed by Mario Carneiro, 18-Feb-2014)

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

Proof

Step Hyp Ref Expression
1 isprm4 
 |-  ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. ( ZZ>= ` 2 ) ( z || P -> z = P ) ) )
2 prmuz2 
 |-  ( z e. Prime -> z e. ( ZZ>= ` 2 ) )
3 2 a1i 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( z e. Prime -> z e. ( ZZ>= ` 2 ) ) )
4 eluz2gt1 
 |-  ( P e. ( ZZ>= ` 2 ) -> 1 < P )
5 eluzelre 
 |-  ( P e. ( ZZ>= ` 2 ) -> P e. RR )
6 eluz2nn 
 |-  ( P e. ( ZZ>= ` 2 ) -> P e. NN )
7 6 nngt0d 
 |-  ( P e. ( ZZ>= ` 2 ) -> 0 < P )
8 ltmulgt11 
 |-  ( ( P e. RR /\ P e. RR /\ 0 < P ) -> ( 1 < P <-> P < ( P x. P ) ) )
9 5 5 7 8 syl3anc 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( 1 < P <-> P < ( P x. P ) ) )
10 4 9 mpbid 
 |-  ( P e. ( ZZ>= ` 2 ) -> P < ( P x. P ) )
11 5 5 remulcld 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( P x. P ) e. RR )
12 5 11 ltnled 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( P < ( P x. P ) <-> -. ( P x. P ) <_ P ) )
13 10 12 mpbid 
 |-  ( P e. ( ZZ>= ` 2 ) -> -. ( P x. P ) <_ P )
14 oveq12 
 |-  ( ( z = P /\ z = P ) -> ( z x. z ) = ( P x. P ) )
15 14 anidms 
 |-  ( z = P -> ( z x. z ) = ( P x. P ) )
16 15 breq1d 
 |-  ( z = P -> ( ( z x. z ) <_ P <-> ( P x. P ) <_ P ) )
17 16 notbid 
 |-  ( z = P -> ( -. ( z x. z ) <_ P <-> -. ( P x. P ) <_ P ) )
18 13 17 syl5ibrcom 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( z = P -> -. ( z x. z ) <_ P ) )
19 18 imim2d 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( ( z || P -> z = P ) -> ( z || P -> -. ( z x. z ) <_ P ) ) )
20 con2 
 |-  ( ( z || P -> -. ( z x. z ) <_ P ) -> ( ( z x. z ) <_ P -> -. z || P ) )
21 19 20 syl6 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( ( z || P -> z = P ) -> ( ( z x. z ) <_ P -> -. z || P ) ) )
22 3 21 imim12d 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( ( z e. ( ZZ>= ` 2 ) -> ( z || P -> z = P ) ) -> ( z e. Prime -> ( ( z x. z ) <_ P -> -. z || P ) ) ) )
23 22 ralimdv2 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( A. z e. ( ZZ>= ` 2 ) ( z || P -> z = P ) -> A. z e. Prime ( ( z x. z ) <_ P -> -. z || P ) ) )
24 annim 
 |-  ( ( z || P /\ -. z = P ) <-> -. ( z || P -> z = P ) )
25 oveq12 
 |-  ( ( x = z /\ x = z ) -> ( x x. x ) = ( z x. z ) )
26 25 anidms 
 |-  ( x = z -> ( x x. x ) = ( z x. z ) )
27 26 breq1d 
 |-  ( x = z -> ( ( x x. x ) <_ P <-> ( z x. z ) <_ P ) )
28 breq1 
 |-  ( x = z -> ( x || P <-> z || P ) )
29 27 28 anbi12d 
 |-  ( x = z -> ( ( ( x x. x ) <_ P /\ x || P ) <-> ( ( z x. z ) <_ P /\ z || P ) ) )
30 29 rspcev 
 |-  ( ( z e. ( ZZ>= ` 2 ) /\ ( ( z x. z ) <_ P /\ z || P ) ) -> E. x e. ( ZZ>= ` 2 ) ( ( x x. x ) <_ P /\ x || P ) )
31 30 ancom2s 
 |-  ( ( z e. ( ZZ>= ` 2 ) /\ ( z || P /\ ( z x. z ) <_ P ) ) -> E. x e. ( ZZ>= ` 2 ) ( ( x x. x ) <_ P /\ x || P ) )
32 31 expr 
 |-  ( ( z e. ( ZZ>= ` 2 ) /\ z || P ) -> ( ( z x. z ) <_ P -> E. x e. ( ZZ>= ` 2 ) ( ( x x. x ) <_ P /\ x || P ) ) )
33 32 ad2ant2lr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( ( z x. z ) <_ P -> E. x e. ( ZZ>= ` 2 ) ( ( x x. x ) <_ P /\ x || P ) ) )
34 simprl 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> z || P )
35 eluzelz 
 |-  ( z e. ( ZZ>= ` 2 ) -> z e. ZZ )
36 35 ad2antlr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> z e. ZZ )
37 eluz2nn 
 |-  ( z e. ( ZZ>= ` 2 ) -> z e. NN )
38 37 ad2antlr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> z e. NN )
39 38 nnne0d 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> z =/= 0 )
40 eluzelz 
 |-  ( P e. ( ZZ>= ` 2 ) -> P e. ZZ )
41 40 ad2antrr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> P e. ZZ )
42 dvdsval2 
 |-  ( ( z e. ZZ /\ z =/= 0 /\ P e. ZZ ) -> ( z || P <-> ( P / z ) e. ZZ ) )
43 36 39 41 42 syl3anc 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( z || P <-> ( P / z ) e. ZZ ) )
44 34 43 mpbid 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( P / z ) e. ZZ )
45 eluzelre 
 |-  ( z e. ( ZZ>= ` 2 ) -> z e. RR )
46 45 ad2antlr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> z e. RR )
47 46 recnd 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> z e. CC )
48 47 mulid2d 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( 1 x. z ) = z )
49 5 ad2antrr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> P e. RR )
50 6 ad2antrr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> P e. NN )
51 dvdsle 
 |-  ( ( z e. ZZ /\ P e. NN ) -> ( z || P -> z <_ P ) )
52 51 imp 
 |-  ( ( ( z e. ZZ /\ P e. NN ) /\ z || P ) -> z <_ P )
53 36 50 34 52 syl21anc 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> z <_ P )
54 simprr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> -. z = P )
55 54 neqned 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> z =/= P )
56 55 necomd 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> P =/= z )
57 46 49 53 56 leneltd 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> z < P )
58 48 57 eqbrtrd 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( 1 x. z ) < P )
59 1red 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> 1 e. RR )
60 41 zred 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> P e. RR )
61 nnre 
 |-  ( z e. NN -> z e. RR )
62 nngt0 
 |-  ( z e. NN -> 0 < z )
63 61 62 jca 
 |-  ( z e. NN -> ( z e. RR /\ 0 < z ) )
64 38 63 syl 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( z e. RR /\ 0 < z ) )
65 ltmuldiv 
 |-  ( ( 1 e. RR /\ P e. RR /\ ( z e. RR /\ 0 < z ) ) -> ( ( 1 x. z ) < P <-> 1 < ( P / z ) ) )
66 59 60 64 65 syl3anc 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( ( 1 x. z ) < P <-> 1 < ( P / z ) ) )
67 58 66 mpbid 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> 1 < ( P / z ) )
68 eluz2b1 
 |-  ( ( P / z ) e. ( ZZ>= ` 2 ) <-> ( ( P / z ) e. ZZ /\ 1 < ( P / z ) ) )
69 44 67 68 sylanbrc 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( P / z ) e. ( ZZ>= ` 2 ) )
70 46 46 remulcld 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( z x. z ) e. RR )
71 38 38 nnmulcld 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( z x. z ) e. NN )
72 nnrp 
 |-  ( P e. NN -> P e. RR+ )
73 nnrp 
 |-  ( ( z x. z ) e. NN -> ( z x. z ) e. RR+ )
74 rpdivcl 
 |-  ( ( P e. RR+ /\ ( z x. z ) e. RR+ ) -> ( P / ( z x. z ) ) e. RR+ )
75 72 73 74 syl2an 
 |-  ( ( P e. NN /\ ( z x. z ) e. NN ) -> ( P / ( z x. z ) ) e. RR+ )
76 50 71 75 syl2anc 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( P / ( z x. z ) ) e. RR+ )
77 49 70 76 lemul1d 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( P <_ ( z x. z ) <-> ( P x. ( P / ( z x. z ) ) ) <_ ( ( z x. z ) x. ( P / ( z x. z ) ) ) ) )
78 49 recnd 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> P e. CC )
79 78 47 78 47 39 39 divmuldivd 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( ( P / z ) x. ( P / z ) ) = ( ( P x. P ) / ( z x. z ) ) )
80 71 nncnd 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( z x. z ) e. CC )
81 71 nnne0d 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( z x. z ) =/= 0 )
82 78 78 80 81 divassd 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( ( P x. P ) / ( z x. z ) ) = ( P x. ( P / ( z x. z ) ) ) )
83 79 82 eqtrd 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( ( P / z ) x. ( P / z ) ) = ( P x. ( P / ( z x. z ) ) ) )
84 78 80 81 divcan2d 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( ( z x. z ) x. ( P / ( z x. z ) ) ) = P )
85 84 eqcomd 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> P = ( ( z x. z ) x. ( P / ( z x. z ) ) ) )
86 83 85 breq12d 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( ( ( P / z ) x. ( P / z ) ) <_ P <-> ( P x. ( P / ( z x. z ) ) ) <_ ( ( z x. z ) x. ( P / ( z x. z ) ) ) ) )
87 77 86 bitr4d 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( P <_ ( z x. z ) <-> ( ( P / z ) x. ( P / z ) ) <_ P ) )
88 87 biimpd 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( P <_ ( z x. z ) -> ( ( P / z ) x. ( P / z ) ) <_ P ) )
89 78 47 39 divcan2d 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( z x. ( P / z ) ) = P )
90 dvds0lem 
 |-  ( ( ( z e. ZZ /\ ( P / z ) e. ZZ /\ P e. ZZ ) /\ ( z x. ( P / z ) ) = P ) -> ( P / z ) || P )
91 36 44 41 89 90 syl31anc 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( P / z ) || P )
92 88 91 jctird 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( P <_ ( z x. z ) -> ( ( ( P / z ) x. ( P / z ) ) <_ P /\ ( P / z ) || P ) ) )
93 oveq12 
 |-  ( ( x = ( P / z ) /\ x = ( P / z ) ) -> ( x x. x ) = ( ( P / z ) x. ( P / z ) ) )
94 93 anidms 
 |-  ( x = ( P / z ) -> ( x x. x ) = ( ( P / z ) x. ( P / z ) ) )
95 94 breq1d 
 |-  ( x = ( P / z ) -> ( ( x x. x ) <_ P <-> ( ( P / z ) x. ( P / z ) ) <_ P ) )
96 breq1 
 |-  ( x = ( P / z ) -> ( x || P <-> ( P / z ) || P ) )
97 95 96 anbi12d 
 |-  ( x = ( P / z ) -> ( ( ( x x. x ) <_ P /\ x || P ) <-> ( ( ( P / z ) x. ( P / z ) ) <_ P /\ ( P / z ) || P ) ) )
98 97 rspcev 
 |-  ( ( ( P / z ) e. ( ZZ>= ` 2 ) /\ ( ( ( P / z ) x. ( P / z ) ) <_ P /\ ( P / z ) || P ) ) -> E. x e. ( ZZ>= ` 2 ) ( ( x x. x ) <_ P /\ x || P ) )
99 69 92 98 syl6an 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( P <_ ( z x. z ) -> E. x e. ( ZZ>= ` 2 ) ( ( x x. x ) <_ P /\ x || P ) ) )
100 70 49 letrid 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> ( ( z x. z ) <_ P \/ P <_ ( z x. z ) ) )
101 33 99 100 mpjaod 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ ( z || P /\ -. z = P ) ) -> E. x e. ( ZZ>= ` 2 ) ( ( x x. x ) <_ P /\ x || P ) )
102 101 ex 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) -> ( ( z || P /\ -. z = P ) -> E. x e. ( ZZ>= ` 2 ) ( ( x x. x ) <_ P /\ x || P ) ) )
103 24 102 syl5bir 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) -> ( -. ( z || P -> z = P ) -> E. x e. ( ZZ>= ` 2 ) ( ( x x. x ) <_ P /\ x || P ) ) )
104 103 rexlimdva 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( E. z e. ( ZZ>= ` 2 ) -. ( z || P -> z = P ) -> E. x e. ( ZZ>= ` 2 ) ( ( x x. x ) <_ P /\ x || P ) ) )
105 prmz 
 |-  ( z e. Prime -> z e. ZZ )
106 105 ad2antrl 
 |-  ( ( ( ( P e. ( ZZ>= ` 2 ) /\ x e. ( ZZ>= ` 2 ) ) /\ ( ( x x. x ) <_ P /\ x || P ) ) /\ ( z e. Prime /\ z || x ) ) -> z e. ZZ )
107 106 zred 
 |-  ( ( ( ( P e. ( ZZ>= ` 2 ) /\ x e. ( ZZ>= ` 2 ) ) /\ ( ( x x. x ) <_ P /\ x || P ) ) /\ ( z e. Prime /\ z || x ) ) -> z e. RR )
108 107 107 remulcld 
 |-  ( ( ( ( P e. ( ZZ>= ` 2 ) /\ x e. ( ZZ>= ` 2 ) ) /\ ( ( x x. x ) <_ P /\ x || P ) ) /\ ( z e. Prime /\ z || x ) ) -> ( z x. z ) e. RR )
109 eluzelz 
 |-  ( x e. ( ZZ>= ` 2 ) -> x e. ZZ )
110 109 ad3antlr 
 |-  ( ( ( ( P e. ( ZZ>= ` 2 ) /\ x e. ( ZZ>= ` 2 ) ) /\ ( ( x x. x ) <_ P /\ x || P ) ) /\ ( z e. Prime /\ z || x ) ) -> x e. ZZ )
111 110 zred 
 |-  ( ( ( ( P e. ( ZZ>= ` 2 ) /\ x e. ( ZZ>= ` 2 ) ) /\ ( ( x x. x ) <_ P /\ x || P ) ) /\ ( z e. Prime /\ z || x ) ) -> x e. RR )
112 111 111 remulcld 
 |-  ( ( ( ( P e. ( ZZ>= ` 2 ) /\ x e. ( ZZ>= ` 2 ) ) /\ ( ( x x. x ) <_ P /\ x || P ) ) /\ ( z e. Prime /\ z || x ) ) -> ( x x. x ) e. RR )
113 40 ad3antrrr 
 |-  ( ( ( ( P e. ( ZZ>= ` 2 ) /\ x e. ( ZZ>= ` 2 ) ) /\ ( ( x x. x ) <_ P /\ x || P ) ) /\ ( z e. Prime /\ z || x ) ) -> P e. ZZ )
114 113 zred 
 |-  ( ( ( ( P e. ( ZZ>= ` 2 ) /\ x e. ( ZZ>= ` 2 ) ) /\ ( ( x x. x ) <_ P /\ x || P ) ) /\ ( z e. Prime /\ z || x ) ) -> P e. RR )
115 eluz2nn 
 |-  ( x e. ( ZZ>= ` 2 ) -> x e. NN )
116 115 ad3antlr 
 |-  ( ( ( ( P e. ( ZZ>= ` 2 ) /\ x e. ( ZZ>= ` 2 ) ) /\ ( ( x x. x ) <_ P /\ x || P ) ) /\ ( z e. Prime /\ z || x ) ) -> x e. NN )
117 simprr 
 |-  ( ( ( ( P e. ( ZZ>= ` 2 ) /\ x e. ( ZZ>= ` 2 ) ) /\ ( ( x x. x ) <_ P /\ x || P ) ) /\ ( z e. Prime /\ z || x ) ) -> z || x )
118 dvdsle 
 |-  ( ( z e. ZZ /\ x e. NN ) -> ( z || x -> z <_ x ) )
119 118 imp 
 |-  ( ( ( z e. ZZ /\ x e. NN ) /\ z || x ) -> z <_ x )
120 106 116 117 119 syl21anc 
 |-  ( ( ( ( P e. ( ZZ>= ` 2 ) /\ x e. ( ZZ>= ` 2 ) ) /\ ( ( x x. x ) <_ P /\ x || P ) ) /\ ( z e. Prime /\ z || x ) ) -> z <_ x )
121 eluzge2nn0 
 |-  ( z e. ( ZZ>= ` 2 ) -> z e. NN0 )
122 121 nn0ge0d 
 |-  ( z e. ( ZZ>= ` 2 ) -> 0 <_ z )
123 2 122 syl 
 |-  ( z e. Prime -> 0 <_ z )
124 123 ad2antrl 
 |-  ( ( ( ( P e. ( ZZ>= ` 2 ) /\ x e. ( ZZ>= ` 2 ) ) /\ ( ( x x. x ) <_ P /\ x || P ) ) /\ ( z e. Prime /\ z || x ) ) -> 0 <_ z )
125 nnnn0 
 |-  ( x e. NN -> x e. NN0 )
126 125 nn0ge0d 
 |-  ( x e. NN -> 0 <_ x )
127 116 126 syl 
 |-  ( ( ( ( P e. ( ZZ>= ` 2 ) /\ x e. ( ZZ>= ` 2 ) ) /\ ( ( x x. x ) <_ P /\ x || P ) ) /\ ( z e. Prime /\ z || x ) ) -> 0 <_ x )
128 le2msq 
 |-  ( ( ( z e. RR /\ 0 <_ z ) /\ ( x e. RR /\ 0 <_ x ) ) -> ( z <_ x <-> ( z x. z ) <_ ( x x. x ) ) )
129 107 124 111 127 128 syl22anc 
 |-  ( ( ( ( P e. ( ZZ>= ` 2 ) /\ x e. ( ZZ>= ` 2 ) ) /\ ( ( x x. x ) <_ P /\ x || P ) ) /\ ( z e. Prime /\ z || x ) ) -> ( z <_ x <-> ( z x. z ) <_ ( x x. x ) ) )
130 120 129 mpbid 
 |-  ( ( ( ( P e. ( ZZ>= ` 2 ) /\ x e. ( ZZ>= ` 2 ) ) /\ ( ( x x. x ) <_ P /\ x || P ) ) /\ ( z e. Prime /\ z || x ) ) -> ( z x. z ) <_ ( x x. x ) )
131 simplrl 
 |-  ( ( ( ( P e. ( ZZ>= ` 2 ) /\ x e. ( ZZ>= ` 2 ) ) /\ ( ( x x. x ) <_ P /\ x || P ) ) /\ ( z e. Prime /\ z || x ) ) -> ( x x. x ) <_ P )
132 108 112 114 130 131 letrd 
 |-  ( ( ( ( P e. ( ZZ>= ` 2 ) /\ x e. ( ZZ>= ` 2 ) ) /\ ( ( x x. x ) <_ P /\ x || P ) ) /\ ( z e. Prime /\ z || x ) ) -> ( z x. z ) <_ P )
133 simplrr 
 |-  ( ( ( ( P e. ( ZZ>= ` 2 ) /\ x e. ( ZZ>= ` 2 ) ) /\ ( ( x x. x ) <_ P /\ x || P ) ) /\ ( z e. Prime /\ z || x ) ) -> x || P )
134 106 110 113 117 133 dvdstrd 
 |-  ( ( ( ( P e. ( ZZ>= ` 2 ) /\ x e. ( ZZ>= ` 2 ) ) /\ ( ( x x. x ) <_ P /\ x || P ) ) /\ ( z e. Prime /\ z || x ) ) -> z || P )
135 132 134 jc 
 |-  ( ( ( ( P e. ( ZZ>= ` 2 ) /\ x e. ( ZZ>= ` 2 ) ) /\ ( ( x x. x ) <_ P /\ x || P ) ) /\ ( z e. Prime /\ z || x ) ) -> -. ( ( z x. z ) <_ P -> -. z || P ) )
136 exprmfct 
 |-  ( x e. ( ZZ>= ` 2 ) -> E. z e. Prime z || x )
137 136 ad2antlr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ x e. ( ZZ>= ` 2 ) ) /\ ( ( x x. x ) <_ P /\ x || P ) ) -> E. z e. Prime z || x )
138 135 137 reximddv 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ x e. ( ZZ>= ` 2 ) ) /\ ( ( x x. x ) <_ P /\ x || P ) ) -> E. z e. Prime -. ( ( z x. z ) <_ P -> -. z || P ) )
139 138 ex 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ x e. ( ZZ>= ` 2 ) ) -> ( ( ( x x. x ) <_ P /\ x || P ) -> E. z e. Prime -. ( ( z x. z ) <_ P -> -. z || P ) ) )
140 139 rexlimdva 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( E. x e. ( ZZ>= ` 2 ) ( ( x x. x ) <_ P /\ x || P ) -> E. z e. Prime -. ( ( z x. z ) <_ P -> -. z || P ) ) )
141 104 140 syld 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( E. z e. ( ZZ>= ` 2 ) -. ( z || P -> z = P ) -> E. z e. Prime -. ( ( z x. z ) <_ P -> -. z || P ) ) )
142 rexnal 
 |-  ( E. z e. ( ZZ>= ` 2 ) -. ( z || P -> z = P ) <-> -. A. z e. ( ZZ>= ` 2 ) ( z || P -> z = P ) )
143 rexnal 
 |-  ( E. z e. Prime -. ( ( z x. z ) <_ P -> -. z || P ) <-> -. A. z e. Prime ( ( z x. z ) <_ P -> -. z || P ) )
144 141 142 143 3imtr3g 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( -. A. z e. ( ZZ>= ` 2 ) ( z || P -> z = P ) -> -. A. z e. Prime ( ( z x. z ) <_ P -> -. z || P ) ) )
145 23 144 impcon4bid 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( A. z e. ( ZZ>= ` 2 ) ( z || P -> z = P ) <-> A. z e. Prime ( ( z x. z ) <_ P -> -. z || P ) ) )
146 prmnn 
 |-  ( z e. Prime -> z e. NN )
147 146 nncnd 
 |-  ( z e. Prime -> z e. CC )
148 147 sqvald 
 |-  ( z e. Prime -> ( z ^ 2 ) = ( z x. z ) )
149 148 breq1d 
 |-  ( z e. Prime -> ( ( z ^ 2 ) <_ P <-> ( z x. z ) <_ P ) )
150 149 imbi1d 
 |-  ( z e. Prime -> ( ( ( z ^ 2 ) <_ P -> -. z || P ) <-> ( ( z x. z ) <_ P -> -. z || P ) ) )
151 150 ralbiia 
 |-  ( A. z e. Prime ( ( z ^ 2 ) <_ P -> -. z || P ) <-> A. z e. Prime ( ( z x. z ) <_ P -> -. z || P ) )
152 145 151 bitr4di 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( A. z e. ( ZZ>= ` 2 ) ( z || P -> z = P ) <-> A. z e. Prime ( ( z ^ 2 ) <_ P -> -. z || P ) ) )
153 152 pm5.32i 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ A. z e. ( ZZ>= ` 2 ) ( z || P -> z = P ) ) <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. Prime ( ( z ^ 2 ) <_ P -> -. z || P ) ) )
154 1 153 bitri 
 |-  ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. Prime ( ( z ^ 2 ) <_ P -> -. z || P ) ) )