This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xmulneg2

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

Ref Expression
Assertion xmulneg2 ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ·e -𝑒 𝐵 ) = -𝑒 ( 𝐴 ·e 𝐵 ) )

Proof

Step Hyp Ref Expression
1 xmulneg1 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( -𝑒 𝐵 ·e 𝐴 ) = -𝑒 ( 𝐵 ·e 𝐴 ) )
2 1 ancoms ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( -𝑒 𝐵 ·e 𝐴 ) = -𝑒 ( 𝐵 ·e 𝐴 ) )
3 xnegcl ⊢ ( 𝐵 ∈ ℝ* → -𝑒 𝐵 ∈ ℝ* )
4 xmulcom ⊢ ( ( 𝐴 ∈ ℝ* ∧ -𝑒 𝐵 ∈ ℝ* ) → ( 𝐴 ·e -𝑒 𝐵 ) = ( -𝑒 𝐵 ·e 𝐴 ) )
5 3 4 sylan2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ·e -𝑒 𝐵 ) = ( -𝑒 𝐵 ·e 𝐴 ) )
6 xmulcom ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ·e 𝐵 ) = ( 𝐵 ·e 𝐴 ) )
7 xnegeq ⊢ ( ( 𝐴 ·e 𝐵 ) = ( 𝐵 ·e 𝐴 ) → -𝑒 ( 𝐴 ·e 𝐵 ) = -𝑒 ( 𝐵 ·e 𝐴 ) )
8 6 7 syl ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → -𝑒 ( 𝐴 ·e 𝐵 ) = -𝑒 ( 𝐵 ·e 𝐴 ) )
9 2 5 8 3eqtr4d ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ·e -𝑒 𝐵 ) = -𝑒 ( 𝐴 ·e 𝐵 ) )