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	$$⊢\left(A\in {ℝ}^{+}\wedge N\in \mathbb{Z}\right)\to A^N\in {ℝ}^{+}$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(A\in {ℝ}^{+}\wedge N\in \mathbb{Z}\right)\to A\in {ℝ}^{+}$$
2		rpne0	$$⊢A\in {ℝ}^{+}\to A\ne 0$$
3	2	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge N\in \mathbb{Z}\right)\to A\ne 0$$
4		simpr	$$⊢\left(A\in {ℝ}^{+}\wedge N\in \mathbb{Z}\right)\to N\in \mathbb{Z}$$
5		rpssre	$$⊢{ℝ}^{+}\subseteq ℝ$$
6		ax-resscn	$$⊢ℝ\subseteq ℂ$$
7	5 6	sstri	$$⊢{ℝ}^{+}\subseteq ℂ$$
8		rpmulcl	$$⊢\left(x\in {ℝ}^{+}\wedge y\in {ℝ}^{+}\right)\to xy\in {ℝ}^{+}$$
9		1rp	$$⊢1\in {ℝ}^{+}$$
10		rpreccl	$$⊢x\in {ℝ}^{+}\to \frac{1}{x}\in {ℝ}^{+}$$
11	10	adantr	$$⊢\left(x\in {ℝ}^{+}\wedge x\ne 0\right)\to \frac{1}{x}\in {ℝ}^{+}$$
12	7 8 9 11	expcl2lem	$$⊢\left(A\in {ℝ}^{+}\wedge A\ne 0\wedge N\in \mathbb{Z}\right)\to A^N\in {ℝ}^{+}$$
13	1 3 4 12	syl3anc	$$⊢\left(A\in {ℝ}^{+}\wedge N\in \mathbb{Z}\right)\to A^N\in {ℝ}^{+}$$