Metamath Proof Explorer

Theorem ere

Description: Euler's constant _e = 2.71828... is a real number. (Contributed by NM, 19-Mar-2005) (Revised by Steve Rodriguez, 8-Mar-2006)

Ref Expression
Assertion ere 
|- _e e. RR

Proof

Step Hyp Ref Expression
1 df-e 
 |-  _e = ( exp ` 1 )
2 1re 
 |-  1 e. RR
3 reefcl 
 |-  ( 1 e. RR -> ( exp ` 1 ) e. RR )
4 2 3 ax-mp 
 |-  ( exp ` 1 ) e. RR
5 1 4 eqeltri 
 |-  _e e. RR