Theorem rpexpcl

Description: Closure law for integer exponentiation of positive reals. (Contributed by NM, 24-Feb-2008) (Revised by Mario Carneiro, 9-Sep-2014)

	Ref	Expression
Assertion	rpexpcl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℝ+ )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → 𝐴 ∈ ℝ+ )
2		rpne0	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ≠ 0 )
3	2	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → 𝐴 ≠ 0 )
4		simpr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
5		rpssre	⊢ ℝ+ ⊆ ℝ
6		ax-resscn	⊢ ℝ ⊆ ℂ
7	5 6	sstri	⊢ ℝ+ ⊆ ℂ
8		rpmulcl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) → ( 𝑥 · 𝑦 ) ∈ ℝ+ )
9		1rp	⊢ 1 ∈ ℝ+
10		rpreccl	⊢ ( 𝑥 ∈ ℝ+ → ( 1 / 𝑥 ) ∈ ℝ+ )
11	10	adantr	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑥 ≠ 0 ) → ( 1 / 𝑥 ) ∈ ℝ+ )
12	7 8 9 11	expcl2lem	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℝ+ )
13	1 3 4 12	syl3anc	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℝ+ )