Theorem rprisefaccl

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

	Ref	Expression
Assertion	rprisefaccl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 RiseFac 𝑁 ) ∈ ℝ+ )

Proof

Step	Hyp	Ref	Expression
1		rpssre	⊢ ℝ+ ⊆ ℝ
2		ax-resscn	⊢ ℝ ⊆ ℂ
3	1 2	sstri	⊢ ℝ+ ⊆ ℂ
4		1rp	⊢ 1 ∈ ℝ+
5		rpmulcl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) → ( 𝑥 · 𝑦 ) ∈ ℝ+ )
6		rpre	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ )
7		nn0re	⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ )
8		readdcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝐴 + 𝑘 ) ∈ ℝ )
9	6 7 8	syl2an	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 + 𝑘 ) ∈ ℝ )
10	6	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ ℝ )
11	7	adantl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℝ )
12		rpgt0	⊢ ( 𝐴 ∈ ℝ+ → 0 < 𝐴 )
13	12	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑘 ∈ ℕ0 ) → 0 < 𝐴 )
14		nn0ge0	⊢ ( 𝑘 ∈ ℕ0 → 0 ≤ 𝑘 )
15	14	adantl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑘 ∈ ℕ0 ) → 0 ≤ 𝑘 )
16	10 11 13 15	addgtge0d	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑘 ∈ ℕ0 ) → 0 < ( 𝐴 + 𝑘 ) )
17	9 16	elrpd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 + 𝑘 ) ∈ ℝ+ )
18	3 4 5 17	risefaccllem	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 RiseFac 𝑁 ) ∈ ℝ+ )