Metamath Proof Explorer

Theorem mulneg2

Description: The product with a negative is the negative of the product. (Contributed by NM, 30-Jul-2004)

Ref Expression
Assertion mulneg2 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ − B = − A ⁢ B

Proof

Step Hyp Ref Expression
1 mulneg1 ⊢ B ∈ ℂ ∧ A ∈ ℂ → − B ⁢ A = − B ⁢ A
2 1 ancoms ⊢ A ∈ ℂ ∧ B ∈ ℂ → − B ⁢ A = − B ⁢ A
3 negcl ⊢ B ∈ ℂ → − B ∈ ℂ
4 mulcom ⊢ A ∈ ℂ ∧ − B ∈ ℂ → A ⁢ − B = − B ⁢ A
5 3 4 sylan2 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ − B = − B ⁢ A
6 mulcom ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B = B ⁢ A
7 6 negeqd ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A ⁢ B = − B ⁢ A
8 2 5 7 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ − B = − A ⁢ B