Metamath Proof Explorer


Theorem hgt750leme

Description: An upper bound on the contribution of the non-prime terms in the Statement 7.50 of Helfgott p. 69. (Contributed by Thierry Arnoux, 29-Dec-2021)

Ref Expression
Hypotheses hgt750leme.o O = z | ¬ 2 z
hgt750leme.n φ N
hgt750leme.0 φ 10 27 N
hgt750leme.h φ H : 0 +∞
hgt750leme.k φ K : 0 +∞
hgt750leme.1 φ m K m 1.079955
hgt750leme.2 φ m H m 1.414
Assertion hgt750leme φ n repr 3 N O repr 3 N Λ n 0 H n 0 Λ n 1 K n 1 Λ n 2 K n 2 7.348 log N N N 2

Proof

Step Hyp Ref Expression
1 hgt750leme.o O = z | ¬ 2 z
2 hgt750leme.n φ N
3 hgt750leme.0 φ 10 27 N
4 hgt750leme.h φ H : 0 +∞
5 hgt750leme.k φ K : 0 +∞
6 hgt750leme.1 φ m K m 1.079955
7 hgt750leme.2 φ m H m 1.414
8 2 nnnn0d φ N 0
9 3nn0 3 0
10 9 a1i φ 3 0
11 ssidd φ
12 8 10 11 reprfi2 φ repr 3 N Fin
13 diffi repr 3 N Fin repr 3 N O repr 3 N Fin
14 12 13 syl φ repr 3 N O repr 3 N Fin
15 vmaf Λ :
16 15 a1i φ n repr 3 N O repr 3 N Λ :
17 ssidd φ n repr 3 N O repr 3 N
18 2 nnzd φ N
19 18 adantr φ n repr 3 N O repr 3 N N
20 9 a1i φ n repr 3 N O repr 3 N 3 0
21 simpr φ n repr 3 N O repr 3 N n repr 3 N O repr 3 N
22 21 eldifad φ n repr 3 N O repr 3 N n repr 3 N
23 17 19 20 22 reprf φ n repr 3 N O repr 3 N n : 0 ..^ 3
24 c0ex 0 V
25 24 tpid1 0 0 1 2
26 fzo0to3tp 0 ..^ 3 = 0 1 2
27 25 26 eleqtrri 0 0 ..^ 3
28 27 a1i φ n repr 3 N O repr 3 N 0 0 ..^ 3
29 23 28 ffvelrnd φ n repr 3 N O repr 3 N n 0
30 16 29 ffvelrnd φ n repr 3 N O repr 3 N Λ n 0
31 rge0ssre 0 +∞
32 4 adantr φ n repr 3 N O repr 3 N H : 0 +∞
33 32 29 ffvelrnd φ n repr 3 N O repr 3 N H n 0 0 +∞
34 31 33 sselid φ n repr 3 N O repr 3 N H n 0
35 30 34 remulcld φ n repr 3 N O repr 3 N Λ n 0 H n 0
36 1ex 1 V
37 36 tpid2 1 0 1 2
38 37 26 eleqtrri 1 0 ..^ 3
39 38 a1i φ n repr 3 N O repr 3 N 1 0 ..^ 3
40 23 39 ffvelrnd φ n repr 3 N O repr 3 N n 1
41 16 40 ffvelrnd φ n repr 3 N O repr 3 N Λ n 1
42 5 adantr φ n repr 3 N O repr 3 N K : 0 +∞
43 42 40 ffvelrnd φ n repr 3 N O repr 3 N K n 1 0 +∞
44 31 43 sselid φ n repr 3 N O repr 3 N K n 1
45 41 44 remulcld φ n repr 3 N O repr 3 N Λ n 1 K n 1
46 2ex 2 V
47 46 tpid3 2 0 1 2
48 47 26 eleqtrri 2 0 ..^ 3
49 48 a1i φ n repr 3 N O repr 3 N 2 0 ..^ 3
50 23 49 ffvelrnd φ n repr 3 N O repr 3 N n 2
51 16 50 ffvelrnd φ n repr 3 N O repr 3 N Λ n 2
52 42 50 ffvelrnd φ n repr 3 N O repr 3 N K n 2 0 +∞
53 31 52 sselid φ n repr 3 N O repr 3 N K n 2
54 51 53 remulcld φ n repr 3 N O repr 3 N Λ n 2 K n 2
55 45 54 remulcld φ n repr 3 N O repr 3 N Λ n 1 K n 1 Λ n 2 K n 2
56 35 55 remulcld φ n repr 3 N O repr 3 N Λ n 0 H n 0 Λ n 1 K n 1 Λ n 2 K n 2
57 14 56 fsumrecl φ n repr 3 N O repr 3 N Λ n 0 H n 0 Λ n 1 K n 1 Λ n 2 K n 2
58 3re 3
59 58 a1i φ 3
60 1nn0 1 0
61 0nn0 0 0
62 7nn0 7 0
63 9nn0 9 0
64 5nn0 5 0
65 5nn 5
66 nnrp 5 5 +
67 65 66 ax-mp 5 +
68 64 67 rpdp2cl 55 +
69 63 68 rpdp2cl 955 +
70 63 69 rpdp2cl 9955 +
71 62 70 rpdp2cl 79955 +
72 61 71 rpdp2cl 079955 +
73 60 72 rpdpcl 1.079955 +
74 73 a1i φ 1.079955 +
75 74 rpred φ 1.079955
76 75 resqcld φ 1.079955 2
77 4nn0 4 0
78 4nn 4
79 nnrp 4 4 +
80 78 79 ax-mp 4 +
81 60 80 rpdp2cl 14 +
82 77 81 rpdp2cl 414 +
83 60 82 rpdpcl 1.414 +
84 83 a1i φ 1.414 +
85 84 rpred φ 1.414
86 76 85 remulcld φ 1.079955 2 1.414
87 fveq1 d = c d 0 = c 0
88 87 eleq1d d = c d 0 O c 0 O
89 88 notbid d = c ¬ d 0 O ¬ c 0 O
90 89 cbvrabv d repr 3 N | ¬ d 0 O = c repr 3 N | ¬ c 0 O
91 90 ssrab3 d repr 3 N | ¬ d 0 O repr 3 N
92 ssfi repr 3 N Fin d repr 3 N | ¬ d 0 O repr 3 N d repr 3 N | ¬ d 0 O Fin
93 12 91 92 sylancl φ d repr 3 N | ¬ d 0 O Fin
94 15 a1i φ n d repr 3 N | ¬ d 0 O Λ :
95 ssidd φ n d repr 3 N | ¬ d 0 O
96 18 adantr φ n d repr 3 N | ¬ d 0 O N
97 9 a1i φ n d repr 3 N | ¬ d 0 O 3 0
98 91 a1i φ d repr 3 N | ¬ d 0 O repr 3 N
99 98 sselda φ n d repr 3 N | ¬ d 0 O n repr 3 N
100 95 96 97 99 reprf φ n d repr 3 N | ¬ d 0 O n : 0 ..^ 3
101 27 a1i φ n d repr 3 N | ¬ d 0 O 0 0 ..^ 3
102 100 101 ffvelrnd φ n d repr 3 N | ¬ d 0 O n 0
103 94 102 ffvelrnd φ n d repr 3 N | ¬ d 0 O Λ n 0
104 38 a1i φ n d repr 3 N | ¬ d 0 O 1 0 ..^ 3
105 100 104 ffvelrnd φ n d repr 3 N | ¬ d 0 O n 1
106 94 105 ffvelrnd φ n d repr 3 N | ¬ d 0 O Λ n 1
107 48 a1i φ n d repr 3 N | ¬ d 0 O 2 0 ..^ 3
108 100 107 ffvelrnd φ n d repr 3 N | ¬ d 0 O n 2
109 94 108 ffvelrnd φ n d repr 3 N | ¬ d 0 O Λ n 2
110 106 109 remulcld φ n d repr 3 N | ¬ d 0 O Λ n 1 Λ n 2
111 103 110 remulcld φ n d repr 3 N | ¬ d 0 O Λ n 0 Λ n 1 Λ n 2
112 93 111 fsumrecl φ n d repr 3 N | ¬ d 0 O Λ n 0 Λ n 1 Λ n 2
113 86 112 remulcld φ 1.079955 2 1.414 n d repr 3 N | ¬ d 0 O Λ n 0 Λ n 1 Λ n 2
114 59 113 remulcld φ 3 1.079955 2 1.414 n d repr 3 N | ¬ d 0 O Λ n 0 Λ n 1 Λ n 2
115 4re 4
116 8re 8
117 115 116 pm3.2i 4 8
118 dp2cl 4 8 48
119 117 118 ax-mp 48
120 58 119 pm3.2i 3 48
121 dp2cl 3 48 348
122 120 121 ax-mp 348
123 dpcl 7 0 348 7.348
124 62 122 123 mp2an 7.348
125 124 a1i φ 7.348
126 2 nnrpd φ N +
127 126 relogcld φ log N
128 2 nnred φ N
129 126 rpge0d φ 0 N
130 128 129 resqrtcld φ N
131 126 rpsqrtcld φ N +
132 131 rpne0d φ N 0
133 127 130 132 redivcld φ log N N
134 125 133 remulcld φ 7.348 log N N
135 128 resqcld φ N 2
136 134 135 remulcld φ 7.348 log N N N 2
137 0re 0
138 7re 7
139 9re 9
140 5re 5
141 140 140 pm3.2i 5 5
142 dp2cl 5 5 55
143 141 142 ax-mp 55
144 139 143 pm3.2i 9 55
145 dp2cl 9 55 955
146 144 145 ax-mp 955
147 139 146 pm3.2i 9 955
148 dp2cl 9 955 9955
149 147 148 ax-mp 9955
150 138 149 pm3.2i 7 9955
151 dp2cl 7 9955 79955
152 150 151 ax-mp 79955
153 137 152 pm3.2i 0 79955
154 dp2cl 0 79955 079955
155 153 154 ax-mp 079955
156 dpcl 1 0 079955 1.079955
157 60 155 156 mp2an 1.079955
158 157 a1i φ 1.079955
159 158 resqcld φ 1.079955 2
160 1re 1
161 160 115 pm3.2i 1 4
162 dp2cl 1 4 14
163 161 162 ax-mp 14
164 115 163 pm3.2i 4 14
165 dp2cl 4 14 414
166 164 165 ax-mp 414
167 dpcl 1 0 414 1.414
168 60 166 167 mp2an 1.414
169 168 a1i φ 1.414
170 159 169 remulcld φ 1.079955 2 1.414
171 41 51 remulcld φ n repr 3 N O repr 3 N Λ n 1 Λ n 2
172 30 171 remulcld φ n repr 3 N O repr 3 N Λ n 0 Λ n 1 Λ n 2
173 14 172 fsumrecl φ n repr 3 N O repr 3 N Λ n 0 Λ n 1 Λ n 2
174 170 173 remulcld φ 1.079955 2 1.414 n repr 3 N O repr 3 N Λ n 0 Λ n 1 Λ n 2
175 59 112 remulcld φ 3 n d repr 3 N | ¬ d 0 O Λ n 0 Λ n 1 Λ n 2
176 170 175 remulcld φ 1.079955 2 1.414 3 n d repr 3 N | ¬ d 0 O Λ n 0 Λ n 1 Λ n 2
177 14 158 169 4 5 29 40 50 6 7 hgt750lemf φ n repr 3 N O repr 3 N Λ n 0 H n 0 Λ n 1 K n 1 Λ n 2 K n 2 1.079955 2 1.414 n repr 3 N O repr 3 N Λ n 0 Λ n 1 Λ n 2
178 2re 2
179 178 a1i φ 2
180 10nn0 10 0
181 2nn0 2 0
182 181 62 deccl 27 0
183 180 182 nn0expcli 10 27 0
184 183 nn0rei 10 27
185 184 a1i φ 10 27
186 180 numexp1 10 1 = 10
187 180 nn0rei 10
188 186 187 eqeltri 10 1
189 188 a1i φ 10 1
190 1nn 1
191 2lt9 2 < 9
192 178 139 191 ltleii 2 9
193 190 61 181 192 declei 2 10
194 193 186 breqtrri 2 10 1
195 194 a1i φ 2 10 1
196 1z 1
197 182 nn0zi 27
198 187 196 197 3pm3.2i 10 1 27
199 1lt10 1 < 10
200 198 199 pm3.2i 10 1 27 1 < 10
201 2nn 2
202 1lt9 1 < 9
203 160 139 202 ltleii 1 9
204 201 62 60 203 declei 1 27
205 leexp2 10 1 27 1 < 10 1 27 10 1 10 27
206 205 biimpa 10 1 27 1 < 10 1 27 10 1 10 27
207 200 204 206 mp2an 10 1 10 27
208 207 a1i φ 10 1 10 27
209 179 189 185 195 208 letrd φ 2 10 27
210 179 185 128 209 3 letrd φ 2 N
211 eqid e c repr 3 N | ¬ c a O e if a = 0 I 0 ..^ 3 pmTrsp 0 ..^ 3 a 0 = e c repr 3 N | ¬ c a O e if a = 0 I 0 ..^ 3 pmTrsp 0 ..^ 3 a 0
212 1 2 210 90 211 hgt750lema φ n repr 3 N O repr 3 N Λ n 0 Λ n 1 Λ n 2 3 n d repr 3 N | ¬ d 0 O Λ n 0 Λ n 1 Λ n 2
213 2z 2
214 213 a1i φ 2
215 74 214 rpexpcld φ 1.079955 2 +
216 215 84 rpmulcld φ 1.079955 2 1.414 +
217 173 175 216 lemul2d φ n repr 3 N O repr 3 N Λ n 0 Λ n 1 Λ n 2 3 n d repr 3 N | ¬ d 0 O Λ n 0 Λ n 1 Λ n 2 1.079955 2 1.414 n repr 3 N O repr 3 N Λ n 0 Λ n 1 Λ n 2 1.079955 2 1.414 3 n d repr 3 N | ¬ d 0 O Λ n 0 Λ n 1 Λ n 2
218 212 217 mpbid φ 1.079955 2 1.414 n repr 3 N O repr 3 N Λ n 0 Λ n 1 Λ n 2 1.079955 2 1.414 3 n d repr 3 N | ¬ d 0 O Λ n 0 Λ n 1 Λ n 2
219 57 174 176 177 218 letrd φ n repr 3 N O repr 3 N Λ n 0 H n 0 Λ n 1 K n 1 Λ n 2 K n 2 1.079955 2 1.414 3 n d repr 3 N | ¬ d 0 O Λ n 0 Λ n 1 Λ n 2
220 158 recnd φ 1.079955
221 220 sqcld φ 1.079955 2
222 169 recnd φ 1.414
223 221 222 mulcld φ 1.079955 2 1.414
224 3cn 3
225 224 a1i φ 3
226 112 recnd φ n d repr 3 N | ¬ d 0 O Λ n 0 Λ n 1 Λ n 2
227 223 225 226 mul12d φ 1.079955 2 1.414 3 n d repr 3 N | ¬ d 0 O Λ n 0 Λ n 1 Λ n 2 = 3 1.079955 2 1.414 n d repr 3 N | ¬ d 0 O Λ n 0 Λ n 1 Λ n 2
228 219 227 breqtrd φ n repr 3 N O repr 3 N Λ n 0 H n 0 Λ n 1 K n 1 Λ n 2 K n 2 3 1.079955 2 1.414 n d repr 3 N | ¬ d 0 O Λ n 0 Λ n 1 Λ n 2
229 fzfi 1 N Fin
230 diffi 1 N Fin 1 N Fin
231 229 230 ax-mp 1 N Fin
232 snfi 2 Fin
233 unfi 1 N Fin 2 Fin 1 N 2 Fin
234 231 232 233 mp2an 1 N 2 Fin
235 234 a1i φ 1 N 2 Fin
236 15 a1i φ i 1 N 2 Λ :
237 fz1ssnn 1 N
238 237 a1i φ 1 N
239 238 ssdifssd φ 1 N
240 201 a1i φ 2
241 240 snssd φ 2
242 239 241 unssd φ 1 N 2
243 242 sselda φ i 1 N 2 i
244 236 243 ffvelrnd φ i 1 N 2 Λ i
245 235 244 fsumrecl φ i 1 N 2 Λ i
246 chpvalz N ψ N = j = 1 N Λ j
247 18 246 syl φ ψ N = j = 1 N Λ j
248 chpf ψ :
249 248 a1i φ ψ :
250 249 128 ffvelrnd φ ψ N
251 247 250 eqeltrrd φ j = 1 N Λ j
252 245 251 remulcld φ i 1 N 2 Λ i j = 1 N Λ j
253 127 252 remulcld φ log N i 1 N 2 Λ i j = 1 N Λ j
254 86 253 remulcld φ 1.079955 2 1.414 log N i 1 N 2 Λ i j = 1 N Λ j
255 59 254 remulcld φ 3 1.079955 2 1.414 log N i 1 N 2 Λ i j = 1 N Λ j
256 1 2 210 90 hgt750lemb φ n d repr 3 N | ¬ d 0 O Λ n 0 Λ n 1 Λ n 2 log N i 1 N 2 Λ i j = 1 N Λ j
257 112 253 216 lemul2d φ n d repr 3 N | ¬ d 0 O Λ n 0 Λ n 1 Λ n 2 log N i 1 N 2 Λ i j = 1 N Λ j 1.079955 2 1.414 n d repr 3 N | ¬ d 0 O Λ n 0 Λ n 1 Λ n 2 1.079955 2 1.414 log N i 1 N 2 Λ i j = 1 N Λ j
258 256 257 mpbid φ 1.079955 2 1.414 n d repr 3 N | ¬ d 0 O Λ n 0 Λ n 1 Λ n 2 1.079955 2 1.414 log N i 1 N 2 Λ i j = 1 N Λ j
259 3rp 3 +
260 259 a1i φ 3 +
261 113 254 260 lemul2d φ 1.079955 2 1.414 n d repr 3 N | ¬ d 0 O Λ n 0 Λ n 1 Λ n 2 1.079955 2 1.414 log N i 1 N 2 Λ i j = 1 N Λ j 3 1.079955 2 1.414 n d repr 3 N | ¬ d 0 O Λ n 0 Λ n 1 Λ n 2 3 1.079955 2 1.414 log N i 1 N 2 Λ i j = 1 N Λ j
262 258 261 mpbid φ 3 1.079955 2 1.414 n d repr 3 N | ¬ d 0 O Λ n 0 Λ n 1 Λ n 2 3 1.079955 2 1.414 log N i 1 N 2 Λ i j = 1 N Λ j
263 6re 6
264 263 58 pm3.2i 6 3
265 dp2cl 6 3 63
266 264 265 ax-mp 63
267 178 266 pm3.2i 2 63
268 dp2cl 2 63 263
269 267 268 ax-mp 263
270 115 269 pm3.2i 4 263
271 dp2cl 4 263 4263
272 270 271 ax-mp 4263
273 dpcl 1 0 4263 1.4263
274 60 272 273 mp2an 1.4263
275 274 a1i φ 1.4263
276 275 130 remulcld φ 1.4263 N
277 116 58 pm3.2i 8 3
278 dp2cl 8 3 83
279 277 278 ax-mp 83
280 116 279 pm3.2i 8 83
281 dp2cl 8 83 883
282 280 281 ax-mp 883
283 58 282 pm3.2i 3 883
284 dp2cl 3 883 3883
285 283 284 ax-mp 3883
286 137 285 pm3.2i 0 3883
287 dp2cl 0 3883 03883
288 286 287 ax-mp 03883
289 dpcl 1 0 03883 1.03883
290 60 288 289 mp2an 1.03883
291 290 a1i φ 1.03883
292 291 128 remulcld φ 1.03883 N
293 276 292 remulcld φ 1.4263 N 1.03883 N
294 127 293 remulcld φ log N 1.4263 N 1.03883 N
295 86 294 remulcld φ 1.079955 2 1.414 log N 1.4263 N 1.03883 N
296 59 295 remulcld φ 3 1.079955 2 1.414 log N 1.4263 N 1.03883 N
297 vmage0 i 0 Λ i
298 243 297 syl φ i 1 N 2 0 Λ i
299 235 244 298 fsumge0 φ 0 i 1 N 2 Λ i
300 2 3 hgt750lemd φ i 1 N 2 Λ i < 1.4263 N
301 fzfid φ 1 N Fin
302 15 a1i φ j 1 N Λ :
303 238 sselda φ j 1 N j
304 302 303 ffvelrnd φ j 1 N Λ j
305 vmage0 j 0 Λ j
306 303 305 syl φ j 1 N 0 Λ j
307 301 304 306 fsumge0 φ 0 j = 1 N Λ j
308 2 hgt750lemc φ j = 1 N Λ j < 1.03883 N
309 245 276 251 292 299 300 307 308 ltmul12ad φ i 1 N 2 Λ i j = 1 N Λ j < 1.4263 N 1.03883 N
310 252 293 309 ltled φ i 1 N 2 Λ i j = 1 N Λ j 1.4263 N 1.03883 N
311 160 a1i φ 1
312 1lt2 1 < 2
313 312 a1i φ 1 < 2
314 311 179 128 313 210 ltletrd φ 1 < N
315 128 314 rplogcld φ log N +
316 252 293 315 lemul2d φ i 1 N 2 Λ i j = 1 N Λ j 1.4263 N 1.03883 N log N i 1 N 2 Λ i j = 1 N Λ j log N 1.4263 N 1.03883 N
317 310 316 mpbid φ log N i 1 N 2 Λ i j = 1 N Λ j log N 1.4263 N 1.03883 N
318 253 294 216 lemul2d φ log N i 1 N 2 Λ i j = 1 N Λ j log N 1.4263 N 1.03883 N 1.079955 2 1.414 log N i 1 N 2 Λ i j = 1 N Λ j 1.079955 2 1.414 log N 1.4263 N 1.03883 N
319 317 318 mpbid φ 1.079955 2 1.414 log N i 1 N 2 Λ i j = 1 N Λ j 1.079955 2 1.414 log N 1.4263 N 1.03883 N
320 254 295 260 lemul2d φ 1.079955 2 1.414 log N i 1 N 2 Λ i j = 1 N Λ j 1.079955 2 1.414 log N 1.4263 N 1.03883 N 3 1.079955 2 1.414 log N i 1 N 2 Λ i j = 1 N Λ j 3 1.079955 2 1.414 log N 1.4263 N 1.03883 N
321 319 320 mpbid φ 3 1.079955 2 1.414 log N i 1 N 2 Λ i j = 1 N Λ j 3 1.079955 2 1.414 log N 1.4263 N 1.03883 N
322 157 resqcli 1.079955 2
323 322 168 remulcli 1.079955 2 1.414
324 274 290 remulcli 1.4263 1.03883
325 323 324 remulcli 1.079955 2 1.414 1.4263 1.03883
326 58 325 remulcli 3 1.079955 2 1.414 1.4263 1.03883
327 hgt750lem2 3 1.079955 2 1.414 1.4263 1.03883 < 7.348
328 326 124 327 ltleii 3 1.079955 2 1.414 1.4263 1.03883 7.348
329 326 a1i φ 3 1.079955 2 1.414 1.4263 1.03883
330 315 131 rpdivcld φ log N N +
331 126 214 rpexpcld φ N 2 +
332 330 331 rpmulcld φ log N N N 2 +
333 329 125 332 lemul1d φ 3 1.079955 2 1.414 1.4263 1.03883 7.348 3 1.079955 2 1.414 1.4263 1.03883 log N N N 2 7.348 log N N N 2
334 328 333 mpbii φ 3 1.079955 2 1.414 1.4263 1.03883 log N N N 2 7.348 log N N N 2
335 275 recnd φ 1.4263
336 130 recnd φ N
337 291 recnd φ 1.03883
338 128 recnd φ N
339 335 336 337 338 mul4d φ 1.4263 N 1.03883 N = 1.4263 1.03883 N N
340 339 oveq2d φ log N 1.4263 N 1.03883 N = log N 1.4263 1.03883 N N
341 127 recnd φ log N
342 335 337 mulcld φ 1.4263 1.03883
343 336 338 mulcld φ N N
344 342 343 mulcld φ 1.4263 1.03883 N N
345 341 344 mulcomd φ log N 1.4263 1.03883 N N = 1.4263 1.03883 N N log N
346 340 345 eqtrd φ log N 1.4263 N 1.03883 N = 1.4263 1.03883 N N log N
347 342 343 341 mulassd φ 1.4263 1.03883 N N log N = 1.4263 1.03883 N N log N
348 346 347 eqtrd φ log N 1.4263 N 1.03883 N = 1.4263 1.03883 N N log N
349 348 oveq2d φ 1.079955 2 1.414 log N 1.4263 N 1.03883 N = 1.079955 2 1.414 1.4263 1.03883 N N log N
350 86 recnd φ 1.079955 2 1.414
351 343 341 mulcld φ N N log N
352 350 342 351 mulassd φ 1.079955 2 1.414 1.4263 1.03883 N N log N = 1.079955 2 1.414 1.4263 1.03883 N N log N
353 349 352 eqtr4d φ 1.079955 2 1.414 log N 1.4263 N 1.03883 N = 1.079955 2 1.414 1.4263 1.03883 N N log N
354 353 oveq2d φ 3 1.079955 2 1.414 log N 1.4263 N 1.03883 N = 3 1.079955 2 1.414 1.4263 1.03883 N N log N
355 59 recnd φ 3
356 350 342 mulcld φ 1.079955 2 1.414 1.4263 1.03883
357 355 356 351 mulassd φ 3 1.079955 2 1.414 1.4263 1.03883 N N log N = 3 1.079955 2 1.414 1.4263 1.03883 N N log N
358 354 357 eqtr4d φ 3 1.079955 2 1.414 log N 1.4263 N 1.03883 N = 3 1.079955 2 1.414 1.4263 1.03883 N N log N
359 135 recnd φ N 2
360 341 336 359 132 div32d φ log N N N 2 = log N N 2 N
361 359 336 132 divcld φ N 2 N
362 341 361 mulcomd φ log N N 2 N = N 2 N log N
363 338 sqvald φ N 2 = N N
364 363 oveq1d φ N 2 N = N N N
365 338 338 336 132 divassd φ N N N = N N N
366 divsqrtid N + N N = N
367 126 366 syl φ N N = N
368 367 oveq2d φ N N N = N N
369 364 365 368 3eqtrd φ N 2 N = N N
370 338 336 mulcomd φ N N = N N
371 369 370 eqtrd φ N 2 N = N N
372 371 oveq1d φ N 2 N log N = N N log N
373 360 362 372 3eqtrrd φ N N log N = log N N N 2
374 373 oveq2d φ 3 1.079955 2 1.414 1.4263 1.03883 N N log N = 3 1.079955 2 1.414 1.4263 1.03883 log N N N 2
375 358 374 eqtrd φ 3 1.079955 2 1.414 log N 1.4263 N 1.03883 N = 3 1.079955 2 1.414 1.4263 1.03883 log N N N 2
376 125 recnd φ 7.348
377 133 recnd φ log N N
378 376 377 359 mulassd φ 7.348 log N N N 2 = 7.348 log N N N 2
379 334 375 378 3brtr4d φ 3 1.079955 2 1.414 log N 1.4263 N 1.03883 N 7.348 log N N N 2
380 255 296 136 321 379 letrd φ 3 1.079955 2 1.414 log N i 1 N 2 Λ i j = 1 N Λ j 7.348 log N N N 2
381 114 255 136 262 380 letrd φ 3 1.079955 2 1.414 n d repr 3 N | ¬ d 0 O Λ n 0 Λ n 1 Λ n 2 7.348 log N N N 2
382 57 114 136 228 381 letrd φ n repr 3 N O repr 3 N Λ n 0 H n 0 Λ n 1 K n 1 Λ n 2 K n 2 7.348 log N N N 2