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

Metamath Proof Explorer

Theorem binomfallfaclem2

Description: Lemma for binomfallfac . Inductive step. (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 )
binomfallfaclem.4 
|- ( ps -> ( ( A + B ) FallFac N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) )
Assertion binomfallfaclem2 
|- ( ( ph /\ ps ) -> ( ( A + B ) FallFac ( N + 1 ) ) = sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( N + 1 ) _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) )

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 binomfallfaclem.4 
 |-  ( ps -> ( ( A + B ) FallFac N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) )
5 elfzelz 
 |-  ( k e. ( 0 ... N ) -> k e. ZZ )
6 bccl 
 |-  ( ( N e. NN0 /\ k e. ZZ ) -> ( N _C k ) e. NN0 )
7 3 5 6 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( N _C k ) e. NN0 )
8 7 nn0cnd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( N _C k ) e. CC )
9 fznn0sub 
 |-  ( k e. ( 0 ... N ) -> ( N - k ) e. NN0 )
10 fallfaccl 
 |-  ( ( A e. CC /\ ( N - k ) e. NN0 ) -> ( A FallFac ( N - k ) ) e. CC )
11 1 9 10 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( A FallFac ( N - k ) ) e. CC )
12 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
13 fallfaccl 
 |-  ( ( B e. CC /\ k e. NN0 ) -> ( B FallFac k ) e. CC )
14 2 12 13 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( B FallFac k ) e. CC )
15 11 14 mulcld 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) e. CC )
16 1 2 addcld 
 |-  ( ph -> ( A + B ) e. CC )
17 3 nn0cnd 
 |-  ( ph -> N e. CC )
18 16 17 subcld 
 |-  ( ph -> ( ( A + B ) - N ) e. CC )
19 18 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( A + B ) - N ) e. CC )
20 8 15 19 mulassd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) x. ( ( A + B ) - N ) ) = ( ( N _C k ) x. ( ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) x. ( ( A + B ) - N ) ) ) )
21 9 nn0cnd 
 |-  ( k e. ( 0 ... N ) -> ( N - k ) e. CC )
22 subcl 
 |-  ( ( A e. CC /\ ( N - k ) e. CC ) -> ( A - ( N - k ) ) e. CC )
23 1 21 22 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( A - ( N - k ) ) e. CC )
24 12 nn0cnd 
 |-  ( k e. ( 0 ... N ) -> k e. CC )
25 subcl 
 |-  ( ( B e. CC /\ k e. CC ) -> ( B - k ) e. CC )
26 2 24 25 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( B - k ) e. CC )
27 15 23 26 adddid 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) x. ( ( A - ( N - k ) ) + ( B - k ) ) ) = ( ( ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) x. ( A - ( N - k ) ) ) + ( ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) x. ( B - k ) ) ) )
28 1 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> A e. CC )
29 17 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> N e. CC )
30 28 29 subcld 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( A - N ) e. CC )
31 24 adantl 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> k e. CC )
32 2 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> B e. CC )
33 30 31 32 ppncand 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( A - N ) + k ) + ( B - k ) ) = ( ( A - N ) + B ) )
34 28 29 31 subsubd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( A - ( N - k ) ) = ( ( A - N ) + k ) )
35 34 oveq1d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( A - ( N - k ) ) + ( B - k ) ) = ( ( ( A - N ) + k ) + ( B - k ) ) )
36 28 32 29 addsubd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( A + B ) - N ) = ( ( A - N ) + B ) )
37 33 35 36 3eqtr4d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( A - ( N - k ) ) + ( B - k ) ) = ( ( A + B ) - N ) )
38 37 oveq2d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) x. ( ( A - ( N - k ) ) + ( B - k ) ) ) = ( ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) x. ( ( A + B ) - N ) ) )
39 11 14 23 mul32d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) x. ( A - ( N - k ) ) ) = ( ( ( A FallFac ( N - k ) ) x. ( A - ( N - k ) ) ) x. ( B FallFac k ) ) )
40 1cnd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> 1 e. CC )
41 29 40 31 addsubd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( N + 1 ) - k ) = ( ( N - k ) + 1 ) )
42 41 oveq2d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( A FallFac ( ( N + 1 ) - k ) ) = ( A FallFac ( ( N - k ) + 1 ) ) )
43 fallfacp1 
 |-  ( ( A e. CC /\ ( N - k ) e. NN0 ) -> ( A FallFac ( ( N - k ) + 1 ) ) = ( ( A FallFac ( N - k ) ) x. ( A - ( N - k ) ) ) )
