# Metamath Proof Explorer

## Theorem rprisefaccl

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

Ref Expression
Assertion rprisefaccl ${⊢}\left({A}\in {ℝ}^{+}\wedge {N}\in {ℕ}_{0}\right)\to {{A}}^{\stackrel{‾}{{N}}}\in {ℝ}^{+}$

### Proof

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