Theorem mulneg2

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

	Ref	Expression
Assertion	mulneg2	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A\left(-B\right)=-AB$$

Proof

Step	Hyp	Ref	Expression
1		mulneg1	$$⊢\left(B\in ℂ\wedge A\in ℂ\right)\to \left(-B\right)A=-BA$$
2	1	ancoms	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(-B\right)A=-BA$$
3		negcl	$$⊢B\in ℂ\to -B\in ℂ$$
4		mulcom	$$⊢\left(A\in ℂ\wedge -B\in ℂ\right)\to A\left(-B\right)=\left(-B\right)A$$
5	3 4	sylan2	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A\left(-B\right)=\left(-B\right)A$$
6		mulcom	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to AB=BA$$
7	6	negeqd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to -AB=-BA$$
8	2 5 7	3eqtr4d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A\left(-B\right)=-AB$$