MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bposlem9 Unicode version

Theorem bposlem9 22372
Description: Lemma for bpos 22373. Derive a contradiction. (Contributed by Mario Carneiro, 14-Mar-2014.)
Hypotheses
Ref Expression
bposlem7.1
bposlem7.2
bposlem9.3
bposlem9.4
bposlem9.5
Assertion
Ref Expression
bposlem9
Distinct variable groups:   ,N   ,   ,   N,   ,N

Proof of Theorem bposlem9
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 bposlem9.4 . . 3
2 bposlem7.1 . . . 4
3 bposlem7.2 . . . 4
4 6nn0 10546 . . . . . 6
5 4nn 10427 . . . . . 6
64, 5decnncl 10713 . . . . 5
76a1i 11 . . . 4
8 bposlem9.3 . . . 4
9 ere 13314 . . . . . . . 8
10 8re 10352 . . . . . . . 8
11 egt2lt3 13428 . . . . . . . . . 10
1211simpri 452 . . . . . . . . 9
13 3lt8 10459 . . . . . . . . 9
14 3re 10341 . . . . . . . . . 10
159, 14, 10lttri 9446 . . . . . . . . 9
1612, 13, 15mp2an 657 . . . . . . . 8
179, 10, 16ltleii 9443 . . . . . . 7
18 0re 9332 . . . . . . . . 9
19 epos 13429 . . . . . . . . 9
2018, 9, 19ltleii 9443 . . . . . . . 8
21 8pos 10368 . . . . . . . . 9
2218, 10, 21ltleii 9443 . . . . . . . 8
23 le2sq 11881 . . . . . . . 8
249, 20, 10, 22, 23mp4an 658 . . . . . . 7
2517, 24mpbi 202 . . . . . 6
2610recni 9344 . . . . . . . 8
2726sqvali 11886 . . . . . . 7
28 8t8e64 10794 . . . . . . 7
2927, 28eqtri 2442 . . . . . 6
3025, 29breqtri 4290 . . . . 5
3130a1i 11 . . . 4
329resqcli 11892 . . . . . 6
3332a1i 11 . . . . 5
346nnrei 10277 . . . . . 6
3534a1i 11 . . . . 5
368nnred 10283 . . . . 5
37 ltle 9409 . . . . . . 7
3834, 36, 37sylancr 648 . . . . . 6
391, 38mpd 15 . . . . 5
4033, 35, 36, 31, 39letrd 9474 . . . 4
412, 3, 7, 8, 31, 40bposlem7 22370 . . 3
421, 41mpd 15 . 2
432, 3bposlem8 22371 . . . . 5
4443a1i 11 . . . 4
4544simpld 449 . . 3
46 fveq2 5661 . . . . . . . . . 10
4746fveq2d 5665 . . . . . . . . 9
4847oveq2d 6077 . . . . . . . 8
49 oveq1 6068 . . . . . . . . . 10
5049fveq2d 5665 . . . . . . . . 9
5150oveq2d 6077 . . . . . . . 8
5248, 51oveq12d 6079 . . . . . . 7
53 oveq2 6069 . . . . . . . . 9
5453fveq2d 5665 . . . . . . . 8
5554oveq2d 6077 . . . . . . 7
5652, 55oveq12d 6079 . . . . . 6
57 ovex 6086 . . . . . 6
5856, 2, 57fvmpt 5744 . . . . 5
598, 58syl 16 . . . 4
60 sqr2re 13472 . . . . . . 7
618nnrpd 10971 . . . . . . . . . 10
6261rpsqrcld 12839 . . . . . . . . 9
63 fveq2 5661 . . . . . . . . . . 11
64 id 21 . . . . . . . . . . 11
6563, 64oveq12d 6079 . . . . . . . . . 10
66 ovex 6086 . . . . . . . . . 10
6765, 3, 66fvmpt 5744 . . . . . . . . 9
6862, 67syl 16 . . . . . . . 8
6962relogcld 21813 . . . . . . . . 9
7069, 62rerpdivcld 10999 . . . . . . . 8
7168, 70eqeltrd 2496 . . . . . . 7
72 remulcl 9313 . . . . . . 7
7360, 71, 72sylancr 648 . . . . . 6
74 9re 10354 . . . . . . . 8
75 4re 10344 . . . . . . . 8
76 4ne0 10364 . . . . . . . 8
7774, 75, 76redivcli 10044 . . . . . . 7
7861rphalfcld 10984 . . . . . . . . 9
79 fveq2 5661 . . . . . . . . . . 11
80 id 21 . . . . . . . . . . 11
8179, 80oveq12d 6079 . . . . . . . . . 10
82 ovex 6086 . . . . . . . . . 10
8381, 3, 82fvmpt 5744 . . . . . . . . 9
8478, 83syl 16 . . . . . . . 8
8578relogcld 21813 . . . . . . . . 9
8685, 78rerpdivcld 10999 . . . . . . . 8
8784, 86eqeltrd 2496 . . . . . . 7
88 remulcl 9313 . . . . . . 7
8977, 87, 88sylancr 648 . . . . . 6
9073, 89readdcld 9359 . . . . 5
91 2rp 10941 . . . . . . 7
92 relogcl 21768 . . . . . . 7
9391, 92ax-mp 5 . . . . . 6
94 rpmulcl 10957 . . . . . . . 8
9591, 61, 94sylancr 648 . . . . . . 7
9695rpsqrcld 12839 . . . . . 6
97 rerpdivcl 10963 . . . . . 6
9893, 96, 97sylancr 648 . . . . 5
9990, 98readdcld 9359 . . . 4
10059, 99eqeltrd 2496 . . 3
10193a1i 11 . . . 4
10244simprd 453 . . . 4
103 nnrp 10945 . . . . . . . . . . 11
1045, 103ax-mp 5 . . . . . . . . . 10
105 relogcl 21768 . . . . . . . . . 10
106104, 105ax-mp 5 . . . . . . . . 9
107 remulcl 9313 . . . . . . . . 9
10836, 106, 107sylancl 647 . . . . . . . 8
10961relogcld 21813 . . . . . . . 8
110108, 109resubcld 9722 . . . . . . 7
111 rpre 10942 . . . . . . . . . . . . 13
112 rpge0 10948 . . . . . . . . . . . . 13
113111, 112resqrcld 12845 . . . . . . . . . . . 12
11495, 113syl 16 . . . . . . . . . . 11
115 3nn 10426 . . . . . . . . . . 11
116 nndivre 10303 . . . . . . . . . . 11
117114, 115, 116sylancl 647 . . . . . . . . . 10
118 2re 10337 . . . . . . . . . 10
119 readdcl 9311 . . . . . . . . . 10
120117, 118, 119sylancl 647 . . . . . . . . 9
12195relogcld 21813 . . . . . . . . 9
122120, 121remulcld 9360 . . . . . . . 8
123 remulcl 9313 . . . . . . . . . . . 12
12475, 36, 123sylancr 648 . . . . . . . . . . 11
125 nndivre 10303 . . . . . . . . . . 11
126124, 115, 125sylancl 647 . . . . . . . . . 10
127 5re 10346 . . . . . . . . . 10
128 resubcl 9619 . . . . . . . . . 10
129126, 127, 128sylancl 647 . . . . . . . . 9
130 remulcl 9313 . . . . . . . . 9
131129, 93, 130sylancl 647 . . . . . . . 8
132122, 131readdcld 9359 . . . . . . 7
133 remulcl 9313 . . . . . . . . 9
134126, 93, 133sylancl 647 . . . . . . . 8
135134, 109resubcld 9722 . . . . . . 7
1368nnzd 10691 . . . . . . . . . . 11
137 df-5 10329 . . . . . . . . . . . 12
13875a1i 11 . . . . . . . . . . . . . 14
139 6nn 10429 . . . . . . . . . . . . . . . 16
140 4nn0 10544 . . . . . . . . . . . . . . . 16
141 4lt10 10475 . . . . . . . . . . . . . . . 16
142139, 140, 140, 141declti 10725 . . . . . . . . . . . . . . 15
143142a1i 11 . . . . . . . . . . . . . 14
144138, 35, 36, 143, 1lttrd 9478 . . . . . . . . . . . . 13
1455nnzi 10615 . . . . . . . . . . . . . 14
146 zltp1le 10639 . . . . . . . . . . . . . 14
147145, 136, 146sylancr 648 . . . . . . . . . . . . 13
148144, 147mpbid 204 . . . . . . . . . . . 12
149137, 148syl5eqbr 4300 . . . . . . . . . . 11
150 5nn 10428 . . . . . . . . . . . . 13
151150nnzi 10615 . . . . . . . . . . . 12
152151eluz1i 10813 . . . . . . . . . . 11
153136, 149, 152sylanbrc 649 . . . . . . . . . 10
154 bposlem9.5 . . . . . . . . . . 11
155 breq2 4271 . . . . . . . . . . . . 13
156 breq1 4270 . . . . . . . . . . . . 13
157155, 156anbi12d 695 . . . . . . . . . . . 12
158157cbvrexv 2927 . . . . . . . . . . 11
159154, 158sylnib 298 . . . . . . . . . 10
160 eqid 2422 . . . . . . . . . 10
161 eqid 2422 . . . . . . . . . 10
162 eqid 2422 . . . . . . . . . 10
163153, 159, 160, 161, 162bposlem6 22369 . . . . . . . . 9
164 reexplog 21784 . . . . . . . . . . . 12
165104, 136, 164sylancr 648 . . . . . . . . . . 11
16661reeflogd 21814 . . . . . . . . . . . 12
167166eqcomd 2427 . . . . . . . . . . 11
168165, 167oveq12d 6079 . . . . . . . . . 10
169108recnd 9358 . . . . . . . . . . 11
170109recnd 9358 . . . . . . . . . . 11
171 efsub 13324 . . . . . . . . . . 11
172169, 170, 171syl2anc 646 . . . . . . . . . 10
173168, 172eqtr4d 2457 . . . . . . . . 9
17495rpcnd 10974 . . . . . . . . . . . 12
17595rpne0d 10977 . . . . . . . . . . . 12
176120recnd 9358 . . . . . . . . . . . 12
177174, 175, 176cxpefd 21898 . . . . . . . . . . 11
178129recnd 9358 . . . . . . . . . . . 12
179 2cn 10338 . . . . . . . . . . . . 13
180 2ne0 10360 . . . . . . . . . . . . 13
181 cxpef 21851 . . . . . . . . . . . . 13
182179, 180, 181mp3an12 1289 . . . . . . . . . . . 12
183178, 182syl 16 . . . . . . . . . . 11
184177, 183oveq12d 6079 . . . . . . . . . 10
185122recnd 9358 . . . . . . . . . . 11
186131recnd 9358 . . . . . . . . . . 11
187 efadd 13319 . . . . . . . . . . 11
188185, 186, 187syl2anc 646 . . . . . . . . . 10
189184, 188eqtr4d 2457 . . . . . . . . 9
190163, 173, 1893brtr3d 4296 . . . . . . . 8
191 eflt 13341 . . . . . . . . 9
192110, 132, 191syl2anc 646 . . . . . . . 8
193190, 192mpbird 226 . . . . . . 7
194110, 132, 135, 193ltsub1dd 9897 . . . . . 6
19536recnd 9358 . . . . . . . . . . 11
196 mulcom 9314 . . . . . . . . . . 11
197179, 195, 196sylancr 648 . . . . . . . . . 10
198197oveq1d 6076 . . . . . . . . 9
19993recni 9344 . . . . . . . . . . . 12
200 mulass 9316 . . . . . . . . . . . 12
201179, 199, 200mp3an23 1291 . . . . . . . . . . 11
202195, 201syl 16 . . . . . . . . . 10
2031992timesi 10388 . . . . . . . . . . . 12
204 relogmul 21781 . . . . . . . . . . . . 13
20591, 91, 204mp2an 657 . . . . . . . . . . . 12
206 2t2e4 10417 . . . . . . . . . . . . 13
207206fveq2i 5664 . . . . . . . . . . . 12
208203, 205, 2073eqtr2i 2448 . . . . . . . . . . 11
209208oveq2i 6072 . . . . . . . . . 10
210202, 209syl6eq 2470 . . . . . . . . 9
211198, 210eqtrd 2454 . . . . . . . 8
212211oveq1d 6076 . . . . . . 7
213 4p2e6 10402 . . . . . . . . . . . . . . 15
214213oveq1i 6071 . . . . . . . . . . . . . 14
2155nncni 10278 . . . . . . . . . . . . . . . 16
216 adddir 9323 . . . . . . . . . . . . . . . 16
217215, 179, 216mp3an12 1289 . . . . . . . . . . . . . . 15
218195, 217syl 16 . . . . . . . . . . . . . 14
219214, 218syl5eqr 2468 . . . . . . . . . . . . 13
220219oveq1d 6076 . . . . . . . . . . . 12
221 6cn 10349 . . . . . . . . . . . . . . 15
222 3cn 10342 . . . . . . . . . . . . . . . 16
223 3ne0 10362 . . . . . . . . . . . . . . . 16
224222, 223pm3.2i 445 . . . . . . . . . . . . . . 15
225 div23 9959 . . . . . . . . . . . . . . 15
226221, 224, 225mp3an13 1290 . . . . . . . . . . . . . 14
227195, 226syl 16 . . . . . . . . . . . . 13
228 3t2e6 10419 . . . . . . . . . . . . . . . 16
229228oveq1i 6071 . . . . . . . . . . . . . . 15
230179, 222, 223divcan3i 10023 . . . . . . . . . . . . . . 15
231229, 230eqtr3i 2444 . . . . . . . . . . . . . 14
232231oveq1i 6071 . . . . . . . . . . . . 13
233227, 232syl6eq 2470 . . . . . . . . . . . 12
234124recnd 9358 . . . . . . . . . . . . 13
235 remulcl 9313 . . . . . . . . . . . . . . 15
236118, 36, 235sylancr 648 . . . . . . . . . . . . . 14
237236recnd 9358 . . . . . . . . . . . . 13
238 divdir 9963 . . . . . . . . . . . . . 14
239224, 238mp3an3 1288 . . . . . . . . . . . . 13
240234, 237, 239syl2anc 646 . . . . . . . . . . . 12
241220, 233, 2403eqtr3d 2462 . . . . . . . . . . 11
242241oveq1d 6076 . . . . . . . . . 10
243126recnd 9358 . . . . . . . . . . 11
244 nnrp 10945 . . . . . . . . . . . . . 14
245115, 244ax-mp 5 . . . . . . . . . . . . 13
246 rpdivcl 10958 . . . . . . . . . . . . 13
24795, 245, 246sylancl 647 . . . . . . . . . . . 12
248247rpcnd 10974 . . . . . . . . . . 11
249243, 248pncan2d 9667 . . . . . . . . . 10
250242, 249eqtrd 2454 . . . . . . . . 9
251250oveq1d 6076 . . . . . . . 8
252101recnd 9358 . . . . . . . . 9
253237, 243, 252subdird 9747 . . . . . . . 8
254251, 253eqtr3d 2456 . . . . . . 7
255134recnd 9358 . . . . . . . 8
256169, 255, 170nnncan2d 9700 . . . . . . 7
257212, 254, 2563eqtr4d 2464 . . . . . 6
258117recnd 9358 . . . . . . . . . 10
259179a1i 11 . . . . . . . . . 10
260121recnd 9358 . . . . . . . . . 10
261258, 259, 260adddird 9357 . . . . . . . . 9
262 relogmul 21781 . . . . . . . . . . . . 13
26391, 61, 262sylancr 648 . . . . . . . . . . . 12
264263oveq2d 6077 . . . . . . . . . . 11
265259, 252, 170adddid 9356 . . . . . . . . . . 11
266264, 265eqtrd 2454 . . . . . . . . . 10
267266oveq2d 6077 . . . . . . . . 9
268261, 267eqtrd 2454 . . . . . . . 8
269 5cn 10347 . . . . . . . . . . . 12
270269a1i 11 . . . . . . . . . . 11
271243, 270, 252subdird 9747 . . . . . . . . . 10
272271oveq1d 6076 . . . . . . . . 9
273269, 199mulcli 9337 . . . . . . . . . . 11
274273a1i 11 . . . . . . . . . 10
275255, 274, 170nnncan1d 9699 . . . . . . . . 9
276272, 275eqtrd 2454 . . . . . . . 8
277268, 276oveq12d 6079 . . . . . . 7
278135recnd 9358 . . . . . . . 8
279185, 186, 278addsubassd 9685 . . . . . . 7
280269, 222, 199subdiri 9740 . . . . . . . . . . . . 13
281 3p2e5 10400 . . . . . . . . . . . . . . . 16
282281oveq1i 6071 . . . . . . . . . . . . . . 15
283 pncan2 9563 . . . . . . . . . . . . . . . 16
284222, 179, 283mp2an 657 . . . . . . . . . . . . . . 15
285282, 284eqtr3i 2444 . . . . . . . . . . . . . 14
286285oveq1i 6071 . . . . . . . . . . . . 13
287280, 286eqtr3i 2444 . . . . . . . . . . . 12
288287a1i 11 . . . . . . . . . . 11
289 df-3 10327 . . . . . . . . . . . . . . . 16
290289oveq1i 6071 . . . . . . . . . . . . . . 15
291 1cnd 9348 . . . . . . . . . . . . . . . 16
292259, 291, 170adddird 9357 . . . . . . . . . . . . . . 15
293290, 292syl5eq 2466 . . . . . . . . . . . . . 14
294170mulid2d 9350 . . . . . . . . . . . . . . 15
295294oveq2d 6077 . . . . . . . . . . . . . 14
296293, 295eqtrd 2454 . . . . . . . . . . . . 13
297296oveq1d 6076 . . . . . . . . . . . 12
298 mulcl 9312 . . . . . . . . . . . . . 14
299179, 170, 298sylancr 648 . . . . . . . . . . . . 13
300299, 170, 274addsubassd 9685 . . . . . . . . . . . 12
301297, 300eqtrd 2454 . . . . . . . . . . 11
302288, 301oveq12d 6079 . . . . . . . . . 10
303 relogdiv 21782 . . . . . . . . . . . . . 14
30461, 91, 303sylancl 647 . . . . . . . . . . . . 13
305304oveq2d 6077 . . . . . . . . . . . 12
306 subdi 9724 . . . . . . . . . . . . . 14
307222, 199, 306mp3an13 1290 . . . . . . . . . . . . 13
308170, 307syl 16 . . . . . . . . . . . 12
309305, 308eqtrd 2454 . . . . . . . . . . 11
310 div23 9959 . . . . . . . . . . . . . . . . 17
311179, 224, 310mp3an13 1290 . . . . . . . . . . . . . . . 16
312195, 311syl 16 . . . . . . . . . . . . . . 15
313222, 179, 222, 179, 180, 180divmuldivi 10037 . . . . . . . . . . . . . . . . 17
314 3t3e9 10420 . . . . . . . . . . . . . . . . . 18
315314, 206oveq12i 6073 . . . . . . . . . . . . . . . . 17