Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > xlemul1a | Structured version Visualization version Unicode version | ||
| Description: Extended real version of lemul1a 10456. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| Ref | Expression |
|---|---|
| xlemul1a |
     ![/\](wedge.gif "/\"){kind=small}  
      |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0xr 9684 |
. . . . . 6
| |
| 2 | simpr 463 |
. . . . . 6
| |
| 3 | xrleloe 11440 |
. . . . . 6
   | |
| 4 | 1, 2, 3 | sylancr 668 |
. . . . 5
|
| 5 | simpllr 768 |
. . . . . . . . . . . 12
| |
| 6 | elxr 11413 |
. . . . . . . . . . . 12
  | |
| 7 | 5, 6 | sylib 200 |
. . . . . . . . . . 11
|
| 8 | simplrr 770 |
. . . . . . . . . . . . . . 15
| |
| 9 | simprll 771 |
. . . . . . . . . . . . . . . 16
| |
| 10 | simprlr 772 |
. . . . . . . . . . . . . . . 16
| |
| 11 | simprr 765 |
. . . . . . . . . . . . . . . 16
| |
| 12 | simplrl 769 |
. . . . . . . . . . . . . . . 16
| |
| 13 | lemul1 10454 |
. . . . . . . . . . . . . . . 16
| |
| 14 | 9, 10, 11, 12, 13 | syl112anc 1271 |
. . . . . . . . . . . . . . 15
|
| 15 | 8, 14 | mpbid 214 |
. . . . . . . . . . . . . 14
|
| 16 | rexmul 11554 |
. . . . . . . . . . . . . . 15
| |
| 17 | 9, 11, 16 | syl2anc 666 |
. . . . . . . . . . . . . 14
|
| 18 | rexmul 11554 |
. . . . . . . . . . . . . . 15
| |
| 19 | 10, 11, 18 | syl2anc 666 |
. . . . . . . . . . . . . 14
|
| 20 | 15, 17, 19 | 3brtr4d 4432 |
. . . . . . . . . . . . 13
|
| 21 | 20 | expr 619 |
. . . . . . . . . . . 12
|
| 22 | simprl 763 |
. . . . . . . . . . . . . . 15
| |
| 23 | 0re 9640 |
. . . . . . . . . . . . . . 15
| |
| 24 | lttri4 9715 |
. . . . . . . . . . . . . . 15
| |
| 25 | 22, 23, 24 | sylancl 667 |
. . . . . . . . . . . . . 14
|
| 26 | simplll 767 |
. . . . . . . . . . . . . . . . . . 19
| |
| 27 | 26 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
|
| 28 | xmulpnf1n 11561 |
. . . . . . . . . . . . . . . . . 18
| |
| 29 | 27, 28 | sylan 474 |
. . . . . . . . . . . . . . . . 17
|
| 30 | simpllr 768 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 31 | 30 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
|
| 32 | 31 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
|
| 33 | pnfxr 11409 |
. . . . . . . . . . . . . . . . . . 19
| |
| 34 | xmulcl 11556 |
. . . . . . . . . . . . . . . . . . 19
| |
| 35 | 32, 33, 34 | sylancl 667 |
. . . . . . . . . . . . . . . . . 18
|
| 36 | mnfle 11432 |
. . . . . . . . . . . . . . . . . 18
| |
| 37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
| 38 | 29, 37 | eqbrtrd 4422 |
. . . . . . . . . . . . . . . 16
|
| 39 | 38 | ex 436 |
. . . . . . . . . . . . . . 15
|
| 40 | oveq1 6295 |
. . . . . . . . . . . . . . . . . . 19
| |
| 41 | xmul02 11551 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 42 | 33, 41 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
|
| 43 | 40, 42 | syl6eq 2500 |
. . . . . . . . . . . . . . . . . 18
|
| 44 | 43 | adantl 468 |
. . . . . . . . . . . . . . . . 17
|
| 45 | simplrr 770 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 46 | breq1 4404 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 47 | 45, 46 | syl5ibcom 224 |
. . . . . . . . . . . . . . . . . . . 20
|
| 48 | simprr 765 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 49 | leloe 9717 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 50 | 23, 48, 49 | sylancr 668 |
. . . . . . . . . . . . . . . . . . . 20
|
| 51 | 47, 50 | sylibd 218 |
. . . . . . . . . . . . . . . . . . 19
|
| 52 | 51 | imp 431 |
. . . . . . . . . . . . . . . . . 18
|
| 53 | pnfge 11429 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 54 | 1, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
|
| 55 | xmulpnf1 11557 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 56 | 31, 55 | sylan 474 |
. . . . . . . . . . . . . . . . . . . 20
|
| 57 | 54, 56 | syl5breqr 4438 |
. . . . . . . . . . . . . . . . . . 19
|
| 58 | xrleid 11446 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 59 | 1, 58 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 60 | 59, 42 | breqtrri 4427 |
. . . . . . . . . . . . . . . . . . . 20
|
| 61 | simpr 463 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 62 | 61 | oveq1d 6303 |
. . . . . . . . . . . . . . . . . . . 20
|
| 63 | 60, 62 | syl5breq 4437 |
. . . . . . . . . . . . . . . . . . 19
|
| 64 | 57, 63 | jaodan 793 |
. . . . . . . . . . . . . . . . . 18
|
| 65 | 52, 64 | syldan 473 |
. . . . . . . . . . . . . . . . 17
|
| 66 | 44, 65 | eqbrtrd 4422 |
. . . . . . . . . . . . . . . 16
|
| 67 | 66 | ex 436 |
. . . . . . . . . . . . . . 15
|
| 68 | pnfge 11429 |
. . . . . . . . . . . . . . . . . 18
| |
| 69 | 33, 68 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
| 70 | 26 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
|
| 71 | simprr 765 |
. . . . . . . . . . . . . . . . . . 19
| |
| 72 | xmulpnf1 11557 |
. . . . . . . . . . . . . . . . . . 19
| |
| 73 | 70, 71, 72 | syl2anc 666 |
. . . . . . . . . . . . . . . . . 18
|
| 74 | 30 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
|
| 75 | ltletr 9722 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 76 | 23, 75 | mp3an1 1350 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 77 | 76 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 78 | 45, 77 | mpan2d 679 |
. . . . . . . . . . . . . . . . . . . 20
|
| 79 | 78 | impr 624 |
. . . . . . . . . . . . . . . . . . 19
|
| 80 | 74, 79, 55 | syl2anc 666 |
. . . . . . . . . . . . . . . . . 18
|
| 81 | 73, 80 | breq12d 4414 |
. . . . . . . . . . . . . . . . 17
|
| 82 | 69, 81 | mpbiri 237 |
. . . . . . . . . . . . . . . 16
|
| 83 | 82 | expr 619 |
. . . . . . . . . . . . . . 15
|
| 84 | 39, 67, 83 | 3jaod 1331 |
. . . . . . . . . . . . . 14
|
| 85 | 25, 84 | mpd 15 |
. . . . . . . . . . . . 13
|
| 86 | oveq2 6296 |
. . . . . . . . . . . . . 14
| |
| 87 | oveq2 6296 |
. . . . . . . . . . . . . 14
| |
| 88 | 86, 87 | breq12d 4414 |
. . . . . . . . . . . . 13
|
| 89 | 85, 88 | syl5ibrcom 226 |
. . . . . . . . . . . 12
|
| 90 | nltmnf 11428 |
. . . . . . . . . . . . . . . . . 18
 | |
| 91 | 1, 90 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
| 92 | breq2 4405 |
. . . . . . . . . . . . . . . . 17
| |
| 93 | 91, 92 | mtbiri 305 |
. . . . . . . . . . . . . . . 16
|
| 94 | 93 | con2i 124 |
. . . . . . . . . . . . . . 15
|
| 95 | 94 | ad2antrl 733 |
. . . . . . . . . . . . . 14
|
| 96 | 95 | adantr 467 |
. . . . . . . . . . . . 13
|
| 97 | 96 | pm2.21d 110 |
. . . . . . . . . . . 12
|
| 98 | 21, 89, 97 | 3jaod 1331 |
. . . . . . . . . . 11
|
| 99 | 7, 98 | mpd 15 |
. . . . . . . . . 10
|
| 100 | 99 | anassrs 653 |
. . . . . . . . 9
|
| 101 | xmulcl 11556 |
. . . . . . . . . . . . . 14
| |
| 102 | 101 | adantlr 720 |
. . . . . . . . . . . . 13
|
| 103 | 102 | ad2antrr 731 |
. . . . . . . . . . . 12
|
| 104 | pnfge 11429 |
. . . . . . . . . . . 12
| |
| 105 | 103, 104 | syl 17 |
. . . . . . . . . . 11
|
| 106 | oveq1 6295 |
. . . . . . . . . . . 12
| |
| 107 | xmulpnf2 11558 |
. . . . . . . . . . . . 13
| |
| 108 | 107 | ad2ant2lr 753 |
. . . . . . . . . . . 12
|
| 109 | 106, 108 | sylan9eqr 2506 |
. . . . . . . . . . 11
|
| 110 | 105, 109 | breqtrrd 4428 |
. . . . . . . . . 10
|
| 111 | 110 | adantlr 720 |
. . . . . . . . 9
|
| 112 | simplrr 770 |
. . . . . . . . . . . . 13
| |
| 113 | simpr 463 |
. . . . . . . . . . . . . 14
| |
| 114 | 26 | adantr 467 |
. . . . . . . . . . . . . . 15
|
| 115 | mnfle 11432 |
. . . . . . . . . . . . . . 15
| |
| 116 | 114, 115 | syl 17 |
. . . . . . . . . . . . . 14
|
| 117 | 113, 116 | eqbrtrd 4422 |
. . . . . . . . . . . . 13
|
| 118 | xrletri3 11448 |
. . . . . . . . . . . . . 14
| |
| 119 | 118 | ad3antrrr 735 |
. . . . . . . . . . . . 13
|
| 120 | 112, 117, 119 | mpbir2and 932 |
. . . . . . . . . . . 12
|
| 121 | 120 | oveq1d 6303 |
. . . . . . . . . . 11
|
| 122 | xmulcl 11556 |
. . . . . . . . . . . . . 14
| |
| 123 | 122 | adantll 719 |
. . . . . . . . . . . . 13
|
| 124 | 123 | ad2antrr 731 |
. . . . . . . . . . . 12
|
| 125 | xrleid 11446 |
. . . . . . . . . . . 12
| |
| 126 | 124, 125 | syl 17 |
. . . . . . . . . . 11
|
| 127 | 121, 126 | eqbrtrd 4422 |
. . . . . . . . . 10
|
| 128 | 127 | adantlr 720 |
. . . . . . . . 9
|
| 129 | elxr 11413 |
. . . . . . . . . . 11
| |
| 130 | 30, 129 | sylib 200 |
. . . . . . . . . 10
|
| 131 | 130 | adantr 467 |
. . . . . . . . 9
|
| 132 | 100, 111, 128, 131 | mpjao3dan 1334 |
. . . . . . . 8
|
| 133 | simplrr 770 |
. . . . . . . . . . 11
| |
| 134 | 30 | adantr 467 |
. . . . . . . . . . . . 13
|
| 135 | pnfge 11429 |
. . . . . . . . . . . . 13
| |
| 136 | 134, 135 | syl 17 |
. . . . . . . . . . . 12
|
| 137 | simpr 463 |
. . . . . . . . . . . 12
| |
| 138 | 136, 137 | breqtrrd 4428 |
. . . . . . . . . . 11
|
| 139 | 118 | ad3antrrr 735 |
. . . . . . . . . . 11
|
| 140 | 133, 138, 139 | mpbir2and 932 |
. . . . . . . . . 10
|
| 141 | 140 | oveq1d 6303 |
. . . . . . . . 9
|
| 142 | 123, 125 | syl 17 |
. . . . . . . . . 10
|
| 143 | 142 | ad2antrr 731 |
. . . . . . . . 9
|
| 144 | 141, 143 | eqbrtrd 4422 |
. . . . . . . 8
|
| 145 | oveq1 6295 |
. . . . . . . . . 10
| |
| 146 | xmulmnf2 11560 |
. . . . . . . . . . 11
| |
| 147 | 146 | ad2ant2lr 753 |
. . . . . . . . . 10
|
| 148 | 145, 147 | sylan9eqr 2506 |
. . . . . . . . 9
|
| 149 | 123 | ad2antrr 731 |
. . . . . . . . . 10
|
| 150 | mnfle 11432 |
. . . . . . . . . 10
| |
| 151 | 149, 150 | syl 17 |
. . . . . . . . 9
|
| 152 | 148, 151 | eqbrtrd 4422 |
. . . . . . . 8
|
| 153 | elxr 11413 |
. . . . . . . . 9
| |
| 154 | 26, 153 | sylib 200 |
. . . . . . . 8
|
| 155 | 132, 144, 152, 154 | mpjao3dan 1334 |
. . . . . . 7
|
| 156 | 155 | exp32 609 |
. . . . . 6
|
| 157 | xmul01 11550 |
. . . . . . . . . . 11
| |
| 158 | 157 | ad2antrr 731 |
. . . . . . . . . 10
|
| 159 | xmul01 11550 |
. . . . . . . . . . 11
| |
| 160 | 159 | ad2antlr 732 |
. . . . . . . . . 10
|
| 161 | 158, 160 | breq12d 4414 |
. . . . . . . . 9
|
| 162 | 59, 161 | mpbiri 237 |
. . . . . . . 8
|
| 163 | oveq2 6296 |
. . . . . . . . 9
| |
| 164 | oveq2 6296 |
. . . . . . . . 9
| |
| 165 | 163, 164 | breq12d 4414 |
. . . . . . . 8
|
| 166 | 162, 165 | syl5ibcom 224 |
. . . . . . 7
|
| 167 | 166 | a1dd 47 |
. . . . . 6
|
| 168 | 156, 167 | jaod 382 |
. . . . 5
|
| 169 | 4, 168 | sylbid 219 |
. . . 4
|
| 170 | 169 | expimpd 607 |
. . 3
|
| 171 | 170 | 3impia 1204 |
. 2
|
| 172 | 171 | imp 431 |
1
|
| Colors of variables: wff setvar class |
| Syntax hints: wn 3
wi 4
wb 188 wo 370 wa 371 w3o 983 w3a 984 wceq 1443 wcel 1886 class class class wbr 4401
(class class class)co 6288 cr 9535 cc0 9536 cmul 9541 cpnf 9669 cmnf 9670 cxr 9671 clt 9672 cle 9673 cxmu 11405 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612 ax-pre-mulgt0 9613 |
| This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-op 3974 df-uni 4198 df-iun 4279 df-br 4402 df-opab 4461 df-mpt 4462 df-id 4748 df-po 4754 df-so 4755 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-1st 6790 df-2nd 6791 df-er 7360 df-en 7567 df-dom 7568 df-sdom 7569 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-sub 9859 df-neg 9860 df-xneg 11406 df-xmul 11408 |
| This theorem is referenced by: xlemul2a 11572 xlemul1 11573 nmoi2 21728 nmoi2OLD 21744 esumcst 28877 |
| Copyright terms: Public domain | W3C validator |