Theorem negid

Description: Addition of a number and its negative. (Contributed by NM, 14-Mar-2005)

	Ref	Expression
Assertion	negid	$$⊢A\in ℂ\to A+\left(-A\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		df-neg	$$⊢-A=0-A$$
2	1	oveq2i	$$⊢A+\left(-A\right)=A+0-A$$
3		0cn	$$⊢0\in ℂ$$
4		pncan3	$$⊢\left(A\in ℂ\wedge 0\in ℂ\right)\to A+0-A=0$$
5	3 4	mpan2	$$⊢A\in ℂ\to A+0-A=0$$
6	2 5	eqtrid	$$⊢A\in ℂ\to A+\left(-A\right)=0$$