44 1 9 43 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( A FallFac ( ( N - k ) + 1 ) ) = ( ( A FallFac ( N - k ) ) x. ( A - ( N - k ) ) ) )
45 42 44 eqtrd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( A FallFac ( ( N + 1 ) - k ) ) = ( ( A FallFac ( N - k ) ) x. ( A - ( N - k ) ) ) )
46 45 oveq1d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) = ( ( ( A FallFac ( N - k ) ) x. ( A - ( N - k ) ) ) x. ( B FallFac k ) ) )
47 39 46 eqtr4d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) x. ( A - ( N - k ) ) ) = ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) )
48 11 14 26 mulassd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) x. ( B - k ) ) = ( ( A FallFac ( N - k ) ) x. ( ( B FallFac k ) x. ( B - k ) ) ) )
49 fallfacp1 
 |-  ( ( B e. CC /\ k e. NN0 ) -> ( B FallFac ( k + 1 ) ) = ( ( B FallFac k ) x. ( B - k ) ) )
50 2 12 49 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( B FallFac ( k + 1 ) ) = ( ( B FallFac k ) x. ( B - k ) ) )
51 50 oveq2d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) = ( ( A FallFac ( N - k ) ) x. ( ( B FallFac k ) x. ( B - k ) ) ) )
52 48 51 eqtr4d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) x. ( B - k ) ) = ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) )
53 47 52 oveq12d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) x. ( A - ( N - k ) ) ) + ( ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) x. ( B - k ) ) ) = ( ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) + ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) ) )
54 27 38 53 3eqtr3d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) x. ( ( A + B ) - N ) ) = ( ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) + ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) ) )
55 54 oveq2d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) x. ( ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) x. ( ( A + B ) - N ) ) ) = ( ( N _C k ) x. ( ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) + ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) ) ) )
56 3 nn0zd 
 |-  ( ph -> N e. ZZ )
57 uzid 
 |-  ( N e. ZZ -> N e. ( ZZ>= ` N ) )
58 peano2uz 
 |-  ( N e. ( ZZ>= ` N ) -> ( N + 1 ) e. ( ZZ>= ` N ) )
59 fzss2 
 |-  ( ( N + 1 ) e. ( ZZ>= ` N ) -> ( 0 ... N ) C_ ( 0 ... ( N + 1 ) ) )
60 56 57 58 59 4syl 
 |-  ( ph -> ( 0 ... N ) C_ ( 0 ... ( N + 1 ) ) )
61 60 sselda 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> k e. ( 0 ... ( N + 1 ) ) )
62 fznn0sub 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> ( ( N + 1 ) - k ) e. NN0 )
63 fallfaccl 
 |-  ( ( A e. CC /\ ( ( N + 1 ) - k ) e. NN0 ) -> ( A FallFac ( ( N + 1 ) - k ) ) e. CC )
64 1 62 63 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( A FallFac ( ( N + 1 ) - k ) ) e. CC )
65 61 64 syldan 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( A FallFac ( ( N + 1 ) - k ) ) e. CC )
66 65 14 mulcld 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) e. CC )
67 peano2nn0 
 |-  ( k e. NN0 -> ( k + 1 ) e. NN0 )
68 12 67 syl 
 |-  ( k e. ( 0 ... N ) -> ( k + 1 ) e. NN0 )
69 fallfaccl 
 |-  ( ( B e. CC /\ ( k + 1 ) e. NN0 ) -> ( B FallFac ( k + 1 ) ) e. CC )
