Theorem eqneg

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

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

Proof

Step	Hyp	Ref	Expression
1		1p1times	$$⊢A\in ℂ\to \left(1+1\right)A=A+A$$
2		ax-1cn	$$⊢1\in ℂ$$
3	2 2	addcli	$$⊢1+1\in ℂ$$
4	3	mul01i	$$⊢\left(1+1\right)\cdot 0=0$$
5		negid	$$⊢A\in ℂ\to A+\left(-A\right)=0$$
6	4 5	eqtr4id	$$⊢A\in ℂ\to \left(1+1\right)\cdot 0=A+\left(-A\right)$$
7	1 6	eqeq12d	$$⊢A\in ℂ\to \left(\left(1+1\right)A=\left(1+1\right)\cdot 0\leftrightarrow A+A=A+\left(-A\right)\right)$$
8		id	$$⊢A\in ℂ\to A\in ℂ$$
9		0cnd	$$⊢A\in ℂ\to 0\in ℂ$$
10	3	a1i	$$⊢A\in ℂ\to 1+1\in ℂ$$
11		1re	$$⊢1\in ℝ$$
12	11 11	readdcli	$$⊢1+1\in ℝ$$
13		0lt1	$$⊢0<1$$
14	11 11 13 13	addgt0ii	$$⊢0<1+1$$
15	12 14	gt0ne0ii	$$⊢1+1\ne 0$$
16	15	a1i	$$⊢A\in ℂ\to 1+1\ne 0$$
17	8 9 10 16	mulcand	$$⊢A\in ℂ\to \left(\left(1+1\right)A=\left(1+1\right)\cdot 0\leftrightarrow A=0\right)$$
18		negcl	$$⊢A\in ℂ\to -A\in ℂ$$
19	8 8 18	addcand	$$⊢A\in ℂ\to \left(A+A=A+\left(-A\right)\leftrightarrow A=-A\right)$$
20	7 17 19	3bitr3rd	$$⊢A\in ℂ\to \left(A=-A\leftrightarrow A=0\right)$$