Theorem mulneg2

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

	Ref	Expression
Assertion	mulneg2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · - 𝐵 ) = - ( 𝐴 · 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		mulneg1	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - 𝐵 · 𝐴 ) = - ( 𝐵 · 𝐴 ) )
2	1	ancoms	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 𝐵 · 𝐴 ) = - ( 𝐵 · 𝐴 ) )
3		negcl	⊢ ( 𝐵 ∈ ℂ → - 𝐵 ∈ ℂ )
4		mulcom	⊢ ( ( 𝐴 ∈ ℂ ∧ - 𝐵 ∈ ℂ ) → ( 𝐴 · - 𝐵 ) = ( - 𝐵 · 𝐴 ) )
5	3 4	sylan2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · - 𝐵 ) = ( - 𝐵 · 𝐴 ) )
6		mulcom	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
7	6	negeqd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → - ( 𝐴 · 𝐵 ) = - ( 𝐵 · 𝐴 ) )
8	2 5 7	3eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · - 𝐵 ) = - ( 𝐴 · 𝐵 ) )