Metamath Proof Explorer


Theorem bposlem6

Description: Lemma for bpos . By using the various bounds at our disposal, arrive at an inequality that is false for N large enough. (Contributed by Mario Carneiro, 14-Mar-2014) (Revised by Wolf Lammen, 12-Sep-2020)

Ref Expression
Hypotheses bpos.1 φ N 5
bpos.2 φ ¬ p N < p p 2 N
bpos.3 F = n if n n n pCnt ( 2 N N) 1
bpos.4 K = 2 N 3
bpos.5 M = 2 N
Assertion bposlem6 φ 4 N N < 2 N 2 N 3 + 2 2 4 N 3 5

Proof

Step Hyp Ref Expression
1 bpos.1 φ N 5
2 bpos.2 φ ¬ p N < p p 2 N
3 bpos.3 F = n if n n n pCnt ( 2 N N) 1
4 bpos.4 K = 2 N 3
5 bpos.5 M = 2 N
6 4nn 4
7 5nn 5
8 eluznn 5 N 5 N
9 7 1 8 sylancr φ N
10 9 nnnn0d φ N 0
11 nnexpcl 4 N 0 4 N
12 6 10 11 sylancr φ 4 N
13 12 nnred φ 4 N
14 13 9 nndivred φ 4 N N
15 fzctr N 0 N 0 2 N
16 10 15 syl φ N 0 2 N
17 bccl2 N 0 2 N ( 2 N N)
18 16 17 syl φ ( 2 N N)
19 18 nnred φ ( 2 N N)
20 2nn 2
21 nnmulcl 2 N 2 N
22 20 9 21 sylancr φ 2 N
23 22 nnrpd φ 2 N +
24 22 nnred φ 2 N
25 23 rpge0d φ 0 2 N
26 24 25 resqrtcld φ 2 N
27 3nn 3
28 nndivre 2 N 3 2 N 3
29 26 27 28 sylancl φ 2 N 3
30 2re 2
31 readdcl 2 N 3 2 2 N 3 + 2
32 29 30 31 sylancl φ 2 N 3 + 2
33 23 32 rpcxpcld φ 2 N 2 N 3 + 2 +
34 33 rpred φ 2 N 2 N 3 + 2
35 2rp 2 +
36 nnmulcl 4 N 4 N
37 6 9 36 sylancr φ 4 N
38 37 nnred φ 4 N
39 nndivre 4 N 3 4 N 3
40 38 27 39 sylancl φ 4 N 3
41 5re 5
42 resubcl 4 N 3 5 4 N 3 5
43 40 41 42 sylancl φ 4 N 3 5
44 rpcxpcl 2 + 4 N 3 5 2 4 N 3 5 +
45 35 43 44 sylancr φ 2 4 N 3 5 +
46 45 rpred φ 2 4 N 3 5
47 34 46 remulcld φ 2 N 2 N 3 + 2 2 4 N 3 5
48 df-5 5 = 4 + 1
49 4z 4
50 uzid 4 4 4
51 peano2uz 4 4 4 + 1 4
52 49 50 51 mp2b 4 + 1 4
53 48 52 eqeltri 5 4
54 eqid 4 = 4
55 54 uztrn2 5 4 N 5 N 4
56 53 1 55 sylancr φ N 4
57 bclbnd N 4 4 N N < ( 2 N N)
58 56 57 syl φ 4 N N < ( 2 N N)
59 id n n
60 pccl n ( 2 N N) n pCnt ( 2 N N) 0
61 59 18 60 syl2anr φ n n pCnt ( 2 N N) 0
62 61 ralrimiva φ n n pCnt ( 2 N N) 0
63 3 62 pcmptcl φ F : seq 1 × F :
64 63 simprd φ seq 1 × F :
65 1 2 3 4 5 bposlem4 φ M 3 K
66 elfzuz M 3 K M 3
67 65 66 syl φ M 3
68 eluznn 3 M 3 M
69 27 67 68 sylancr φ M
70 64 69 ffvelrnd φ seq 1 × F M
71 70 nnred φ seq 1 × F M
72 2z 2
73 nndivre 2 N 3 2 N 3
74 24 27 73 sylancl φ 2 N 3
75 74 flcld φ 2 N 3
76 4 75 eqeltrid φ K
77 zmulcl 2 K 2 K
78 72 76 77 sylancr φ 2 K
79 7 nnzi 5
80 zsubcl 2 K 5 2 K 5
81 78 79 80 sylancl φ 2 K 5
82 81 zred φ 2 K 5
83 rpcxpcl 2 + 2 K 5 2 2 K 5 +
84 35 82 83 sylancr φ 2 2 K 5 +
85 84 rpred φ 2 2 K 5
86 71 85 remulcld φ seq 1 × F M 2 2 K 5
87 1 2 3 4 bposlem3 φ seq 1 × F K = ( 2 N N)
88 elfzuz3 M 3 K K M
89 65 88 syl φ K M
90 3 62 69 89 pcmptdvds φ seq 1 × F M seq 1 × F K
91 70 nnzd φ seq 1 × F M
92 70 nnne0d φ seq 1 × F M 0
93 uztrn K M M 3 K 3
94 89 67 93 syl2anc φ K 3
95 eluznn 3 K 3 K
96 27 94 95 sylancr φ K
97 64 96 ffvelrnd φ seq 1 × F K
98 97 nnzd φ seq 1 × F K
99 dvdsval2 seq 1 × F M seq 1 × F M 0 seq 1 × F K seq 1 × F M seq 1 × F K seq 1 × F K seq 1 × F M
100 91 92 98 99 syl3anc φ seq 1 × F M seq 1 × F K seq 1 × F K seq 1 × F M
101 90 100 mpbid φ seq 1 × F K seq 1 × F M
102 101 zred φ seq 1 × F K seq 1 × F M
103 69 nnred φ M
104 76 zred φ K
105 eluzle K M M K
106 89 105 syl φ M K
107 efchtdvds M K M K e θ M e θ K
108 103 104 106 107 syl3anc φ e θ M e θ K
109 efchtcl M e θ M
110 103 109 syl φ e θ M
111 110 nnzd φ e θ M
112 110 nnne0d φ e θ M 0
113 efchtcl K e θ K
114 104 113 syl φ e θ K
115 114 nnzd φ e θ K
116 dvdsval2 e θ M e θ M 0 e θ K e θ M e θ K e θ K e θ M
117 111 112 115 116 syl3anc φ e θ M e θ K e θ K e θ M
118 108 117 mpbid φ e θ K e θ M
119 118 zred φ e θ K e θ M
120 prmz p p
121 fllt 2 N p 2 N < p 2 N < p
122 26 120 121 syl2an φ p 2 N < p 2 N < p
123 5 breq1i M < p 2 N < p
124 122 123 bitr4di φ p 2 N < p M < p
125 120 zred p p
126 ltnle M p M < p ¬ p M
127 103 125 126 syl2an φ p M < p ¬ p M
128 124 127 bitrd φ p 2 N < p ¬ p M
129 bposlem1 N p p p pCnt ( 2 N N) 2 N
130 9 129 sylan φ p p p pCnt ( 2 N N) 2 N
131 125 adantl φ p p
132 id p p
133 pccl p ( 2 N N) p pCnt ( 2 N N) 0
134 132 18 133 syl2anr φ p p pCnt ( 2 N N) 0
135 131 134 reexpcld φ p p p pCnt ( 2 N N)
136 24 adantr φ p 2 N
137 131 resqcld φ p p 2
138 lelttr p p pCnt ( 2 N N) 2 N p 2 p p pCnt ( 2 N N) 2 N 2 N < p 2 p p pCnt ( 2 N N) < p 2
139 135 136 137 138 syl3anc φ p p p pCnt ( 2 N N) 2 N 2 N < p 2 p p pCnt ( 2 N N) < p 2
140 130 139 mpand φ p 2 N < p 2 p p pCnt ( 2 N N) < p 2
141 resqrtth 2 N 0 2 N 2 N 2 = 2 N
142 24 25 141 syl2anc φ 2 N 2 = 2 N
143 142 breq1d φ 2 N 2 < p 2 2 N < p 2
144 143 adantr φ p 2 N 2 < p 2 2 N < p 2
145 134 nn0zd φ p p pCnt ( 2 N N)
146 72 a1i φ p 2
147 prmgt1 p 1 < p
148 147 adantl φ p 1 < p
149 131 145 146 148 ltexp2d φ p p pCnt ( 2 N N) < 2 p p pCnt ( 2 N N) < p 2
150 140 144 149 3imtr4d φ p 2 N 2 < p 2 p pCnt ( 2 N N) < 2
151 df-2 2 = 1 + 1
152 151 breq2i p pCnt ( 2 N N) < 2 p pCnt ( 2 N N) < 1 + 1
153 150 152 syl6ib φ p 2 N 2 < p 2 p pCnt ( 2 N N) < 1 + 1
154 26 adantr φ p 2 N
155 24 25 sqrtge0d φ 0 2 N
156 155 adantr φ p 0 2 N
157 prmnn p p
158 157 nnrpd p p +
159 158 rpge0d p 0 p
160 159 adantl φ p 0 p
161 154 131 156 160 lt2sqd φ p 2 N < p 2 N 2 < p 2
162 1z 1
163 zleltp1 p pCnt ( 2 N N) 1 p pCnt ( 2 N N) 1 p pCnt ( 2 N N) < 1 + 1
164 145 162 163 sylancl φ p p pCnt ( 2 N N) 1 p pCnt ( 2 N N) < 1 + 1
165 153 161 164 3imtr4d φ p 2 N < p p pCnt ( 2 N N) 1
166 128 165 sylbird φ p ¬ p M p pCnt ( 2 N N) 1
167 166 imp φ p ¬ p M p pCnt ( 2 N N) 1
168 167 adantrl φ p p K ¬ p M p pCnt ( 2 N N) 1
169 iftrue p K ¬ p M if p K ¬ p M p pCnt ( 2 N N) 0 = p pCnt ( 2 N N)
170 169 adantl φ p p K ¬ p M if p K ¬ p M p pCnt ( 2 N N) 0 = p pCnt ( 2 N N)
171 iftrue p K ¬ p M if p K ¬ p M 1 0 = 1
172 171 adantl φ p p K ¬ p M if p K ¬ p M 1 0 = 1
173 168 170 172 3brtr4d φ p p K ¬ p M if p K ¬ p M p pCnt ( 2 N N) 0 if p K ¬ p M 1 0
174 0le0 0 0
175 iffalse ¬ p K ¬ p M if p K ¬ p M p pCnt ( 2 N N) 0 = 0
176 iffalse ¬ p K ¬ p M if p K ¬ p M 1 0 = 0
177 175 176 breq12d ¬ p K ¬ p M if p K ¬ p M p pCnt ( 2 N N) 0 if p K ¬ p M 1 0 0 0
178 174 177 mpbiri ¬ p K ¬ p M if p K ¬ p M p pCnt ( 2 N N) 0 if p K ¬ p M 1 0
179 178 adantl φ p ¬ p K ¬ p M if p K ¬ p M p pCnt ( 2 N N) 0 if p K ¬ p M 1 0
180 173 179 pm2.61dan φ p if p K ¬ p M p pCnt ( 2 N N) 0 if p K ¬ p M 1 0
181 62 adantr φ p n n pCnt ( 2 N N) 0
182 69 adantr φ p M
183 simpr φ p p
184 oveq1 n = p n pCnt ( 2 N N) = p pCnt ( 2 N N)
185 89 adantr φ p K M
186 3 181 182 183 184 185 pcmpt2 φ p p pCnt seq 1 × F K seq 1 × F M = if p K ¬ p M p pCnt ( 2 N N) 0
187 eqid n if n n 1 = n if n n 1
188 187 prmorcht K e θ K = seq 1 × n if n n 1 K
189 96 188 syl φ e θ K = seq 1 × n if n n 1 K
190 187 prmorcht M e θ M = seq 1 × n if n n 1 M
191 69 190 syl φ e θ M = seq 1 × n if n n 1 M
192 189 191 oveq12d φ e θ K e θ M = seq 1 × n if n n 1 K seq 1 × n if n n 1 M
193 192 adantr φ p e θ K e θ M = seq 1 × n if n n 1 K seq 1 × n if n n 1 M
194 193 oveq2d φ p p pCnt e θ K e θ M = p pCnt seq 1 × n if n n 1 K seq 1 × n if n n 1 M
195 nncn n n
196 195 exp1d n n 1 = n
197 196 ifeq1d n if n n 1 1 = if n n 1
198 197 mpteq2ia n if n n 1 1 = n if n n 1
199 198 eqcomi n if n n 1 = n if n n 1 1
200 1nn0 1 0
201 200 a1i φ n 1 0
202 201 ralrimiva φ n 1 0
203 202 adantr φ p n 1 0
204 eqidd n = p 1 = 1
205 199 203 182 183 204 185 pcmpt2 φ p p pCnt seq 1 × n if n n 1 K seq 1 × n if n n 1 M = if p K ¬ p M 1 0
206 194 205 eqtrd φ p p pCnt e θ K e θ M = if p K ¬ p M 1 0
207 180 186 206 3brtr4d φ p p pCnt seq 1 × F K seq 1 × F M p pCnt e θ K e θ M
208 207 ralrimiva φ p p pCnt seq 1 × F K seq 1 × F M p pCnt e θ K e θ M
209 pc2dvds seq 1 × F K seq 1 × F M e θ K e θ M seq 1 × F K seq 1 × F M e θ K e θ M p p pCnt seq 1 × F K seq 1 × F M p pCnt e θ K e θ M
210 101 118 209 syl2anc φ seq 1 × F K seq 1 × F M e θ K e θ M p p pCnt seq 1 × F K seq 1 × F M p pCnt e θ K e θ M
211 208 210 mpbird φ seq 1 × F K seq 1 × F M e θ K e θ M
212 114 nnred φ e θ K
213 110 nnred φ e θ M
214 114 nngt0d φ 0 < e θ K
215 110 nngt0d φ 0 < e θ M
216 212 213 214 215 divgt0d φ 0 < e θ K e θ M
217 elnnz e θ K e θ M e θ K e θ M 0 < e θ K e θ M
218 118 216 217 sylanbrc φ e θ K e θ M
219 dvdsle seq 1 × F K seq 1 × F M e θ K e θ M seq 1 × F K seq 1 × F M e θ K e θ M seq 1 × F K seq 1 × F M e θ K e θ M
220 101 218 219 syl2anc φ seq 1 × F K seq 1 × F M e θ K e θ M seq 1 × F K seq 1 × F M e θ K e θ M
221 211 220 mpd φ seq 1 × F K seq 1 × F M e θ K e θ M
222 nndivre e θ K 4 e θ K 4
223 212 6 222 sylancl φ e θ K 4
224 4re 4
225 224 a1i φ 4
226 6re 6
227 226 a1i φ 6
228 4lt6 4 < 6
229 228 a1i φ 4 < 6
230 cht3 θ 3 = log 6
231 230 fveq2i e θ 3 = e log 6
232 6pos 0 < 6
233 226 232 elrpii 6 +
234 reeflog 6 + e log 6 = 6
235 233 234 ax-mp e log 6 = 6
236 231 235 eqtri e θ 3 = 6
237 3re 3
238 237 a1i φ 3
239 eluzle M 3 3 M
240 67 239 syl φ 3 M
241 chtwordi 3 M 3 M θ 3 θ M
242 238 103 240 241 syl3anc φ θ 3 θ M
243 chtcl 3 θ 3
244 237 243 ax-mp θ 3
245 chtcl M θ M
246 103 245 syl φ θ M
247 efle θ 3 θ M θ 3 θ M e θ 3 e θ M
248 244 246 247 sylancr φ θ 3 θ M e θ 3 e θ M
249 242 248 mpbid φ e θ 3 e θ M
250 236 249 eqbrtrrid φ 6 e θ M
251 225 227 213 229 250 ltletrd φ 4 < e θ M
252 4pos 0 < 4
253 252 a1i φ 0 < 4
254 ltdiv2 4 0 < 4 e θ M 0 < e θ M e θ K 0 < e θ K 4 < e θ M e θ K e θ M < e θ K 4
255 225 253 213 215 212 214 254 syl222anc φ 4 < e θ M e θ K e θ M < e θ K 4
256 251 255 mpbid φ e θ K e θ M < e θ K 4
257 30 a1i φ 2
258 2lt3 2 < 3
259 258 a1i φ 2 < 3
260 238 103 104 240 106 letrd φ 3 K
261 257 238 104 259 260 ltletrd φ 2 < K
262 chtub K 2 < K θ K < log 2 2 K 3
263 104 261 262 syl2anc φ θ K < log 2 2 K 3
264 chtcl K θ K
265 104 264 syl φ θ K
266 relogcl 2 + log 2
267 35 266 ax-mp log 2
268 3z 3
269 zsubcl 2 K 3 2 K 3
270 78 268 269 sylancl φ 2 K 3
271 270 zred φ 2 K 3
272 remulcl log 2 2 K 3 log 2 2 K 3
273 267 271 272 sylancr φ log 2 2 K 3
274 eflt θ K log 2 2 K 3 θ K < log 2 2 K 3 e θ K < e log 2 2 K 3
275 265 273 274 syl2anc φ θ K < log 2 2 K 3 e θ K < e log 2 2 K 3
276 263 275 mpbid φ e θ K < e log 2 2 K 3
277 reexplog 2 + 2 K 3 2 2 K 3 = e 2 K 3 log 2
278 35 270 277 sylancr φ 2 2 K 3 = e 2 K 3 log 2
279 270 zcnd φ 2 K 3
280 267 recni log 2
281 mulcom 2 K 3 log 2 2 K 3 log 2 = log 2 2 K 3
282 279 280 281 sylancl φ 2 K 3 log 2 = log 2 2 K 3
283 282 fveq2d φ e 2 K 3 log 2 = e log 2 2 K 3
284 278 283 eqtrd φ 2 2 K 3 = e log 2 2 K 3
285 276 284 breqtrrd φ e θ K < 2 2 K 3
286 3p2e5 3 + 2 = 5
287 286 oveq1i 3 + 2 - 2 = 5 2
288 3cn 3
289 2cn 2
290 288 289 pncan3oi 3 + 2 - 2 = 3
291 287 290 eqtr3i 5 2 = 3
292 291 oveq2i 2 K 5 2 = 2 K 3
293 78 zcnd φ 2 K
294 5cn 5
295 subsub 2 K 5 2 2 K 5 2 = 2 K - 5 + 2
296 294 289 295 mp3an23 2 K 2 K 5 2 = 2 K - 5 + 2
297 293 296 syl φ 2 K 5 2 = 2 K - 5 + 2
298 292 297 eqtr3id φ 2 K 3 = 2 K - 5 + 2
299 298 oveq2d φ 2 2 K 3 = 2 2 K - 5 + 2
300 2ne0 2 0
301 cxpexpz 2 2 0 2 K 3 2 2 K 3 = 2 2 K 3
302 289 300 270 301 mp3an12i φ 2 2 K 3 = 2 2 K 3
303 81 zcnd φ 2 K 5
304 2cnne0 2 2 0
305 cxpadd 2 2 0 2 K 5 2 2 2 K - 5 + 2 = 2 2 K 5 2 2
306 304 289 305 mp3an13 2 K 5 2 2 K - 5 + 2 = 2 2 K 5 2 2
307 303 306 syl φ 2 2 K - 5 + 2 = 2 2 K 5 2 2
308 299 302 307 3eqtr3d φ 2 2 K 3 = 2 2 K 5 2 2
309 2nn0 2 0
310 cxpexp 2 2 0 2 2 = 2 2
311 289 309 310 mp2an 2 2 = 2 2
312 sq2 2 2 = 4
313 311 312 eqtri 2 2 = 4
314 313 oveq2i 2 2 K 5 2 2 = 2 2 K 5 4
315 308 314 eqtrdi φ 2 2 K 3 = 2 2 K 5 4
316 285 315 breqtrd φ e θ K < 2 2 K 5 4
317 224 252 pm3.2i 4 0 < 4
318 317 a1i φ 4 0 < 4
319 ltdivmul2 e θ K 2 2 K 5 4 0 < 4 e θ K 4 < 2 2 K 5 e θ K < 2 2 K 5 4
320 212 85 318 319 syl3anc φ e θ K 4 < 2 2 K 5 e θ K < 2 2 K 5 4
321 316 320 mpbird φ e θ K 4 < 2 2 K 5
322 119 223 85 256 321 lttrd φ e θ K e θ M < 2 2 K 5
323 102 119 85 221 322 lelttrd φ seq 1 × F K seq 1 × F M < 2 2 K 5
324 97 nnred φ seq 1 × F K
325 nnre seq 1 × F M seq 1 × F M
326 nngt0 seq 1 × F M 0 < seq 1 × F M
327 325 326 jca seq 1 × F M seq 1 × F M 0 < seq 1 × F M
328 70 327 syl φ seq 1 × F M 0 < seq 1 × F M
329 ltdivmul seq 1 × F K 2 2 K 5 seq 1 × F M 0 < seq 1 × F M seq 1 × F K seq 1 × F M < 2 2 K 5 seq 1 × F K < seq 1 × F M 2 2 K 5
330 324 85 328 329 syl3anc φ seq 1 × F K seq 1 × F M < 2 2 K 5 seq 1 × F K < seq 1 × F M 2 2 K 5
331 323 330 mpbid φ seq 1 × F K < seq 1 × F M 2 2 K 5
332 87 331 eqbrtrrd φ ( 2 N N) < seq 1 × F M 2 2 K 5
333 34 85 remulcld φ 2 N 2 N 3 + 2 2 2 K 5
334 1 2 3 4 5 bposlem5 φ seq 1 × F M 2 N 2 N 3 + 2
335 71 34 84 lemul1d φ seq 1 × F M 2 N 2 N 3 + 2 seq 1 × F M 2 2 K 5 2 N 2 N 3 + 2 2 2 K 5
336 334 335 mpbid φ seq 1 × F M 2 2 K 5 2 N 2 N 3 + 2 2 2 K 5
337 78 zred φ 2 K
338 41 a1i φ 5
339 flle 2 N 3 2 N 3 2 N 3
340 74 339 syl φ 2 N 3 2 N 3
341 4 340 eqbrtrid φ K 2 N 3
342 2pos 0 < 2
343 30 342 pm3.2i 2 0 < 2
344 343 a1i φ 2 0 < 2
345 lemul2 K 2 N 3 2 0 < 2 K 2 N 3 2 K 2 2 N 3
346 104 74 344 345 syl3anc φ K 2 N 3 2 K 2 2 N 3
347 341 346 mpbid φ 2 K 2 2 N 3
348 22 nncnd φ 2 N
349 3ne0 3 0
350 288 349 pm3.2i 3 3 0
351 divass 2 2 N 3 3 0 2 2 N 3 = 2 2 N 3
352 289 350 351 mp3an13 2 N 2 2 N 3 = 2 2 N 3
353 348 352 syl φ 2 2 N 3 = 2 2 N 3
354 9 nncnd φ N
355 mulass 2 2 N 2 2 N = 2 2 N
356 289 289 354 355 mp3an12i φ 2 2 N = 2 2 N
357 2t2e4 2 2 = 4
358 357 oveq1i 2 2 N = 4 N
359 356 358 eqtr3di φ 2 2 N = 4 N
360 359 oveq1d φ 2 2 N 3 = 4 N 3
361 353 360 eqtr3d φ 2 2 N 3 = 4 N 3
362 347 361 breqtrd φ 2 K 4 N 3
363 337 40 338 362 lesub1dd φ 2 K 5 4 N 3 5
364 1lt2 1 < 2
365 364 a1i φ 1 < 2
366 257 365 82 43 cxpled φ 2 K 5 4 N 3 5 2 2 K 5 2 4 N 3 5
367 363 366 mpbid φ 2 2 K 5 2 4 N 3 5
368 85 46 33 lemul2d φ 2 2 K 5 2 4 N 3 5 2 N 2 N 3 + 2 2 2 K 5 2 N 2 N 3 + 2 2 4 N 3 5
369 367 368 mpbid φ 2 N 2 N 3 + 2 2 2 K 5 2 N 2 N 3 + 2 2 4 N 3 5
370 86 333 47 336 369 letrd φ seq 1 × F M 2 2 K 5 2 N 2 N 3 + 2 2 4 N 3 5
371 19 86 47 332 370 ltletrd φ ( 2 N N) < 2 N 2 N 3 + 2 2 4 N 3 5
372 14 19 47 58 371 lttrd φ 4 N N < 2 N 2 N 3 + 2 2 4 N 3 5