Metamath Proof Explorer


Theorem epos

Description: Euler's constant _e is greater than 0. (Contributed by Jeff Hankins, 22-Nov-2008)

Ref Expression
Assertion epos
|- 0 < _e

Proof

Step Hyp Ref Expression
1 2pos
 |-  0 < 2
2 egt2lt3
 |-  ( 2 < _e /\ _e < 3 )
3 2 simpli
 |-  2 < _e
4 0re
 |-  0 e. RR
5 2re
 |-  2 e. RR
6 ere
 |-  _e e. RR
7 4 5 6 lttri
 |-  ( ( 0 < 2 /\ 2 < _e ) -> 0 < _e )
8 1 3 7 mp2an
 |-  0 < _e