This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )