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 A = A A = 0

Proof

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