Theorem reexpclz

Description: Closure of exponentiation of reals. (Contributed by Mario Carneiro, 4-Jun-2014) (Revised by Mario Carneiro, 9-Sep-2014)

	Ref	Expression
Assertion	reexpclz	$$⊢\left(A\in ℝ\wedge A\ne 0\wedge N\in \mathbb{Z}\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		rereccl	$$⊢\left(x\in ℝ\wedge x\ne 0\right)\to \frac{1}{x}\in ℝ$$
5	1 2 3 4	expcl2lem	$$⊢\left(A\in ℝ\wedge A\ne 0\wedge N\in \mathbb{Z}\right)\to A^N\in ℝ$$