Metamath Proof Explorer


Theorem bposlem9

Description: Lemma for bpos . Derive a contradiction. (Contributed by Mario Carneiro, 14-Mar-2014) (Proof shortened by AV, 15-Sep-2021)

Ref Expression
Hypotheses bposlem7.1 F = n 2 G n + 9 4 G n 2 + log 2 2 n
bposlem7.2 G = x + log x x
bposlem9.3 φ N
bposlem9.4 φ 64 < N
bposlem9.5 φ ¬ p N < p p 2 N
Assertion bposlem9 φ ψ

Proof

Step Hyp Ref Expression
1 bposlem7.1 F = n 2 G n + 9 4 G n 2 + log 2 2 n
2 bposlem7.2 G = x + log x x
3 bposlem9.3 φ N
4 bposlem9.4 φ 64 < N
5 bposlem9.5 φ ¬ p N < p p 2 N
6 6nn0 6 0
7 4nn 4
8 6 7 decnncl 64
9 8 a1i φ 64
10 ere e
11 8re 8
12 egt2lt3 2 < e e < 3
13 12 simpri e < 3
14 3lt8 3 < 8
15 3re 3
16 10 15 11 lttri e < 3 3 < 8 e < 8
17 13 14 16 mp2an e < 8
18 10 11 17 ltleii e 8
19 0re 0
20 epos 0 < e
21 19 10 20 ltleii 0 e
22 8pos 0 < 8
23 19 11 22 ltleii 0 8
24 le2sq e 0 e 8 0 8 e 8 e 2 8 2
25 10 21 11 23 24 mp4an e 8 e 2 8 2
26 18 25 mpbi e 2 8 2
27 11 recni 8
28 27 sqvali 8 2 = 8 8
29 8t8e64 8 8 = 64
30 28 29 eqtri 8 2 = 64
31 26 30 breqtri e 2 64
32 31 a1i φ e 2 64
33 10 resqcli e 2
34 33 a1i φ e 2
35 8 nnrei 64
36 35 a1i φ 64
37 3 nnred φ N
38 ltle 64 N 64 < N 64 N
39 35 37 38 sylancr φ 64 < N 64 N
40 4 39 mpd φ 64 N
41 34 36 37 32 40 letrd φ e 2 N
42 1 2 9 3 32 41 bposlem7 φ 64 < N F N < F 64
43 4 42 mpd φ F N < F 64
44 1 2 bposlem8 F 64 F 64 < log 2
45 44 a1i φ F 64 F 64 < log 2
46 45 simpld φ F 64
47 2fveq3 n = N G n = G N
48 47 oveq2d n = N 2 G n = 2 G N
49 fvoveq1 n = N G n 2 = G N 2
50 49 oveq2d n = N 9 4 G n 2 = 9 4 G N 2
51 48 50 oveq12d n = N 2 G n + 9 4 G n 2 = 2 G N + 9 4 G N 2
52 oveq2 n = N 2 n = 2 N
53 52 fveq2d n = N 2 n = 2 N
54 53 oveq2d n = N log 2 2 n = log 2 2 N
55 51 54 oveq12d n = N 2 G n + 9 4 G n 2 + log 2 2 n = 2 G N + 9 4 G N 2 + log 2 2 N
56 ovex 2 G N + 9 4 G N 2 + log 2 2 N V
57 55 1 56 fvmpt N F N = 2 G N + 9 4 G N 2 + log 2 2 N
58 3 57 syl φ F N = 2 G N + 9 4 G N 2 + log 2 2 N
59 sqrt2re 2
60 3 nnrpd φ N +
61 60 rpsqrtcld φ N +
62 fveq2 x = N log x = log N
63 id x = N x = N
64 62 63 oveq12d x = N log x x = log N N
65 ovex log N N V
66 64 2 65 fvmpt N + G N = log N N
67 61 66 syl φ G N = log N N
68 61 relogcld φ log N
69 68 61 rerpdivcld φ log N N
70 67 69 eqeltrd φ G N
71 remulcl 2 G N 2 G N
72 59 70 71 sylancr φ 2 G N
73 9re 9
74 4re 4
75 4ne0 4 0
76 73 74 75 redivcli 9 4
77 60 rphalfcld φ N 2 +
78 fveq2 x = N 2 log x = log N 2
79 id x = N 2 x = N 2
80 78 79 oveq12d x = N 2 log x x = log N 2 N 2
81 ovex log N 2 N 2 V
82 80 2 81 fvmpt N 2 + G N 2 = log N 2 N 2
83 77 82 syl φ G N 2 = log N 2 N 2
84 77 relogcld φ log N 2
85 84 77 rerpdivcld φ log N 2 N 2
86 83 85 eqeltrd φ G N 2
87 remulcl 9 4 G N 2 9 4 G N 2
88 76 86 87 sylancr φ 9 4 G N 2
89 72 88 readdcld φ 2 G N + 9 4 G N 2
90 2rp 2 +
91 relogcl 2 + log 2
92 90 91 ax-mp log 2
93 rpmulcl 2 + N + 2 N +
94 90 60 93 sylancr φ 2 N +
95 94 rpsqrtcld φ 2 N +
96 rerpdivcl log 2 2 N + log 2 2 N
97 92 95 96 sylancr φ log 2 2 N
98 89 97 readdcld φ 2 G N + 9 4 G N 2 + log 2 2 N
99 58 98 eqeltrd φ F N
100 92 a1i φ log 2
101 45 simprd φ F 64 < log 2
102 nnrp 4 4 +
103 7 102 ax-mp 4 +
104 relogcl 4 + log 4
105 103 104 ax-mp log 4
106 remulcl N log 4 N log 4
107 37 105 106 sylancl φ N log 4
108 60 relogcld φ log N
109 107 108 resubcld φ N log 4 log N
110 rpre 2 N + 2 N
111 rpge0 2 N + 0 2 N
112 110 111 resqrtcld 2 N + 2 N
113 94 112 syl φ 2 N
114 3nn 3
115 nndivre 2 N 3 2 N 3
116 113 114 115 sylancl φ 2 N 3
117 2re 2
118 readdcl 2 N 3 2 2 N 3 + 2
119 116 117 118 sylancl φ 2 N 3 + 2
120 94 relogcld φ log 2 N
121 119 120 remulcld φ 2 N 3 + 2 log 2 N
122 remulcl 4 N 4 N
123 74 37 122 sylancr φ 4 N
124 nndivre 4 N 3 4 N 3
125 123 114 124 sylancl φ 4 N 3
126 5re 5
127 resubcl 4 N 3 5 4 N 3 5
128 125 126 127 sylancl φ 4 N 3 5
129 remulcl 4 N 3 5 log 2 4 N 3 5 log 2
130 128 92 129 sylancl φ 4 N 3 5 log 2
131 121 130 readdcld φ 2 N 3 + 2 log 2 N + 4 N 3 5 log 2
132 remulcl 4 N 3 log 2 4 N 3 log 2
133 125 92 132 sylancl φ 4 N 3 log 2
134 133 108 resubcld φ 4 N 3 log 2 log N
135 3 nnzd φ N
136 df-5 5 = 4 + 1
137 74 a1i φ 4
138 6nn 6
139 4nn0 4 0
140 4lt10 4 < 10
141 138 139 139 140 declti 4 < 64
142 141 a1i φ 4 < 64
143 137 36 37 142 4 lttrd φ 4 < N
144 4z 4
145 zltp1le 4 N 4 < N 4 + 1 N
146 144 135 145 sylancr φ 4 < N 4 + 1 N
147 143 146 mpbid φ 4 + 1 N
148 136 147 eqbrtrid φ 5 N
149 5nn 5
150 149 nnzi 5
151 150 eluz1i N 5 N 5 N
152 135 148 151 sylanbrc φ N 5
153 breq2 p = q N < p N < q
154 breq1 p = q p 2 N q 2 N
155 153 154 anbi12d p = q N < p p 2 N N < q q 2 N
156 155 cbvrexvw p N < p p 2 N q N < q q 2 N
157 5 156 sylnib φ ¬ q N < q q 2 N
158 eqid n if n n n pCnt ( 2 N N) 1 = n if n n n pCnt ( 2 N N) 1
159 eqid 2 N 3 = 2 N 3
160 eqid 2 N = 2 N
161 152 157 158 159 160 bposlem6 φ 4 N N < 2 N 2 N 3 + 2 2 4 N 3 5
162 reexplog 4 + N 4 N = e N log 4
163 103 135 162 sylancr φ 4 N = e N log 4
164 60 reeflogd φ e log N = N
165 164 eqcomd φ N = e log N
166 163 165 oveq12d φ 4 N N = e N log 4 e log N
167 107 recnd φ N log 4
168 108 recnd φ log N
169 efsub N log 4 log N e N log 4 log N = e N log 4 e log N
170 167 168 169 syl2anc φ e N log 4 log N = e N log 4 e log N
171 166 170 eqtr4d φ 4 N N = e N log 4 log N
172 94 rpcnd φ 2 N
173 94 rpne0d φ 2 N 0
174 119 recnd φ 2 N 3 + 2
175 172 173 174 cxpefd φ 2 N 2 N 3 + 2 = e 2 N 3 + 2 log 2 N
176 2cn 2
177 2ne0 2 0
178 128 recnd φ 4 N 3 5
179 cxpef 2 2 0 4 N 3 5 2 4 N 3 5 = e 4 N 3 5 log 2
180 176 177 178 179 mp3an12i φ 2 4 N 3 5 = e 4 N 3 5 log 2
181 175 180 oveq12d φ 2 N 2 N 3 + 2 2 4 N 3 5 = e 2 N 3 + 2 log 2 N e 4 N 3 5 log 2
182 121 recnd φ 2 N 3 + 2 log 2 N
183 130 recnd φ 4 N 3 5 log 2
184 efadd 2 N 3 + 2 log 2 N 4 N 3 5 log 2 e 2 N 3 + 2 log 2 N + 4 N 3 5 log 2 = e 2 N 3 + 2 log 2 N e 4 N 3 5 log 2
185 182 183 184 syl2anc φ e 2 N 3 + 2 log 2 N + 4 N 3 5 log 2 = e 2 N 3 + 2 log 2 N e 4 N 3 5 log 2
186 181 185 eqtr4d φ 2 N 2 N 3 + 2 2 4 N 3 5 = e 2 N 3 + 2 log 2 N + 4 N 3 5 log 2
187 161 171 186 3brtr3d φ e N log 4 log N < e 2 N 3 + 2 log 2 N + 4 N 3 5 log 2
188 eflt N log 4 log N 2 N 3 + 2 log 2 N + 4 N 3 5 log 2 N log 4 log N < 2 N 3 + 2 log 2 N + 4 N 3 5 log 2 e N log 4 log N < e 2 N 3 + 2 log 2 N + 4 N 3 5 log 2
189 109 131 188 syl2anc φ N log 4 log N < 2 N 3 + 2 log 2 N + 4 N 3 5 log 2 e N log 4 log N < e 2 N 3 + 2 log 2 N + 4 N 3 5 log 2
190 187 189 mpbird φ N log 4 log N < 2 N 3 + 2 log 2 N + 4 N 3 5 log 2
191 109 131 134 190 ltsub1dd φ N log 4 - log N - 4 N 3 log 2 log N < 2 N 3 + 2 log 2 N + 4 N 3 5 log 2 - 4 N 3 log 2 log N
192 37 recnd φ N
193 mulcom 2 N 2 N = N 2
194 176 192 193 sylancr φ 2 N = N 2
195 194 oveq1d φ 2 N log 2 = N 2 log 2
196 92 recni log 2
197 mulass N 2 log 2 N 2 log 2 = N 2 log 2
198 176 196 197 mp3an23 N N 2 log 2 = N 2 log 2
199 192 198 syl φ N 2 log 2 = N 2 log 2
200 196 2timesi 2 log 2 = log 2 + log 2
201 relogmul 2 + 2 + log 2 2 = log 2 + log 2
202 90 90 201 mp2an log 2 2 = log 2 + log 2
203 2t2e4 2 2 = 4
204 203 fveq2i log 2 2 = log 4
205 200 202 204 3eqtr2i 2 log 2 = log 4
206 205 oveq2i N 2 log 2 = N log 4
207 199 206 eqtrdi φ N 2 log 2 = N log 4
208 195 207 eqtrd φ 2 N log 2 = N log 4
209 208 oveq1d φ 2 N log 2 4 N 3 log 2 = N log 4 4 N 3 log 2
210 125 recnd φ 4 N 3
211 3rp 3 +
212 rpdivcl 2 N + 3 + 2 N 3 +
213 94 211 212 sylancl φ 2 N 3 +
214 213 rpcnd φ 2 N 3
215 4p2e6 4 + 2 = 6
216 215 oveq1i 4 + 2 N = 6 N
217 4cn 4
218 adddir 4 2 N 4 + 2 N = 4 N + 2 N
219 217 176 192 218 mp3an12i φ 4 + 2 N = 4 N + 2 N
220 216 219 eqtr3id φ 6 N = 4 N + 2 N
221 220 oveq1d φ 6 N 3 = 4 N + 2 N 3
222 6cn 6
223 3cn 3
224 3ne0 3 0
225 223 224 pm3.2i 3 3 0
226 div23 6 N 3 3 0 6 N 3 = 6 3 N
227 222 225 226 mp3an13 N 6 N 3 = 6 3 N
228 192 227 syl φ 6 N 3 = 6 3 N
229 3t2e6 3 2 = 6
230 229 oveq1i 3 2 3 = 6 3
231 176 223 224 divcan3i 3 2 3 = 2
232 230 231 eqtr3i 6 3 = 2
233 232 oveq1i 6 3 N = 2 N
234 228 233 eqtrdi φ 6 N 3 = 2 N
235 123 recnd φ 4 N
236 remulcl 2 N 2 N
237 117 37 236 sylancr φ 2 N
238 237 recnd φ 2 N
239 divdir 4 N 2 N 3 3 0 4 N + 2 N 3 = 4 N 3 + 2 N 3
240 225 239 mp3an3 4 N 2 N 4 N + 2 N 3 = 4 N 3 + 2 N 3
241 235 238 240 syl2anc φ 4 N + 2 N 3 = 4 N 3 + 2 N 3
242 221 234 241 3eqtr3d φ 2 N = 4 N 3 + 2 N 3
243 210 214 242 mvrladdd φ 2 N 4 N 3 = 2 N 3
244 243 oveq1d φ 2 N 4 N 3 log 2 = 2 N 3 log 2
245 100 recnd φ log 2
246 238 210 245 subdird φ 2 N 4 N 3 log 2 = 2 N log 2 4 N 3 log 2
247 244 246 eqtr3d φ 2 N 3 log 2 = 2 N log 2 4 N 3 log 2
248 133 recnd φ 4 N 3 log 2
249 167 248 168 nnncan2d φ N log 4 - log N - 4 N 3 log 2 log N = N log 4 4 N 3 log 2
250 209 247 249 3eqtr4d φ 2 N 3 log 2 = N log 4 - log N - 4 N 3 log 2 log N
251 116 recnd φ 2 N 3
252 176 a1i φ 2
253 120 recnd φ log 2 N
254 251 252 253 adddird φ 2 N 3 + 2 log 2 N = 2 N 3 log 2 N + 2 log 2 N
255 relogmul 2 + N + log 2 N = log 2 + log N
256 90 60 255 sylancr φ log 2 N = log 2 + log N
257 256 oveq2d φ 2 log 2 N = 2 log 2 + log N
258 252 245 168 adddid φ 2 log 2 + log N = 2 log 2 + 2 log N
259 257 258 eqtrd φ 2 log 2 N = 2 log 2 + 2 log N
260 259 oveq2d φ 2 N 3 log 2 N + 2 log 2 N = 2 N 3 log 2 N + 2 log 2 + 2 log N
261 254 260 eqtrd φ 2 N 3 + 2 log 2 N = 2 N 3 log 2 N + 2 log 2 + 2 log N
262 5cn 5
263 262 a1i φ 5
264 210 263 245 subdird φ 4 N 3 5 log 2 = 4 N 3 log 2 5 log 2
265 264 oveq1d φ 4 N 3 5 log 2 4 N 3 log 2 log N = 4 N 3 log 2 - 5 log 2 - 4 N 3 log 2 log N
266 262 196 mulcli 5 log 2
267 266 a1i φ 5 log 2
268 248 267 168 nnncan1d φ 4 N 3 log 2 - 5 log 2 - 4 N 3 log 2 log N = log N 5 log 2
269 265 268 eqtrd φ 4 N 3 5 log 2 4 N 3 log 2 log N = log N 5 log 2
270 261 269 oveq12d φ 2 N 3 + 2 log 2 N + 4 N 3 5 log 2 - 4 N 3 log 2 log N = 2 N 3 log 2 N + 2 log 2 + 2 log N + log N 5 log 2
271 134 recnd φ 4 N 3 log 2 log N
272 182 183 271 addsubassd φ 2 N 3 + 2 log 2 N + 4 N 3 5 log 2 - 4 N 3 log 2 log N = 2 N 3 + 2 log 2 N + 4 N 3 5 log 2 - 4 N 3 log 2 log N
273 262 223 196 subdiri 5 3 log 2 = 5 log 2 3 log 2
274 3p2e5 3 + 2 = 5
275 274 oveq1i 3 + 2 - 3 = 5 3
276 pncan2 3 2 3 + 2 - 3 = 2
277 223 176 276 mp2an 3 + 2 - 3 = 2
278 275 277 eqtr3i 5 3 = 2
279 278 oveq1i 5 3 log 2 = 2 log 2
280 273 279 eqtr3i 5 log 2 3 log 2 = 2 log 2
281 280 a1i φ 5 log 2 3 log 2 = 2 log 2
282 mulcl 2 log N 2 log N
283 176 168 282 sylancr φ 2 log N
284 df-3 3 = 2 + 1
285 284 oveq1i 3 log N = 2 + 1 log N
286 1cnd φ 1
287 252 286 168 adddird φ 2 + 1 log N = 2 log N + 1 log N
288 285 287 syl5eq φ 3 log N = 2 log N + 1 log N
289 168 mulid2d φ 1 log N = log N
290 289 oveq2d φ 2 log N + 1 log N = 2 log N + log N
291 288 290 eqtrd φ 3 log N = 2 log N + log N
292 291 oveq1d φ 3 log N 5 log 2 = 2 log N + log N - 5 log 2
293 283 168 267 292 assraddsubd φ 3 log N 5 log 2 = 2 log N + log N - 5 log 2
294 281 293 oveq12d φ 5 log 2 3 log 2 + 3 log N - 5 log 2 = 2 log 2 + 2 log N + log N 5 log 2
295 relogdiv N + 2 + log N 2 = log N log 2
296 60 90 295 sylancl φ log N 2 = log N log 2
297 296 oveq2d φ 3 log N 2 = 3 log N log 2
298 subdi 3 log N log 2 3 log N log 2 = 3 log N 3 log 2
299 223 196 298 mp3an13 log N 3 log N log 2 = 3 log N 3 log 2
300 168 299 syl φ 3 log N log 2 = 3 log N 3 log 2
301 297 300 eqtrd φ 3 log N 2 = 3 log N 3 log 2
302 div23 2 N 3 3 0 2 N 3 = 2 3 N
303 176 225 302 mp3an13 N 2 N 3 = 2 3 N
304 192 303 syl φ 2 N 3 = 2 3 N
305 223 176 223 176 177 177 divmuldivi 3 2 3 2 = 3 3 2 2
306 3t3e9 3 3 = 9
307 306 203 oveq12i 3 3 2 2 = 9 4
308 305 307 eqtr2i 9 4 = 3 2 3 2
309 308 a1i φ 9 4 = 3 2 3 2
310 304 309 oveq12d φ 2 N 3 9 4 = 2 3 N 3 2 3 2
311 176 223 224 divcli 2 3
312 223 176 177 divcli 3 2
313 mul4 2 3 N 3 2 3 2 2 3 N 3 2 3 2 = 2 3 3 2 N 3 2
314 312 312 313 mpanr12 2 3 N 2 3 N 3 2 3 2 = 2 3 3 2 N 3 2
315 311 192 314 sylancr φ 2 3 N 3 2 3 2 = 2 3 3 2 N 3 2
316 divcan6 2 2 0 3 3 0 2 3 3 2 = 1
317 176 177 223 224 316 mp4an 2 3 3 2 = 1
318 317 oveq1i 2 3 3 2 N 3 2 = 1 N 3 2
319 mulcl N 3 2 N 3 2
320 192 312 319 sylancl φ N 3 2
321 320 mulid2d φ 1 N 3 2 = N 3 2
322 318 321 syl5eq φ 2 3 3 2 N 3 2 = N 3 2
323 2cnne0 2 2 0
324 div12 N 3 2 2 0 N 3 2 = 3 N 2
325 223 323 324 mp3an23 N N 3 2 = 3 N 2
326 192 325 syl φ N 3 2 = 3 N 2
327 322 326 eqtrd φ 2 3 3 2 N 3 2 = 3 N 2
328 310 315 327 3eqtrd φ 2 N 3 9 4 = 3 N 2
329 328 83 oveq12d φ 2 N 3 9 4 G N 2 = 3 N 2 log N 2 N 2
330 76 recni 9 4
331 330 a1i φ 9 4
332 86 recnd φ G N 2
333 214 331 332 mulassd φ 2 N 3 9 4 G N 2 = 2 N 3 9 4 G N 2
334 223 a1i φ 3
335 77 rpcnd φ N 2
336 84 recnd φ log N 2
337 77 rpne0d φ N 2 0
338 336 335 337 divcld φ log N 2 N 2
339 334 335 338 mulassd φ 3 N 2 log N 2 N 2 = 3 N 2 log N 2 N 2
340 336 335 337 divcan2d φ N 2 log N 2 N 2 = log N 2
341 340 oveq2d φ 3 N 2 log N 2 N 2 = 3 log N 2
342 339 341 eqtrd φ 3 N 2 log N 2 N 2 = 3 log N 2
343 329 333 342 3eqtr3d φ 2 N 3 9 4 G N 2 = 3 log N 2
344 223 196 mulcli 3 log 2
345 344 a1i φ 3 log 2
346 mulcl 3 log N 3 log N
347 223 168 346 sylancr φ 3 log N
348 267 345 347 npncan3d φ 5 log 2 3 log 2 + 3 log N - 5 log 2 = 3 log N 3 log 2
349 301 343 348 3eqtr4d φ 2 N 3 9 4 G N 2 = 5 log 2 3 log 2 + 3 log N - 5 log 2
350 117 92 remulcli 2 log 2
351 350 recni 2 log 2
352 351 a1i φ 2 log 2
353 subcl log N 5 log 2 log N 5 log 2
354 168 266 353 sylancl φ log N 5 log 2
355 352 283 354 addassd φ 2 log 2 + 2 log N + log N 5 log 2 = 2 log 2 + 2 log N + log N 5 log 2
356 294 349 355 3eqtr4d φ 2 N 3 9 4 G N 2 = 2 log 2 + 2 log N + log N 5 log 2
357 356 oveq2d φ 2 N 3 log 2 N + 2 N 3 9 4 G N 2 = 2 N 3 log 2 N + 2 log 2 + 2 log N + log N 5 log 2
358 mulcl 2 N 3 log 2 2 N 3 log 2
359 251 196 358 sylancl φ 2 N 3 log 2
360 251 168 mulcld φ 2 N 3 log N
361 88 recnd φ 9 4 G N 2
362 214 361 mulcld φ 2 N 3 9 4 G N 2
363 359 360 362 addassd φ 2 N 3 log 2 + 2 N 3 log N + 2 N 3 9 4 G N 2 = 2 N 3 log 2 + 2 N 3 log N + 2 N 3 9 4 G N 2
364 256 oveq2d φ 2 N 3 log 2 N = 2 N 3 log 2 + log N
365 251 245 168 adddid φ 2 N 3 log 2 + log N = 2 N 3 log 2 + 2 N 3 log N
366 364 365 eqtrd φ 2 N 3 log 2 N = 2 N 3 log 2 + 2 N 3 log N
367 366 oveq1d φ 2 N 3 log 2 N + 2 N 3 9 4 G N 2 = 2 N 3 log 2 + 2 N 3 log N + 2 N 3 9 4 G N 2
368 58 oveq2d φ 2 N 3 F N = 2 N 3 2 G N + 9 4 G N 2 + log 2 2 N
369 89 recnd φ 2 G N + 9 4 G N 2
370 97 recnd φ log 2 2 N
371 214 369 370 adddid φ 2 N 3 2 G N + 9 4 G N 2 + log 2 2 N = 2 N 3 2 G N + 9 4 G N 2 + 2 N 3 log 2 2 N
372 368 371 eqtrd φ 2 N 3 F N = 2 N 3 2 G N + 9 4 G N 2 + 2 N 3 log 2 2 N
373 72 recnd φ 2 G N
374 214 373 361 adddid φ 2 N 3 2 G N + 9 4 G N 2 = 2 N 3 2 G N + 2 N 3 9 4 G N 2
375 94 rpge0d φ 0 2 N
376 remsqsqrt 2 N 0 2 N 2 N 2 N = 2 N
377 237 375 376 syl2anc φ 2 N 2 N = 2 N
378 377 oveq1d φ 2 N 2 N 3 = 2 N 3
379 113 recnd φ 2 N
380 224 a1i φ 3 0
381 379 379 334 380 div23d φ 2 N 2 N 3 = 2 N 3 2 N
382 378 381 eqtr3d φ 2 N 3 = 2 N 3 2 N
383 382 oveq1d φ 2 N 3 2 G N = 2 N 3 2 N 2 G N
384 251 379 373 mulassd φ 2 N 3 2 N 2 G N = 2 N 3 2 N 2 G N
385 0le2 0 2
386 117 385 pm3.2i 2 0 2
387 60 rprege0d φ N 0 N
388 sqrtmul 2 0 2 N 0 N 2 N = 2 N
389 386 387 388 sylancr φ 2 N = 2 N
390 389 oveq1d φ 2 N 2 G N = 2 N 2 G N
391 59 recni 2
392 391 a1i φ 2
393 61 rpcnd φ N
394 70 recnd φ G N
395 392 393 392 394 mul4d φ 2 N 2 G N = 2 2 N G N
396 remsqsqrt 2 0 2 2 2 = 2
397 117 385 396 mp2an 2 2 = 2
398 397 a1i φ 2 2 = 2
399 67 oveq2d φ N G N = N log N N
400 68 recnd φ log N
401 61 rpne0d φ N 0
402 400 393 401 divcan2d φ N log N N = log N
403 399 402 eqtrd φ N G N = log N
404 398 403 oveq12d φ 2 2 N G N = 2 log N
405 400 2timesd φ 2 log N = log N + log N
406 61 61 relogmuld φ log N N = log N + log N
407 remsqsqrt N 0 N N N = N
408 387 407 syl φ N N = N
409 408 fveq2d φ log N N = log N
410 406 409 eqtr3d φ log N + log N = log N
411 404 405 410 3eqtrd φ 2 2 N G N = log N
412 390 395 411 3eqtrd φ 2 N 2 G N = log N
413 412 oveq2d φ 2 N 3 2 N 2 G N = 2 N 3 log N
414 383 384 413 3eqtrd φ 2 N 3 2 G N = 2 N 3 log N
415 414 oveq1d φ 2 N 3 2 G N + 2 N 3 9 4 G N 2 = 2 N 3 log N + 2 N 3 9 4 G N 2
416 374 415 eqtrd φ 2 N 3 2 G N + 9 4 G N 2 = 2 N 3 log N + 2 N 3 9 4 G N 2
417 382 oveq1d φ 2 N 3 log 2 2 N = 2 N 3 2 N log 2 2 N
418 251 379 370 mulassd φ 2 N 3 2 N log 2 2 N = 2 N 3 2 N log 2 2 N
419 95 rpne0d φ 2 N 0
420 245 379 419 divcan2d φ 2 N log 2 2 N = log 2
421 420 oveq2d φ 2 N 3 2 N log 2 2 N = 2 N 3 log 2
422 417 418 421 3eqtrd φ 2 N 3 log 2 2 N = 2 N 3 log 2
423 416 422 oveq12d φ 2 N 3 2 G N + 9 4 G N 2 + 2 N 3 log 2 2 N = 2 N 3 log N + 2 N 3 9 4 G N 2 + 2 N 3 log 2
424 360 362 addcld φ 2 N 3 log N + 2 N 3 9 4 G N 2
425 424 359 addcomd φ 2 N 3 log N + 2 N 3 9 4 G N 2 + 2 N 3 log 2 = 2 N 3 log 2 + 2 N 3 log N + 2 N 3 9 4 G N 2
426 372 423 425 3eqtrd φ 2 N 3 F N = 2 N 3 log 2 + 2 N 3 log N + 2 N 3 9 4 G N 2
427 363 367 426 3eqtr4rd φ 2 N 3 F N = 2 N 3 log 2 N + 2 N 3 9 4 G N 2
428 251 253 mulcld φ 2 N 3 log 2 N
429 addcl 2 log 2 2 log N 2 log 2 + 2 log N
430 351 283 429 sylancr φ 2 log 2 + 2 log N
431 428 430 354 addassd φ 2 N 3 log 2 N + 2 log 2 + 2 log N + log N 5 log 2 = 2 N 3 log 2 N + 2 log 2 + 2 log N + log N 5 log 2
432 357 427 431 3eqtr4d φ 2 N 3 F N = 2 N 3 log 2 N + 2 log 2 + 2 log N + log N 5 log 2
433 270 272 432 3eqtr4rd φ 2 N 3 F N = 2 N 3 + 2 log 2 N + 4 N 3 5 log 2 - 4 N 3 log 2 log N
434 191 250 433 3brtr4d φ 2 N 3 log 2 < 2 N 3 F N
435 100 99 213 ltmul2d φ log 2 < F N 2 N 3 log 2 < 2 N 3 F N
436 434 435 mpbird φ log 2 < F N
437 46 100 99 101 436 lttrd φ F 64 < F N
438 46 99 437 ltnsymd φ ¬ F N < F 64
439 43 438 pm2.21dd φ ψ