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 10417. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| Ref | Expression |
|---|---|
| xlemul1a |
     ![/\](wedge.gif "/\"){kind=small}  
      |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0xr 9657 |
. . . . . 6
| |
| 2 | simpr 461 |
. . . . . 6
| |
| 3 | xrleloe 11375 |
. . . . . 6
   | |
| 4 | 1, 2, 3 | sylancr 663 |
. . . . 5
|
| 5 | simpllr 760 |
. . . . . . . . . . . 12
| |
| 6 | elxr 11350 |
. . . . . . . . . . . 12
  | |
| 7 | 5, 6 | sylib 196 |
. . . . . . . . . . 11
|
| 8 | simplrr 762 |
. . . . . . . . . . . . . . 15
| |
| 9 | simprll 763 |
. . . . . . . . . . . . . . . 16
| |
| 10 | simprlr 764 |
. . . . . . . . . . . . . . . 16
| |
| 11 | simprr 757 |
. . . . . . . . . . . . . . . 16
| |
| 12 | simplrl 761 |
. . . . . . . . . . . . . . . 16
| |
| 13 | lemul1 10415 |
. . . . . . . . . . . . . . . 16
| |
| 14 | 9, 10, 11, 12, 13 | syl112anc 1232 |
. . . . . . . . . . . . . . 15
|
| 15 | 8, 14 | mpbid 210 |
. . . . . . . . . . . . . 14
|
| 16 | rexmul 11488 |
. . . . . . . . . . . . . . 15
| |
| 17 | 9, 11, 16 | syl2anc 661 |
. . . . . . . . . . . . . 14
|
| 18 | rexmul 11488 |
. . . . . . . . . . . . . . 15
| |
| 19 | 10, 11, 18 | syl2anc 661 |
. . . . . . . . . . . . . 14
|
| 20 | 15, 17, 19 | 3brtr4d 4486 |
. . . . . . . . . . . . 13
|
| 21 | 20 | expr 615 |
. . . . . . . . . . . 12
|
| 22 | simprl 756 |
. . . . . . . . . . . . . . 15
| |
| 23 | 0re 9613 |
. . . . . . . . . . . . . . 15
| |
| 24 | lttri4 9686 |
. . . . . . . . . . . . . . 15
| |
| 25 | 22, 23, 24 | sylancl 662 |
. . . . . . . . . . . . . 14
|
| 26 | simplll 759 |
. . . . . . . . . . . . . . . . . . 19
| |
| 27 | 26 | adantr 465 |
. . . . . . . . . . . . . . . . . 18
|
| 28 | xmulpnf1n 11495 |
. . . . . . . . . . . . . . . . . 18
| |
| 29 | 27, 28 | sylan 471 |
. . . . . . . . . . . . . . . . 17
|
| 30 | simpllr 760 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 31 | 30 | adantr 465 |
. . . . . . . . . . . . . . . . . . . 20
|
| 32 | 31 | adantr 465 |
. . . . . . . . . . . . . . . . . . 19
|
| 33 | pnfxr 11346 |
. . . . . . . . . . . . . . . . . . 19
| |
| 34 | xmulcl 11490 |
. . . . . . . . . . . . . . . . . . 19
| |
| 35 | 32, 33, 34 | sylancl 662 |
. . . . . . . . . . . . . . . . . 18
|
| 36 | mnfle 11367 |
. . . . . . . . . . . . . . . . . 18
| |
| 37 | 35, 36 | syl 16 |
. . . . . . . . . . . . . . . . 17
|
| 38 | 29, 37 | eqbrtrd 4476 |
. . . . . . . . . . . . . . . 16
|
| 39 | 38 | ex 434 |
. . . . . . . . . . . . . . 15
|
| 40 | oveq1 6303 |
. . . . . . . . . . . . . . . . . . 19
| |
| 41 | xmul02 11485 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 42 | 33, 41 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
|
| 43 | 40, 42 | syl6eq 2514 |
. . . . . . . . . . . . . . . . . 18
|
| 44 | 43 | adantl 466 |
. . . . . . . . . . . . . . . . 17
|
| 45 | simplrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 46 | breq1 4459 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 47 | 45, 46 | syl5ibcom 220 |
. . . . . . . . . . . . . . . . . . . 20
|
| 48 | simprr 757 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 49 | leloe 9688 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 50 | 23, 48, 49 | sylancr 663 |
. . . . . . . . . . . . . . . . . . . 20
|
| 51 | 47, 50 | sylibd 214 |
. . . . . . . . . . . . . . . . . . 19
|
| 52 | 51 | imp 429 |
. . . . . . . . . . . . . . . . . 18
|
| 53 | pnfge 11364 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 54 | 1, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
|
| 55 | xmulpnf1 11491 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 56 | 31, 55 | sylan 471 |
. . . . . . . . . . . . . . . . . . . 20
|
| 57 | 54, 56 | syl5breqr 4492 |
. . . . . . . . . . . . . . . . . . 19
|
| 58 | xrleid 11381 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 59 | 1, 58 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 60 | 59, 42 | breqtrri 4481 |
. . . . . . . . . . . . . . . . . . . 20
|
| 61 | simpr 461 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 62 | 61 | oveq1d 6311 |
. . . . . . . . . . . . . . . . . . . 20
|
| 63 | 60, 62 | syl5breq 4491 |
. . . . . . . . . . . . . . . . . . 19
|
| 64 | 57, 63 | jaodan 785 |
. . . . . . . . . . . . . . . . . 18
|
| 65 | 52, 64 | syldan 470 |
. . . . . . . . . . . . . . . . 17
|
| 66 | 44, 65 | eqbrtrd 4476 |
. . . . . . . . . . . . . . . 16
|
| 67 | 66 | ex 434 |
. . . . . . . . . . . . . . 15
|
| 68 | pnfge 11364 |
. . . . . . . . . . . . . . . . . 18
| |
| 69 | 33, 68 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
| 70 | 26 | adantr 465 |
. . . . . . . . . . . . . . . . . . 19
|
| 71 | simprr 757 |
. . . . . . . . . . . . . . . . . . 19
| |
| 72 | xmulpnf1 11491 |
. . . . . . . . . . . . . . . . . . 19
| |
| 73 | 70, 71, 72 | syl2anc 661 |
. . . . . . . . . . . . . . . . . 18
|
| 74 | 30 | adantr 465 |
. . . . . . . . . . . . . . . . . . 19
|
| 75 | ltletr 9693 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 76 | 23, 75 | mp3an1 1311 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 77 | 76 | adantl 466 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 78 | 45, 77 | mpan2d 674 |
. . . . . . . . . . . . . . . . . . . 20
|
| 79 | 78 | impr 619 |
. . . . . . . . . . . . . . . . . . 19
|
| 80 | 74, 79, 55 | syl2anc 661 |
. . . . . . . . . . . . . . . . . 18
|
| 81 | 73, 80 | breq12d 4469 |
. . . . . . . . . . . . . . . . 17
|
| 82 | 69, 81 | mpbiri 233 |
. . . . . . . . . . . . . . . 16
|
| 83 | 82 | expr 615 |
. . . . . . . . . . . . . . 15
|
| 84 | 39, 67, 83 | 3jaod 1292 |
. . . . . . . . . . . . . 14
|
| 85 | 25, 84 | mpd 15 |
. . . . . . . . . . . . 13
|
| 86 | oveq2 6304 |
. . . . . . . . . . . . . 14
| |
| 87 | oveq2 6304 |
. . . . . . . . . . . . . 14
| |
| 88 | 86, 87 | breq12d 4469 |
. . . . . . . . . . . . 13
|
| 89 | 85, 88 | syl5ibrcom 222 |
. . . . . . . . . . . 12
|
| 90 | nltmnf 11363 |
. . . . . . . . . . . . . . . . . 18
 | |
| 91 | 1, 90 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
| 92 | breq2 4460 |
. . . . . . . . . . . . . . . . 17
| |
| 93 | 91, 92 | mtbiri 303 |
. . . . . . . . . . . . . . . 16
|
| 94 | 93 | con2i 120 |
. . . . . . . . . . . . . . 15
|
| 95 | 94 | ad2antrl 727 |
. . . . . . . . . . . . . 14
|
| 96 | 95 | adantr 465 |
. . . . . . . . . . . . 13
|
| 97 | 96 | pm2.21d 106 |
. . . . . . . . . . . 12
|
| 98 | 21, 89, 97 | 3jaod 1292 |
. . . . . . . . . . 11
|
| 99 | 7, 98 | mpd 15 |
. . . . . . . . . 10
|
| 100 | 99 | anassrs 648 |
. . . . . . . . 9
|
| 101 | xmulcl 11490 |
. . . . . . . . . . . . . 14
| |
| 102 | 101 | adantlr 714 |
. . . . . . . . . . . . 13
|
| 103 | 102 | ad2antrr 725 |
. . . . . . . . . . . 12
|
| 104 | pnfge 11364 |
. . . . . . . . . . . 12
| |
| 105 | 103, 104 | syl 16 |
. . . . . . . . . . 11
|
| 106 | oveq1 6303 |
. . . . . . . . . . . 12
| |
| 107 | xmulpnf2 11492 |
. . . . . . . . . . . . 13
| |
| 108 | 107 | ad2ant2lr 747 |
. . . . . . . . . . . 12
|
| 109 | 106, 108 | sylan9eqr 2520 |
. . . . . . . . . . 11
|
| 110 | 105, 109 | breqtrrd 4482 |
. . . . . . . . . 10
|
| 111 | 110 | adantlr 714 |
. . . . . . . . 9
|
| 112 | simplrr 762 |
. . . . . . . . . . . . 13
| |
| 113 | simpr 461 |
. . . . . . . . . . . . . 14
| |
| 114 | 26 | adantr 465 |
. . . . . . . . . . . . . . 15
|
| 115 | mnfle 11367 |
. . . . . . . . . . . . . . 15
| |
| 116 | 114, 115 | syl 16 |
. . . . . . . . . . . . . 14
|
| 117 | 113, 116 | eqbrtrd 4476 |
. . . . . . . . . . . . 13
|
| 118 | xrletri3 11383 |
. . . . . . . . . . . . . 14
| |
| 119 | 118 | ad3antrrr 729 |
. . . . . . . . . . . . 13
|
| 120 | 112, 117, 119 | mpbir2and 922 |
. . . . . . . . . . . 12
|
| 121 | 120 | oveq1d 6311 |
. . . . . . . . . . 11
|
| 122 | xmulcl 11490 |
. . . . . . . . . . . . . 14
| |
| 123 | 122 | adantll 713 |
. . . . . . . . . . . . 13
|
| 124 | 123 | ad2antrr 725 |
. . . . . . . . . . . 12
|
| 125 | xrleid 11381 |
. . . . . . . . . . . 12
| |
| 126 | 124, 125 | syl 16 |
. . . . . . . . . . 11
|
| 127 | 121, 126 | eqbrtrd 4476 |
. . . . . . . . . 10
|
| 128 | 127 | adantlr 714 |
. . . . . . . . 9
|
| 129 | elxr 11350 |
. . . . . . . . . . 11
| |
| 130 | 30, 129 | sylib 196 |
. . . . . . . . . 10
|
| 131 | 130 | adantr 465 |
. . . . . . . . 9
|
| 132 | 100, 111, 128, 131 | mpjao3dan 1295 |
. . . . . . . 8
|
| 133 | simplrr 762 |
. . . . . . . . . . 11
| |
| 134 | 30 | adantr 465 |
. . . . . . . . . . . . 13
|
| 135 | pnfge 11364 |
. . . . . . . . . . . . 13
| |
| 136 | 134, 135 | syl 16 |
. . . . . . . . . . . 12
|
| 137 | simpr 461 |
. . . . . . . . . . . 12
| |
| 138 | 136, 137 | breqtrrd 4482 |
. . . . . . . . . . 11
|
| 139 | 118 | ad3antrrr 729 |
. . . . . . . . . . 11
|
| 140 | 133, 138, 139 | mpbir2and 922 |
. . . . . . . . . 10
|
| 141 | 140 | oveq1d 6311 |
. . . . . . . . 9
|
| 142 | 123, 125 | syl 16 |
. . . . . . . . . 10
|
| 143 | 142 | ad2antrr 725 |
. . . . . . . . 9
|
| 144 | 141, 143 | eqbrtrd 4476 |
. . . . . . . 8
|
| 145 | oveq1 6303 |
. . . . . . . . . 10
| |
| 146 | xmulmnf2 11494 |
. . . . . . . . . . 11
| |
| 147 | 146 | ad2ant2lr 747 |
. . . . . . . . . 10
|
| 148 | 145, 147 | sylan9eqr 2520 |
. . . . . . . . 9
|
| 149 | 123 | ad2antrr 725 |
. . . . . . . . . 10
|
| 150 | mnfle 11367 |
. . . . . . . . . 10
| |
| 151 | 149, 150 | syl 16 |
. . . . . . . . 9
|
| 152 | 148, 151 | eqbrtrd 4476 |
. . . . . . . 8
|
| 153 | elxr 11350 |
. . . . . . . . 9
| |
| 154 | 26, 153 | sylib 196 |
. . . . . . . 8
|
| 155 | 132, 144, 152, 154 | mpjao3dan 1295 |
. . . . . . 7
|
| 156 | 155 | exp32 605 |
. . . . . 6
|
| 157 | xmul01 11484 |
. . . . . . . . . . 11
| |
| 158 | 157 | ad2antrr 725 |
. . . . . . . . . 10
|
| 159 | xmul01 11484 |
. . . . . . . . . . 11
| |
| 160 | 159 | ad2antlr 726 |
. . . . . . . . . 10
|
| 161 | 158, 160 | breq12d 4469 |
. . . . . . . . 9
|
| 162 | 59, 161 | mpbiri 233 |
. . . . . . . 8
|
| 163 | oveq2 6304 |
. . . . . . . . 9
| |
| 164 | oveq2 6304 |
. . . . . . . . 9
| |
| 165 | 163, 164 | breq12d 4469 |
. . . . . . . 8
|
| 166 | 162, 165 | syl5ibcom 220 |
. . . . . . 7
|
| 167 | 166 | a1dd 46 |
. . . . . 6
|
| 168 | 156, 167 | jaod 380 |
. . . . 5
|
| 169 | 4, 168 | sylbid 215 |
. . . 4
|
| 170 | 169 | expimpd 603 |
. . 3
|
| 171 | 170 | 3impia 1193 |
. 2
|
| 172 | 171 | 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 1395 wcel 1819 class class class wbr 4456
(class class class)co 6296 cr 9508 cc0 9509 cmul 9514 cpnf 9642 cmnf 9643 cxr 9644 clt 9645 cle 9646 cxmu 11342 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 |
| This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-op 4039 df-uni 4252 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-id 4804 df-po 4809 df-so 4810 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-1st 6799 df-2nd 6800 df-er 7329 df-en 7536 df-dom 7537 df-sdom 7538 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-xneg 11343 df-xmul 11345 |
| This theorem is referenced by: xlemul2a 11506 xlemul1 11507 nmoi2 21362 esumcst 28226 |
| Copyright terms: Public domain | W3C validator |