Theorem reexpcl

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

	Ref	Expression
Assertion	reexpcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		ax-resscn	⊢ ℝ ⊆ ℂ
2		remulcl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
3		1re	⊢ 1 ∈ ℝ
4	1 2 3	expcllem	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℝ )