Metamath Proof Explorer


Theorem negneg

Description: A number is equal to the negative of its negative. Theorem I.4 of Apostol p. 18. (Contributed by NM, 12-Jan-2002) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion negneg AA=A

Proof

Step Hyp Ref Expression
1 df-neg A=0A
2 0cn 0
3 subneg 0A0A=0+A
4 2 3 mpan A0A=0+A
5 1 4 eqtrid AA=0+A
6 addid2 A0+A=A
7 5 6 eqtrd AA=A