Theorem risefaccllem

Description: Lemma for rising factorial closure laws. (Contributed by Scott Fenton, 5-Jan-2018)

	Ref	Expression
Hypotheses	risefallfaccllem.1	$$⊢S\subseteq ℂ$$
	risefallfaccllem.2	$$⊢1\in S$$
	risefallfaccllem.3	$$⊢\left(x\in S\wedge y\in S\right)\to xy\in S$$
	risefaccllem.4	$$⊢\left(A\in S\wedge k\in {\mathbb{N}}_0\right)\to A+k\in S$$
Assertion	risefaccllem	$$⊢\left(A\in S\wedge N\in {\mathbb{N}}_0\right)\to A^{\bar{N}}\in S$$

Proof

Step	Hyp	Ref	Expression
1		risefallfaccllem.1	$$⊢S\subseteq ℂ$$
2		risefallfaccllem.2	$$⊢1\in S$$
3		risefallfaccllem.3	$$⊢\left(x\in S\wedge y\in S\right)\to xy\in S$$
4		risefaccllem.4	$$⊢\left(A\in S\wedge k\in {\mathbb{N}}_0\right)\to A+k\in S$$
5	1	sseli	$$⊢A\in S\to A\in ℂ$$
6		risefacval	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to A^{\bar{N}}=\prod _{k=0}^{N-1}\left(A+k\right)$$
7	5 6	sylan	$$⊢\left(A\in S\wedge N\in {\mathbb{N}}_0\right)\to A^{\bar{N}}=\prod _{k=0}^{N-1}\left(A+k\right)$$
8	1	a1i	$$⊢A\in S\to S\subseteq ℂ$$
9	3	adantl	$$⊢\left(A\in S\wedge \left(x\in S\wedge y\in S\right)\right)\to xy\in S$$
10		fzfid	$$⊢A\in S\to \left(0\dots N-1\right)\in \mathrm{Fin}$$
11		elfznn0	$$⊢k\in \left(0\dots N-1\right)\to k\in {\mathbb{N}}_0$$
12	11 4	sylan2	$$⊢\left(A\in S\wedge k\in \left(0\dots N-1\right)\right)\to A+k\in S$$
13	2	a1i	$$⊢A\in S\to 1\in S$$
14	8 9 10 12 13	fprodcllem	$$⊢A\in S\to \prod _{k=0}^{N-1}\left(A+k\right)\in S$$
15	14	adantr	$$⊢\left(A\in S\wedge N\in {\mathbb{N}}_0\right)\to \prod _{k=0}^{N-1}\left(A+k\right)\in S$$
16	7 15	eqeltrd	$$⊢\left(A\in S\wedge N\in {\mathbb{N}}_0\right)\to A^{\bar{N}}\in S$$