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

Metamath Proof Explorer

Theorem mulneg1

Description: Product with negative is negative of product. Theorem I.12 of Apostol p. 18. (Contributed by NM, 14-May-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 0cn ⊢ 0 ∈ ℂ
2 subdir ⊢ 0 ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ ℂ → 0 − A ⁢ B = 0 ⋅ B − A ⁢ B
3 1 2 mp3an1 ⊢ A ∈ ℂ ∧ B ∈ ℂ → 0 − A ⁢ B = 0 ⋅ B − A ⁢ B
4 simpr ⊢ A ∈ ℂ ∧ B ∈ ℂ → B ∈ ℂ
5 4 mul02d ⊢ A ∈ ℂ ∧ B ∈ ℂ → 0 ⋅ B = 0
6 5 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ → 0 ⋅ B − A ⁢ B = 0 − A ⁢ B
7 3 6 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → 0 − A ⁢ B = 0 − A ⁢ B
8 df-neg ⊢ − A = 0 − A
9 8 oveq1i ⊢ − A ⁢ B = 0 − A ⁢ B
10 df-neg ⊢ − A ⁢ B = 0 − A ⁢ B
11 7 9 10 3eqtr4g ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A ⁢ B = − A ⁢ B