Theorem nnrisefaccl

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

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

Proof

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