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 ∈ ℝ
2 epos 0 < e
3 1 2 gt0ne0ii e ≠ 0