Description: The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | xneg0 | ⊢ -𝑒 0 = 0 |
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 |