Metamath Proof Explorer

Theorem rpefcl

Description: The exponential of a real number is a positive real. (Contributed by Mario Carneiro, 10-Nov-2013)

Ref Expression
Assertion rpefcl 
|- ( A e. RR -> ( exp ` A ) e. RR+ )

Proof

Step Hyp Ref Expression
1 reefcl 
 |-  ( A e. RR -> ( exp ` A ) e. RR )
2 efgt0 
 |-  ( A e. RR -> 0 < ( exp ` A ) )
3 1 2 elrpd 
 |-  ( A e. RR -> ( exp ` A ) e. RR+ )