Theorem negeq0

Description: A number is zero iff its negative is zero. (Contributed by NM, 12-Jul-2005) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		0cn	$$⊢0\in ℂ$$
2		neg11	$$⊢\left(A\in ℂ\wedge 0\in ℂ\right)\to \left(-A=-0\leftrightarrow A=0\right)$$
3	1 2	mpan2	$$⊢A\in ℂ\to \left(-A=-0\leftrightarrow A=0\right)$$
4		neg0	$$⊢-0=0$$
5	4	eqeq2i	$$⊢-A=-0\leftrightarrow -A=0$$
6	3 5	bitr3di	$$⊢A\in ℂ\to \left(A=0\leftrightarrow -A=0\right)$$