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 10204. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| Ref | Expression |
|---|---|
| xlemul1a |
     ![/\](wedge.gif "/\"){kind=small}  
      |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0xr 9451 |
. . . . . 6
| |
| 2 | simpr 461 |
. . . . . 6
| |
| 3 | xrleloe 11142 |
. . . . . 6
   | |
| 4 | 1, 2, 3 | sylancr 663 |
. . . . 5
|
| 5 | simplll 757 |
. . . . . . . . 9
| |
| 6 | elxr 11117 |
. . . . . . . . 9
   | |
| 7 | 5, 6 | sylib 196 |
. . . . . . . 8
|
| 8 | simpllr 758 |
. . . . . . . . . . . 12
| |
| 9 | elxr 11117 |
. . . . . . . . . . . 12
| |
| 10 | 8, 9 | sylib 196 |
. . . . . . . . . . 11
|
| 11 | 10 | adantr 465 |
. . . . . . . . . 10
|
| 12 | simpllr 758 |
. . . . . . . . . . . . . 14
| |
| 13 | elxr 11117 |
. . . . . . . . . . . . . 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 10202 |
. . . . . . . . . . . . . . . . . 18
| |
| 21 | 16, 17, 18, 19, 20 | syl112anc 1222 |
. . . . . . . . . . . . . . . . 17
|
| 22 | 15, 21 | mpbid 210 |
. . . . . . . . . . . . . . . 16
|
| 23 | rexmul 11255 |
. . . . . . . . . . . . . . . . 17
| |
| 24 | 16, 18, 23 | syl2anc 661 |
. . . . . . . . . . . . . . . 16
|
| 25 | rexmul 11255 |
. . . . . . . . . . . . . . . . 17
| |
| 26 | 17, 18, 25 | syl2anc 661 |
. . . . . . . . . . . . . . . 16
|
| 27 | 22, 24, 26 | 3brtr4d 4343 |
. . . . . . . . . . . . . . 15
|
| 28 | 27 | expr 615 |
. . . . . . . . . . . . . 14
|
| 29 | simprl 755 |
. . . . . . . . . . . . . . . . 17
| |
| 30 | 0re 9407 |
. . . . . . . . . . . . . . . . 17
| |
| 31 | lttri4 9480 |
. . . . . . . . . . . . . . . . 17
| |
| 32 | 29, 30, 31 | sylancl 662 |
. . . . . . . . . . . . . . . 16
|
| 33 | 5 | adantr 465 |
. . . . . . . . . . . . . . . . . . . 20
|
| 34 | xmulpnf1n 11262 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 35 | 33, 34 | sylan 471 |
. . . . . . . . . . . . . . . . . . 19
|
| 36 | 8 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 37 | 36 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 38 | pnfxr 11113 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 39 | xmulcl 11257 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 40 | 37, 38, 39 | sylancl 662 |
. . . . . . . . . . . . . . . . . . . 20
|
| 41 | mnfle 11134 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 42 | 40, 41 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
|
| 43 | 35, 42 | eqbrtrd 4333 |
. . . . . . . . . . . . . . . . . 18
|
| 44 | 43 | ex 434 |
. . . . . . . . . . . . . . . . 17
|
| 45 | oveq1 6119 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 46 | xmul02 11252 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 47 | 38, 46 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 48 | 45, 47 | syl6eq 2491 |
. . . . . . . . . . . . . . . . . . . 20
|
| 49 | 48 | adantl 466 |
. . . . . . . . . . . . . . . . . . 19
|
| 50 | simplrr 760 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 51 | breq1 4316 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 52 | 50, 51 | syl5ibcom 220 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 53 | simprr 756 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 54 | leloe 9482 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 55 | 30, 53, 54 | sylancr 663 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 56 | 52, 55 | sylibd 214 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 57 | 56 | imp 429 |
. . . . . . . . . . . . . . . . . . . 20
|
| 58 | pnfge 11131 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 59 | 1, 58 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 60 | xmulpnf1 11258 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 61 | 36, 60 | sylan 471 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 62 | 59, 61 | syl5breqr 4349 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 63 | xrleid 11148 |
. . . . . . . . . . . . . . . . . . . . . . . 24
| |
| 64 | 1, 63 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 65 | 64, 47 | breqtrri 4338 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 66 | simpr 461 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 67 | 66 | oveq1d 6127 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 68 | 65, 67 | syl5breq 4348 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 69 | 62, 68 | jaodan 783 |
. . . . . . . . . . . . . . . . . . . 20
|
| 70 | 57, 69 | syldan 470 |
. . . . . . . . . . . . . . . . . . 19
|
| 71 | 49, 70 | eqbrtrd 4333 |
. . . . . . . . . . . . . . . . . 18
|
| 72 | 71 | ex 434 |
. . . . . . . . . . . . . . . . 17
|
| 73 | pnfge 11131 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 74 | 38, 73 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
|
| 75 | 5 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 76 | simprr 756 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 77 | xmulpnf1 11258 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 78 | 75, 76, 77 | syl2anc 661 |
. . . . . . . . . . . . . . . . . . . 20
|
| 79 | 8 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 80 | ltletr 9487 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
| |
| 81 | 30, 80 | mp3an1 1301 |
. . . . . . . . . . . . . . . . . . . . . . . 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 4326 |
. . . . . . . . . . . . . . . . . . 19
|
| 87 | 74, 86 | mpbiri 233 |
. . . . . . . . . . . . . . . . . 18
|
| 88 | 87 | expr 615 |
. . . . . . . . . . . . . . . . 17
|
| 89 | 44, 72, 88 | 3jaod 1282 |
. . . . . . . . . . . . . . . 16
|
| 90 | 32, 89 | mpd 15 |
. . . . . . . . . . . . . . 15
|
| 91 | oveq2 6120 |
. . . . . . . . . . . . . . . 16
| |
| 92 | oveq2 6120 |
. . . . . . . . . . . . . . . 16
| |
| 93 | 91, 92 | breq12d 4326 |
. . . . . . . . . . . . . . 15
|
| 94 | 90, 93 | syl5ibrcom 222 |
. . . . . . . . . . . . . 14
|
| 95 | nltmnf 11130 |
. . . . . . . . . . . . . . . . . . . 20
 | |
| 96 | 1, 95 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
|
| 97 | breq2 4317 |
. . . . . . . . . . . . . . . . . . 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 1282 |
. . . . . . . . . . . . 13
|
| 104 | 14, 103 | mpd 15 |
. . . . . . . . . . . 12
|
| 105 | 104 | anassrs 648 |
. . . . . . . . . . 11
|
| 106 | xmulcl 11257 |
. . . . . . . . . . . . . . . 16
| |
| 107 | 106 | adantlr 714 |
. . . . . . . . . . . . . . 15
|
| 108 | 107 | ad2antrr 725 |
. . . . . . . . . . . . . 14
|
| 109 | pnfge 11131 |
. . . . . . . . . . . . . 14
| |
| 110 | 108, 109 | syl 16 |
. . . . . . . . . . . . 13
|
| 111 | oveq1 6119 |
. . . . . . . . . . . . . 14
| |
| 112 | xmulpnf2 11259 |
. . . . . . . . . . . . . . 15
| |
| 113 | 112 | ad2ant2lr 747 |
. . . . . . . . . . . . . 14
|
| 114 | 111, 113 | sylan9eqr 2497 |
. . . . . . . . . . . . 13
|
| 115 | 110, 114 | breqtrrd 4339 |
. . . . . . . . . . . 12
|
| 116 | 115 | adantlr 714 |
. . . . . . . . . . 11
|
| 117 | simplrr 760 |
. . . . . . . . . . . . . . 15
| |
| 118 | simpr 461 |
. . . . . . . . . . . . . . . 16
| |
| 119 | 5 | adantr 465 |
. . . . . . . . . . . . . . . . 17
|
| 120 | mnfle 11134 |
. . . . . . . . . . . . . . . . 17
| |
| 121 | 119, 120 | syl 16 |
. . . . . . . . . . . . . . . 16
|
| 122 | 118, 121 | eqbrtrd 4333 |
. . . . . . . . . . . . . . 15
|
| 123 | xrletri3 11150 |
. . . . . . . . . . . . . . . 16
| |
| 124 | 123 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
|
| 125 | 117, 122, 124 | mpbir2and 913 |
. . . . . . . . . . . . . 14
|
| 126 | 125 | oveq1d 6127 |
. . . . . . . . . . . . 13
|
| 127 | xmulcl 11257 |
. . . . . . . . . . . . . . . 16
| |
| 128 | 127 | adantll 713 |
. . . . . . . . . . . . . . 15
|
| 129 | 128 | ad2antrr 725 |
. . . . . . . . . . . . . 14
|
| 130 | xrleid 11148 |
. . . . . . . . . . . . . 14
| |
| 131 | 129, 130 | syl 16 |
. . . . . . . . . . . . 13
|
| 132 | 126, 131 | eqbrtrd 4333 |
. . . . . . . . . . . 12
|
| 133 | 132 | adantlr 714 |
. . . . . . . . . . 11
|
| 134 | 105, 116, 133 | 3jaodan 1284 |
. . . . . . . . . 10
|
| 135 | 11, 134 | mpdan 668 |
. . . . . . . . 9
|
| 136 | simplrr 760 |
. . . . . . . . . . . 12
| |
| 137 | 8 | adantr 465 |
. . . . . . . . . . . . . 14
|
| 138 | pnfge 11131 |
. . . . . . . . . . . . . 14
| |
| 139 | 137, 138 | syl 16 |
. . . . . . . . . . . . 13
|
| 140 | simpr 461 |
. . . . . . . . . . . . 13
| |
| 141 | 139, 140 | breqtrrd 4339 |
. . . . . . . . . . . 12
|
| 142 | 123 | ad3antrrr 729 |
. . . . . . . . . . . 12
|
| 143 | 136, 141, 142 | mpbir2and 913 |
. . . . . . . . . . 11
|
| 144 | 143 | oveq1d 6127 |
. . . . . . . . . 10
|
| 145 | 128, 130 | syl 16 |
. . . . . . . . . . 11
|
| 146 | 145 | ad2antrr 725 |
. . . . . . . . . 10
|
| 147 | 144, 146 | eqbrtrd 4333 |
. . . . . . . . 9
|
| 148 | oveq1 6119 |
. . . . . . . . . . 11
| |
| 149 | xmulmnf2 11261 |
. . . . . . . . . . . 12
| |
| 150 | 149 | ad2ant2lr 747 |
. . . . . . . . . . 11
|
| 151 | 148, 150 | sylan9eqr 2497 |
. . . . . . . . . 10
|
| 152 | 128 | ad2antrr 725 |
. . . . . . . . . . 11
|
| 153 | mnfle 11134 |
. . . . . . . . . . 11
| |
| 154 | 152, 153 | syl 16 |
. . . . . . . . . 10
|
| 155 | 151, 154 | eqbrtrd 4333 |
. . . . . . . . 9
|
| 156 | 135, 147, 155 | 3jaodan 1284 |
. . . . . . . 8
|
| 157 | 7, 156 | mpdan 668 |
. . . . . . 7
|
| 158 | 157 | exp32 605 |
. . . . . 6
|
| 159 | xmul01 11251 |
. . . . . . . . . . 11
| |
| 160 | 159 | ad2antrr 725 |
. . . . . . . . . 10
|
| 161 | xmul01 11251 |
. . . . . . . . . . 11
| |
| 162 | 161 | ad2antlr 726 |
. . . . . . . . . 10
|
| 163 | 160, 162 | breq12d 4326 |
. . . . . . . . 9
|
| 164 | 64, 163 | mpbiri 233 |
. . . . . . . 8
|
| 165 | oveq2 6120 |
. . . . . . . . 9
| |
| 166 | oveq2 6120 |
. . . . . . . . 9
| |
| 167 | 165, 166 | breq12d 4326 |
. . . . . . . 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 1184 |
. 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 964 w3a 965 wceq 1369 wcel 1756 class class class wbr 4313
(class class class)co 6112 cr 9302 cc0 9303 cmul 9308 cpnf 9436 cmnf 9437 cxr 9438 clt 9439 cle 9440 cxmu 11109 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-sep 4434 ax-nul 4442 ax-pow 4491 ax-pr 4552 ax-un 6393 ax-cnex 9359 ax-resscn 9360 ax-1cn 9361 ax-icn 9362 ax-addcl 9363 ax-addrcl 9364 ax-mulcl 9365 ax-mulrcl 9366 ax-mulcom 9367 ax-addass 9368 ax-mulass 9369 ax-distr 9370 ax-i2m1 9371 ax-1ne0 9372 ax-1rid 9373 ax-rnegex 9374 ax-rrecex 9375 ax-cnre 9376 ax-pre-lttri 9377 ax-pre-lttrn 9378 ax-pre-ltadd 9379 ax-pre-mulgt0 9380 |
| This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2577 df-ne 2622 df-nel 2623 df-ral 2741 df-rex 2742 df-reu 2743 df-rab 2745 df-v 2995 df-sbc 3208 df-csb 3310 df-dif 3352 df-un 3354 df-in 3356 df-ss 3363 df-nul 3659 df-if 3813 df-pw 3883 df-sn 3899 df-pr 3901 df-op 3905 df-uni 4113 df-iun 4194 df-br 4314 df-opab 4372 df-mpt 4373 df-id 4657 df-po 4662 df-so 4663 df-xp 4867 df-rel 4868 df-cnv 4869 df-co 4870 df-dm 4871 df-rn 4872 df-res 4873 df-ima 4874 df-iota 5402 df-fun 5441 df-fn 5442 df-f 5443 df-f1 5444 df-fo 5445 df-f1o 5446 df-fv 5447 df-riota 6073 df-ov 6115 df-oprab 6116 df-mpt2 6117 df-1st 6598 df-2nd 6599 df-er 7122 df-en 7332 df-dom 7333 df-sdom 7334 df-pnf 9441 df-mnf 9442 df-xr 9443 df-ltxr 9444 df-le 9445 df-sub 9618 df-neg 9619 df-xneg 11110 df-xmul 11112 |
| This theorem is referenced by: xlemul2a 11273 xlemul1 11274 nmoi2 20331 esumcst 26536 |
| Copyright terms: Public domain | W3C validator |