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	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(-A\right)B=-AB$$

Proof

Step	Hyp	Ref	Expression
1		0cn	$$⊢0\in ℂ$$
2		subdir	$$⊢\left(0\in ℂ\wedge A\in ℂ\wedge B\in ℂ\right)\to \left(0-A\right)B=0\cdot B-AB$$
3	1 2	mp3an1	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(0-A\right)B=0\cdot B-AB$$
4		simpr	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to B\in ℂ$$
5	4	mul02d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 0\cdot B=0$$
6	5	oveq1d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 0\cdot B-AB=0-AB$$
7	3 6	eqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(0-A\right)B=0-AB$$
8		df-neg	$$⊢-A=0-A$$
9	8	oveq1i	$$⊢\left(-A\right)B=\left(0-A\right)B$$
10		df-neg	$$⊢-AB=0-AB$$
11	7 9 10	3eqtr4g	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(-A\right)B=-AB$$