Theorem mul2neg

Description: Product of two negatives. Theorem I.12 of Apostol p. 18. (Contributed by NM, 30-Jul-2004) (Proof shortened by Andrew Salmon, 19-Nov-2011)

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

Proof

Step	Hyp	Ref	Expression
1		negcl	$$⊢B\in ℂ\to -B\in ℂ$$
2		mulneg12	$$⊢\left(A\in ℂ\wedge -B\in ℂ\right)\to \left(-A\right)\left(-B\right)=A\left(-\left(-B\right)\right)$$
3	1 2	sylan2	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(-A\right)\left(-B\right)=A\left(-\left(-B\right)\right)$$
4		negneg	$$⊢B\in ℂ\to -\left(-B\right)=B$$
5	4	adantl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to -\left(-B\right)=B$$
6	5	oveq2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A\left(-\left(-B\right)\right)=AB$$
7	3 6	eqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(-A\right)\left(-B\right)=AB$$