| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Multiplication of signed reals is commutative. |
| Ref | Expression |
|---|---|
| mulcomsr.1 |
|
| mulcomsr.2 |
|
| Ref | Expression |
|---|---|
| mulcomsr |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-nr 5319 |
. . 3
| |
| 2 | mulsrpr 5337 |
. . 3
| |
| 3 | mulsrpr 5337 |
. . 3
| |
| 4 | visset 1858 |
. . . . 5
| |
| 5 | visset 1858 |
. . . . 5
| |
| 6 | 4, 5 | mulcompr 5277 |
. . . 4
|
| 7 | visset 1858 |
. . . . 5
| |
| 8 | visset 1858 |
. . . . 5
| |
| 9 | 7, 8 | mulcompr 5277 |
. . . 4
|
| 10 | 6, 9 | opreq12i 4029 |
. . 3
|
| 11 | 4, 8 | mulcompr 5277 |
. . . . 5
|
| 12 | 7, 5 | mulcompr 5277 |
. . . . 5
|
| 13 | 11, 12 | opreq12i 4029 |
. . . 4
|
| 14 | oprex 4039 |
. . . . 5
| |
| 15 | oprex 4039 |
. . . . 5
| |
| 16 | 14, 15 | addcompr 5275 |
. . . 4
|
| 17 | 13, 16 | eqtri 1537 |
. . 3
|
| 18 | 1, 2, 3, 10, 17 | ecoprcom 4458 |
. 2
|
| 19 | mulcomsr.2 |
. . 3
| |
| 20 | dmmulsr 5347 |
. . 3
| |
| 21 | mulcomsr.1 |
. . 3
| |
| 22 | 19, 20, 21 | ndmoprcom 4106 |
. 2
|
| 23 | 18, 22 | pm2.61i 124 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: sqgt0sr 5367 mulresr 5409 axmulcom 5428 axmulass 5430 axcnre 5438 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 997 ax-gen 998 ax-8 999 ax-9 1000 ax-10 1001 ax-11 1002 ax-12 1003 ax-13 1004 ax-14 1005 ax-17 1006 ax-4 1008 ax-5o 1010 ax-6o 1013 ax-9o 1158 ax-10o 1176 ax-16 1246 ax-11o 1254 ax-ext 1499 ax-rep 2766 ax-sep 2776 ax-nul 2783 ax-pow 2817 ax-pr 2854 ax-un 3088 ax-inf2 4768 |
| This theorem depends on definitions: df-bi 145 df-or 222 df-an 223 df-3or 781 df-3an 782 df-ex 1016 df-sb 1208 df-eu 1420 df-mo 1421 df-clab 1505 df-cleq 1510 df-clel 1513 df-ne 1629 df-ral 1694 df-rex 1695 df-reu 1696 df-rab 1697 df-v 1857 df-sbc 1986 df-csb 2051 df-dif 2100 df-un 2101 df-in 2102 df-ss 2104 df-pss 2106 df-nul 2332 df-if 2415 df-pw 2458 df-sn 2469 df-pr 2470 df-tp 2472 df-op 2473 df-uni 2569 df-int 2600 df-iun 2634 df-br 2692 df-opab 2740 df-tr 2754 df-eprel 2909 df-id 2912 df-po 2917 df-so 2928 df-fr 2946 df-we 2961 df-ord 2977 df-on 2978 df-lim 2979 df-suc 2980 df-om 3218 df-xp 3264 df-rel 3265 df-cnv 3266 df-co 3267 df-dm 3268 df-rn 3269 df-res 3270 df-ima 3271 df-fun 3272 df-fn 3273 df-f 3274 df-fv 3278 df-opr 4021 df-oprab 4022 df-1st 4138 df-2nd 4139 df-rdg 4231 df-1o 4267 df-oadd 4269 df-omul 4270 df-er 4399 df-ec 4401 df-qs 4404 df-ni 5152 df-pli 5153 df-mi 5154 df-lti 5155 df-plpq 5187 df-mpq 5188 df-enq 5189 df-nq 5190 df-plq 5191 df-mq 5192 df-rq 5193 df-ltq 5194 df-1q 5195 df-np 5238 df-plp 5240 df-mp 5241 df-ltp 5242 df-mpr 5317 df-enr 5318 df-nr 5319 df-mr 5321 |