70 2 68 69 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( B FallFac ( k + 1 ) ) e. CC )
71 11 70 mulcld 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) e. CC )
72 8 66 71 adddid 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) x. ( ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) + ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) ) ) = ( ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) + ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) ) ) )
73 20 55 72 3eqtrd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) x. ( ( A + B ) - N ) ) = ( ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) + ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) ) ) )
74 73 sumeq2dv 
 |-  ( ph -> sum_ k e. ( 0 ... N ) ( ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) x. ( ( A + B ) - N ) ) = sum_ k e. ( 0 ... N ) ( ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) + ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) ) ) )
75 74 adantr 
 |-  ( ( ph /\ ps ) -> sum_ k e. ( 0 ... N ) ( ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) x. ( ( A + B ) - N ) ) = sum_ k e. ( 0 ... N ) ( ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) + ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) ) ) )
76 16 3 fallfacp1d 
 |-  ( ph -> ( ( A + B ) FallFac ( N + 1 ) ) = ( ( ( A + B ) FallFac N ) x. ( ( A + B ) - N ) ) )
77 4 oveq1d 
 |-  ( ps -> ( ( ( A + B ) FallFac N ) x. ( ( A + B ) - N ) ) = ( sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) x. ( ( A + B ) - N ) ) )
78 76 77 sylan9eq 
 |-  ( ( ph /\ ps ) -> ( ( A + B ) FallFac ( N + 1 ) ) = ( sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) x. ( ( A + B ) - N ) ) )
79 fzfid 
 |-  ( ph -> ( 0 ... N ) e. Fin )
80 8 15 mulcld 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) e. CC )
81 79 18 80 fsummulc1 
 |-  ( ph -> ( sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) x. ( ( A + B ) - N ) ) = sum_ k e. ( 0 ... N ) ( ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) x. ( ( A + B ) - N ) ) )
82 81 adantr 
 |-  ( ( ph /\ ps ) -> ( sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) x. ( ( A + B ) - N ) ) = sum_ k e. ( 0 ... N ) ( ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) x. ( ( A + B ) - N ) ) )
83 78 82 eqtrd 
 |-  ( ( ph /\ ps ) -> ( ( A + B ) FallFac ( N + 1 ) ) = sum_ k e. ( 0 ... N ) ( ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) x. ( ( A + B ) - N ) ) )
84 elfzelz 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> k e. ZZ )
85 bcpasc 
 |-  ( ( N e. NN0 /\ k e. ZZ ) -> ( ( N _C k ) + ( N _C ( k - 1 ) ) ) = ( ( N + 1 ) _C k ) )
86 3 84 85 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N _C k ) + ( N _C ( k - 1 ) ) ) = ( ( N + 1 ) _C k ) )
87 86 oveq1d 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( N _C k ) + ( N _C ( k - 1 ) ) ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) = ( ( ( N + 1 ) _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) )
88 3 84 6 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( N _C k ) e. NN0 )
89 88 nn0cnd 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( N _C k ) e. CC )
90 peano2zm 
 |-  ( k e. ZZ -> ( k - 1 ) e. ZZ )
91 84 90 syl 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> ( k - 1 ) e. ZZ )
92 bccl 
 |-  ( ( N e. NN0 /\ ( k - 1 ) e. ZZ ) -> ( N _C ( k - 1 ) ) e. NN0 )
93 3 91 92 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( N _C ( k - 1 ) ) e. NN0 )
94 93 nn0cnd 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( N _C ( k - 1 ) ) e. CC )
95 elfznn0 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> k e. NN0 )
96 2 95 13 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( B FallFac k ) e. CC )
97 64 96 mulcld 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) e. CC )
98 89 94 97 adddird 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( N _C k ) + ( N _C ( k - 1 ) ) ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) = ( ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) + ( ( N _C ( k - 1 ) ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) ) )
99 87 98 eqtr3d 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( N + 1 ) _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) = ( ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) + ( ( N _C ( k - 1 ) ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) ) )
100 99 sumeq2dv 
 |-  ( ph -> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( N + 1 ) _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) = sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) + ( ( N _C ( k - 1 ) ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) ) )
101 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
102 3 101 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
103 89 97 mulcld 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) e. CC )
104 oveq2 
 |-  ( k = ( N + 1 ) -> ( N _C k ) = ( N _C ( N + 1 ) ) )
