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