Metamath Proof Explorer


Theorem epr

Description: Euler's constant _e is a positive real. (Contributed by Jeff Hankins, 22-Nov-2008)

Ref Expression
Assertion epr
|- _e e. RR+

Proof

Step Hyp Ref Expression
1 ere
 |-  _e e. RR
2 epos
 |-  0 < _e
3 1 2 elrpii
 |-  _e e. RR+