105 oveq2 
 |-  ( k = ( N + 1 ) -> ( ( N + 1 ) - k ) = ( ( N + 1 ) - ( N + 1 ) ) )
106 105 oveq2d 
 |-  ( k = ( N + 1 ) -> ( A FallFac ( ( N + 1 ) - k ) ) = ( A FallFac ( ( N + 1 ) - ( N + 1 ) ) ) )
107 oveq2 
 |-  ( k = ( N + 1 ) -> ( B FallFac k ) = ( B FallFac ( N + 1 ) ) )
108 106 107 oveq12d 
 |-  ( k = ( N + 1 ) -> ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) = ( ( A FallFac ( ( N + 1 ) - ( N + 1 ) ) ) x. ( B FallFac ( N + 1 ) ) ) )
109 104 108 oveq12d 
 |-  ( k = ( N + 1 ) -> ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) = ( ( N _C ( N + 1 ) ) x. ( ( A FallFac ( ( N + 1 ) - ( N + 1 ) ) ) x. ( B FallFac ( N + 1 ) ) ) ) )
110 102 103 109 fsump1 
 |-  ( ph -> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) = ( sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) + ( ( N _C ( N + 1 ) ) x. ( ( A FallFac ( ( N + 1 ) - ( N + 1 ) ) ) x. ( B FallFac ( N + 1 ) ) ) ) ) )
111 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
112 3 111 syl 
 |-  ( ph -> ( N + 1 ) e. NN0 )
113 112 nn0zd 
 |-  ( ph -> ( N + 1 ) e. ZZ )
114 3 nn0red 
 |-  ( ph -> N e. RR )
115 114 ltp1d 
 |-  ( ph -> N < ( N + 1 ) )
116 115 olcd 
 |-  ( ph -> ( ( N + 1 ) < 0 \/ N < ( N + 1 ) ) )
117 bcval4 
 |-  ( ( N e. NN0 /\ ( N + 1 ) e. ZZ /\ ( ( N + 1 ) < 0 \/ N < ( N + 1 ) ) ) -> ( N _C ( N + 1 ) ) = 0 )
118 3 113 116 117 syl3anc 
 |-  ( ph -> ( N _C ( N + 1 ) ) = 0 )
119 118 oveq1d 
 |-  ( ph -> ( ( N _C ( N + 1 ) ) x. ( ( A FallFac ( ( N + 1 ) - ( N + 1 ) ) ) x. ( B FallFac ( N + 1 ) ) ) ) = ( 0 x. ( ( A FallFac ( ( N + 1 ) - ( N + 1 ) ) ) x. ( B FallFac ( N + 1 ) ) ) ) )
120 112 nn0cnd 
 |-  ( ph -> ( N + 1 ) e. CC )
121 120 subidd 
 |-  ( ph -> ( ( N + 1 ) - ( N + 1 ) ) = 0 )
122 121 oveq2d 
 |-  ( ph -> ( A FallFac ( ( N + 1 ) - ( N + 1 ) ) ) = ( A FallFac 0 ) )
123 0nn0 
 |-  0 e. NN0
124 fallfaccl 
 |-  ( ( A e. CC /\ 0 e. NN0 ) -> ( A FallFac 0 ) e. CC )
125 1 123 124 sylancl 
 |-  ( ph -> ( A FallFac 0 ) e. CC )
126 122 125 eqeltrd 
 |-  ( ph -> ( A FallFac ( ( N + 1 ) - ( N + 1 ) ) ) e. CC )
127 fallfaccl 
 |-  ( ( B e. CC /\ ( N + 1 ) e. NN0 ) -> ( B FallFac ( N + 1 ) ) e. CC )
128 2 112 127 syl2anc 
 |-  ( ph -> ( B FallFac ( N + 1 ) ) e. CC )
129 126 128 mulcld 
 |-  ( ph -> ( ( A FallFac ( ( N + 1 ) - ( N + 1 ) ) ) x. ( B FallFac ( N + 1 ) ) ) e. CC )
130 129 mul02d 
 |-  ( ph -> ( 0 x. ( ( A FallFac ( ( N + 1 ) - ( N + 1 ) ) ) x. ( B FallFac ( N + 1 ) ) ) ) = 0 )
