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 {\mathbb{N}}_0\right)\to A^{\bar{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 xy\in {ℝ}^{+}$$
6		rpre	$$⊢A\in {ℝ}^{+}\to A\in ℝ$$
7		nn0re	$$⊢k\in {\mathbb{N}}_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 {\mathbb{N}}_0\right)\to A+k\in ℝ$$
10	6	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge k\in {\mathbb{N}}_0\right)\to A\in ℝ$$
11	7	adantl	$$⊢\left(A\in {ℝ}^{+}\wedge k\in {\mathbb{N}}_0\right)\to k\in ℝ$$
12		rpgt0	$$⊢A\in {ℝ}^{+}\to 0<A$$
13	12	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge k\in {\mathbb{N}}_0\right)\to 0<A$$
14		nn0ge0	$$⊢k\in {\mathbb{N}}_0\to 0\le k$$
15	14	adantl	$$⊢\left(A\in {ℝ}^{+}\wedge k\in {\mathbb{N}}_0\right)\to 0\le k$$
16	10 11 13 15	addgtge0d	$$⊢\left(A\in {ℝ}^{+}\wedge k\in {\mathbb{N}}_0\right)\to 0<A+k$$
17	9 16	elrpd	$$⊢\left(A\in {ℝ}^{+}\wedge k\in {\mathbb{N}}_0\right)\to A+k\in {ℝ}^{+}$$
18	3 4 5 17	risefaccllem	$$⊢\left(A\in {ℝ}^{+}\wedge N\in {\mathbb{N}}_0\right)\to A^{\bar{N}}\in {ℝ}^{+}$$