Theorem risefaccl

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

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

Proof

Step	Hyp	Ref	Expression
1		ssid	$$⊢ℂ\subseteq ℂ$$
2		ax-1cn	$$⊢1\in ℂ$$
3		mulcl	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to xy\in ℂ$$
4		nn0cn	$$⊢k\in {\mathbb{N}}_0\to k\in ℂ$$
5		addcl	$$⊢\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 ℂ$$