Theorem reexpcl

Description: Closure of exponentiation of reals. For integer exponents, see reexpclz . (Contributed by NM, 14-Dec-2005)

	Ref	Expression
Assertion	reexpcl	$$⊢\left(A\in ℝ\wedge N\in {\mathbb{N}}_0\right)\to A^N\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		ax-resscn	$$⊢ℝ\subseteq ℂ$$
2		remulcl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to xy\in ℝ$$
3		1re	$$⊢1\in ℝ$$
4	1 2 3	expcllem	$$⊢\left(A\in ℝ\wedge N\in {\mathbb{N}}_0\right)\to A^N\in ℝ$$