Metamath Proof Explorer


Theorem binomfallfaclem2

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

Ref Expression
Hypotheses binomfallfaclem.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„‚ )
binomfallfaclem.2 โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„‚ )
binomfallfaclem.3 โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„•0 )
binomfallfaclem.4 โŠข ( ๐œ“ โ†’ ( ( ๐ด + ๐ต ) FallFac ๐‘ ) = ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘ ) ( ( ๐‘ C ๐‘˜ ) ยท ( ( ๐ด FallFac ( ๐‘ โˆ’ ๐‘˜ ) ) ยท ( ๐ต FallFac ๐‘˜ ) ) ) )
Assertion binomfallfaclem2 ( ( ๐œ‘ โˆง ๐œ“ ) โ†’ ( ( ๐ด + ๐ต ) FallFac ( ๐‘ + 1 ) ) = ฮฃ ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) ( ( ( ๐‘ + 1 ) C ๐‘˜ ) ยท ( ( ๐ด FallFac ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) ) ยท ( ๐ต FallFac ๐‘˜ ) ) ) )

Proof

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