Theorem binomfallfaclem1

Description: Lemma for binomfallfac . Closure law. (Contributed by Scott Fenton, 13-Mar-2018)

	Ref	Expression
Hypotheses	binomfallfaclem.1	|- ( ph -> A e. CC )
	binomfallfaclem.2	|- ( ph -> B e. CC )
	binomfallfaclem.3	|- ( ph -> N e. NN0 )
Assertion	binomfallfaclem1	|- ( ( ph /\ K e. ( 0 ... N ) ) -> ( ( N _C K ) x. ( ( A FallFac ( N - K ) ) x. ( B FallFac ( K + 1 ) ) ) ) e. CC )

Proof

Step	Hyp	Ref	Expression
1		binomfallfaclem.1	|- ( ph -> A e. CC )
2		binomfallfaclem.2	|- ( ph -> B e. CC )
3		binomfallfaclem.3	|- ( ph -> N e. NN0 )
4		elfzelz	|- ( K e. ( 0 ... N ) -> K e. ZZ )
5		bccl	|- ( ( N e. NN0 /\ K e. ZZ ) -> ( N _C K ) e. NN0 )
6	3 4 5	syl2an	|- ( ( ph /\ K e. ( 0 ... N ) ) -> ( N _C K ) e. NN0 )
7	6	nn0cnd	|- ( ( ph /\ K e. ( 0 ... N ) ) -> ( N _C K ) e. CC )
8		fznn0sub	|- ( K e. ( 0 ... N ) -> ( N - K ) e. NN0 )
9		fallfaccl	|- ( ( A e. CC /\ ( N - K ) e. NN0 ) -> ( A FallFac ( N - K ) ) e. CC )
10	1 8 9	syl2an	|- ( ( ph /\ K e. ( 0 ... N ) ) -> ( A FallFac ( N - K ) ) e. CC )
11		elfznn0	|- ( K e. ( 0 ... N ) -> K e. NN0 )
12		peano2nn0	|- ( K e. NN0 -> ( K + 1 ) e. NN0 )
13	11 12	syl	|- ( K e. ( 0 ... N ) -> ( K + 1 ) e. NN0 )
14		fallfaccl	|- ( ( B e. CC /\ ( K + 1 ) e. NN0 ) -> ( B FallFac ( K + 1 ) ) e. CC )
15	2 13 14	syl2an	|- ( ( ph /\ K e. ( 0 ... N ) ) -> ( B FallFac ( K + 1 ) ) e. CC )
16	10 15	mulcld	|- ( ( ph /\ K e. ( 0 ... N ) ) -> ( ( A FallFac ( N - K ) ) x. ( B FallFac ( K + 1 ) ) ) e. CC )
17	7 16	mulcld	|- ( ( ph /\ K e. ( 0 ... N ) ) -> ( ( N _C K ) x. ( ( A FallFac ( N - K ) ) x. ( B FallFac ( K + 1 ) ) ) ) e. CC )