Metamath Proof Explorer

Theorem xneg0

Description: The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xneg0 
|- -e 0 = 0

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 rexneg 
 |-  ( 0 e. RR -> -e 0 = -u 0 )
3 1 2 ax-mp 
 |-  -e 0 = -u 0
4 neg0 
 |-  -u 0 = 0
5 3 4 eqtri 
 |-  -e 0 = 0