Metamath Proof Explorer


Theorem ene0

Description: _e is not 0. (Contributed by David A. Wheeler, 17-Oct-2017)

Ref Expression
Assertion ene0
|- _e =/= 0

Proof

Step Hyp Ref Expression
1 ere
 |-  _e e. RR
2 epos
 |-  0 < _e
3 1 2 gt0ne0ii
 |-  _e =/= 0