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 10179. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| Ref | Expression |
|---|---|
| xlemul1a |
     ![/\](wedge.gif "/\"){kind=small}  
      |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0xr 9426 |
. . . . . 6
| |
| 2 | simpr 458 |
. . . . . 6
| |
| 3 | xrleloe 11117 |
. . . . . 6
   | |
| 4 | 1, 2, 3 | sylancr 658 |
. . . . 5
|
| 5 | simplll 752 |
. . . . . . . . 9
| |
| 6 | elxr 11092 |
. . . . . . . . 9
   | |
| 7 | 5, 6 | sylib 196 |
. . . . . . . 8
|
| 8 | simpllr 753 |
. . . . . . . . . . . 12
| |
| 9 | elxr 11092 |
. . . . . . . . . . . 12
| |
| 10 | 8, 9 | sylib 196 |
. . . . . . . . . . 11
|
| 11 | 10 | adantr 462 |
. . . . . . . . . 10
|
| 12 | simpllr 753 |
. . . . . . . . . . . . . 14
| |
| 13 | elxr 11092 |
. . . . . . . . . . . . . 14
| |
| 14 | 12, 13 | sylib 196 |
. . . . . . . . . . . . 13
|
| 15 | simplrr 755 |
. . . . . . . . . . . . . . . . 17
| |
| 16 | simprll 756 |
. . . . . . . . . . . . . . . . . 18
| |
| 17 | simprlr 757 |
. . . . . . . . . . . . . . . . . 18
| |
| 18 | simprr 751 |
. . . . . . . . . . . . . . . . . 18
| |
| 19 | simplrl 754 |
. . . . . . . . . . . . . . . . . 18
| |
| 20 | lemul1 10177 |
. . . . . . . . . . . . . . . . . 18
| |
| 21 | 16, 17, 18, 19, 20 | syl112anc 1217 |
. . . . . . . . . . . . . . . . 17
|
| 22 | 15, 21 | mpbid 210 |
. . . . . . . . . . . . . . . 16
|
| 23 | rexmul 11230 |
. . . . . . . . . . . . . . . . 17
| |
| 24 | 16, 18, 23 | syl2anc 656 |
. . . . . . . . . . . . . . . 16
|
| 25 | rexmul 11230 |
. . . . . . . . . . . . . . . . 17
| |
| 26 | 17, 18, 25 | syl2anc 656 |
. . . . . . . . . . . . . . . 16
|
| 27 | 22, 24, 26 | 3brtr4d 4319 |
. . . . . . . . . . . . . . 15
|
| 28 | 27 | expr 612 |
. . . . . . . . . . . . . 14
|
| 29 | simprl 750 |
. . . . . . . . . . . . . . . . 17
| |
| 30 | 0re 9382 |
. . . . . . . . . . . . . . . . 17
| |
| 31 | lttri4 9455 |
. . . . . . . . . . . . . . . . 17
| |
| 32 | 29, 30, 31 | sylancl 657 |
. . . . . . . . . . . . . . . 16
|
| 33 | 5 | adantr 462 |
. . . . . . . . . . . . . . . . . . . 20
|
| 34 | xmulpnf1n 11237 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 35 | 33, 34 | sylan 468 |
. . . . . . . . . . . . . . . . . . 19
|
| 36 | 8 | adantr 462 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 37 | 36 | adantr 462 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 38 | pnfxr 11088 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 39 | xmulcl 11232 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 40 | 37, 38, 39 | sylancl 657 |
. . . . . . . . . . . . . . . . . . . 20
|
| 41 | mnfle 11109 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 42 | 40, 41 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
|
| 43 | 35, 42 | eqbrtrd 4309 |
. . . . . . . . . . . . . . . . . 18
|
| 44 | 43 | ex 434 |
. . . . . . . . . . . . . . . . 17
|
| 45 | oveq1 6097 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 46 | xmul02 11227 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 47 | 38, 46 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 48 | 45, 47 | syl6eq 2489 |
. . . . . . . . . . . . . . . . . . . 20
|
| 49 | 48 | adantl 463 |
. . . . . . . . . . . . . . . . . . 19
|
| 50 | simplrr 755 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 51 | breq1 4292 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 52 | 50, 51 | syl5ibcom 220 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 53 | simprr 751 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 54 | leloe 9457 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 55 | 30, 53, 54 | sylancr 658 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 56 | 52, 55 | sylibd 214 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 57 | 56 | imp 429 |
. . . . . . . . . . . . . . . . . . . 20
|
| 58 | pnfge 11106 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 59 | 1, 58 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 60 | xmulpnf1 11233 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 61 | 36, 60 | sylan 468 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 62 | 59, 61 | syl5breqr 4325 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 63 | xrleid 11123 |
. . . . . . . . . . . . . . . . . . . . . . . 24
| |
| 64 | 1, 63 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 65 | 64, 47 | breqtrri 4314 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 66 | simpr 458 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 67 | 66 | oveq1d 6105 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 68 | 65, 67 | syl5breq 4324 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 69 | 62, 68 | jaodan 778 |
. . . . . . . . . . . . . . . . . . . 20
|
| 70 | 57, 69 | syldan 467 |
. . . . . . . . . . . . . . . . . . 19
|
| 71 | 49, 70 | eqbrtrd 4309 |
. . . . . . . . . . . . . . . . . 18
|
| 72 | 71 | ex 434 |
. . . . . . . . . . . . . . . . 17
|
| 73 | pnfge 11106 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 74 | 38, 73 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
|
| 75 | 5 | adantr 462 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 76 | simprr 751 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 77 | xmulpnf1 11233 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 78 | 75, 76, 77 | syl2anc 656 |
. . . . . . . . . . . . . . . . . . . 20
|
| 79 | 8 | adantr 462 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 80 | ltletr 9462 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
| |
| 81 | 30, 80 | mp3an1 1296 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 82 | 81 | adantl 463 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 83 | 50, 82 | mpan2d 669 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 84 | 83 | impr 616 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 85 | 79, 84, 60 | syl2anc 656 |
. . . . . . . . . . . . . . . . . . . 20
|
| 86 | 78, 85 | breq12d 4302 |
. . . . . . . . . . . . . . . . . . 19
|
| 87 | 74, 86 | mpbiri 233 |
. . . . . . . . . . . . . . . . . 18
|
| 88 | 87 | expr 612 |
. . . . . . . . . . . . . . . . 17
|
| 89 | 44, 72, 88 | 3jaod 1277 |
. . . . . . . . . . . . . . . 16
|
| 90 | 32, 89 | mpd 15 |
. . . . . . . . . . . . . . 15
|
| 91 | oveq2 6098 |
. . . . . . . . . . . . . . . 16
| |
| 92 | oveq2 6098 |
. . . . . . . . . . . . . . . 16
| |
| 93 | 91, 92 | breq12d 4302 |
. . . . . . . . . . . . . . 15
|
| 94 | 90, 93 | syl5ibrcom 222 |
. . . . . . . . . . . . . 14
|
| 95 | nltmnf 11105 |
. . . . . . . . . . . . . . . . . . . 20
 | |
| 96 | 1, 95 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
|
| 97 | breq2 4293 |
. . . . . . . . . . . . . . . . . . 19
| |
| 98 | 96, 97 | mtbiri 303 |
. . . . . . . . . . . . . . . . . 18
|
| 99 | 98 | con2i 120 |
. . . . . . . . . . . . . . . . 17
|
| 100 | 99 | ad2antrl 722 |
. . . . . . . . . . . . . . . 16
|
| 101 | 100 | adantr 462 |
. . . . . . . . . . . . . . 15
|
| 102 | 101 | pm2.21d 106 |
. . . . . . . . . . . . . 14
|
| 103 | 28, 94, 102 | 3jaod 1277 |
. . . . . . . . . . . . 13
|
| 104 | 14, 103 | mpd 15 |
. . . . . . . . . . . 12
|
| 105 | 104 | anassrs 643 |
. . . . . . . . . . 11
|
| 106 | xmulcl 11232 |
. . . . . . . . . . . . . . . 16
| |
| 107 | 106 | adantlr 709 |
. . . . . . . . . . . . . . 15
|
| 108 | 107 | ad2antrr 720 |
. . . . . . . . . . . . . 14
|
| 109 | pnfge 11106 |
. . . . . . . . . . . . . 14
| |
| 110 | 108, 109 | syl 16 |
. . . . . . . . . . . . 13
|
| 111 | oveq1 6097 |
. . . . . . . . . . . . . 14
| |
| 112 | xmulpnf2 11234 |
. . . . . . . . . . . . . . 15
| |
| 113 | 112 | ad2ant2lr 742 |
. . . . . . . . . . . . . 14
|
| 114 | 111, 113 | sylan9eqr 2495 |
. . . . . . . . . . . . 13
|
| 115 | 110, 114 | breqtrrd 4315 |
. . . . . . . . . . . 12
|
| 116 | 115 | adantlr 709 |
. . . . . . . . . . 11
|
| 117 | simplrr 755 |
. . . . . . . . . . . . . . 15
| |
| 118 | simpr 458 |
. . . . . . . . . . . . . . . 16
| |
| 119 | 5 | adantr 462 |
. . . . . . . . . . . . . . . . 17
|
| 120 | mnfle 11109 |
. . . . . . . . . . . . . . . . 17
| |
| 121 | 119, 120 | syl 16 |
. . . . . . . . . . . . . . . 16
|
| 122 | 118, 121 | eqbrtrd 4309 |
. . . . . . . . . . . . . . 15
|
| 123 | xrletri3 11125 |
. . . . . . . . . . . . . . . 16
| |
| 124 | 123 | ad3antrrr 724 |
. . . . . . . . . . . . . . 15
|
| 125 | 117, 122, 124 | mpbir2and 908 |
. . . . . . . . . . . . . 14
|
| 126 | 125 | oveq1d 6105 |
. . . . . . . . . . . . 13
|
| 127 | xmulcl 11232 |
. . . . . . . . . . . . . . . 16
| |
| 128 | 127 | adantll 708 |
. . . . . . . . . . . . . . 15
|
| 129 | 128 | ad2antrr 720 |
. . . . . . . . . . . . . 14
|
| 130 | xrleid 11123 |
. . . . . . . . . . . . . 14
| |
| 131 | 129, 130 | syl 16 |
. . . . . . . . . . . . 13
|
| 132 | 126, 131 | eqbrtrd 4309 |
. . . . . . . . . . . 12
|
| 133 | 132 | adantlr 709 |
. . . . . . . . . . 11
|
| 134 | 105, 116, 133 | 3jaodan 1279 |
. . . . . . . . . 10
|
| 135 | 11, 134 | mpdan 663 |
. . . . . . . . 9
|
| 136 | simplrr 755 |
. . . . . . . . . . . 12
| |
| 137 | 8 | adantr 462 |
. . . . . . . . . . . . . 14
|
| 138 | pnfge 11106 |
. . . . . . . . . . . . . 14
| |
| 139 | 137, 138 | syl 16 |
. . . . . . . . . . . . 13
|
| 140 | simpr 458 |
. . . . . . . . . . . . 13
| |
| 141 | 139, 140 | breqtrrd 4315 |
. . . . . . . . . . . 12
|
| 142 | 123 | ad3antrrr 724 |
. . . . . . . . . . . 12
|
| 143 | 136, 141, 142 | mpbir2and 908 |
. . . . . . . . . . 11
|
| 144 | 143 | oveq1d 6105 |
. . . . . . . . . 10
|
| 145 | 128, 130 | syl 16 |
. . . . . . . . . . 11
|
| 146 | 145 | ad2antrr 720 |
. . . . . . . . . 10
|
| 147 | 144, 146 | eqbrtrd 4309 |
. . . . . . . . 9
|
| 148 | oveq1 6097 |
. . . . . . . . . . 11
| |
| 149 | xmulmnf2 11236 |
. . . . . . . . . . . 12
| |
| 150 | 149 | ad2ant2lr 742 |
. . . . . . . . . . 11
|
| 151 | 148, 150 | sylan9eqr 2495 |
. . . . . . . . . 10
|
| 152 | 128 | ad2antrr 720 |
. . . . . . . . . . 11
|
| 153 | mnfle 11109 |
. . . . . . . . . . 11
| |
| 154 | 152, 153 | syl 16 |
. . . . . . . . . 10
|
| 155 | 151, 154 | eqbrtrd 4309 |
. . . . . . . . 9
|
| 156 | 135, 147, 155 | 3jaodan 1279 |
. . . . . . . 8
|
| 157 | 7, 156 | mpdan 663 |
. . . . . . 7
|
| 158 | 157 | exp32 602 |
. . . . . 6
|
| 159 | xmul01 11226 |
. . . . . . . . . . 11
| |
| 160 | 159 | ad2antrr 720 |
. . . . . . . . . 10
|
| 161 | xmul01 11226 |
. . . . . . . . . . 11
| |
| 162 | 161 | ad2antlr 721 |
. . . . . . . . . 10
|
| 163 | 160, 162 | breq12d 4302 |
. . . . . . . . 9
|
| 164 | 64, 163 | mpbiri 233 |
. . . . . . . 8
|
| 165 | oveq2 6098 |
. . . . . . . . 9
| |
| 166 | oveq2 6098 |
. . . . . . . . 9
| |
| 167 | 165, 166 | breq12d 4302 |
. . . . . . . 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 600 |
. . 3
|
| 173 | 172 | 3impia 1179 |
. 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 959 w3a 960 wceq 1364 wcel 1761 class class class wbr 4289
(class class class)co 6090 cr 9277 cc0 9278 cmul 9283 cpnf 9411 cmnf 9412 cxr 9413 clt 9414 cle 9415 cxmu 11084 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371 ax-cnex 9334 ax-resscn 9335 ax-1cn 9336 ax-icn 9337 ax-addcl 9338 ax-addrcl 9339 ax-mulcl 9340 ax-mulrcl 9341 ax-mulcom 9342 ax-addass 9343 ax-mulass 9344 ax-distr 9345 ax-i2m1 9346 ax-1ne0 9347 ax-1rid 9348 ax-rnegex 9349 ax-rrecex 9350 ax-cnre 9351 ax-pre-lttri 9352 ax-pre-lttrn 9353 ax-pre-ltadd 9354 ax-pre-mulgt0 9355 |
| This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 961 df-3an 962 df-tru 1367 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2261 df-mo 2262 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-nel 2607 df-ral 2718 df-rex 2719 df-reu 2720 df-rab 2722 df-v 2972 df-sbc 3184 df-csb 3286 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-nul 3635 df-if 3789 df-pw 3859 df-sn 3875 df-pr 3877 df-op 3881 df-uni 4089 df-iun 4170 df-br 4290 df-opab 4348 df-mpt 4349 df-id 4632 df-po 4637 df-so 4638 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-res 4848 df-ima 4849 df-iota 5378 df-fun 5417 df-fn 5418 df-f 5419 df-f1 5420 df-fo 5421 df-f1o 5422 df-fv 5423 df-riota 6049 df-ov 6093 df-oprab 6094 df-mpt2 6095 df-1st 6576 df-2nd 6577 df-er 7097 df-en 7307 df-dom 7308 df-sdom 7309 df-pnf 9416 df-mnf 9417 df-xr 9418 df-ltxr 9419 df-le 9420 df-sub 9593 df-neg 9594 df-xneg 11085 df-xmul 11087 |
| This theorem is referenced by: xlemul2a 11248 xlemul1 11249 nmoi2 20268 esumcst 26450 |
| Copyright terms: Public domain | W3C validator |