Database
REAL AND COMPLEX NUMBERS
Elementary trigonometry
_e is irrational
ene0
Next ⟩
ene1
Metamath Proof Explorer
Ascii
Structured
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