Theorem nn0risefaccl

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

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

Proof

Step	Hyp	Ref	Expression
1		nn0sscn	$$⊢{\mathbb{N}}_0\subseteq ℂ$$
2		1nn0	$$⊢1\in {\mathbb{N}}_0$$
3		nn0mulcl	$$⊢\left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\to xy\in {\mathbb{N}}_0$$
4		nn0addcl	$$⊢\left(A\in {\mathbb{N}}_0\wedge k\in {\mathbb{N}}_0\right)\to A+k\in {\mathbb{N}}_0$$
5	1 2 3 4	risefaccllem	$$⊢\left(A\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to A^{\bar{N}}\in {\mathbb{N}}_0$$