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

Proof

Step Hyp Ref Expression
1 reefcl AeA
2 efgt0 A0<eA
3 1 2 elrpd AeA+