Theorem rpefcld

Description: The exponential of a real number is a positive real. (Contributed by Mario Carneiro, 29-May-2016)

	Ref	Expression
Hypothesis	rpefcld.1	$$⊢\phi \to A\in ℝ$$
Assertion	rpefcld	$$⊢\phi \to {\mathrm{e}}^A\in {ℝ}^{+}$$

Proof

Step	Hyp	Ref	Expression
1		rpefcld.1	$$⊢\phi \to A\in ℝ$$
2		rpefcl	$$⊢A\in ℝ\to {\mathrm{e}}^A\in {ℝ}^{+}$$
3	1 2	syl	$$⊢\phi \to {\mathrm{e}}^A\in {ℝ}^{+}$$