Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
| Mirrors > Home > MPE Home > Th. List > xlemul1a | Structured version Unicode version | |
| Description: Extended real version of lemul1a 10397. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| Ref | Expression |
|---|---|
| xlemul1a |
     ![/\](wedge.gif "/\"){kind=small}  
      |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0xr 9641 |
. . . . . 6
| |
| 2 | simpr 461 |
. . . . . 6
| |
| 3 | xrleloe 11351 |
. . . . . 6
   | |
| 4 | 1, 2, 3 | sylancr 663 |
. . . . 5
|
| 5 | simplll 757 |
. . . . . . . . 9
| |
| 6 | elxr 11326 |
. . . . . . . . 9
   | |
| 7 | 5, 6 | sylib 196 |
. . . . . . . 8
|
| 8 | simpllr 758 |
. . . . . . . . . . . 12
| |
| 9 | elxr 11326 |
. . . . . . . . . . . 12
| |
| 10 | 8, 9 | sylib 196 |
. . . . . . . . . . 11
|
| 11 | 10 | adantr 465 |
. . . . . . . . . 10
|
| 12 | simpllr 758 |
. . . . . . . . . . . . . 14
| |
| 13 | elxr 11326 |
. . . . . . . . . . . . . 14
| |
| 14 | 12, 13 | sylib 196 |
. . . . . . . . . . . . 13
|
| 15 | simplrr 760 |
. . . . . . . . . . . . . . . . 17
| |
| 16 | simprll 761 |
. . . . . . . . . . . . . . . . . 18
| |
| 17 | simprlr 762 |
. . . . . . . . . . . . . . . . . 18
| |
| 18 | simprr 756 |
. . . . . . . . . . . . . . . . . 18
| |
| 19 | simplrl 759 |
. . . . . . . . . . . . . . . . . 18
| |
| 20 | lemul1 10395 |
. . . . . . . . . . . . . . . . . 18
| |
| 21 | 16, 17, 18, 19, 20 | syl112anc 1232 |
. . . . . . . . . . . . . . . . 17
|
| 22 | 15, 21 | mpbid 210 |
. . . . . . . . . . . . . . . 16
|
| 23 | rexmul 11464 |
. . . . . . . . . . . . . . . . 17
| |
| 24 | 16, 18, 23 | syl2anc 661 |
. . . . . . . . . . . . . . . 16
|
| 25 | rexmul 11464 |
. . . . . . . . . . . . . . . . 17
| |
| 26 | 17, 18, 25 | syl2anc 661 |
. . . . . . . . . . . . . . . 16
|
| 27 | 22, 24, 26 | 3brtr4d 4477 |
. . . . . . . . . . . . . . 15
|
| 28 | 27 | expr 615 |
. . . . . . . . . . . . . 14
|
| 29 | simprl 755 |
. . . . . . . . . . . . . . . . 17
| |
| 30 | 0re 9597 |
. . . . . . . . . . . . . . . . 17
| |
| 31 | lttri4 9670 |
. . . . . . . . . . . . . . . . 17
| |
| 32 | 29, 30, 31 | sylancl 662 |
. . . . . . . . . . . . . . . 16
|
| 33 | 5 | adantr 465 |
. . . . . . . . . . . . . . . . . . . 20
|
| 34 | xmulpnf1n 11471 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 35 | 33, 34 | sylan 471 |
. . . . . . . . . . . . . . . . . . 19
|
| 36 | 8 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 37 | 36 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 38 | pnfxr 11322 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 39 | xmulcl 11466 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 40 | 37, 38, 39 | sylancl 662 |
. . . . . . . . . . . . . . . . . . . 20
|
| 41 | mnfle 11343 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 42 | 40, 41 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
|
| 43 | 35, 42 | eqbrtrd 4467 |
. . . . . . . . . . . . . . . . . 18
|
| 44 | 43 | ex 434 |
. . . . . . . . . . . . . . . . 17
|
| 45 | oveq1 6292 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 46 | xmul02 11461 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 47 | 38, 46 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 48 | 45, 47 | syl6eq 2524 |
. . . . . . . . . . . . . . . . . . . 20
|
| 49 | 48 | adantl 466 |
. . . . . . . . . . . . . . . . . . 19
|
| 50 | simplrr 760 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 51 | breq1 4450 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 52 | 50, 51 | syl5ibcom 220 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 53 | simprr 756 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 54 | leloe 9672 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 55 | 30, 53, 54 | sylancr 663 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 56 | 52, 55 | sylibd 214 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 57 | 56 | imp 429 |
. . . . . . . . . . . . . . . . . . . 20
|
| 58 | pnfge 11340 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 59 | 1, 58 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 60 | xmulpnf1 11467 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 61 | 36, 60 | sylan 471 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 62 | 59, 61 | syl5breqr 4483 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 63 | xrleid 11357 |
. . . . . . . . . . . . . . . . . . . . . . . 24
| |
| 64 | 1, 63 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 65 | 64, 47 | breqtrri 4472 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 66 | simpr 461 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 67 | 66 | oveq1d 6300 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 68 | 65, 67 | syl5breq 4482 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 69 | 62, 68 | jaodan 783 |
. . . . . . . . . . . . . . . . . . . 20
|
| 70 | 57, 69 | syldan 470 |
. . . . . . . . . . . . . . . . . . 19
|
| 71 | 49, 70 | eqbrtrd 4467 |
. . . . . . . . . . . . . . . . . 18
|
| 72 | 71 | ex 434 |
. . . . . . . . . . . . . . . . 17
|
| 73 | pnfge 11340 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 74 | 38, 73 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
|
| 75 | 5 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 76 | simprr 756 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 77 | xmulpnf1 11467 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 78 | 75, 76, 77 | syl2anc 661 |
. . . . . . . . . . . . . . . . . . . 20
|
| 79 | 8 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 80 | ltletr 9677 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
| |
| 81 | 30, 80 | mp3an1 1311 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 82 | 81 | adantl 466 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 83 | 50, 82 | mpan2d 674 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 84 | 83 | impr 619 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 85 | 79, 84, 60 | syl2anc 661 |
. . . . . . . . . . . . . . . . . . . 20
|
| 86 | 78, 85 | breq12d 4460 |
. . . . . . . . . . . . . . . . . . 19
|
| 87 | 74, 86 | mpbiri 233 |
. . . . . . . . . . . . . . . . . 18
|
| 88 | 87 | expr 615 |
. . . . . . . . . . . . . . . . 17
|
| 89 | 44, 72, 88 | 3jaod 1292 |
. . . . . . . . . . . . . . . 16
|
| 90 | 32, 89 | mpd 15 |
. . . . . . . . . . . . . . 15
|
| 91 | oveq2 6293 |
. . . . . . . . . . . . . . . 16
| |
| 92 | oveq2 6293 |
. . . . . . . . . . . . . . . 16
| |
| 93 | 91, 92 | breq12d 4460 |
. . . . . . . . . . . . . . 15
|
| 94 | 90, 93 | syl5ibrcom 222 |
. . . . . . . . . . . . . 14
|
| 95 | nltmnf 11339 |
. . . . . . . . . . . . . . . . . . . 20
 | |
| 96 | 1, 95 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
|
| 97 | breq2 4451 |
. . . . . . . . . . . . . . . . . . 19
| |
| 98 | 96, 97 | mtbiri 303 |
. . . . . . . . . . . . . . . . . 18
|
| 99 | 98 | con2i 120 |
. . . . . . . . . . . . . . . . 17
|
| 100 | 99 | ad2antrl 727 |
. . . . . . . . . . . . . . . 16
|
| 101 | 100 | adantr 465 |
. . . . . . . . . . . . . . 15
|
| 102 | 101 | pm2.21d 106 |
. . . . . . . . . . . . . 14
|
| 103 | 28, 94, 102 | 3jaod 1292 |
. . . . . . . . . . . . 13
|
| 104 | 14, 103 | mpd 15 |
. . . . . . . . . . . 12
|
| 105 | 104 | anassrs 648 |
. . . . . . . . . . 11
|
| 106 | xmulcl 11466 |
. . . . . . . . . . . . . . . 16
| |
| 107 | 106 | adantlr 714 |
. . . . . . . . . . . . . . 15
|
| 108 | 107 | ad2antrr 725 |
. . . . . . . . . . . . . 14
|
| 109 | pnfge 11340 |
. . . . . . . . . . . . . 14
| |
| 110 | 108, 109 | syl 16 |
. . . . . . . . . . . . 13
|
| 111 | oveq1 6292 |
. . . . . . . . . . . . . 14
| |
| 112 | xmulpnf2 11468 |
. . . . . . . . . . . . . . 15
| |
| 113 | 112 | ad2ant2lr 747 |
. . . . . . . . . . . . . 14
|
| 114 | 111, 113 | sylan9eqr 2530 |
. . . . . . . . . . . . 13
|
| 115 | 110, 114 | breqtrrd 4473 |
. . . . . . . . . . . 12
|
| 116 | 115 | adantlr 714 |
. . . . . . . . . . 11
|
| 117 | simplrr 760 |
. . . . . . . . . . . . . . 15
| |
| 118 | simpr 461 |
. . . . . . . . . . . . . . . 16
| |
| 119 | 5 | adantr 465 |
. . . . . . . . . . . . . . . . 17
|
| 120 | mnfle 11343 |
. . . . . . . . . . . . . . . . 17
| |
| 121 | 119, 120 | syl 16 |
. . . . . . . . . . . . . . . 16
|
| 122 | 118, 121 | eqbrtrd 4467 |
. . . . . . . . . . . . . . 15
|
| 123 | xrletri3 11359 |
. . . . . . . . . . . . . . . 16
| |
| 124 | 123 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
|
| 125 | 117, 122, 124 | mpbir2and 920 |
. . . . . . . . . . . . . 14
|
| 126 | 125 | oveq1d 6300 |
. . . . . . . . . . . . 13
|
| 127 | xmulcl 11466 |
. . . . . . . . . . . . . . . 16
| |
| 128 | 127 | adantll 713 |
. . . . . . . . . . . . . . 15
|
| 129 | 128 | ad2antrr 725 |
. . . . . . . . . . . . . 14
|
| 130 | xrleid 11357 |
. . . . . . . . . . . . . 14
| |
| 131 | 129, 130 | syl 16 |
. . . . . . . . . . . . 13
|
| 132 | 126, 131 | eqbrtrd 4467 |
. . . . . . . . . . . 12
|
| 133 | 132 | adantlr 714 |
. . . . . . . . . . 11
|
| 134 | 105, 116, 133 | 3jaodan 1294 |
. . . . . . . . . 10
|
| 135 | 11, 134 | mpdan 668 |
. . . . . . . . 9
|
| 136 | simplrr 760 |
. . . . . . . . . . . 12
| |
| 137 | 8 | adantr 465 |
. . . . . . . . . . . . . 14
|
| 138 | pnfge 11340 |
. . . . . . . . . . . . . 14
| |
| 139 | 137, 138 | syl 16 |
. . . . . . . . . . . . 13
|
| 140 | simpr 461 |
. . . . . . . . . . . . 13
| |
| 141 | 139, 140 | breqtrrd 4473 |
. . . . . . . . . . . 12
|
| 142 | 123 | ad3antrrr 729 |
. . . . . . . . . . . 12
|
| 143 | 136, 141, 142 | mpbir2and 920 |
. . . . . . . . . . 11
|
| 144 | 143 | oveq1d 6300 |
. . . . . . . . . 10
|
| 145 | 128, 130 | syl 16 |
. . . . . . . . . . 11
|
| 146 | 145 | ad2antrr 725 |
. . . . . . . . . 10
|
| 147 | 144, 146 | eqbrtrd 4467 |
. . . . . . . . 9
|
| 148 | oveq1 6292 |
. . . . . . . . . . 11
| |
| 149 | xmulmnf2 11470 |
. . . . . . . . . . . 12
| |
| 150 | 149 | ad2ant2lr 747 |
. . . . . . . . . . 11
|
| 151 | 148, 150 | sylan9eqr 2530 |
. . . . . . . . . 10
|
| 152 | 128 | ad2antrr 725 |
. . . . . . . . . . 11
|
| 153 | mnfle 11343 |
. . . . . . . . . . 11
| |
| 154 | 152, 153 | syl 16 |
. . . . . . . . . 10
|
| 155 | 151, 154 | eqbrtrd 4467 |
. . . . . . . . 9
|
| 156 | 135, 147, 155 | 3jaodan 1294 |
. . . . . . . 8
|
| 157 | 7, 156 | mpdan 668 |
. . . . . . 7
|
| 158 | 157 | exp32 605 |
. . . . . 6
|
| 159 | xmul01 11460 |
. . . . . . . . . . 11
| |
| 160 | 159 | ad2antrr 725 |
. . . . . . . . . 10
|
| 161 | xmul01 11460 |
. . . . . . . . . . 11
| |
| 162 | 161 | ad2antlr 726 |
. . . . . . . . . 10
|
| 163 | 160, 162 | breq12d 4460 |
. . . . . . . . 9
|
| 164 | 64, 163 | mpbiri 233 |
. . . . . . . 8
|
| 165 | oveq2 6293 |
. . . . . . . . 9
| |
| 166 | oveq2 6293 |
. . . . . . . . 9
| |
| 167 | 165, 166 | breq12d 4460 |
. . . . . . . 8
|
| 168 | 164, 167 | syl5ibcom 220 |
. . . . . . 7
|
| 169 | 168 | a1dd 46 |
. . . . . 6
|
| 170 | 158, 169 | jaod 380 |
. . . . 5
|
| 171 | 4, 170 | sylbid 215 |
. . . 4
|
| 172 | 171 | expimpd 603 |
. . 3
|
| 173 | 172 | 3impia 1193 |
. 2
|
| 174 | 173 | imp 429 |
1
|
| Colors of variables: wff setvar class |
| Syntax hints: wn 3
wi 4
wb 184 wo 368 wa 369 w3o 972 w3a 973 wceq 1379 wcel 1767 class class class wbr 4447
(class class class)co 6285 cr 9492 cc0 9493 cmul 9498 cpnf 9626 cmnf 9627 cxr 9628 clt 9629 cle 9630 cxmu 11318 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6577 ax-cnex 9549 ax-resscn 9550 ax-1cn 9551 ax-icn 9552 ax-addcl 9553 ax-addrcl 9554 ax-mulcl 9555 ax-mulrcl 9556 ax-mulcom 9557 ax-addass 9558 ax-mulass 9559 ax-distr 9560 ax-i2m1 9561 ax-1ne0 9562 ax-1rid 9563 ax-rnegex 9564 ax-rrecex 9565 ax-cnre 9566 ax-pre-lttri 9567 ax-pre-lttrn 9568 ax-pre-ltadd 9569 ax-pre-mulgt0 9570 |
| This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-op 4034 df-uni 4246 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-id 4795 df-po 4800 df-so 4801 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fn 5591 df-f 5592 df-f1 5593 df-fo 5594 df-f1o 5595 df-fv 5596 df-riota 6246 df-ov 6288 df-oprab 6289 df-mpt2 6290 df-1st 6785 df-2nd 6786 df-er 7312 df-en 7518 df-dom 7519 df-sdom 7520 df-pnf 9631 df-mnf 9632 df-xr 9633 df-ltxr 9634 df-le 9635 df-sub 9808 df-neg 9809 df-xneg 11319 df-xmul 11321 |
| This theorem is referenced by: xlemul2a 11482 xlemul1 11483 nmoi2 21064 esumcst 27822 |
| Copyright terms: Public domain | W3C validator |