This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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+