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

Theorem bposlem9 23031
Description: Lemma for bpos 23032. 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 10738 . . . . . 6
5 4nn 10619 . . . . . 6
64, 5decnncl 10907 . . . . 5
76a1i 11 . . . 4
8 bposlem9.3 . . . 4
9 ere 13532 . . . . . . . 8
10 8re 10544 . . . . . . . 8
11 egt2lt3 13646 . . . . . . . . . 10
1211simpri 462 . . . . . . . . 9
13 3lt8 10651 . . . . . . . . 9
14 3re 10533 . . . . . . . . . 10
159, 14, 10lttri 9637 . . . . . . . . 9
1612, 13, 15mp2an 672 . . . . . . . 8
179, 10, 16ltleii 9634 . . . . . . 7
18 0re 9523 . . . . . . . . 9
19 epos 13647 . . . . . . . . 9
2018, 9, 19ltleii 9634 . . . . . . . 8
21 8pos 10560 . . . . . . . . 9
2218, 10, 21ltleii 9634 . . . . . . . 8
23 le2sq 12097 . . . . . . . 8
249, 20, 10, 22, 23mp4an 673 . . . . . . 7
2517, 24mpbi 208 . . . . . 6
2610recni 9535 . . . . . . . 8
2726sqvali 12102 . . . . . . 7
28 8t8e64 10988 . . . . . . 7
2927, 28eqtri 2483 . . . . . 6
3025, 29breqtri 4432 . . . . 5
3130a1i 11 . . . 4
329resqcli 12108 . . . . . 6
3332a1i 11 . . . . 5
346nnrei 10469 . . . . . 6
3534a1i 11 . . . . 5
368nnred 10475 . . . . 5
37 ltle 9600 . . . . . . 7
3834, 36, 37sylancr 663 . . . . . 6
391, 38mpd 15 . . . . 5
4033, 35, 36, 31, 39letrd 9665 . . . 4
412, 3, 7, 8, 31, 40bposlem7 23029 . . 3
421, 41mpd 15 . 2
432, 3bposlem8 23030 . . . . 5
4443a1i 11 . . . 4
4544simpld 459 . . 3
46 fveq2 5813 . . . . . . . . . 10
4746fveq2d 5817 . . . . . . . . 9
4847oveq2d 6238 . . . . . . . 8
49 oveq1 6229 . . . . . . . . . 10
5049fveq2d 5817 . . . . . . . . 9
5150oveq2d 6238 . . . . . . . 8
5248, 51oveq12d 6240 . . . . . . 7
53 oveq2 6230 . . . . . . . . 9
5453fveq2d 5817 . . . . . . . 8
5554oveq2d 6238 . . . . . . 7
5652, 55oveq12d 6240 . . . . . 6
57 ovex 6247 . . . . . 6
5856, 2, 57fvmpt 5897 . . . . 5
598, 58syl 16 . . . 4
60 sqr2re 13690 . . . . . . 7
618nnrpd 11165 . . . . . . . . . 10
6261rpsqrcld 13056 . . . . . . . . 9
63 fveq2 5813 . . . . . . . . . . 11
64 id 22 . . . . . . . . . . 11
6563, 64oveq12d 6240 . . . . . . . . . 10
66 ovex 6247 . . . . . . . . . 10
6765, 3, 66fvmpt 5897 . . . . . . . . 9
6862, 67syl 16 . . . . . . . 8
6962relogcld 22472 . . . . . . . . 9
7069, 62rerpdivcld 11193 . . . . . . . 8
7168, 70eqeltrd 2542 . . . . . . 7
72 remulcl 9504 . . . . . . 7
7360, 71, 72sylancr 663 . . . . . 6
74 9re 10546 . . . . . . . 8
75 4re 10536 . . . . . . . 8
76 4ne0 10556 . . . . . . . 8
7774, 75, 76redivcli 10235 . . . . . . 7
7861rphalfcld 11178 . . . . . . . . 9
79 fveq2 5813 . . . . . . . . . . 11
80 id 22 . . . . . . . . . . 11
8179, 80oveq12d 6240 . . . . . . . . . 10
82 ovex 6247 . . . . . . . . . 10
8381, 3, 82fvmpt 5897 . . . . . . . . 9
8478, 83syl 16 . . . . . . . 8
8578relogcld 22472 . . . . . . . . 9
8685, 78rerpdivcld 11193 . . . . . . . 8
8784, 86eqeltrd 2542 . . . . . . 7
88 remulcl 9504 . . . . . . 7
8977, 87, 88sylancr 663 . . . . . 6
9073, 89readdcld 9550 . . . . 5
91 2rp 11135 . . . . . . 7
92 relogcl 22427 . . . . . . 7
9391, 92ax-mp 5 . . . . . 6
94 rpmulcl 11151 . . . . . . . 8
9591, 61, 94sylancr 663 . . . . . . 7
9695rpsqrcld 13056 . . . . . 6
97 rerpdivcl 11157 . . . . . 6
9893, 96, 97sylancr 663 . . . . 5
9990, 98readdcld 9550 . . . 4
10059, 99eqeltrd 2542 . . 3
10193a1i 11 . . . 4
10244simprd 463 . . . 4
103 nnrp 11139 . . . . . . . . . . 11
1045, 103ax-mp 5 . . . . . . . . . 10
105 relogcl 22427 . . . . . . . . . 10
106104, 105ax-mp 5 . . . . . . . . 9
107 remulcl 9504 . . . . . . . . 9
10836, 106, 107sylancl 662 . . . . . . . 8
10961relogcld 22472 . . . . . . . 8
110108, 109resubcld 9913 . . . . . . 7
111 rpre 11136 . . . . . . . . . . . . 13
112 rpge0 11142 . . . . . . . . . . . . 13
113111, 112resqrcld 13062 . . . . . . . . . . . 12
11495, 113syl 16 . . . . . . . . . . 11
115 3nn 10618 . . . . . . . . . . 11
116 nndivre 10495 . . . . . . . . . . 11
117114, 115, 116sylancl 662 . . . . . . . . . 10
118 2re 10529 . . . . . . . . . 10
119 readdcl 9502 . . . . . . . . . 10
120117, 118, 119sylancl 662 . . . . . . . . 9
12195relogcld 22472 . . . . . . . . 9
122120, 121remulcld 9551 . . . . . . . 8
123 remulcl 9504 . . . . . . . . . . . 12
12475, 36, 123sylancr 663 . . . . . . . . . . 11
125 nndivre 10495 . . . . . . . . . . 11
126124, 115, 125sylancl 662 . . . . . . . . . 10
127 5re 10538 . . . . . . . . . 10
128 resubcl 9810 . . . . . . . . . 10
129126, 127, 128sylancl 662 . . . . . . . . 9
130 remulcl 9504 . . . . . . . . 9
131129, 93, 130sylancl 662 . . . . . . . 8
132122, 131readdcld 9550 . . . . . . 7
133 remulcl 9504 . . . . . . . . 9
134126, 93, 133sylancl 662 . . . . . . . 8
135134, 109resubcld 9913 . . . . . . 7
1368nnzd 10884 . . . . . . . . . . 11
137 df-5 10521 . . . . . . . . . . . 12
13875a1i 11 . . . . . . . . . . . . . 14
139 6nn 10621 . . . . . . . . . . . . . . . 16
140 4nn0 10736 . . . . . . . . . . . . . . . 16
141 4lt10 10667 . . . . . . . . . . . . . . . 16
142139, 140, 140, 141declti 10919 . . . . . . . . . . . . . . 15
143142a1i 11 . . . . . . . . . . . . . 14
144138, 35, 36, 143, 1lttrd 9669 . . . . . . . . . . . . 13
1455nnzi 10808 . . . . . . . . . . . . . 14
146 zltp1le 10832 . . . . . . . . . . . . . 14
147145, 136, 146sylancr 663 . . . . . . . . . . . . 13
148144, 147mpbid 210 . . . . . . . . . . . 12
149137, 148syl5eqbr 4442 . . . . . . . . . . 11
150 5nn 10620 . . . . . . . . . . . . 13
151150nnzi 10808 . . . . . . . . . . . 12
152151eluz1i 11007 . . . . . . . . . . 11
153136, 149, 152sylanbrc 664 . . . . . . . . . 10
154 bposlem9.5 . . . . . . . . . . 11
155 breq2 4413 . . . . . . . . . . . . 13
156 breq1 4412 . . . . . . . . . . . . 13
157155, 156anbi12d 710 . . . . . . . . . . . 12
158157cbvrexv 3057 . . . . . . . . . . 11
159154, 158sylnib 304 . . . . . . . . . 10
160 eqid 2454 . . . . . . . . . 10
161 eqid 2454 . . . . . . . . . 10
162 eqid 2454 . . . . . . . . . 10
163153, 159, 160, 161, 162bposlem6 23028 . . . . . . . . 9
164 reexplog 22443 . . . . . . . . . . . 12
165104, 136, 164sylancr 663 . . . . . . . . . . 11
16661reeflogd 22473 . . . . . . . . . . . 12
167166eqcomd 2462 . . . . . . . . . . 11
168165, 167oveq12d 6240 . . . . . . . . . 10
169108recnd 9549 . . . . . . . . . . 11
170109recnd 9549 . . . . . . . . . . 11
171 efsub 13542 . . . . . . . . . . 11
172169, 170, 171syl2anc 661 . . . . . . . . . 10
173168, 172eqtr4d 2498 . . . . . . . . 9
17495rpcnd 11168 . . . . . . . . . . . 12
17595rpne0d 11171 . . . . . . . . . . . 12
176120recnd 9549 . . . . . . . . . . . 12
177174, 175, 176cxpefd 22557 . . . . . . . . . . 11
178129recnd 9549 . . . . . . . . . . . 12
179 2cn 10530 . . . . . . . . . . . . 13
180 2ne0 10552 . . . . . . . . . . . . 13
181 cxpef 22510 . . . . . . . . . . . . 13
182179, 180, 181mp3an12 1305 . . . . . . . . . . . 12
183178, 182syl 16 . . . . . . . . . . 11
184177, 183oveq12d 6240 . . . . . . . . . 10
185122recnd 9549 . . . . . . . . . . 11
186131recnd 9549 . . . . . . . . . . 11
187 efadd 13537 . . . . . . . . . . 11
188185, 186, 187syl2anc 661 . . . . . . . . . 10
189184, 188eqtr4d 2498 . . . . . . . . 9
190163, 173, 1893brtr3d 4438 . . . . . . . 8
191 eflt 13559 . . . . . . . . 9
192110, 132, 191syl2anc 661 . . . . . . . 8
193190, 192mpbird 232 . . . . . . 7
194110, 132, 135, 193ltsub1dd 10088 . . . . . 6
19536recnd 9549 . . . . . . . . . . 11
196 mulcom 9505 . . . . . . . . . . 11
197179, 195, 196sylancr 663 . . . . . . . . . 10
198197oveq1d 6237 . . . . . . . . 9
19993recni 9535 . . . . . . . . . . . 12
200 mulass 9507 . . . . . . . . . . . 12
201179, 199, 200mp3an23 1307 . . . . . . . . . . 11
202195, 201syl 16 . . . . . . . . . 10
2031992timesi 10580 . . . . . . . . . . . 12
204 relogmul 22440 . . . . . . . . . . . . 13
20591, 91, 204mp2an 672 . . . . . . . . . . . 12
206 2t2e4 10609 . . . . . . . . . . . . 13
207206fveq2i 5816 . . . . . . . . . . . 12
208203, 205, 2073eqtr2i 2489 . . . . . . . . . . 11
209208oveq2i 6233 . . . . . . . . . 10
210202, 209syl6eq 2511 . . . . . . . . 9
211198, 210eqtrd 2495 . . . . . . . 8
212211oveq1d 6237 . . . . . . 7
213 4p2e6 10594 . . . . . . . . . . . . . . 15
214213oveq1i 6232 . . . . . . . . . . . . . 14
2155nncni 10470 . . . . . . . . . . . . . . . 16
216 adddir 9514 . . . . . . . . . . . . . . . 16
217215, 179, 216mp3an12 1305 . . . . . . . . . . . . . . 15
218195, 217syl 16 . . . . . . . . . . . . . 14
219214, 218syl5eqr 2509 . . . . . . . . . . . . 13
220219oveq1d 6237 . . . . . . . . . . . 12
221 6cn 10541 . . . . . . . . . . . . . . 15
222 3cn 10534 . . . . . . . . . . . . . . . 16
223 3ne0 10554 . . . . . . . . . . . . . . . 16
224222, 223pm3.2i 455 . . . . . . . . . . . . . . 15
225 div23 10150 . . . . . . . . . . . . . . 15
226221, 224, 225mp3an13 1306 . . . . . . . . . . . . . 14
227195, 226syl 16 . . . . . . . . . . . . 13
228 3t2e6 10611 . . . . . . . . . . . . . . . 16
229228oveq1i 6232 . . . . . . . . . . . . . . 15
230179, 222, 223divcan3i 10214 . . . . . . . . . . . . . . 15
231229, 230eqtr3i 2485 . . . . . . . . . . . . . 14
232231oveq1i 6232 . . . . . . . . . . . . 13
233227, 232syl6eq 2511 . . . . . . . . . . . 12
234124recnd 9549 . . . . . . . . . . . . 13
235 remulcl 9504 . . . . . . . . . . . . . . 15
236118, 36, 235sylancr 663 . . . . . . . . . . . . . 14
237236recnd 9549 . . . . . . . . . . . . 13
238 divdir 10154 . . . . . . . . . . . . . 14
239224, 238mp3an3 1304 . . . . . . . . . . . . 13
240234, 237, 239syl2anc 661 . . . . . . . . . . . 12
241220, 233, 2403eqtr3d 2503 . . . . . . . . . . 11
242241oveq1d 6237 . . . . . . . . . 10
243126recnd 9549 . . . . . . . . . . 11
244 nnrp 11139 . . . . . . . . . . . . . 14
245115, 244ax-mp 5 . . . . . . . . . . . . 13
246 rpdivcl 11152 . . . . . . . . . . . . 13
24795, 245, 246sylancl 662 . . . . . . . . . . . 12
248247rpcnd 11168 . . . . . . . . . . 11
249243, 248pncan2d 9858 . . . . . . . . . 10
250242, 249eqtrd 2495 . . . . . . . . 9
251250oveq1d 6237 . . . . . . . 8
252101recnd 9549 . . . . . . . . 9
253237, 243, 252subdird 9938 . . . . . . . 8
254251, 253eqtr3d 2497 . . . . . . 7
255134recnd 9549 . . . . . . . 8
256169, 255, 170nnncan2d 9891 . . . . . . 7
257212, 254, 2563eqtr4d 2505 . . . . . 6
258117recnd 9549 . . . . . . . . . 10
259179a1i 11 . . . . . . . . . 10
260121recnd 9549 . . . . . . . . . 10
261258, 259, 260adddird 9548 . . . . . . . . 9
262 relogmul 22440 . . . . . . . . . . . . 13
26391, 61, 262sylancr 663 . . . . . . . . . . . 12
264263oveq2d 6238 . . . . . . . . . . 11
265259, 252, 170adddid 9547 . . . . . . . . . . 11
266264, 265eqtrd 2495 . . . . . . . . . 10
267266oveq2d 6238 . . . . . . . . 9
268261, 267eqtrd 2495 . . . . . . . 8
269 5cn 10539 . . . . . . . . . . . 12
270269a1i 11 . . . . . . . . . . 11
271243, 270, 252subdird 9938 . . . . . . . . . 10
272271oveq1d 6237 . . . . . . . . 9
273269, 199mulcli 9528 . . . . . . . . . . 11
274273a1i 11 . . . . . . . . . 10
275255, 274, 170nnncan1d 9890 . . . . . . . . 9
276272, 275eqtrd 2495 . . . . . . . 8
277268, 276oveq12d 6240 . . . . . . 7
278135recnd 9549 . . . . . . . 8
279185, 186, 278addsubassd 9876 . . . . . . 7
280269, 222, 199subdiri 9931 . . . . . . . . . . . . 13
281 3p2e5 10592 . . . . . . . . . . . . . . . 16
282281oveq1i 6232 . . . . . . . . . . . . . . 15
283 pncan2 9754 . . . . . . . . . . . . . . . 16
284222, 179, 283mp2an 672 . . . . . . . . . . . . . . 15
285282, 284eqtr3i 2485 . . . . . . . . . . . . . 14
286285oveq1i 6232 . . . . . . . . . . . . 13
287280, 286eqtr3i 2485 . . . . . . . . . . . 12
288287a1i 11 . . . . . . . . . . 11
289 df-3 10519 . . . . . . . . . . . . . . . 16
290289oveq1i 6232 . . . . . . . . . . . . . . 15
291 1cnd 9539 . . . . . . . . . . . . . . . 16
292259, 291, 170adddird 9548 . . . . . . . . . . . . . . 15
293290, 292syl5eq 2507 . . . . . . . . . . . . . 14
294170mulid2d 9541 . . . . . . . . . . . . . . 15
295294oveq2d 6238 . . . . . . . . . . . . . 14
296293, 295eqtrd 2495 . . . . . . . . . . . . 13
297296oveq1d 6237 . . . . . . . . . . . 12
298 mulcl 9503 . . . . . . . . . . . . . 14
299179, 170, 298sylancr 663 . . . . . . . . . . . . 13
300299, 170, 274addsubassd 9876 . . . . . . . . . . . 12
301297, 300eqtrd 2495 . . . . . . . . . . 11
302288, 301oveq12d 6240 . . . . . . . . . 10
303 relogdiv 22441 . . . . . . . . . . . . . 14
30461, 91, 303sylancl 662 . . . . . . . . . . . . 13
305304oveq2d 6238 . . . . . . . . . . . 12
306 subdi 9915 . . . . . . . . . . . . . 14
307222, 199, 306mp3an13 1306 . . . . . . . . . . . . 13
308170, 307syl 16 . . . . . . . . . . . 12
309305, 308eqtrd 2495 . . . . . . . . . . 11
310 div23 10150 . . . . . . . . . . . . . . . . 17
311179, 224, 310mp3an13 1306 . . . . . . . . . . . . . . . 16
312195, 311syl 16 . . . . . . . . . . . . . . 15
313222, 179, 222, 179, 180, 180divmuldivi 10228 . . . . . . . . . . . . . . . . 17
314 3t3e9 10612 . . . . . . . . . . . . . . . . . 18
315314, 206oveq12i 6234 . . . . . . . . . . . . . . . . 17