Metamath Proof Explorer


Theorem xneg0

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

Ref Expression
Assertion xneg0 -𝑒 0 = 0

Proof

Step Hyp Ref Expression
1 0re 0 ∈ ℝ
2 rexneg ( 0 ∈ ℝ → -𝑒 0 = - 0 )
3 1 2 ax-mp -𝑒 0 = - 0
4 neg0 - 0 = 0
5 3 4 eqtri -𝑒 0 = 0