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