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