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 10481. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| Ref | Expression |
|---|---|
| xlemul1a |
     ![/\](wedge.gif "/\"){kind=small}  
      |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0xr 9705 |
. . . . . 6
| |
| 2 | simpr 468 |
. . . . . 6
| |
| 3 | xrleloe 11466 |
. . . . . 6
   | |
| 4 | 1, 2, 3 | sylancr 676 |
. . . . 5
|
| 5 | simpllr 777 |
. . . . . . . . . . . 12
| |
| 6 | elxr 11439 |
. . . . . . . . . . . 12
  | |
| 7 | 5, 6 | sylib 201 |
. . . . . . . . . . 11
|
| 8 | simplrr 779 |
. . . . . . . . . . . . . . 15
| |
| 9 | simprll 780 |
. . . . . . . . . . . . . . . 16
| |
| 10 | simprlr 781 |
. . . . . . . . . . . . . . . 16
| |
| 11 | simprr 774 |
. . . . . . . . . . . . . . . 16
| |
| 12 | simplrl 778 |
. . . . . . . . . . . . . . . 16
| |
| 13 | lemul1 10479 |
. . . . . . . . . . . . . . . 16
| |
| 14 | 9, 10, 11, 12, 13 | syl112anc 1296 |
. . . . . . . . . . . . . . 15
|
| 15 | 8, 14 | mpbid 215 |
. . . . . . . . . . . . . 14
|
| 16 | rexmul 11582 |
. . . . . . . . . . . . . . 15
| |
| 17 | 9, 11, 16 | syl2anc 673 |
. . . . . . . . . . . . . 14
|
| 18 | rexmul 11582 |
. . . . . . . . . . . . . . 15
| |
| 19 | 10, 11, 18 | syl2anc 673 |
. . . . . . . . . . . . . 14
|
| 20 | 15, 17, 19 | 3brtr4d 4426 |
. . . . . . . . . . . . 13
|
| 21 | 20 | expr 626 |
. . . . . . . . . . . 12
|
| 22 | simprl 772 |
. . . . . . . . . . . . . . 15
| |
| 23 | 0re 9661 |
. . . . . . . . . . . . . . 15
| |
| 24 | lttri4 9736 |
. . . . . . . . . . . . . . 15
| |
| 25 | 22, 23, 24 | sylancl 675 |
. . . . . . . . . . . . . 14
|
| 26 | simplll 776 |
. . . . . . . . . . . . . . . . . . 19
| |
| 27 | 26 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
|
| 28 | xmulpnf1n 11589 |
. . . . . . . . . . . . . . . . . 18
| |
| 29 | 27, 28 | sylan 479 |
. . . . . . . . . . . . . . . . 17
|
| 30 | simpllr 777 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 31 | 30 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
|
| 32 | 31 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
|
| 33 | pnfxr 11435 |
. . . . . . . . . . . . . . . . . . 19
| |
| 34 | xmulcl 11584 |
. . . . . . . . . . . . . . . . . . 19
| |
| 35 | 32, 33, 34 | sylancl 675 |
. . . . . . . . . . . . . . . . . 18
|
| 36 | mnfle 11458 |
. . . . . . . . . . . . . . . . . 18
| |
| 37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
| 38 | 29, 37 | eqbrtrd 4416 |
. . . . . . . . . . . . . . . 16
|
| 39 | 38 | ex 441 |
. . . . . . . . . . . . . . 15
|
| 40 | oveq1 6315 |
. . . . . . . . . . . . . . . . . . 19
| |
| 41 | xmul02 11579 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 42 | 33, 41 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
|
| 43 | 40, 42 | syl6eq 2521 |
. . . . . . . . . . . . . . . . . 18
|
| 44 | 43 | adantl 473 |
. . . . . . . . . . . . . . . . 17
|
| 45 | simplrr 779 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 46 | breq1 4398 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 47 | 45, 46 | syl5ibcom 228 |
. . . . . . . . . . . . . . . . . . . 20
|
| 48 | simprr 774 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 49 | leloe 9738 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 50 | 23, 48, 49 | sylancr 676 |
. . . . . . . . . . . . . . . . . . . 20
|
| 51 | 47, 50 | sylibd 222 |
. . . . . . . . . . . . . . . . . . 19
|
| 52 | 51 | imp 436 |
. . . . . . . . . . . . . . . . . 18
|
| 53 | pnfge 11455 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 54 | 1, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
|
| 55 | xmulpnf1 11585 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 56 | 31, 55 | sylan 479 |
. . . . . . . . . . . . . . . . . . . 20
|
| 57 | 54, 56 | syl5breqr 4432 |
. . . . . . . . . . . . . . . . . . 19
|
| 58 | xrleid 11472 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 59 | 1, 58 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 60 | 59, 42 | breqtrri 4421 |
. . . . . . . . . . . . . . . . . . . 20
|
| 61 | simpr 468 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 62 | 61 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . 20
|
| 63 | 60, 62 | syl5breq 4431 |
. . . . . . . . . . . . . . . . . . 19
|
| 64 | 57, 63 | jaodan 802 |
. . . . . . . . . . . . . . . . . 18
|
| 65 | 52, 64 | syldan 478 |
. . . . . . . . . . . . . . . . 17
|
| 66 | 44, 65 | eqbrtrd 4416 |
. . . . . . . . . . . . . . . 16
|
| 67 | 66 | ex 441 |
. . . . . . . . . . . . . . 15
|
| 68 | pnfge 11455 |
. . . . . . . . . . . . . . . . . 18
| |
| 69 | 33, 68 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
| 70 | 26 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
|
| 71 | simprr 774 |
. . . . . . . . . . . . . . . . . . 19
| |
| 72 | xmulpnf1 11585 |
. . . . . . . . . . . . . . . . . . 19
| |
| 73 | 70, 71, 72 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
|
| 74 | 30 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
|
| 75 | ltletr 9743 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 76 | 23, 75 | mp3an1 1377 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 77 | 76 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 78 | 45, 77 | mpan2d 688 |
. . . . . . . . . . . . . . . . . . . 20
|
| 79 | 78 | impr 631 |
. . . . . . . . . . . . . . . . . . 19
|
| 80 | 74, 79, 55 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
|
| 81 | 73, 80 | breq12d 4408 |
. . . . . . . . . . . . . . . . 17
|
| 82 | 69, 81 | mpbiri 241 |
. . . . . . . . . . . . . . . 16
|
| 83 | 82 | expr 626 |
. . . . . . . . . . . . . . 15
|
| 84 | 39, 67, 83 | 3jaod 1358 |
. . . . . . . . . . . . . 14
|
| 85 | 25, 84 | mpd 15 |
. . . . . . . . . . . . 13
|
| 86 | oveq2 6316 |
. . . . . . . . . . . . . 14
| |
| 87 | oveq2 6316 |
. . . . . . . . . . . . . 14
| |
| 88 | 86, 87 | breq12d 4408 |
. . . . . . . . . . . . 13
|
| 89 | 85, 88 | syl5ibrcom 230 |
. . . . . . . . . . . 12
|
| 90 | nltmnf 11454 |
. . . . . . . . . . . . . . . . . 18
 | |
| 91 | 1, 90 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
| 92 | breq2 4399 |
. . . . . . . . . . . . . . . . 17
| |
| 93 | 91, 92 | mtbiri 310 |
. . . . . . . . . . . . . . . 16
|
| 94 | 93 | con2i 124 |
. . . . . . . . . . . . . . 15
|
| 95 | 94 | ad2antrl 742 |
. . . . . . . . . . . . . 14
|
| 96 | 95 | adantr 472 |
. . . . . . . . . . . . 13
|
| 97 | 96 | pm2.21d 109 |
. . . . . . . . . . . 12
|
| 98 | 21, 89, 97 | 3jaod 1358 |
. . . . . . . . . . 11
|
| 99 | 7, 98 | mpd 15 |
. . . . . . . . . 10
|
| 100 | 99 | anassrs 660 |
. . . . . . . . 9
|
| 101 | xmulcl 11584 |
. . . . . . . . . . . . . 14
| |
| 102 | 101 | adantlr 729 |
. . . . . . . . . . . . 13
|
| 103 | 102 | ad2antrr 740 |
. . . . . . . . . . . 12
|
| 104 | pnfge 11455 |
. . . . . . . . . . . 12
| |
| 105 | 103, 104 | syl 17 |
. . . . . . . . . . 11
|
| 106 | oveq1 6315 |
. . . . . . . . . . . 12
| |
| 107 | xmulpnf2 11586 |
. . . . . . . . . . . . 13
| |
| 108 | 107 | ad2ant2lr 762 |
. . . . . . . . . . . 12
|
| 109 | 106, 108 | sylan9eqr 2527 |
. . . . . . . . . . 11
|
| 110 | 105, 109 | breqtrrd 4422 |
. . . . . . . . . 10
|
| 111 | 110 | adantlr 729 |
. . . . . . . . 9
|
| 112 | simplrr 779 |
. . . . . . . . . . . . 13
| |
| 113 | simpr 468 |
. . . . . . . . . . . . . 14
| |
| 114 | 26 | adantr 472 |
. . . . . . . . . . . . . . 15
|
| 115 | mnfle 11458 |
. . . . . . . . . . . . . . 15
| |
| 116 | 114, 115 | syl 17 |
. . . . . . . . . . . . . 14
|
| 117 | 113, 116 | eqbrtrd 4416 |
. . . . . . . . . . . . 13
|
| 118 | xrletri3 11474 |
. . . . . . . . . . . . . 14
| |
| 119 | 118 | ad3antrrr 744 |
. . . . . . . . . . . . 13
|
| 120 | 112, 117, 119 | mpbir2and 936 |
. . . . . . . . . . . 12
|
| 121 | 120 | oveq1d 6323 |
. . . . . . . . . . 11
|
| 122 | xmulcl 11584 |
. . . . . . . . . . . . . 14
| |
| 123 | 122 | adantll 728 |
. . . . . . . . . . . . 13
|
| 124 | 123 | ad2antrr 740 |
. . . . . . . . . . . 12
|
| 125 | xrleid 11472 |
. . . . . . . . . . . 12
| |
| 126 | 124, 125 | syl 17 |
. . . . . . . . . . 11
|
| 127 | 121, 126 | eqbrtrd 4416 |
. . . . . . . . . 10
|
| 128 | 127 | adantlr 729 |
. . . . . . . . 9
|
| 129 | elxr 11439 |
. . . . . . . . . . 11
| |
| 130 | 30, 129 | sylib 201 |
. . . . . . . . . 10
|
| 131 | 130 | adantr 472 |
. . . . . . . . 9
|
| 132 | 100, 111, 128, 131 | mpjao3dan 1361 |
. . . . . . . 8
|
| 133 | simplrr 779 |
. . . . . . . . . . 11
| |
| 134 | 30 | adantr 472 |
. . . . . . . . . . . . 13
|
| 135 | pnfge 11455 |
. . . . . . . . . . . . 13
| |
| 136 | 134, 135 | syl 17 |
. . . . . . . . . . . 12
|
| 137 | simpr 468 |
. . . . . . . . . . . 12
| |
| 138 | 136, 137 | breqtrrd 4422 |
. . . . . . . . . . 11
|
| 139 | 118 | ad3antrrr 744 |
. . . . . . . . . . 11
|
| 140 | 133, 138, 139 | mpbir2and 936 |
. . . . . . . . . 10
|
| 141 | 140 | oveq1d 6323 |
. . . . . . . . 9
|
| 142 | 123, 125 | syl 17 |
. . . . . . . . . 10
|
| 143 | 142 | ad2antrr 740 |
. . . . . . . . 9
|
| 144 | 141, 143 | eqbrtrd 4416 |
. . . . . . . 8
|
| 145 | oveq1 6315 |
. . . . . . . . . 10
| |
| 146 | xmulmnf2 11588 |
. . . . . . . . . . 11
| |
| 147 | 146 | ad2ant2lr 762 |
. . . . . . . . . 10
|
| 148 | 145, 147 | sylan9eqr 2527 |
. . . . . . . . 9
|
| 149 | 123 | ad2antrr 740 |
. . . . . . . . . 10
|
| 150 | mnfle 11458 |
. . . . . . . . . 10
| |
| 151 | 149, 150 | syl 17 |
. . . . . . . . 9
|
| 152 | 148, 151 | eqbrtrd 4416 |
. . . . . . . 8
|
| 153 | elxr 11439 |
. . . . . . . . 9
| |
| 154 | 26, 153 | sylib 201 |
. . . . . . . 8
|
| 155 | 132, 144, 152, 154 | mpjao3dan 1361 |
. . . . . . 7
|
| 156 | 155 | exp32 616 |
. . . . . 6
|
| 157 | xmul01 11578 |
. . . . . . . . . . 11
| |
| 158 | 157 | ad2antrr 740 |
. . . . . . . . . 10
|
| 159 | xmul01 11578 |
. . . . . . . . . . 11
| |
| 160 | 159 | ad2antlr 741 |
. . . . . . . . . 10
|
| 161 | 158, 160 | breq12d 4408 |
. . . . . . . . 9
|
| 162 | 59, 161 | mpbiri 241 |
. . . . . . . 8
|
| 163 | oveq2 6316 |
. . . . . . . . 9
| |
| 164 | oveq2 6316 |
. . . . . . . . 9
| |
| 165 | 163, 164 | breq12d 4408 |
. . . . . . . 8
|
| 166 | 162, 165 | syl5ibcom 228 |
. . . . . . 7
|
| 167 | 166 | a1dd 46 |
. . . . . 6
|
| 168 | 156, 167 | jaod 387 |
. . . . 5
|
| 169 | 4, 168 | sylbid 223 |
. . . 4
|
| 170 | 169 | expimpd 614 |
. . 3
|
| 171 | 170 | 3impia 1228 |
. 2
|
| 172 | 171 | imp 436 |
1
|
| Colors of variables: wff setvar class |
| Syntax hints: wn 3
wi 4
wb 189 wo 375 wa 376 w3o 1006 w3a 1007 wceq 1452 wcel 1904 class class class wbr 4395
(class class class)co 6308 cr 9556 cc0 9557 cmul 9562 cpnf 9690 cmnf 9691 cxr 9692 clt 9693 cle 9694 cxmu 11431 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 |
| This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-op 3966 df-uni 4191 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-id 4754 df-po 4760 df-so 4761 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-1st 6812 df-2nd 6813 df-er 7381 df-en 7588 df-dom 7589 df-sdom 7590 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-xneg 11432 df-xmul 11434 |
| This theorem is referenced by: xlemul2a 11600 xlemul1 11601 nmoi2 21813 nmoi2OLD 21829 esumcst 28958 |
| Copyright terms: Public domain | W3C validator |