This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )