Description: Euler's constant _e is greater than 0. (Contributed by Jeff Hankins, 22-Nov-2008)
Ref | Expression | ||
---|---|---|---|
Assertion | epos | |- 0 < _e |
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 |