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

Metamath Proof Explorer

Theorem mulneg12

Description: Swap the negative sign in a product. (Contributed by NM, 30-Jul-2004)

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

Proof

Step Hyp Ref Expression
1 mulneg1 ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A ⁢ B = − A ⁢ B
2 mulneg2 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ − B = − A ⁢ B
3 1 2 eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A ⁢ B = A ⁢ − B