Step |
Hyp |
Ref |
Expression |
1 |
|
hgt750lemc.n |
|- ( ph -> N e. NN ) |
2 |
|
hgt750lemd.0 |
|- ( ph -> ( ; 1 0 ^ ; 2 7 ) <_ N ) |
3 |
|
fzfid |
|- ( ph -> ( 1 ... N ) e. Fin ) |
4 |
|
diffi |
|- ( ( 1 ... N ) e. Fin -> ( ( 1 ... N ) \ Prime ) e. Fin ) |
5 |
3 4
|
syl |
|- ( ph -> ( ( 1 ... N ) \ Prime ) e. Fin ) |
6 |
|
vmaf |
|- Lam : NN --> RR |
7 |
6
|
a1i |
|- ( ( ph /\ i e. ( ( 1 ... N ) \ Prime ) ) -> Lam : NN --> RR ) |
8 |
|
fz1ssnn |
|- ( 1 ... N ) C_ NN |
9 |
8
|
a1i |
|- ( ph -> ( 1 ... N ) C_ NN ) |
10 |
9
|
ssdifssd |
|- ( ph -> ( ( 1 ... N ) \ Prime ) C_ NN ) |
11 |
10
|
sselda |
|- ( ( ph /\ i e. ( ( 1 ... N ) \ Prime ) ) -> i e. NN ) |
12 |
7 11
|
ffvelrnd |
|- ( ( ph /\ i e. ( ( 1 ... N ) \ Prime ) ) -> ( Lam ` i ) e. RR ) |
13 |
5 12
|
fsumrecl |
|- ( ph -> sum_ i e. ( ( 1 ... N ) \ Prime ) ( Lam ` i ) e. RR ) |
14 |
|
2rp |
|- 2 e. RR+ |
15 |
14
|
a1i |
|- ( ph -> 2 e. RR+ ) |
16 |
15
|
relogcld |
|- ( ph -> ( log ` 2 ) e. RR ) |
17 |
|
1nn0 |
|- 1 e. NN0 |
18 |
|
4re |
|- 4 e. RR |
19 |
|
2re |
|- 2 e. RR |
20 |
|
6re |
|- 6 e. RR |
21 |
20 19
|
pm3.2i |
|- ( 6 e. RR /\ 2 e. RR ) |
22 |
|
dp2cl |
|- ( ( 6 e. RR /\ 2 e. RR ) -> _ 6 2 e. RR ) |
23 |
21 22
|
ax-mp |
|- _ 6 2 e. RR |
24 |
19 23
|
pm3.2i |
|- ( 2 e. RR /\ _ 6 2 e. RR ) |
25 |
|
dp2cl |
|- ( ( 2 e. RR /\ _ 6 2 e. RR ) -> _ 2 _ 6 2 e. RR ) |
26 |
24 25
|
ax-mp |
|- _ 2 _ 6 2 e. RR |
27 |
18 26
|
pm3.2i |
|- ( 4 e. RR /\ _ 2 _ 6 2 e. RR ) |
28 |
|
dp2cl |
|- ( ( 4 e. RR /\ _ 2 _ 6 2 e. RR ) -> _ 4 _ 2 _ 6 2 e. RR ) |
29 |
27 28
|
ax-mp |
|- _ 4 _ 2 _ 6 2 e. RR |
30 |
|
dpcl |
|- ( ( 1 e. NN0 /\ _ 4 _ 2 _ 6 2 e. RR ) -> ( 1 . _ 4 _ 2 _ 6 2 ) e. RR ) |
31 |
17 29 30
|
mp2an |
|- ( 1 . _ 4 _ 2 _ 6 2 ) e. RR |
32 |
31
|
a1i |
|- ( ph -> ( 1 . _ 4 _ 2 _ 6 2 ) e. RR ) |
33 |
1
|
nnred |
|- ( ph -> N e. RR ) |
34 |
1
|
nnrpd |
|- ( ph -> N e. RR+ ) |
35 |
34
|
rpge0d |
|- ( ph -> 0 <_ N ) |
36 |
33 35
|
resqrtcld |
|- ( ph -> ( sqrt ` N ) e. RR ) |
37 |
32 36
|
remulcld |
|- ( ph -> ( ( 1 . _ 4 _ 2 _ 6 2 ) x. ( sqrt ` N ) ) e. RR ) |
38 |
|
0nn0 |
|- 0 e. NN0 |
39 |
|
0re |
|- 0 e. RR |
40 |
|
1re |
|- 1 e. RR |
41 |
39 40
|
pm3.2i |
|- ( 0 e. RR /\ 1 e. RR ) |
42 |
|
dp2cl |
|- ( ( 0 e. RR /\ 1 e. RR ) -> _ 0 1 e. RR ) |
43 |
41 42
|
ax-mp |
|- _ 0 1 e. RR |
44 |
39 43
|
pm3.2i |
|- ( 0 e. RR /\ _ 0 1 e. RR ) |
45 |
|
dp2cl |
|- ( ( 0 e. RR /\ _ 0 1 e. RR ) -> _ 0 _ 0 1 e. RR ) |
46 |
44 45
|
ax-mp |
|- _ 0 _ 0 1 e. RR |
47 |
39 46
|
pm3.2i |
|- ( 0 e. RR /\ _ 0 _ 0 1 e. RR ) |
48 |
|
dp2cl |
|- ( ( 0 e. RR /\ _ 0 _ 0 1 e. RR ) -> _ 0 _ 0 _ 0 1 e. RR ) |
49 |
47 48
|
ax-mp |
|- _ 0 _ 0 _ 0 1 e. RR |
50 |
|
dpcl |
|- ( ( 0 e. NN0 /\ _ 0 _ 0 _ 0 1 e. RR ) -> ( 0 . _ 0 _ 0 _ 0 1 ) e. RR ) |
51 |
38 49 50
|
mp2an |
|- ( 0 . _ 0 _ 0 _ 0 1 ) e. RR |
52 |
51
|
a1i |
|- ( ph -> ( 0 . _ 0 _ 0 _ 0 1 ) e. RR ) |
53 |
52 36
|
remulcld |
|- ( ph -> ( ( 0 . _ 0 _ 0 _ 0 1 ) x. ( sqrt ` N ) ) e. RR ) |
54 |
1
|
nnzd |
|- ( ph -> N e. ZZ ) |
55 |
|
chpvalz |
|- ( N e. ZZ -> ( psi ` N ) = sum_ i e. ( 1 ... N ) ( Lam ` i ) ) |
56 |
54 55
|
syl |
|- ( ph -> ( psi ` N ) = sum_ i e. ( 1 ... N ) ( Lam ` i ) ) |
57 |
|
chtvalz |
|- ( N e. ZZ -> ( theta ` N ) = sum_ i e. ( ( 1 ... N ) i^i Prime ) ( log ` i ) ) |
58 |
54 57
|
syl |
|- ( ph -> ( theta ` N ) = sum_ i e. ( ( 1 ... N ) i^i Prime ) ( log ` i ) ) |
59 |
|
inss2 |
|- ( ( 1 ... N ) i^i Prime ) C_ Prime |
60 |
59
|
a1i |
|- ( ph -> ( ( 1 ... N ) i^i Prime ) C_ Prime ) |
61 |
60
|
sselda |
|- ( ( ph /\ i e. ( ( 1 ... N ) i^i Prime ) ) -> i e. Prime ) |
62 |
|
vmaprm |
|- ( i e. Prime -> ( Lam ` i ) = ( log ` i ) ) |
63 |
61 62
|
syl |
|- ( ( ph /\ i e. ( ( 1 ... N ) i^i Prime ) ) -> ( Lam ` i ) = ( log ` i ) ) |
64 |
63
|
sumeq2dv |
|- ( ph -> sum_ i e. ( ( 1 ... N ) i^i Prime ) ( Lam ` i ) = sum_ i e. ( ( 1 ... N ) i^i Prime ) ( log ` i ) ) |
65 |
58 64
|
eqtr4d |
|- ( ph -> ( theta ` N ) = sum_ i e. ( ( 1 ... N ) i^i Prime ) ( Lam ` i ) ) |
66 |
56 65
|
oveq12d |
|- ( ph -> ( ( psi ` N ) - ( theta ` N ) ) = ( sum_ i e. ( 1 ... N ) ( Lam ` i ) - sum_ i e. ( ( 1 ... N ) i^i Prime ) ( Lam ` i ) ) ) |
67 |
|
infi |
|- ( ( 1 ... N ) e. Fin -> ( ( 1 ... N ) i^i Prime ) e. Fin ) |
68 |
3 67
|
syl |
|- ( ph -> ( ( 1 ... N ) i^i Prime ) e. Fin ) |
69 |
6
|
a1i |
|- ( ( ph /\ i e. ( ( 1 ... N ) i^i Prime ) ) -> Lam : NN --> RR ) |
70 |
|
inss1 |
|- ( ( 1 ... N ) i^i Prime ) C_ ( 1 ... N ) |
71 |
70 8
|
sstri |
|- ( ( 1 ... N ) i^i Prime ) C_ NN |
72 |
71
|
a1i |
|- ( ph -> ( ( 1 ... N ) i^i Prime ) C_ NN ) |
73 |
72
|
sselda |
|- ( ( ph /\ i e. ( ( 1 ... N ) i^i Prime ) ) -> i e. NN ) |
74 |
69 73
|
ffvelrnd |
|- ( ( ph /\ i e. ( ( 1 ... N ) i^i Prime ) ) -> ( Lam ` i ) e. RR ) |
75 |
74
|
recnd |
|- ( ( ph /\ i e. ( ( 1 ... N ) i^i Prime ) ) -> ( Lam ` i ) e. CC ) |
76 |
68 75
|
fsumcl |
|- ( ph -> sum_ i e. ( ( 1 ... N ) i^i Prime ) ( Lam ` i ) e. CC ) |
77 |
12
|
recnd |
|- ( ( ph /\ i e. ( ( 1 ... N ) \ Prime ) ) -> ( Lam ` i ) e. CC ) |
78 |
5 77
|
fsumcl |
|- ( ph -> sum_ i e. ( ( 1 ... N ) \ Prime ) ( Lam ` i ) e. CC ) |
79 |
|
inindif |
|- ( ( ( 1 ... N ) i^i Prime ) i^i ( ( 1 ... N ) \ Prime ) ) = (/) |
80 |
79
|
a1i |
|- ( ph -> ( ( ( 1 ... N ) i^i Prime ) i^i ( ( 1 ... N ) \ Prime ) ) = (/) ) |
81 |
|
inundif |
|- ( ( ( 1 ... N ) i^i Prime ) u. ( ( 1 ... N ) \ Prime ) ) = ( 1 ... N ) |
82 |
81
|
eqcomi |
|- ( 1 ... N ) = ( ( ( 1 ... N ) i^i Prime ) u. ( ( 1 ... N ) \ Prime ) ) |
83 |
82
|
a1i |
|- ( ph -> ( 1 ... N ) = ( ( ( 1 ... N ) i^i Prime ) u. ( ( 1 ... N ) \ Prime ) ) ) |
84 |
6
|
a1i |
|- ( ( ph /\ i e. ( 1 ... N ) ) -> Lam : NN --> RR ) |
85 |
9
|
sselda |
|- ( ( ph /\ i e. ( 1 ... N ) ) -> i e. NN ) |
86 |
84 85
|
ffvelrnd |
|- ( ( ph /\ i e. ( 1 ... N ) ) -> ( Lam ` i ) e. RR ) |
87 |
86
|
recnd |
|- ( ( ph /\ i e. ( 1 ... N ) ) -> ( Lam ` i ) e. CC ) |
88 |
80 83 3 87
|
fsumsplit |
|- ( ph -> sum_ i e. ( 1 ... N ) ( Lam ` i ) = ( sum_ i e. ( ( 1 ... N ) i^i Prime ) ( Lam ` i ) + sum_ i e. ( ( 1 ... N ) \ Prime ) ( Lam ` i ) ) ) |
89 |
76 78 88
|
mvrladdd |
|- ( ph -> ( sum_ i e. ( 1 ... N ) ( Lam ` i ) - sum_ i e. ( ( 1 ... N ) i^i Prime ) ( Lam ` i ) ) = sum_ i e. ( ( 1 ... N ) \ Prime ) ( Lam ` i ) ) |
90 |
66 89
|
eqtr2d |
|- ( ph -> sum_ i e. ( ( 1 ... N ) \ Prime ) ( Lam ` i ) = ( ( psi ` N ) - ( theta ` N ) ) ) |
91 |
|
fveq2 |
|- ( x = N -> ( psi ` x ) = ( psi ` N ) ) |
92 |
|
fveq2 |
|- ( x = N -> ( theta ` x ) = ( theta ` N ) ) |
93 |
91 92
|
oveq12d |
|- ( x = N -> ( ( psi ` x ) - ( theta ` x ) ) = ( ( psi ` N ) - ( theta ` N ) ) ) |
94 |
|
fveq2 |
|- ( x = N -> ( sqrt ` x ) = ( sqrt ` N ) ) |
95 |
94
|
oveq2d |
|- ( x = N -> ( ( 1 . _ 4 _ 2 _ 6 2 ) x. ( sqrt ` x ) ) = ( ( 1 . _ 4 _ 2 _ 6 2 ) x. ( sqrt ` N ) ) ) |
96 |
93 95
|
breq12d |
|- ( x = N -> ( ( ( psi ` x ) - ( theta ` x ) ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) x. ( sqrt ` x ) ) <-> ( ( psi ` N ) - ( theta ` N ) ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) x. ( sqrt ` N ) ) ) ) |
97 |
|
ax-ros336 |
|- A. x e. RR+ ( ( psi ` x ) - ( theta ` x ) ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) x. ( sqrt ` x ) ) |
98 |
97
|
a1i |
|- ( ph -> A. x e. RR+ ( ( psi ` x ) - ( theta ` x ) ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) x. ( sqrt ` x ) ) ) |
99 |
96 98 34
|
rspcdva |
|- ( ph -> ( ( psi ` N ) - ( theta ` N ) ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) x. ( sqrt ` N ) ) ) |
100 |
90 99
|
eqbrtrd |
|- ( ph -> sum_ i e. ( ( 1 ... N ) \ Prime ) ( Lam ` i ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) x. ( sqrt ` N ) ) ) |
101 |
40
|
a1i |
|- ( ph -> 1 e. RR ) |
102 |
|
log2le1 |
|- ( log ` 2 ) < 1 |
103 |
102
|
a1i |
|- ( ph -> ( log ` 2 ) < 1 ) |
104 |
|
10nn0 |
|- ; 1 0 e. NN0 |
105 |
|
7nn0 |
|- 7 e. NN0 |
106 |
104 105
|
nn0expcli |
|- ( ; 1 0 ^ 7 ) e. NN0 |
107 |
106
|
nn0rei |
|- ( ; 1 0 ^ 7 ) e. RR |
108 |
107
|
a1i |
|- ( ph -> ( ; 1 0 ^ 7 ) e. RR ) |
109 |
52 108
|
remulcld |
|- ( ph -> ( ( 0 . _ 0 _ 0 _ 0 1 ) x. ( ; 1 0 ^ 7 ) ) e. RR ) |
110 |
104
|
nn0rei |
|- ; 1 0 e. RR |
111 |
|
0z |
|- 0 e. ZZ |
112 |
|
3z |
|- 3 e. ZZ |
113 |
110 111 112
|
3pm3.2i |
|- ( ; 1 0 e. RR /\ 0 e. ZZ /\ 3 e. ZZ ) |
114 |
|
1lt10 |
|- 1 < ; 1 0 |
115 |
|
3pos |
|- 0 < 3 |
116 |
114 115
|
pm3.2i |
|- ( 1 < ; 1 0 /\ 0 < 3 ) |
117 |
|
ltexp2a |
|- ( ( ( ; 1 0 e. RR /\ 0 e. ZZ /\ 3 e. ZZ ) /\ ( 1 < ; 1 0 /\ 0 < 3 ) ) -> ( ; 1 0 ^ 0 ) < ( ; 1 0 ^ 3 ) ) |
118 |
113 116 117
|
mp2an |
|- ( ; 1 0 ^ 0 ) < ( ; 1 0 ^ 3 ) |
119 |
104
|
numexp0 |
|- ( ; 1 0 ^ 0 ) = 1 |
120 |
119
|
eqcomi |
|- 1 = ( ; 1 0 ^ 0 ) |
121 |
110
|
recni |
|- ; 1 0 e. CC |
122 |
|
10pos |
|- 0 < ; 1 0 |
123 |
39 122
|
gtneii |
|- ; 1 0 =/= 0 |
124 |
|
4z |
|- 4 e. ZZ |
125 |
|
expm1 |
|- ( ( ; 1 0 e. CC /\ ; 1 0 =/= 0 /\ 4 e. ZZ ) -> ( ; 1 0 ^ ( 4 - 1 ) ) = ( ( ; 1 0 ^ 4 ) / ; 1 0 ) ) |
126 |
121 123 124 125
|
mp3an |
|- ( ; 1 0 ^ ( 4 - 1 ) ) = ( ( ; 1 0 ^ 4 ) / ; 1 0 ) |
127 |
|
4m1e3 |
|- ( 4 - 1 ) = 3 |
128 |
127
|
oveq2i |
|- ( ; 1 0 ^ ( 4 - 1 ) ) = ( ; 1 0 ^ 3 ) |
129 |
|
4nn0 |
|- 4 e. NN0 |
130 |
104 129
|
nn0expcli |
|- ( ; 1 0 ^ 4 ) e. NN0 |
131 |
130
|
nn0cni |
|- ( ; 1 0 ^ 4 ) e. CC |
132 |
|
divrec2 |
|- ( ( ( ; 1 0 ^ 4 ) e. CC /\ ; 1 0 e. CC /\ ; 1 0 =/= 0 ) -> ( ( ; 1 0 ^ 4 ) / ; 1 0 ) = ( ( 1 / ; 1 0 ) x. ( ; 1 0 ^ 4 ) ) ) |
133 |
131 121 123 132
|
mp3an |
|- ( ( ; 1 0 ^ 4 ) / ; 1 0 ) = ( ( 1 / ; 1 0 ) x. ( ; 1 0 ^ 4 ) ) |
134 |
126 128 133
|
3eqtr3ri |
|- ( ( 1 / ; 1 0 ) x. ( ; 1 0 ^ 4 ) ) = ( ; 1 0 ^ 3 ) |
135 |
118 120 134
|
3brtr4i |
|- 1 < ( ( 1 / ; 1 0 ) x. ( ; 1 0 ^ 4 ) ) |
136 |
|
1rp |
|- 1 e. RR+ |
137 |
136
|
dp0h |
|- ( 0 . 1 ) = ( 1 / ; 1 0 ) |
138 |
137
|
oveq1i |
|- ( ( 0 . 1 ) x. ( ; 1 0 ^ 4 ) ) = ( ( 1 / ; 1 0 ) x. ( ; 1 0 ^ 4 ) ) |
139 |
135 138
|
breqtrri |
|- 1 < ( ( 0 . 1 ) x. ( ; 1 0 ^ 4 ) ) |
140 |
139
|
a1i |
|- ( ph -> 1 < ( ( 0 . 1 ) x. ( ; 1 0 ^ 4 ) ) ) |
141 |
|
4p1e5 |
|- ( 4 + 1 ) = 5 |
142 |
|
5nn0 |
|- 5 e. NN0 |
143 |
142
|
nn0zi |
|- 5 e. ZZ |
144 |
38 136 141 124 143
|
dpexpp1 |
|- ( ( 0 . 1 ) x. ( ; 1 0 ^ 4 ) ) = ( ( 0 . _ 0 1 ) x. ( ; 1 0 ^ 5 ) ) |
145 |
38 136
|
rpdp2cl |
|- _ 0 1 e. RR+ |
146 |
|
5p1e6 |
|- ( 5 + 1 ) = 6 |
147 |
|
6nn0 |
|- 6 e. NN0 |
148 |
147
|
nn0zi |
|- 6 e. ZZ |
149 |
38 145 146 143 148
|
dpexpp1 |
|- ( ( 0 . _ 0 1 ) x. ( ; 1 0 ^ 5 ) ) = ( ( 0 . _ 0 _ 0 1 ) x. ( ; 1 0 ^ 6 ) ) |
150 |
38 145
|
rpdp2cl |
|- _ 0 _ 0 1 e. RR+ |
151 |
|
6p1e7 |
|- ( 6 + 1 ) = 7 |
152 |
105
|
nn0zi |
|- 7 e. ZZ |
153 |
38 150 151 148 152
|
dpexpp1 |
|- ( ( 0 . _ 0 _ 0 1 ) x. ( ; 1 0 ^ 6 ) ) = ( ( 0 . _ 0 _ 0 _ 0 1 ) x. ( ; 1 0 ^ 7 ) ) |
154 |
144 149 153
|
3eqtrri |
|- ( ( 0 . _ 0 _ 0 _ 0 1 ) x. ( ; 1 0 ^ 7 ) ) = ( ( 0 . 1 ) x. ( ; 1 0 ^ 4 ) ) |
155 |
140 154
|
breqtrrdi |
|- ( ph -> 1 < ( ( 0 . _ 0 _ 0 _ 0 1 ) x. ( ; 1 0 ^ 7 ) ) ) |
156 |
38 150
|
rpdp2cl |
|- _ 0 _ 0 _ 0 1 e. RR+ |
157 |
38 156
|
rpdpcl |
|- ( 0 . _ 0 _ 0 _ 0 1 ) e. RR+ |
158 |
157
|
a1i |
|- ( ph -> ( 0 . _ 0 _ 0 _ 0 1 ) e. RR+ ) |
159 |
|
2nn0 |
|- 2 e. NN0 |
160 |
159 105
|
deccl |
|- ; 2 7 e. NN0 |
161 |
104 160
|
nn0expcli |
|- ( ; 1 0 ^ ; 2 7 ) e. NN0 |
162 |
161
|
nn0rei |
|- ( ; 1 0 ^ ; 2 7 ) e. RR |
163 |
162
|
a1i |
|- ( ph -> ( ; 1 0 ^ ; 2 7 ) e. RR ) |
164 |
161
|
nn0ge0i |
|- 0 <_ ( ; 1 0 ^ ; 2 7 ) |
165 |
164
|
a1i |
|- ( ph -> 0 <_ ( ; 1 0 ^ ; 2 7 ) ) |
166 |
163 165
|
resqrtcld |
|- ( ph -> ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) e. RR ) |
167 |
|
expmul |
|- ( ( ; 1 0 e. CC /\ 7 e. NN0 /\ 2 e. NN0 ) -> ( ; 1 0 ^ ( 7 x. 2 ) ) = ( ( ; 1 0 ^ 7 ) ^ 2 ) ) |
168 |
121 105 159 167
|
mp3an |
|- ( ; 1 0 ^ ( 7 x. 2 ) ) = ( ( ; 1 0 ^ 7 ) ^ 2 ) |
169 |
|
7t2e14 |
|- ( 7 x. 2 ) = ; 1 4 |
170 |
169
|
oveq2i |
|- ( ; 1 0 ^ ( 7 x. 2 ) ) = ( ; 1 0 ^ ; 1 4 ) |
171 |
168 170
|
eqtr3i |
|- ( ( ; 1 0 ^ 7 ) ^ 2 ) = ( ; 1 0 ^ ; 1 4 ) |
172 |
171
|
fveq2i |
|- ( sqrt ` ( ( ; 1 0 ^ 7 ) ^ 2 ) ) = ( sqrt ` ( ; 1 0 ^ ; 1 4 ) ) |
173 |
|
expgt0 |
|- ( ( ; 1 0 e. RR /\ 7 e. ZZ /\ 0 < ; 1 0 ) -> 0 < ( ; 1 0 ^ 7 ) ) |
174 |
110 152 122 173
|
mp3an |
|- 0 < ( ; 1 0 ^ 7 ) |
175 |
39 107 174
|
ltleii |
|- 0 <_ ( ; 1 0 ^ 7 ) |
176 |
|
sqrtsq |
|- ( ( ( ; 1 0 ^ 7 ) e. RR /\ 0 <_ ( ; 1 0 ^ 7 ) ) -> ( sqrt ` ( ( ; 1 0 ^ 7 ) ^ 2 ) ) = ( ; 1 0 ^ 7 ) ) |
177 |
107 175 176
|
mp2an |
|- ( sqrt ` ( ( ; 1 0 ^ 7 ) ^ 2 ) ) = ( ; 1 0 ^ 7 ) |
178 |
172 177
|
eqtr3i |
|- ( sqrt ` ( ; 1 0 ^ ; 1 4 ) ) = ( ; 1 0 ^ 7 ) |
179 |
17 129
|
deccl |
|- ; 1 4 e. NN0 |
180 |
179
|
nn0zi |
|- ; 1 4 e. ZZ |
181 |
160
|
nn0zi |
|- ; 2 7 e. ZZ |
182 |
110 180 181
|
3pm3.2i |
|- ( ; 1 0 e. RR /\ ; 1 4 e. ZZ /\ ; 2 7 e. ZZ ) |
183 |
|
4lt10 |
|- 4 < ; 1 0 |
184 |
|
1lt2 |
|- 1 < 2 |
185 |
17 159 129 105 183 184
|
decltc |
|- ; 1 4 < ; 2 7 |
186 |
114 185
|
pm3.2i |
|- ( 1 < ; 1 0 /\ ; 1 4 < ; 2 7 ) |
187 |
|
ltexp2a |
|- ( ( ( ; 1 0 e. RR /\ ; 1 4 e. ZZ /\ ; 2 7 e. ZZ ) /\ ( 1 < ; 1 0 /\ ; 1 4 < ; 2 7 ) ) -> ( ; 1 0 ^ ; 1 4 ) < ( ; 1 0 ^ ; 2 7 ) ) |
188 |
182 186 187
|
mp2an |
|- ( ; 1 0 ^ ; 1 4 ) < ( ; 1 0 ^ ; 2 7 ) |
189 |
104 179
|
nn0expcli |
|- ( ; 1 0 ^ ; 1 4 ) e. NN0 |
190 |
189
|
nn0rei |
|- ( ; 1 0 ^ ; 1 4 ) e. RR |
191 |
|
expgt0 |
|- ( ( ; 1 0 e. RR /\ ; 1 4 e. ZZ /\ 0 < ; 1 0 ) -> 0 < ( ; 1 0 ^ ; 1 4 ) ) |
192 |
110 180 122 191
|
mp3an |
|- 0 < ( ; 1 0 ^ ; 1 4 ) |
193 |
39 190 192
|
ltleii |
|- 0 <_ ( ; 1 0 ^ ; 1 4 ) |
194 |
190 193
|
pm3.2i |
|- ( ( ; 1 0 ^ ; 1 4 ) e. RR /\ 0 <_ ( ; 1 0 ^ ; 1 4 ) ) |
195 |
162 164
|
pm3.2i |
|- ( ( ; 1 0 ^ ; 2 7 ) e. RR /\ 0 <_ ( ; 1 0 ^ ; 2 7 ) ) |
196 |
|
sqrtlt |
|- ( ( ( ( ; 1 0 ^ ; 1 4 ) e. RR /\ 0 <_ ( ; 1 0 ^ ; 1 4 ) ) /\ ( ( ; 1 0 ^ ; 2 7 ) e. RR /\ 0 <_ ( ; 1 0 ^ ; 2 7 ) ) ) -> ( ( ; 1 0 ^ ; 1 4 ) < ( ; 1 0 ^ ; 2 7 ) <-> ( sqrt ` ( ; 1 0 ^ ; 1 4 ) ) < ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) ) |
197 |
194 195 196
|
mp2an |
|- ( ( ; 1 0 ^ ; 1 4 ) < ( ; 1 0 ^ ; 2 7 ) <-> ( sqrt ` ( ; 1 0 ^ ; 1 4 ) ) < ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) |
198 |
188 197
|
mpbi |
|- ( sqrt ` ( ; 1 0 ^ ; 1 4 ) ) < ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) |
199 |
178 198
|
eqbrtrri |
|- ( ; 1 0 ^ 7 ) < ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) |
200 |
199
|
a1i |
|- ( ph -> ( ; 1 0 ^ 7 ) < ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) |
201 |
163 165 33 35
|
sqrtled |
|- ( ph -> ( ( ; 1 0 ^ ; 2 7 ) <_ N <-> ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) <_ ( sqrt ` N ) ) ) |
202 |
2 201
|
mpbid |
|- ( ph -> ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) <_ ( sqrt ` N ) ) |
203 |
108 166 36 200 202
|
ltletrd |
|- ( ph -> ( ; 1 0 ^ 7 ) < ( sqrt ` N ) ) |
204 |
108 36 158 203
|
ltmul2dd |
|- ( ph -> ( ( 0 . _ 0 _ 0 _ 0 1 ) x. ( ; 1 0 ^ 7 ) ) < ( ( 0 . _ 0 _ 0 _ 0 1 ) x. ( sqrt ` N ) ) ) |
205 |
101 109 53 155 204
|
lttrd |
|- ( ph -> 1 < ( ( 0 . _ 0 _ 0 _ 0 1 ) x. ( sqrt ` N ) ) ) |
206 |
16 101 53 103 205
|
lttrd |
|- ( ph -> ( log ` 2 ) < ( ( 0 . _ 0 _ 0 _ 0 1 ) x. ( sqrt ` N ) ) ) |
207 |
13 16 37 53 100 206
|
lt2addd |
|- ( ph -> ( sum_ i e. ( ( 1 ... N ) \ Prime ) ( Lam ` i ) + ( log ` 2 ) ) < ( ( ( 1 . _ 4 _ 2 _ 6 2 ) x. ( sqrt ` N ) ) + ( ( 0 . _ 0 _ 0 _ 0 1 ) x. ( sqrt ` N ) ) ) ) |
208 |
|
nfv |
|- F/ i ph |
209 |
|
nfcv |
|- F/_ i ( log ` 2 ) |
210 |
|
2prm |
|- 2 e. Prime |
211 |
210
|
a1i |
|- ( ph -> 2 e. Prime ) |
212 |
|
elndif |
|- ( 2 e. Prime -> -. 2 e. ( ( 1 ... N ) \ Prime ) ) |
213 |
211 212
|
syl |
|- ( ph -> -. 2 e. ( ( 1 ... N ) \ Prime ) ) |
214 |
|
fveq2 |
|- ( i = 2 -> ( Lam ` i ) = ( Lam ` 2 ) ) |
215 |
|
vmaprm |
|- ( 2 e. Prime -> ( Lam ` 2 ) = ( log ` 2 ) ) |
216 |
210 215
|
ax-mp |
|- ( Lam ` 2 ) = ( log ` 2 ) |
217 |
214 216
|
eqtrdi |
|- ( i = 2 -> ( Lam ` i ) = ( log ` 2 ) ) |
218 |
|
2cnd |
|- ( ph -> 2 e. CC ) |
219 |
|
2ne0 |
|- 2 =/= 0 |
220 |
219
|
a1i |
|- ( ph -> 2 =/= 0 ) |
221 |
218 220
|
logcld |
|- ( ph -> ( log ` 2 ) e. CC ) |
222 |
208 209 5 211 213 77 217 221
|
fsumsplitsn |
|- ( ph -> sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) = ( sum_ i e. ( ( 1 ... N ) \ Prime ) ( Lam ` i ) + ( log ` 2 ) ) ) |
223 |
147 14
|
rpdp2cl |
|- _ 6 2 e. RR+ |
224 |
159 223
|
rpdp2cl |
|- _ 2 _ 6 2 e. RR+ |
225 |
|
3rp |
|- 3 e. RR+ |
226 |
147 225
|
rpdp2cl |
|- _ 6 3 e. RR+ |
227 |
159 226
|
rpdp2cl |
|- _ 2 _ 6 3 e. RR+ |
228 |
|
1p0e1 |
|- ( 1 + 0 ) = 1 |
229 |
|
4cn |
|- 4 e. CC |
230 |
229
|
addid1i |
|- ( 4 + 0 ) = 4 |
231 |
|
2cn |
|- 2 e. CC |
232 |
231
|
addid1i |
|- ( 2 + 0 ) = 2 |
233 |
|
3nn0 |
|- 3 e. NN0 |
234 |
|
eqid |
|- ; 6 2 = ; 6 2 |
235 |
|
eqid |
|- ; 0 1 = ; 0 1 |
236 |
|
6cn |
|- 6 e. CC |
237 |
236
|
addid1i |
|- ( 6 + 0 ) = 6 |
238 |
|
2p1e3 |
|- ( 2 + 1 ) = 3 |
239 |
147 159 38 17 234 235 237 238
|
decadd |
|- ( ; 6 2 + ; 0 1 ) = ; 6 3 |
240 |
147 159 38 17 147 233 239
|
dpadd |
|- ( ( 6 . 2 ) + ( 0 . 1 ) ) = ( 6 . 3 ) |
241 |
147 14 38 136 147 225 159 38 232 240
|
dpadd2 |
|- ( ( 2 . _ 6 2 ) + ( 0 . _ 0 1 ) ) = ( 2 . _ 6 3 ) |
242 |
159 223 38 145 159 226 129 38 230 241
|
dpadd2 |
|- ( ( 4 . _ 2 _ 6 2 ) + ( 0 . _ 0 _ 0 1 ) ) = ( 4 . _ 2 _ 6 3 ) |
243 |
129 224 38 150 129 227 17 38 228 242
|
dpadd2 |
|- ( ( 1 . _ 4 _ 2 _ 6 2 ) + ( 0 . _ 0 _ 0 _ 0 1 ) ) = ( 1 . _ 4 _ 2 _ 6 3 ) |
244 |
243
|
oveq1i |
|- ( ( ( 1 . _ 4 _ 2 _ 6 2 ) + ( 0 . _ 0 _ 0 _ 0 1 ) ) x. ( sqrt ` N ) ) = ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) |
245 |
32
|
recnd |
|- ( ph -> ( 1 . _ 4 _ 2 _ 6 2 ) e. CC ) |
246 |
52
|
recnd |
|- ( ph -> ( 0 . _ 0 _ 0 _ 0 1 ) e. CC ) |
247 |
36
|
recnd |
|- ( ph -> ( sqrt ` N ) e. CC ) |
248 |
245 246 247
|
adddird |
|- ( ph -> ( ( ( 1 . _ 4 _ 2 _ 6 2 ) + ( 0 . _ 0 _ 0 _ 0 1 ) ) x. ( sqrt ` N ) ) = ( ( ( 1 . _ 4 _ 2 _ 6 2 ) x. ( sqrt ` N ) ) + ( ( 0 . _ 0 _ 0 _ 0 1 ) x. ( sqrt ` N ) ) ) ) |
249 |
244 248
|
eqtr3id |
|- ( ph -> ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) = ( ( ( 1 . _ 4 _ 2 _ 6 2 ) x. ( sqrt ` N ) ) + ( ( 0 . _ 0 _ 0 _ 0 1 ) x. ( sqrt ` N ) ) ) ) |
250 |
207 222 249
|
3brtr4d |
|- ( ph -> sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) < ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) ) |