Theorem mulm1

Description: Product with minus one is negative. (Contributed by NM, 16-Nov-1999)

	Ref	Expression
Assertion	mulm1	$$⊢A\in ℂ\to -1A=-A$$

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	$$⊢1\in ℂ$$
2		mulneg1	$$⊢\left(1\in ℂ\wedge A\in ℂ\right)\to -1A=-1A$$
3	1 2	mpan	$$⊢A\in ℂ\to -1A=-1A$$
4		mulid2	$$⊢A\in ℂ\to 1A=A$$
5	4	negeqd	$$⊢A\in ℂ\to -1A=-A$$
6	3 5	eqtrd	$$⊢A\in ℂ\to -1A=-A$$