Theorem reexpclzd

Description: Closure of exponentiation of reals. (Contributed by Mario Carneiro, 28-May-2016)

	Ref	Expression
Hypotheses	rpexpclzd.1	$$⊢\phi \to A\in ℝ$$
	rpexpclzd.2	$$⊢\phi \to A\ne 0$$
	rpexpclzd.3	$$⊢\phi \to N\in \mathbb{Z}$$
Assertion	reexpclzd	$$⊢\phi \to A^N\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		rpexpclzd.1	$$⊢\phi \to A\in ℝ$$
2		rpexpclzd.2	$$⊢\phi \to A\ne 0$$
3		rpexpclzd.3	$$⊢\phi \to N\in \mathbb{Z}$$
4		reexpclz	$$⊢\left(A\in ℝ\wedge A\ne 0\wedge N\in \mathbb{Z}\right)\to A^N\in ℝ$$
5	1 2 3 4	syl3anc	$$⊢\phi \to A^N\in ℝ$$