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 A +

Proof

Step Hyp Ref Expression
1 reefcl A e A
2 efgt0 A 0 < e A
3 1 2 elrpd A e A +