Theorem fallfaccllem

Description: Lemma for falling 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$$
	fallfaccllem.4	$$⊢\left(A\in S\wedge k\in {\mathbb{N}}_0\right)\to A-k\in S$$
Assertion	fallfaccllem	$$⊢\left(A\in S\wedge N\in {\mathbb{N}}_0\right)\to A^{\underset{\_}{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		fallfaccllem.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		fallfacval	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to A^{\underset{\_}{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^{\underset{\_}{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^{\underset{\_}{N}}\in S$$