Metamath Proof Explorer

Theorem xmulneg2

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

Ref Expression
Assertion xmulneg2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ⋅ 𝑒 − B = − A ⋅ 𝑒 B

Proof

Step Hyp Ref Expression
1 xmulneg1 ⊢ B ∈ ℝ * ∧ A ∈ ℝ * → − B ⋅ 𝑒 A = − B ⋅ 𝑒 A
2 1 ancoms ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → − B ⋅ 𝑒 A = − B ⋅ 𝑒 A
3 xnegcl ⊢ B ∈ ℝ * → − B ∈ ℝ *
4 xmulcom ⊢ A ∈ ℝ * ∧ − B ∈ ℝ * → A ⋅ 𝑒 − B = − B ⋅ 𝑒 A
5 3 4 sylan2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ⋅ 𝑒 − B = − B ⋅ 𝑒 A
6 xmulcom ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ⋅ 𝑒 B = B ⋅ 𝑒 A
7 xnegeq ⊢ A ⋅ 𝑒 B = B ⋅ 𝑒 A → − A ⋅ 𝑒 B = − B ⋅ 𝑒 A
8 6 7 syl ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → − A ⋅ 𝑒 B = − B ⋅ 𝑒 A
9 2 5 8 3eqtr4d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ⋅ 𝑒 − B = − A ⋅ 𝑒 B