Theorem rerisefaccl

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

	Ref	Expression
Assertion	rerisefaccl	$$⊢\left(A\in ℝ\wedge N\in {\mathbb{N}}_0\right)\to A^{\bar{N}}\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		ax-resscn	$$⊢ℝ\subseteq ℂ$$
2		1re	$$⊢1\in ℝ$$
3		remulcl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to xy\in ℝ$$
4		nn0re	$$⊢k\in {\mathbb{N}}_0\to k\in ℝ$$
5		readdcl	$$⊢\left(A\in ℝ\wedge k\in ℝ\right)\to A+k\in ℝ$$
6	4 5	sylan2	$$⊢\left(A\in ℝ\wedge k\in {\mathbb{N}}_0\right)\to A+k\in ℝ$$
7	1 2 3 6	risefaccllem	$$⊢\left(A\in ℝ\wedge N\in {\mathbb{N}}_0\right)\to A^{\bar{N}}\in ℝ$$