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	$⊢ (A \in ℝ^{+} \land N \in ℤ) \to A^{N} \in ℝ^{+}$

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

Metamath Proof Explorer