This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑁 ) ∈ ℝ+ )