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 10437. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| Ref | Expression |
|---|---|
| xlemul1a |
     ![/\](wedge.gif "/\"){kind=small}  
      |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0xr 9670 |
. . . . . 6
| |
| 2 | simpr 459 |
. . . . . 6
| |
| 3 | xrleloe 11403 |
. . . . . 6
   | |
| 4 | 1, 2, 3 | sylancr 661 |
. . . . 5
|
| 5 | simpllr 761 |
. . . . . . . . . . . 12
| |
| 6 | elxr 11378 |
. . . . . . . . . . . 12
  | |
| 7 | 5, 6 | sylib 196 |
. . . . . . . . . . 11
|
| 8 | simplrr 763 |
. . . . . . . . . . . . . . 15
| |
| 9 | simprll 764 |
. . . . . . . . . . . . . . . 16
| |
| 10 | simprlr 765 |
. . . . . . . . . . . . . . . 16
| |
| 11 | simprr 758 |
. . . . . . . . . . . . . . . 16
| |
| 12 | simplrl 762 |
. . . . . . . . . . . . . . . 16
| |
| 13 | lemul1 10435 |
. . . . . . . . . . . . . . . 16
| |
| 14 | 9, 10, 11, 12, 13 | syl112anc 1234 |
. . . . . . . . . . . . . . 15
|
| 15 | 8, 14 | mpbid 210 |
. . . . . . . . . . . . . 14
|
| 16 | rexmul 11516 |
. . . . . . . . . . . . . . 15
| |
| 17 | 9, 11, 16 | syl2anc 659 |
. . . . . . . . . . . . . 14
|
| 18 | rexmul 11516 |
. . . . . . . . . . . . . . 15
| |
| 19 | 10, 11, 18 | syl2anc 659 |
. . . . . . . . . . . . . 14
|
| 20 | 15, 17, 19 | 3brtr4d 4425 |
. . . . . . . . . . . . 13
|
| 21 | 20 | expr 613 |
. . . . . . . . . . . 12
|
| 22 | simprl 756 |
. . . . . . . . . . . . . . 15
| |
| 23 | 0re 9626 |
. . . . . . . . . . . . . . 15
| |
| 24 | lttri4 9700 |
. . . . . . . . . . . . . . 15
| |
| 25 | 22, 23, 24 | sylancl 660 |
. . . . . . . . . . . . . 14
|
| 26 | simplll 760 |
. . . . . . . . . . . . . . . . . . 19
| |
| 27 | 26 | adantr 463 |
. . . . . . . . . . . . . . . . . 18
|
| 28 | xmulpnf1n 11523 |
. . . . . . . . . . . . . . . . . 18
| |
| 29 | 27, 28 | sylan 469 |
. . . . . . . . . . . . . . . . 17
|
| 30 | simpllr 761 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 31 | 30 | adantr 463 |
. . . . . . . . . . . . . . . . . . . 20
|
| 32 | 31 | adantr 463 |
. . . . . . . . . . . . . . . . . . 19
|
| 33 | pnfxr 11374 |
. . . . . . . . . . . . . . . . . . 19
| |
| 34 | xmulcl 11518 |
. . . . . . . . . . . . . . . . . . 19
| |
| 35 | 32, 33, 34 | sylancl 660 |
. . . . . . . . . . . . . . . . . 18
|
| 36 | mnfle 11395 |
. . . . . . . . . . . . . . . . . 18
| |
| 37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
| 38 | 29, 37 | eqbrtrd 4415 |
. . . . . . . . . . . . . . . 16
|
| 39 | 38 | ex 432 |
. . . . . . . . . . . . . . 15
|
| 40 | oveq1 6285 |
. . . . . . . . . . . . . . . . . . 19
| |
| 41 | xmul02 11513 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 42 | 33, 41 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
|
| 43 | 40, 42 | syl6eq 2459 |
. . . . . . . . . . . . . . . . . 18
|
| 44 | 43 | adantl 464 |
. . . . . . . . . . . . . . . . 17
|
| 45 | simplrr 763 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 46 | breq1 4398 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 47 | 45, 46 | syl5ibcom 220 |
. . . . . . . . . . . . . . . . . . . 20
|
| 48 | simprr 758 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 49 | leloe 9702 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 50 | 23, 48, 49 | sylancr 661 |
. . . . . . . . . . . . . . . . . . . 20
|
| 51 | 47, 50 | sylibd 214 |
. . . . . . . . . . . . . . . . . . 19
|
| 52 | 51 | imp 427 |
. . . . . . . . . . . . . . . . . 18
|
| 53 | pnfge 11392 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 54 | 1, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
|
| 55 | xmulpnf1 11519 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 56 | 31, 55 | sylan 469 |
. . . . . . . . . . . . . . . . . . . 20
|
| 57 | 54, 56 | syl5breqr 4431 |
. . . . . . . . . . . . . . . . . . 19
|
| 58 | xrleid 11409 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 59 | 1, 58 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 60 | 59, 42 | breqtrri 4420 |
. . . . . . . . . . . . . . . . . . . 20
|
| 61 | simpr 459 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 62 | 61 | oveq1d 6293 |
. . . . . . . . . . . . . . . . . . . 20
|
| 63 | 60, 62 | syl5breq 4430 |
. . . . . . . . . . . . . . . . . . 19
|
| 64 | 57, 63 | jaodan 786 |
. . . . . . . . . . . . . . . . . 18
|
| 65 | 52, 64 | syldan 468 |
. . . . . . . . . . . . . . . . 17
|
| 66 | 44, 65 | eqbrtrd 4415 |
. . . . . . . . . . . . . . . 16
|
| 67 | 66 | ex 432 |
. . . . . . . . . . . . . . 15
|
| 68 | pnfge 11392 |
. . . . . . . . . . . . . . . . . 18
| |
| 69 | 33, 68 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
| 70 | 26 | adantr 463 |
. . . . . . . . . . . . . . . . . . 19
|
| 71 | simprr 758 |
. . . . . . . . . . . . . . . . . . 19
| |
| 72 | xmulpnf1 11519 |
. . . . . . . . . . . . . . . . . . 19
| |
| 73 | 70, 71, 72 | syl2anc 659 |
. . . . . . . . . . . . . . . . . 18
|
| 74 | 30 | adantr 463 |
. . . . . . . . . . . . . . . . . . 19
|
| 75 | ltletr 9707 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 76 | 23, 75 | mp3an1 1313 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 77 | 76 | adantl 464 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 78 | 45, 77 | mpan2d 672 |
. . . . . . . . . . . . . . . . . . . 20
|
| 79 | 78 | impr 617 |
. . . . . . . . . . . . . . . . . . 19
|
| 80 | 74, 79, 55 | syl2anc 659 |
. . . . . . . . . . . . . . . . . 18
|
| 81 | 73, 80 | breq12d 4408 |
. . . . . . . . . . . . . . . . 17
|
| 82 | 69, 81 | mpbiri 233 |
. . . . . . . . . . . . . . . 16
|
| 83 | 82 | expr 613 |
. . . . . . . . . . . . . . 15
|
| 84 | 39, 67, 83 | 3jaod 1294 |
. . . . . . . . . . . . . 14
|
| 85 | 25, 84 | mpd 15 |
. . . . . . . . . . . . 13
|
| 86 | oveq2 6286 |
. . . . . . . . . . . . . 14
| |
| 87 | oveq2 6286 |
. . . . . . . . . . . . . 14
| |
| 88 | 86, 87 | breq12d 4408 |
. . . . . . . . . . . . 13
|
| 89 | 85, 88 | syl5ibrcom 222 |
. . . . . . . . . . . 12
|
| 90 | nltmnf 11391 |
. . . . . . . . . . . . . . . . . 18
 | |
| 91 | 1, 90 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
| 92 | breq2 4399 |
. . . . . . . . . . . . . . . . 17
| |
| 93 | 91, 92 | mtbiri 301 |
. . . . . . . . . . . . . . . 16
|
| 94 | 93 | con2i 120 |
. . . . . . . . . . . . . . 15
|
| 95 | 94 | ad2antrl 726 |
. . . . . . . . . . . . . 14
|
| 96 | 95 | adantr 463 |
. . . . . . . . . . . . 13
|
| 97 | 96 | pm2.21d 106 |
. . . . . . . . . . . 12
|
| 98 | 21, 89, 97 | 3jaod 1294 |
. . . . . . . . . . 11
|
| 99 | 7, 98 | mpd 15 |
. . . . . . . . . 10
|
| 100 | 99 | anassrs 646 |
. . . . . . . . 9
|
| 101 | xmulcl 11518 |
. . . . . . . . . . . . . 14
| |
| 102 | 101 | adantlr 713 |
. . . . . . . . . . . . 13
|
| 103 | 102 | ad2antrr 724 |
. . . . . . . . . . . 12
|
| 104 | pnfge 11392 |
. . . . . . . . . . . 12
| |
| 105 | 103, 104 | syl 17 |
. . . . . . . . . . 11
|
| 106 | oveq1 6285 |
. . . . . . . . . . . 12
| |
| 107 | xmulpnf2 11520 |
. . . . . . . . . . . . 13
| |
| 108 | 107 | ad2ant2lr 746 |
. . . . . . . . . . . 12
|
| 109 | 106, 108 | sylan9eqr 2465 |
. . . . . . . . . . 11
|
| 110 | 105, 109 | breqtrrd 4421 |
. . . . . . . . . 10
|
| 111 | 110 | adantlr 713 |
. . . . . . . . 9
|
| 112 | simplrr 763 |
. . . . . . . . . . . . 13
| |
| 113 | simpr 459 |
. . . . . . . . . . . . . 14
| |
| 114 | 26 | adantr 463 |
. . . . . . . . . . . . . . 15
|
| 115 | mnfle 11395 |
. . . . . . . . . . . . . . 15
| |
| 116 | 114, 115 | syl 17 |
. . . . . . . . . . . . . 14
|
| 117 | 113, 116 | eqbrtrd 4415 |
. . . . . . . . . . . . 13
|
| 118 | xrletri3 11411 |
. . . . . . . . . . . . . 14
| |
| 119 | 118 | ad3antrrr 728 |
. . . . . . . . . . . . 13
|
| 120 | 112, 117, 119 | mpbir2and 923 |
. . . . . . . . . . . 12
|
| 121 | 120 | oveq1d 6293 |
. . . . . . . . . . 11
|
| 122 | xmulcl 11518 |
. . . . . . . . . . . . . 14
| |
| 123 | 122 | adantll 712 |
. . . . . . . . . . . . 13
|
| 124 | 123 | ad2antrr 724 |
. . . . . . . . . . . 12
|
| 125 | xrleid 11409 |
. . . . . . . . . . . 12
| |
| 126 | 124, 125 | syl 17 |
. . . . . . . . . . 11
|
| 127 | 121, 126 | eqbrtrd 4415 |
. . . . . . . . . 10
|
| 128 | 127 | adantlr 713 |
. . . . . . . . 9
|
| 129 | elxr 11378 |
. . . . . . . . . . 11
| |
| 130 | 30, 129 | sylib 196 |
. . . . . . . . . 10
|
| 131 | 130 | adantr 463 |
. . . . . . . . 9
|
| 132 | 100, 111, 128, 131 | mpjao3dan 1297 |
. . . . . . . 8
|
| 133 | simplrr 763 |
. . . . . . . . . . 11
| |
| 134 | 30 | adantr 463 |
. . . . . . . . . . . . 13
|
| 135 | pnfge 11392 |
. . . . . . . . . . . . 13
| |
| 136 | 134, 135 | syl 17 |
. . . . . . . . . . . 12
|
| 137 | simpr 459 |
. . . . . . . . . . . 12
| |
| 138 | 136, 137 | breqtrrd 4421 |
. . . . . . . . . . 11
|
| 139 | 118 | ad3antrrr 728 |
. . . . . . . . . . 11
|
| 140 | 133, 138, 139 | mpbir2and 923 |
. . . . . . . . . 10
|
| 141 | 140 | oveq1d 6293 |
. . . . . . . . 9
|
| 142 | 123, 125 | syl 17 |
. . . . . . . . . 10
|
| 143 | 142 | ad2antrr 724 |
. . . . . . . . 9
|
| 144 | 141, 143 | eqbrtrd 4415 |
. . . . . . . 8
|
| 145 | oveq1 6285 |
. . . . . . . . . 10
| |
| 146 | xmulmnf2 11522 |
. . . . . . . . . . 11
| |
| 147 | 146 | ad2ant2lr 746 |
. . . . . . . . . 10
|
| 148 | 145, 147 | sylan9eqr 2465 |
. . . . . . . . 9
|
| 149 | 123 | ad2antrr 724 |
. . . . . . . . . 10
|
| 150 | mnfle 11395 |
. . . . . . . . . 10
| |
| 151 | 149, 150 | syl 17 |
. . . . . . . . 9
|
| 152 | 148, 151 | eqbrtrd 4415 |
. . . . . . . 8
|
| 153 | elxr 11378 |
. . . . . . . . 9
| |
| 154 | 26, 153 | sylib 196 |
. . . . . . . 8
|
| 155 | 132, 144, 152, 154 | mpjao3dan 1297 |
. . . . . . 7
|
| 156 | 155 | exp32 603 |
. . . . . 6
|
| 157 | xmul01 11512 |
. . . . . . . . . . 11
| |
| 158 | 157 | ad2antrr 724 |
. . . . . . . . . 10
|
| 159 | xmul01 11512 |
. . . . . . . . . . 11
| |
| 160 | 159 | ad2antlr 725 |
. . . . . . . . . 10
|
| 161 | 158, 160 | breq12d 4408 |
. . . . . . . . 9
|
| 162 | 59, 161 | mpbiri 233 |
. . . . . . . 8
|
| 163 | oveq2 6286 |
. . . . . . . . 9
| |
| 164 | oveq2 6286 |
. . . . . . . . 9
| |
| 165 | 163, 164 | breq12d 4408 |
. . . . . . . 8
|
| 166 | 162, 165 | syl5ibcom 220 |
. . . . . . 7
|
| 167 | 166 | a1dd 44 |
. . . . . 6
|
| 168 | 156, 167 | jaod 378 |
. . . . 5
|
| 169 | 4, 168 | sylbid 215 |
. . . 4
|
| 170 | 169 | expimpd 601 |
. . 3
|
| 171 | 170 | 3impia 1194 |
. 2
|
| 172 | 171 | imp 427 |
1
|
| Colors of variables: wff setvar class |
| Syntax hints: wn 3
wi 4
wb 184 wo 366 wa 367 w3o 973 w3a 974 wceq 1405 wcel 1842 class class class wbr 4395
(class class class)co 6278 cr 9521 cc0 9522 cmul 9527 cpnf 9655 cmnf 9656 cxr 9657 clt 9658 cle 9659 cxmu 11370 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1639 ax-4 1652 ax-5 1725 ax-6 1771 ax-7 1814 ax-8 1844 ax-9 1846 ax-10 1861 ax-11 1866 ax-12 1878 ax-13 2026 ax-ext 2380 ax-sep 4517 ax-nul 4525 ax-pow 4572 ax-pr 4630 ax-un 6574 ax-cnex 9578 ax-resscn 9579 ax-1cn 9580 ax-icn 9581 ax-addcl 9582 ax-addrcl 9583 ax-mulcl 9584 ax-mulrcl 9585 ax-mulcom 9586 ax-addass 9587 ax-mulass 9588 ax-distr 9589 ax-i2m1 9590 ax-1ne0 9591 ax-1rid 9592 ax-rnegex 9593 ax-rrecex 9594 ax-cnre 9595 ax-pre-lttri 9596 ax-pre-lttrn 9597 ax-pre-ltadd 9598 ax-pre-mulgt0 9599 |
| This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 975 df-3an 976 df-tru 1408 df-ex 1634 df-nf 1638 df-sb 1764 df-eu 2242 df-mo 2243 df-clab 2388 df-cleq 2394 df-clel 2397 df-nfc 2552 df-ne 2600 df-nel 2601 df-ral 2759 df-rex 2760 df-reu 2761 df-rab 2763 df-v 3061 df-sbc 3278 df-csb 3374 df-dif 3417 df-un 3419 df-in 3421 df-ss 3428 df-nul 3739 df-if 3886 df-pw 3957 df-sn 3973 df-pr 3975 df-op 3979 df-uni 4192 df-iun 4273 df-br 4396 df-opab 4454 df-mpt 4455 df-id 4738 df-po 4744 df-so 4745 df-xp 4829 df-rel 4830 df-cnv 4831 df-co 4832 df-dm 4833 df-rn 4834 df-res 4835 df-ima 4836 df-iota 5533 df-fun 5571 df-fn 5572 df-f 5573 df-f1 5574 df-fo 5575 df-f1o 5576 df-fv 5577 df-riota 6240 df-ov 6281 df-oprab 6282 df-mpt2 6283 df-1st 6784 df-2nd 6785 df-er 7348 df-en 7555 df-dom 7556 df-sdom 7557 df-pnf 9660 df-mnf 9661 df-xr 9662 df-ltxr 9663 df-le 9664 df-sub 9843 df-neg 9844 df-xneg 11371 df-xmul 11373 |
| This theorem is referenced by: xlemul2a 11534 xlemul1 11535 nmoi2 21529 esumcst 28510 |
| Copyright terms: Public domain | W3C validator |