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 e. CC -> ( A = -u A <-> A = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		1p1times	|- ( A e. CC -> ( ( 1 + 1 ) x. A ) = ( A + A ) )
2		ax-1cn	|- 1 e. CC
3	2 2	addcli	|- ( 1 + 1 ) e. CC
4	3	mul01i	|- ( ( 1 + 1 ) x. 0 ) = 0
5		negid	|- ( A e. CC -> ( A + -u A ) = 0 )
6	4 5	eqtr4id	|- ( A e. CC -> ( ( 1 + 1 ) x. 0 ) = ( A + -u A ) )
7	1 6	eqeq12d	|- ( A e. CC -> ( ( ( 1 + 1 ) x. A ) = ( ( 1 + 1 ) x. 0 ) <-> ( A + A ) = ( A + -u A ) ) )
8		id	|- ( A e. CC -> A e. CC )
9		0cnd	|- ( A e. CC -> 0 e. CC )
10	3	a1i	|- ( A e. CC -> ( 1 + 1 ) e. CC )
11		1re	|- 1 e. RR
12	11 11	readdcli	|- ( 1 + 1 ) e. RR
13		0lt1	|- 0 < 1
14	11 11 13 13	addgt0ii	|- 0 < ( 1 + 1 )
15	12 14	gt0ne0ii	|- ( 1 + 1 ) =/= 0
16	15	a1i	|- ( A e. CC -> ( 1 + 1 ) =/= 0 )
17	8 9 10 16	mulcand	|- ( A e. CC -> ( ( ( 1 + 1 ) x. A ) = ( ( 1 + 1 ) x. 0 ) <-> A = 0 ) )
18		negcl	|- ( A e. CC -> -u A e. CC )
19	8 8 18	addcand	|- ( A e. CC -> ( ( A + A ) = ( A + -u A ) <-> A = -u A ) )
20	7 17 19	3bitr3rd	|- ( A e. CC -> ( A = -u A <-> A = 0 ) )