This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in ℝ \to e^{A} \in ℝ^{+}$

Step	Hyp	Ref	Expression
1		reefcl	$⊢ A \in ℝ \to e^{A} \in ℝ$
2		efgt0	$⊢ A \in ℝ \to 0 < e^{A}$
3	1 2	elrpd	$⊢ A \in ℝ \to e^{A} \in ℝ^{+}$