rprisefaccl

Description: Closure law for rising factorial. (Contributed by Scott Fenton, 9-Jan-2018)

		Ref	Expression
	Assertion	rprisefaccl	$⊢ (A \in ℝ^{+} \land N \in ℕ_{0}) \to A^{\overline{N}} \in ℝ^{+}$

Step	Hyp	Ref	Expression
1		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
2		ax-resscn	$⊢ ℝ \subseteq ℂ$
3	1 2	sstri	$⊢ ℝ^{+} \subseteq ℂ$
4		1rp	$⊢ 1 \in ℝ^{+}$
5		rpmulcl	$⊢ (x \in ℝ^{+} \land y \in ℝ^{+}) \to x y \in ℝ^{+}$
6		rpre	$⊢ A \in ℝ^{+} \to A \in ℝ$
7		nn0re	$⊢ k \in ℕ_{0} \to k \in ℝ$
8		readdcl	$⊢ (A \in ℝ \land k \in ℝ) \to A + k \in ℝ$
9	6 7 8	syl2an	$⊢ (A \in ℝ^{+} \land k \in ℕ_{0}) \to A + k \in ℝ$
10	6	adantr	$⊢ (A \in ℝ^{+} \land k \in ℕ_{0}) \to A \in ℝ$
11	7	adantl	$⊢ (A \in ℝ^{+} \land k \in ℕ_{0}) \to k \in ℝ$
12		rpgt0	$⊢ A \in ℝ^{+} \to 0 < A$
13	12	adantr	$⊢ (A \in ℝ^{+} \land k \in ℕ_{0}) \to 0 < A$
14		nn0ge0	$⊢ k \in ℕ_{0} \to 0 \leq k$
15	14	adantl	$⊢ (A \in ℝ^{+} \land k \in ℕ_{0}) \to 0 \leq k$
16	10 11 13 15	addgtge0d	$⊢ (A \in ℝ^{+} \land k \in ℕ_{0}) \to 0 < A + k$
17	9 16	elrpd	$⊢ (A \in ℝ^{+} \land k \in ℕ_{0}) \to A + k \in ℝ^{+}$
18	3 4 5 17	risefaccllem	$⊢ (A \in ℝ^{+} \land N \in ℕ_{0}) \to A^{\overline{N}} \in ℝ^{+}$

Metamath Proof Explorer