# Metamath Proof Explorer

## Theorem xmulneg2

Description: Extended real version of mulneg2 . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmulneg2 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to {A}{\cdot }_{𝑒}\left(-{B}\right)=-\left({A}{\cdot }_{𝑒}{B}\right)$

### Proof

Step Hyp Ref Expression
1 xmulneg1 ${⊢}\left({B}\in {ℝ}^{*}\wedge {A}\in {ℝ}^{*}\right)\to \left(-{B}\right){\cdot }_{𝑒}{A}=-\left({B}{\cdot }_{𝑒}{A}\right)$
2 1 ancoms ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(-{B}\right){\cdot }_{𝑒}{A}=-\left({B}{\cdot }_{𝑒}{A}\right)$
3 xnegcl ${⊢}{B}\in {ℝ}^{*}\to -{B}\in {ℝ}^{*}$
4 xmulcom ${⊢}\left({A}\in {ℝ}^{*}\wedge -{B}\in {ℝ}^{*}\right)\to {A}{\cdot }_{𝑒}\left(-{B}\right)=\left(-{B}\right){\cdot }_{𝑒}{A}$
5 3 4 sylan2 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to {A}{\cdot }_{𝑒}\left(-{B}\right)=\left(-{B}\right){\cdot }_{𝑒}{A}$
6 xmulcom ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to {A}{\cdot }_{𝑒}{B}={B}{\cdot }_{𝑒}{A}$
7 xnegeq ${⊢}{A}{\cdot }_{𝑒}{B}={B}{\cdot }_{𝑒}{A}\to -\left({A}{\cdot }_{𝑒}{B}\right)=-\left({B}{\cdot }_{𝑒}{A}\right)$
8 6 7 syl ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to -\left({A}{\cdot }_{𝑒}{B}\right)=-\left({B}{\cdot }_{𝑒}{A}\right)$
9 2 5 8 3eqtr4d ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to {A}{\cdot }_{𝑒}\left(-{B}\right)=-\left({A}{\cdot }_{𝑒}{B}\right)$