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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 𝐴 · 𝐵 ) = - ( 𝐴 · 𝐵 ) )

Proof

Step Hyp Ref Expression
1 0cn ⊢ 0 ∈ ℂ
2 subdir ⊢ ( ( 0 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 0 − 𝐴 ) · 𝐵 ) = ( ( 0 · 𝐵 ) − ( 𝐴 · 𝐵 ) ) )
3 1 2 mp3an1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 0 − 𝐴 ) · 𝐵 ) = ( ( 0 · 𝐵 ) − ( 𝐴 · 𝐵 ) ) )
4 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
5 4 mul02d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 0 · 𝐵 ) = 0 )
6 5 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 0 · 𝐵 ) − ( 𝐴 · 𝐵 ) ) = ( 0 − ( 𝐴 · 𝐵 ) ) )
7 3 6 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 0 − 𝐴 ) · 𝐵 ) = ( 0 − ( 𝐴 · 𝐵 ) ) )
8 df-neg ⊢ - 𝐴 = ( 0 − 𝐴 )
9 8 oveq1i ⊢ ( - 𝐴 · 𝐵 ) = ( ( 0 − 𝐴 ) · 𝐵 )
10 df-neg ⊢ - ( 𝐴 · 𝐵 ) = ( 0 − ( 𝐴 · 𝐵 ) )
11 7 9 10 3eqtr4g ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 𝐴 · 𝐵 ) = - ( 𝐴 · 𝐵 ) )