Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
| Mirrors > Home > MPE Home > Th. List > xlemul1a | Unicode version | |
| Description: Extended real version of lemul1a 9820. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| Ref | Expression |
|---|---|
| xlemul1a |
     ![/\](wedge.gif "/\"){kind=small}  
      |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0xr 9087 |
. . . . . 6
| |
| 2 | simpr 448 |
. . . . . 6
| |
| 3 | xrleloe 10693 |
. . . . . 6
   | |
| 4 | 1, 2, 3 | sylancr 645 |
. . . . 5
|
| 5 | simplll 735 |
. . . . . . . . 9
| |
| 6 | elxr 10672 |
. . . . . . . . 9
 
 | |
| 7 | 5, 6 | sylib 189 |
. . . . . . . 8
|
| 8 | simpllr 736 |
. . . . . . . . . . . 12
| |
| 9 | elxr 10672 |
. . . . . . . . . . . 12
| |
| 10 | 8, 9 | sylib 189 |
. . . . . . . . . . 11
|
| 11 | 10 | adantr 452 |
. . . . . . . . . 10
|
| 12 | simpllr 736 |
. . . . . . . . . . . . . 14
| |
| 13 | elxr 10672 |
. . . . . . . . . . . . . 14
| |
| 14 | 12, 13 | sylib 189 |
. . . . . . . . . . . . 13
|
| 15 | simplrr 738 |
. . . . . . . . . . . . . . . . 17
| |
| 16 | simprll 739 |
. . . . . . . . . . . . . . . . . 18
| |
| 17 | simprlr 740 |
. . . . . . . . . . . . . . . . . 18
| |
| 18 | simprr 734 |
. . . . . . . . . . . . . . . . . 18
| |
| 19 | simplrl 737 |
. . . . . . . . . . . . . . . . . 18
| |
| 20 | lemul1 9818 |
. . . . . . . . . . . . . . . . . 18
| |
| 21 | 16, 17, 18, 19, 20 | syl112anc 1188 |
. . . . . . . . . . . . . . . . 17
|
| 22 | 15, 21 | mpbid 202 |
. . . . . . . . . . . . . . . 16
|
| 23 | rexmul 10806 |
. . . . . . . . . . . . . . . . 17
| |
| 24 | 16, 18, 23 | syl2anc 643 |
. . . . . . . . . . . . . . . 16
|
| 25 | rexmul 10806 |
. . . . . . . . . . . . . . . . 17
| |
| 26 | 17, 18, 25 | syl2anc 643 |
. . . . . . . . . . . . . . . 16
|
| 27 | 22, 24, 26 | 3brtr4d 4202 |
. . . . . . . . . . . . . . 15
|
| 28 | 27 | expr 599 |
. . . . . . . . . . . . . 14
|
| 29 | simprl 733 |
. . . . . . . . . . . . . . . . 17
| |
| 30 | 0re 9047 |
. . . . . . . . . . . . . . . . 17
| |
| 31 | lttri4 9115 |
. . . . . . . . . . . . . . . . 17
| |
| 32 | 29, 30, 31 | sylancl 644 |
. . . . . . . . . . . . . . . 16
|
| 33 | 5 | adantr 452 |
. . . . . . . . . . . . . . . . . . . 20
|
| 34 | xmulpnf1n 10813 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 35 | 33, 34 | sylan 458 |
. . . . . . . . . . . . . . . . . . 19
|
| 36 | 8 | adantr 452 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 37 | 36 | adantr 452 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 38 | pnfxr 10669 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 39 | xmulcl 10808 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 40 | 37, 38, 39 | sylancl 644 |
. . . . . . . . . . . . . . . . . . . 20
|
| 41 | mnfle 10685 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 42 | 40, 41 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
|
| 43 | 35, 42 | eqbrtrd 4192 |
. . . . . . . . . . . . . . . . . 18
|
| 44 | 43 | ex 424 |
. . . . . . . . . . . . . . . . 17
|
| 45 | oveq1 6047 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 46 | xmul02 10803 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 47 | 38, 46 | ax-mp 8 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 48 | 45, 47 | syl6eq 2452 |
. . . . . . . . . . . . . . . . . . . 20
|
| 49 | 48 | adantl 453 |
. . . . . . . . . . . . . . . . . . 19
|
| 50 | simplrr 738 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 51 | breq1 4175 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 52 | 50, 51 | syl5ibcom 212 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 53 | simprr 734 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 54 | leloe 9117 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 55 | 30, 53, 54 | sylancr 645 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 56 | 52, 55 | sylibd 206 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 57 | 56 | imp 419 |
. . . . . . . . . . . . . . . . . . . 20
|
| 58 | pnfge 10683 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 59 | 1, 58 | ax-mp 8 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 60 | xmulpnf1 10809 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 61 | 36, 60 | sylan 458 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 62 | 59, 61 | syl5breqr 4208 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 63 | xrleid 10699 |
. . . . . . . . . . . . . . . . . . . . . . . 24
| |
| 64 | 1, 63 | ax-mp 8 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 65 | 64, 47 | breqtrri 4197 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 66 | simpr 448 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 67 | 66 | oveq1d 6055 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 68 | 65, 67 | syl5breq 4207 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 69 | 62, 68 | jaodan 761 |
. . . . . . . . . . . . . . . . . . . 20
|
| 70 | 57, 69 | syldan 457 |
. . . . . . . . . . . . . . . . . . 19
|
| 71 | 49, 70 | eqbrtrd 4192 |
. . . . . . . . . . . . . . . . . 18
|
| 72 | 71 | ex 424 |
. . . . . . . . . . . . . . . . 17
|
| 73 | pnfge 10683 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 74 | 38, 73 | ax-mp 8 |
. . . . . . . . . . . . . . . . . . 19
|
| 75 | 5 | adantr 452 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 76 | simprr 734 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 77 | xmulpnf1 10809 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 78 | 75, 76, 77 | syl2anc 643 |
. . . . . . . . . . . . . . . . . . . 20
|
| 79 | 8 | adantr 452 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 80 | ltletr 9122 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
| |
| 81 | 30, 80 | mp3an1 1266 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 82 | 81 | adantl 453 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 83 | 50, 82 | mpan2d 656 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 84 | 83 | impr 603 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 85 | 79, 84, 60 | syl2anc 643 |
. . . . . . . . . . . . . . . . . . . 20
|
| 86 | 78, 85 | breq12d 4185 |
. . . . . . . . . . . . . . . . . . 19
|
| 87 | 74, 86 | mpbiri 225 |
. . . . . . . . . . . . . . . . . 18
|
| 88 | 87 | expr 599 |
. . . . . . . . . . . . . . . . 17
|
| 89 | 44, 72, 88 | 3jaod 1248 |
. . . . . . . . . . . . . . . 16
|
| 90 | 32, 89 | mpd 15 |
. . . . . . . . . . . . . . 15
|
| 91 | oveq2 6048 |
. . . . . . . . . . . . . . . 16
| |
| 92 | oveq2 6048 |
. . . . . . . . . . . . . . . 16
| |
| 93 | 91, 92 | breq12d 4185 |
. . . . . . . . . . . . . . 15
|
| 94 | 90, 93 | syl5ibrcom 214 |
. . . . . . . . . . . . . 14
|
| 95 | nltmnf 10682 |
. . . . . . . . . . . . . . . . . . . 20
 | |
| 96 | 1, 95 | ax-mp 8 |
. . . . . . . . . . . . . . . . . . 19
|
| 97 | breq2 4176 |
. . . . . . . . . . . . . . . . . . 19
| |
| 98 | 96, 97 | mtbiri 295 |
. . . . . . . . . . . . . . . . . 18
|
| 99 | 98 | con2i 114 |
. . . . . . . . . . . . . . . . 17
|
| 100 | 99 | ad2antrl 709 |
. . . . . . . . . . . . . . . 16
|
| 101 | 100 | adantr 452 |
. . . . . . . . . . . . . . 15
|
| 102 | 101 | pm2.21d 100 |
. . . . . . . . . . . . . 14
|
| 103 | 28, 94, 102 | 3jaod 1248 |
. . . . . . . . . . . . 13
|
| 104 | 14, 103 | mpd 15 |
. . . . . . . . . . . 12
|
| 105 | 104 | anassrs 630 |
. . . . . . . . . . 11
|
| 106 | xmulcl 10808 |
. . . . . . . . . . . . . . . 16
| |
| 107 | 106 | adantlr 696 |
. . . . . . . . . . . . . . 15
|
| 108 | 107 | ad2antrr 707 |
. . . . . . . . . . . . . 14
|
| 109 | pnfge 10683 |
. . . . . . . . . . . . . 14
| |
| 110 | 108, 109 | syl 16 |
. . . . . . . . . . . . 13
|
| 111 | oveq1 6047 |
. . . . . . . . . . . . . 14
| |
| 112 | xmulpnf2 10810 |
. . . . . . . . . . . . . . 15
| |
| 113 | 112 | ad2ant2lr 729 |
. . . . . . . . . . . . . 14
|
| 114 | 111, 113 | sylan9eqr 2458 |
. . . . . . . . . . . . 13
|
| 115 | 110, 114 | breqtrrd 4198 |
. . . . . . . . . . . 12
|
| 116 | 115 | adantlr 696 |
. . . . . . . . . . 11
|
| 117 | simplrr 738 |
. . . . . . . . . . . . . . 15
| |
| 118 | simpr 448 |
. . . . . . . . . . . . . . . 16
| |
| 119 | 5 | adantr 452 |
. . . . . . . . . . . . . . . . 17
|
| 120 | mnfle 10685 |
. . . . . . . . . . . . . . . . 17
| |
| 121 | 119, 120 | syl 16 |
. . . . . . . . . . . . . . . 16
|
| 122 | 118, 121 | eqbrtrd 4192 |
. . . . . . . . . . . . . . 15
|
| 123 | xrletri3 10701 |
. . . . . . . . . . . . . . . 16
| |
| 124 | 123 | ad3antrrr 711 |
. . . . . . . . . . . . . . 15
|
| 125 | 117, 122, 124 | mpbir2and 889 |
. . . . . . . . . . . . . 14
|
| 126 | 125 | oveq1d 6055 |
. . . . . . . . . . . . 13
|
| 127 | xmulcl 10808 |
. . . . . . . . . . . . . . . 16
| |
| 128 | 127 | adantll 695 |
. . . . . . . . . . . . . . 15
|
| 129 | 128 | ad2antrr 707 |
. . . . . . . . . . . . . 14
|
| 130 | xrleid 10699 |
. . . . . . . . . . . . . 14
| |
| 131 | 129, 130 | syl 16 |
. . . . . . . . . . . . 13
|
| 132 | 126, 131 | eqbrtrd 4192 |
. . . . . . . . . . . 12
|
| 133 | 132 | adantlr 696 |
. . . . . . . . . . 11
|
| 134 | 105, 116, 133 | 3jaodan 1250 |
. . . . . . . . . 10
|
| 135 | 11, 134 | mpdan 650 |
. . . . . . . . 9
|
| 136 | simplrr 738 |
. . . . . . . . . . . 12
| |
| 137 | 8 | adantr 452 |
. . . . . . . . . . . . . 14
|
| 138 | pnfge 10683 |
. . . . . . . . . . . . . 14
| |
| 139 | 137, 138 | syl 16 |
. . . . . . . . . . . . 13
|
| 140 | simpr 448 |
. . . . . . . . . . . . 13
| |
| 141 | 139, 140 | breqtrrd 4198 |
. . . . . . . . . . . 12
|
| 142 | 123 | ad3antrrr 711 |
. . . . . . . . . . . 12
|
| 143 | 136, 141, 142 | mpbir2and 889 |
. . . . . . . . . . 11
|
| 144 | 143 | oveq1d 6055 |
. . . . . . . . . 10
|
| 145 | 128, 130 | syl 16 |
. . . . . . . . . . 11
|
| 146 | 145 | ad2antrr 707 |
. . . . . . . . . 10
|
| 147 | 144, 146 | eqbrtrd 4192 |
. . . . . . . . 9
|
| 148 | oveq1 6047 |
. . . . . . . . . . 11
| |
| 149 | xmulmnf2 10812 |
. . . . . . . . . . . 12
| |
| 150 | 149 | ad2ant2lr 729 |
. . . . . . . . . . 11
|
| 151 | 148, 150 | sylan9eqr 2458 |
. . . . . . . . . 10
|
| 152 | 128 | ad2antrr 707 |
. . . . . . . . . . 11
|
| 153 | mnfle 10685 |
. . . . . . . . . . 11
| |
| 154 | 152, 153 | syl 16 |
. . . . . . . . . 10
|
| 155 | 151, 154 | eqbrtrd 4192 |
. . . . . . . . 9
|
| 156 | 135, 147, 155 | 3jaodan 1250 |
. . . . . . . 8
|
| 157 | 7, 156 | mpdan 650 |
. . . . . . 7
|
| 158 | 157 | exp32 589 |
. . . . . 6
|
| 159 | xmul01 10802 |
. . . . . . . . . . 11
| |
| 160 | 159 | ad2antrr 707 |
. . . . . . . . . 10
|
| 161 | xmul01 10802 |
. . . . . . . . . . 11
| |
| 162 | 161 | ad2antlr 708 |
. . . . . . . . . 10
|
| 163 | 160, 162 | breq12d 4185 |
. . . . . . . . 9
|
| 164 | 64, 163 | mpbiri 225 |
. . . . . . . 8
|
| 165 | oveq2 6048 |
. . . . . . . . 9
| |
| 166 | oveq2 6048 |
. . . . . . . . 9
| |
| 167 | 165, 166 | breq12d 4185 |
. . . . . . . 8
|
| 168 | 164, 167 | syl5ibcom 212 |
. . . . . . 7
|
| 169 | 168 | a1dd 44 |
. . . . . 6
|
| 170 | 158, 169 | jaod 370 |
. . . . 5
|
| 171 | 4, 170 | sylbid 207 |
. . . 4
|
| 172 | 171 | expimpd 587 |
. . 3
|
| 173 | 172 | 3impia 1150 |
. 2
|
| 174 | 173 | imp 419 |
1
|
| Colors of variables: wff set class |
| Syntax hints: wn 3
wi 4
wb 177 wo 358 wa 359 w3o 935 w3a 936 wceq 1649 wcel 1721 class class class wbr 4172
(class class class)co 6040 cr 8945 cc0 8946 cmul 8951 cpnf 9073 cmnf 9074 cxr 9075 clt 9076 cle 9077 cxmu 10665 |
| This theorem is referenced by: xlemul2a 10824 xlemul1 10825 nmoi2 18717 esumcst 24408 |
| This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 |
| This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-op 3783 df-uni 3976 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-id 4458 df-po 4463 df-so 4464 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-riota 6508 df-er 6864 df-en 7069 df-dom 7070 df-sdom 7071 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-xneg 10666 df-xmul 10668 |
| Copyright terms: Public domain | W3C validator |