131 119 130 eqtrd 
 |-  ( ph -> ( ( N _C ( N + 1 ) ) x. ( ( A FallFac ( ( N + 1 ) - ( N + 1 ) ) ) x. ( B FallFac ( N + 1 ) ) ) ) = 0 )
132 131 oveq2d 
 |-  ( ph -> ( sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) + ( ( N _C ( N + 1 ) ) x. ( ( A FallFac ( ( N + 1 ) - ( N + 1 ) ) ) x. ( B FallFac ( N + 1 ) ) ) ) ) = ( sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) + 0 ) )
133 61 103 syldan 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) e. CC )
134 79 133 fsumcl 
 |-  ( ph -> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) e. CC )
135 134 addridd 
 |-  ( ph -> ( sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) + 0 ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) )
136 110 132 135 3eqtrd 
 |-  ( ph -> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) )
137 112 101 eleqtrdi 
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` 0 ) )
138 94 97 mulcld 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N _C ( k - 1 ) ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) e. CC )
139 oveq1 
 |-  ( k = 0 -> ( k - 1 ) = ( 0 - 1 ) )
140 df-neg 
 |-  -u 1 = ( 0 - 1 )
141 139 140 eqtr4di 
 |-  ( k = 0 -> ( k - 1 ) = -u 1 )
142 141 oveq2d 
 |-  ( k = 0 -> ( N _C ( k - 1 ) ) = ( N _C -u 1 ) )
143 oveq2 
 |-  ( k = 0 -> ( ( N + 1 ) - k ) = ( ( N + 1 ) - 0 ) )
144 143 oveq2d 
 |-  ( k = 0 -> ( A FallFac ( ( N + 1 ) - k ) ) = ( A FallFac ( ( N + 1 ) - 0 ) ) )
145 oveq2 
 |-  ( k = 0 -> ( B FallFac k ) = ( B FallFac 0 ) )
146 144 145 oveq12d 
 |-  ( k = 0 -> ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) = ( ( A FallFac ( ( N + 1 ) - 0 ) ) x. ( B FallFac 0 ) ) )
147 142 146 oveq12d 
 |-  ( k = 0 -> ( ( N _C ( k - 1 ) ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) = ( ( N _C -u 1 ) x. ( ( A FallFac ( ( N + 1 ) - 0 ) ) x. ( B FallFac 0 ) ) ) )
148 137 138 147 fsum1p 
 |-  ( ph -> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) = ( ( ( N _C -u 1 ) x. ( ( A FallFac ( ( N + 1 ) - 0 ) ) x. ( B FallFac 0 ) ) ) + sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) ) )
149 neg1z 
 |-  -u 1 e. ZZ
150 neg1lt0 
 |-  -u 1 < 0
151 150 orci 
 |-  ( -u 1 < 0 \/ N < -u 1 )
152 bcval4 
 |-  ( ( N e. NN0 /\ -u 1 e. ZZ /\ ( -u 1 < 0 \/ N < -u 1 ) ) -> ( N _C -u 1 ) = 0 )
153 149 151 152 mp3an23 
 |-  ( N e. NN0 -> ( N _C -u 1 ) = 0 )
154 3 153 syl 
 |-  ( ph -> ( N _C -u 1 ) = 0 )
155 154 oveq1d 
 |-  ( ph -> ( ( N _C -u 1 ) x. ( ( A FallFac ( ( N + 1 ) - 0 ) ) x. ( B FallFac 0 ) ) ) = ( 0 x. ( ( A FallFac ( ( N + 1 ) - 0 ) ) x. ( B FallFac 0 ) ) ) )
156 120 subid1d 
 |-  ( ph -> ( ( N + 1 ) - 0 ) = ( N + 1 ) )
157 156 oveq2d 
 |-  ( ph -> ( A FallFac ( ( N + 1 ) - 0 ) ) = ( A FallFac ( N + 1 ) ) )
158 fallfaccl 
 |-  ( ( A e. CC /\ ( N + 1 ) e. NN0 ) -> ( A FallFac ( N + 1 ) ) e. CC )
159 1 112 158 syl2anc 
 |-  ( ph -> ( A FallFac ( N + 1 ) ) e. CC )
160 157 159 eqeltrd 
 |-  ( ph -> ( A FallFac ( ( N + 1 ) - 0 ) ) e. CC )
161 fallfaccl 
 |-  ( ( B e. CC /\ 0 e. NN0 ) -> ( B FallFac 0 ) e. CC )
162 2 123 161 sylancl 
 |-  ( ph -> ( B FallFac 0 ) e. CC )
163 160 162 mulcld 
 |-  ( ph -> ( ( A FallFac ( ( N + 1 ) - 0 ) ) x. ( B FallFac 0 ) ) e. CC )
164 163 mul02d 
 |-  ( ph -> ( 0 x. ( ( A FallFac ( ( N + 1 ) - 0 ) ) x. ( B FallFac 0 ) ) ) = 0 )
165 155 164 eqtrd 
 |-  ( ph -> ( ( N _C -u 1 ) x. ( ( A FallFac ( ( N + 1 ) - 0 ) ) x. ( B FallFac 0 ) ) ) = 0 )
166 1zzd 
 |-  ( ph -> 1 e. ZZ )
167 0zd 
 |-  ( ph -> 0 e. ZZ )
168 1 2 3 binomfallfaclem1 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( N _C j ) x. ( ( A FallFac ( N - j ) ) x. ( B FallFac ( j + 1 ) ) ) ) e. CC )
169 oveq2 
 |-  ( j = ( k - 1 ) -> ( N _C j ) = ( N _C ( k - 1 ) ) )
170 oveq2 
 |-  ( j = ( k - 1 ) -> ( N - j ) = ( N - ( k - 1 ) ) )
171 170 oveq2d 
 |-  ( j = ( k - 1 ) -> ( A FallFac ( N - j ) ) = ( A FallFac ( N - ( k - 1 ) ) ) )
172 oveq1 
 |-  ( j = ( k - 1 ) -> ( j + 1 ) = ( ( k - 1 ) + 1 ) )
173 172 oveq2d 
 |-  ( j = ( k - 1 ) -> ( B FallFac ( j + 1 ) ) = ( B FallFac ( ( k - 1 ) + 1 ) ) )
174 171 173 oveq12d 
 |-  ( j = ( k - 1 ) -> ( ( A FallFac ( N - j ) ) x. ( B FallFac ( j + 1 ) ) ) = ( ( A FallFac ( N - ( k - 1 ) ) ) x. ( B FallFac ( ( k - 1 ) + 1 ) ) ) )
175 169 174 oveq12d 
 |-  ( j = ( k - 1 ) -> ( ( N _C j ) x. ( ( A FallFac ( N - j ) ) x. ( B FallFac ( j + 1 ) ) ) ) = ( ( N _C ( k - 1 ) ) x. ( ( A FallFac ( N - ( k - 1 ) ) ) x. ( B FallFac ( ( k - 1 ) + 1 ) ) ) ) )
176 166 167 56 168 175 fsumshft 
 |-  ( ph -> sum_ j e. ( 0 ... N ) ( ( N _C j ) x. ( ( A FallFac ( N - j ) ) x. ( B FallFac ( j + 1 ) ) ) ) = sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( A FallFac ( N - ( k - 1 ) ) ) x. ( B FallFac ( ( k - 1 ) + 1 ) ) ) ) )
177 17 adantr 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> N e. CC )
178 elfzelz 
 |-  ( k e. ( ( 0 + 1 ) ... ( N + 1 ) ) -> k e. ZZ )
179 178 adantl 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> k e. ZZ )
180 179 zcnd 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> k e. CC )
181 1cnd 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> 1 e. CC )
182 177 180 181 subsub3d 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( N - ( k - 1 ) ) = ( ( N + 1 ) - k ) )
183 182 oveq2d 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( A FallFac ( N - ( k - 1 ) ) ) = ( A FallFac ( ( N + 1 ) - k ) ) )
184 180 181 npcand 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( k - 1 ) + 1 ) = k )
185 184 oveq2d 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( B FallFac ( ( k - 1 ) + 1 ) ) = ( B FallFac k ) )
186 183 185 oveq12d 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( A FallFac ( N - ( k - 1 ) ) ) x. ( B FallFac ( ( k - 1 ) + 1 ) ) ) = ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) )
187 186 oveq2d 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( N _C ( k - 1 ) ) x. ( ( A FallFac ( N - ( k - 1 ) ) ) x. ( B FallFac ( ( k - 1 ) + 1 ) ) ) ) = ( ( N _C ( k - 1 ) ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) )
188 187 sumeq2dv 
 |-  ( ph -> sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( A FallFac ( N - ( k - 1 ) ) ) x. ( B FallFac ( ( k - 1 ) + 1 ) ) ) ) = sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) )
189 176 188 eqtr2d 
 |-  ( ph -> sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) = sum_ j e. ( 0 ... N ) ( ( N _C j ) x. ( ( A FallFac ( N - j ) ) x. ( B FallFac ( j + 1 ) ) ) ) )
190 oveq2 
 |-  ( k = j -> ( N _C k ) = ( N _C j ) )
191 oveq2 
 |-  ( k = j -> ( N - k ) = ( N - j ) )
192 191 oveq2d 
 |-  ( k = j -> ( A FallFac ( N - k ) ) = ( A FallFac ( N - j ) ) )
193 oveq1 
 |-  ( k = j -> ( k + 1 ) = ( j + 1 ) )
194 193 oveq2d 
 |-  ( k = j -> ( B FallFac ( k + 1 ) ) = ( B FallFac ( j + 1 ) ) )
195 192 194 oveq12d 
 |-  ( k = j -> ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) = ( ( A FallFac ( N - j ) ) x. ( B FallFac ( j + 1 ) ) ) )
196 190 195 oveq12d 
 |-  ( k = j -> ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) ) = ( ( N _C j ) x. ( ( A FallFac ( N - j ) ) x. ( B FallFac ( j + 1 ) ) ) ) )
197 196 cbvsumv 
 |-  sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) ) = sum_ j e. ( 0 ... N ) ( ( N _C j ) x. ( ( A FallFac ( N - j ) ) x. ( B FallFac ( j + 1 ) ) ) )
198 189 197 eqtr4di 
 |-  ( ph -> sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) ) )
199 165 198 oveq12d 
 |-  ( ph -> ( ( ( N _C -u 1 ) x. ( ( A FallFac ( ( N + 1 ) - 0 ) ) x. ( B FallFac 0 ) ) ) + sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) ) = ( 0 + sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) ) ) )
200 1 2 3 binomfallfaclem1 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) ) e. CC )
201 79 200 fsumcl 
 |-  ( ph -> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) ) e. CC )
202 201 addlidd 
 |-  ( ph -> ( 0 + sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) ) ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) ) )
203 148 199 202 3eqtrd 
 |-  ( ph -> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) ) )
204 136 203 oveq12d 
 |-  ( ph -> ( sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) + sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) ) = ( sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) + sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) ) ) )
205 fzfid 
 |-  ( ph -> ( 0 ... ( N + 1 ) ) e. Fin )
206 205 103 138 fsumadd 
 |-  ( ph -> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) + ( ( N _C ( k - 1 ) ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) ) = ( sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) + sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) ) )
207 79 133 200 fsumadd 
 |-  ( ph -> sum_ k e. ( 0 ... N ) ( ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) + ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) ) ) = ( sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) + sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) ) ) )
208 204 206 207 3eqtr4d 
 |-  ( ph -> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) + ( ( N _C ( k - 1 ) ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) ) = sum_ k e. ( 0 ... N ) ( ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) + ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) ) ) )
209 100 208 eqtrd 
 |-  ( ph -> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( N + 1 ) _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) = sum_ k e. ( 0 ... N ) ( ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) + ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) ) ) )
210 209 adantr 
 |-  ( ( ph /\ ps ) -> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( N + 1 ) _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) = sum_ k e. ( 0 ... N ) ( ( ( N _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) + ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac ( k + 1 ) ) ) ) ) )
211 75 83 210 3eqtr4d 
 |-  ( ( ph /\ ps ) -> ( ( A + B ) FallFac ( N + 1 ) ) = sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( N + 1 ) _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) )