Theorem negcl

Description: Closure law for negative. (Contributed by NM, 6-Aug-2003)

	Ref	Expression
Assertion	negcl	$$⊢A\in ℂ\to -A\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		df-neg	$$⊢-A=0-A$$
2		0cn	$$⊢0\in ℂ$$
3		subcl	$$⊢\left(0\in ℂ\wedge A\in ℂ\right)\to 0-A\in ℂ$$
4	2 3	mpan	$$⊢A\in ℂ\to 0-A\in ℂ$$
5	1 4	eqeltrid	$$⊢A\in ℂ\to -A\in ℂ$$