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