Theorem fallfaccllem

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

	Ref	Expression
Hypotheses	risefallfaccllem.1	|- S C_ CC
	risefallfaccllem.2	|- 1 e. S
	risefallfaccllem.3	|- ( ( x e. S /\ y e. S ) -> ( x x. y ) e. S )
	fallfaccllem.4	|- ( ( A e. S /\ k e. NN0 ) -> ( A - k ) e. S )
Assertion	fallfaccllem	|- ( ( A e. S /\ N e. NN0 ) -> ( A FallFac N ) e. S )

Proof

Step	Hyp	Ref	Expression
1		risefallfaccllem.1	|- S C_ CC
2		risefallfaccllem.2	|- 1 e. S
3		risefallfaccllem.3	|- ( ( x e. S /\ y e. S ) -> ( x x. y ) e. S )
4		fallfaccllem.4	|- ( ( A e. S /\ k e. NN0 ) -> ( A - k ) e. S )
5	1	sseli	|- ( A e. S -> A e. CC )
6		fallfacval	|- ( ( A e. CC /\ N e. NN0 ) -> ( A FallFac N ) = prod_ k e. ( 0 ... ( N - 1 ) ) ( A - k ) )
7	5 6	sylan	|- ( ( A e. S /\ N e. NN0 ) -> ( A FallFac N ) = prod_ k e. ( 0 ... ( N - 1 ) ) ( A - k ) )
8	1	a1i	|- ( A e. S -> S C_ CC )
9	3	adantl	|- ( ( A e. S /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
10		fzfid	|- ( A e. S -> ( 0 ... ( N - 1 ) ) e. Fin )
11		elfznn0	|- ( k e. ( 0 ... ( N - 1 ) ) -> k e. NN0 )
12	11 4	sylan2	|- ( ( A e. S /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( A - k ) e. S )
13	2	a1i	|- ( A e. S -> 1 e. S )
14	8 9 10 12 13	fprodcllem	|- ( A e. S -> prod_ k e. ( 0 ... ( N - 1 ) ) ( A - k ) e. S )
15	14	adantr	|- ( ( A e. S /\ N e. NN0 ) -> prod_ k e. ( 0 ... ( N - 1 ) ) ( A - k ) e. S )
16	7 15	eqeltrd	|- ( ( A e. S /\ N e. NN0 ) -> ( A FallFac N ) e. S )