MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  binomfallfaclem2 Structured version   Visualization version   GIF version

Theorem binomfallfaclem2 15928
Description: Lemma for binomfallfac 15929. Inductive step. (Contributed by Scott Fenton, 13-Mar-2018.)
Hypotheses
Ref Expression
binomfallfaclem.1 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
binomfallfaclem.2 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
binomfallfaclem.3 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•0)
binomfallfaclem.4 (๐œ“ โ†’ ((๐ด + ๐ต) FallFac ๐‘) = ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))))
Assertion
Ref Expression
binomfallfaclem2 ((๐œ‘ โˆง ๐œ“) โ†’ ((๐ด + ๐ต) FallFac (๐‘ + 1)) = ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))(((๐‘ + 1)C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))))
Distinct variable groups:   ๐œ‘,๐‘˜   ๐‘˜,๐‘   ๐ด,๐‘˜   ๐ต,๐‘˜
Allowed substitution hint:   ๐œ“(๐‘˜)

Proof of Theorem binomfallfaclem2
Dummy variable ๐‘— is distinct from all other variables.
StepHypRef Expression
1 binomfallfaclem.3 . . . . . . . 8 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•0)
2 elfzelz 13447 . . . . . . . 8 (๐‘˜ โˆˆ (0...๐‘) โ†’ ๐‘˜ โˆˆ โ„ค)
3 bccl 14228 . . . . . . . 8 ((๐‘ โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„ค) โ†’ (๐‘C๐‘˜) โˆˆ โ„•0)
41, 2, 3syl2an 597 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐‘C๐‘˜) โˆˆ โ„•0)
54nn0cnd 12480 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐‘C๐‘˜) โˆˆ โ„‚)
6 binomfallfaclem.1 . . . . . . . 8 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
7 fznn0sub 13479 . . . . . . . 8 (๐‘˜ โˆˆ (0...๐‘) โ†’ (๐‘ โˆ’ ๐‘˜) โˆˆ โ„•0)
8 fallfaccl 15904 . . . . . . . 8 ((๐ด โˆˆ โ„‚ โˆง (๐‘ โˆ’ ๐‘˜) โˆˆ โ„•0) โ†’ (๐ด FallFac (๐‘ โˆ’ ๐‘˜)) โˆˆ โ„‚)
96, 7, 8syl2an 597 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐ด FallFac (๐‘ โˆ’ ๐‘˜)) โˆˆ โ„‚)
10 binomfallfaclem.2 . . . . . . . 8 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
11 elfznn0 13540 . . . . . . . 8 (๐‘˜ โˆˆ (0...๐‘) โ†’ ๐‘˜ โˆˆ โ„•0)
12 fallfaccl 15904 . . . . . . . 8 ((๐ต โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐ต FallFac ๐‘˜) โˆˆ โ„‚)
1310, 11, 12syl2an 597 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐ต FallFac ๐‘˜) โˆˆ โ„‚)
149, 13mulcld 11180 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)) โˆˆ โ„‚)
156, 10addcld 11179 . . . . . . . 8 (๐œ‘ โ†’ (๐ด + ๐ต) โˆˆ โ„‚)
161nn0cnd 12480 . . . . . . . 8 (๐œ‘ โ†’ ๐‘ โˆˆ โ„‚)
1715, 16subcld 11517 . . . . . . 7 (๐œ‘ โ†’ ((๐ด + ๐ต) โˆ’ ๐‘) โˆˆ โ„‚)
1817adantr 482 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐ด + ๐ต) โˆ’ ๐‘) โˆˆ โ„‚)
195, 14, 18mulassd 11183 . . . . 5 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) ยท ((๐ด + ๐ต) โˆ’ ๐‘)) = ((๐‘C๐‘˜) ยท (((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)) ยท ((๐ด + ๐ต) โˆ’ ๐‘))))
207nn0cnd 12480 . . . . . . . . 9 (๐‘˜ โˆˆ (0...๐‘) โ†’ (๐‘ โˆ’ ๐‘˜) โˆˆ โ„‚)
21 subcl 11405 . . . . . . . . 9 ((๐ด โˆˆ โ„‚ โˆง (๐‘ โˆ’ ๐‘˜) โˆˆ โ„‚) โ†’ (๐ด โˆ’ (๐‘ โˆ’ ๐‘˜)) โˆˆ โ„‚)
226, 20, 21syl2an 597 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐ด โˆ’ (๐‘ โˆ’ ๐‘˜)) โˆˆ โ„‚)
2311nn0cnd 12480 . . . . . . . . 9 (๐‘˜ โˆˆ (0...๐‘) โ†’ ๐‘˜ โˆˆ โ„‚)
24 subcl 11405 . . . . . . . . 9 ((๐ต โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ โ„‚) โ†’ (๐ต โˆ’ ๐‘˜) โˆˆ โ„‚)
2510, 23, 24syl2an 597 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐ต โˆ’ ๐‘˜) โˆˆ โ„‚)
2614, 22, 25adddid 11184 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)) ยท ((๐ด โˆ’ (๐‘ โˆ’ ๐‘˜)) + (๐ต โˆ’ ๐‘˜))) = ((((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)) ยท (๐ด โˆ’ (๐‘ โˆ’ ๐‘˜))) + (((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)) ยท (๐ต โˆ’ ๐‘˜))))
276adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ๐ด โˆˆ โ„‚)
2816adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ๐‘ โˆˆ โ„‚)
2927, 28subcld 11517 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐ด โˆ’ ๐‘) โˆˆ โ„‚)
3023adantl 483 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ๐‘˜ โˆˆ โ„‚)
3110adantr 482 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ๐ต โˆˆ โ„‚)
3229, 30, 31ppncand 11557 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (((๐ด โˆ’ ๐‘) + ๐‘˜) + (๐ต โˆ’ ๐‘˜)) = ((๐ด โˆ’ ๐‘) + ๐ต))
3327, 28, 30subsubd 11545 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐ด โˆ’ (๐‘ โˆ’ ๐‘˜)) = ((๐ด โˆ’ ๐‘) + ๐‘˜))
3433oveq1d 7373 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐ด โˆ’ (๐‘ โˆ’ ๐‘˜)) + (๐ต โˆ’ ๐‘˜)) = (((๐ด โˆ’ ๐‘) + ๐‘˜) + (๐ต โˆ’ ๐‘˜)))
3527, 31, 28addsubd 11538 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐ด + ๐ต) โˆ’ ๐‘) = ((๐ด โˆ’ ๐‘) + ๐ต))
3632, 34, 353eqtr4d 2783 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐ด โˆ’ (๐‘ โˆ’ ๐‘˜)) + (๐ต โˆ’ ๐‘˜)) = ((๐ด + ๐ต) โˆ’ ๐‘))
3736oveq2d 7374 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)) ยท ((๐ด โˆ’ (๐‘ โˆ’ ๐‘˜)) + (๐ต โˆ’ ๐‘˜))) = (((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)) ยท ((๐ด + ๐ต) โˆ’ ๐‘)))
389, 13, 22mul32d 11370 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)) ยท (๐ด โˆ’ (๐‘ โˆ’ ๐‘˜))) = (((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ด โˆ’ (๐‘ โˆ’ ๐‘˜))) ยท (๐ต FallFac ๐‘˜)))
39 1cnd 11155 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ 1 โˆˆ โ„‚)
4028, 39, 30addsubd 11538 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐‘ + 1) โˆ’ ๐‘˜) = ((๐‘ โˆ’ ๐‘˜) + 1))
4140oveq2d 7374 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) = (๐ด FallFac ((๐‘ โˆ’ ๐‘˜) + 1)))
42 fallfacp1 15918 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„‚ โˆง (๐‘ โˆ’ ๐‘˜) โˆˆ โ„•0) โ†’ (๐ด FallFac ((๐‘ โˆ’ ๐‘˜) + 1)) = ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ด โˆ’ (๐‘ โˆ’ ๐‘˜))))
436, 7, 42syl2an 597 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐ด FallFac ((๐‘ โˆ’ ๐‘˜) + 1)) = ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ด โˆ’ (๐‘ โˆ’ ๐‘˜))))
4441, 43eqtrd 2773 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) = ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ด โˆ’ (๐‘ โˆ’ ๐‘˜))))
4544oveq1d 7373 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)) = (((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ด โˆ’ (๐‘ โˆ’ ๐‘˜))) ยท (๐ต FallFac ๐‘˜)))
4638, 45eqtr4d 2776 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)) ยท (๐ด โˆ’ (๐‘ โˆ’ ๐‘˜))) = ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)))
479, 13, 25mulassd 11183 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)) ยท (๐ต โˆ’ ๐‘˜)) = ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท ((๐ต FallFac ๐‘˜) ยท (๐ต โˆ’ ๐‘˜))))
48 fallfacp1 15918 . . . . . . . . . . 11 ((๐ต โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐ต FallFac (๐‘˜ + 1)) = ((๐ต FallFac ๐‘˜) ยท (๐ต โˆ’ ๐‘˜)))
4910, 11, 48syl2an 597 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐ต FallFac (๐‘˜ + 1)) = ((๐ต FallFac ๐‘˜) ยท (๐ต โˆ’ ๐‘˜)))
5049oveq2d 7374 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1))) = ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท ((๐ต FallFac ๐‘˜) ยท (๐ต โˆ’ ๐‘˜))))
5147, 50eqtr4d 2776 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)) ยท (๐ต โˆ’ ๐‘˜)) = ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1))))
5246, 51oveq12d 7376 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)) ยท (๐ด โˆ’ (๐‘ โˆ’ ๐‘˜))) + (((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)) ยท (๐ต โˆ’ ๐‘˜))) = (((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)) + ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1)))))
5326, 37, 523eqtr3d 2781 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)) ยท ((๐ด + ๐ต) โˆ’ ๐‘)) = (((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)) + ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1)))))
5453oveq2d 7374 . . . . 5 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐‘C๐‘˜) ยท (((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)) ยท ((๐ด + ๐ต) โˆ’ ๐‘))) = ((๐‘C๐‘˜) ยท (((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)) + ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1))))))
551nn0zd 12530 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘ โˆˆ โ„ค)
56 uzid 12783 . . . . . . . . . 10 (๐‘ โˆˆ โ„ค โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜๐‘))
57 peano2uz 12831 . . . . . . . . . 10 (๐‘ โˆˆ (โ„คโ‰ฅโ€˜๐‘) โ†’ (๐‘ + 1) โˆˆ (โ„คโ‰ฅโ€˜๐‘))
58 fzss2 13487 . . . . . . . . . 10 ((๐‘ + 1) โˆˆ (โ„คโ‰ฅโ€˜๐‘) โ†’ (0...๐‘) โŠ† (0...(๐‘ + 1)))
5955, 56, 57, 584syl 19 . . . . . . . . 9 (๐œ‘ โ†’ (0...๐‘) โŠ† (0...(๐‘ + 1)))
6059sselda 3945 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ๐‘˜ โˆˆ (0...(๐‘ + 1)))
61 fznn0sub 13479 . . . . . . . . 9 (๐‘˜ โˆˆ (0...(๐‘ + 1)) โ†’ ((๐‘ + 1) โˆ’ ๐‘˜) โˆˆ โ„•0)
62 fallfaccl 15904 . . . . . . . . 9 ((๐ด โˆˆ โ„‚ โˆง ((๐‘ + 1) โˆ’ ๐‘˜) โˆˆ โ„•0) โ†’ (๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) โˆˆ โ„‚)
636, 61, 62syl2an 597 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) โˆˆ โ„‚)
6460, 63syldan 592 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) โˆˆ โ„‚)
6564, 13mulcld 11180 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)) โˆˆ โ„‚)
66 peano2nn0 12458 . . . . . . . . 9 (๐‘˜ โˆˆ โ„•0 โ†’ (๐‘˜ + 1) โˆˆ โ„•0)
6711, 66syl 17 . . . . . . . 8 (๐‘˜ โˆˆ (0...๐‘) โ†’ (๐‘˜ + 1) โˆˆ โ„•0)
68 fallfaccl 15904 . . . . . . . 8 ((๐ต โˆˆ โ„‚ โˆง (๐‘˜ + 1) โˆˆ โ„•0) โ†’ (๐ต FallFac (๐‘˜ + 1)) โˆˆ โ„‚)
6910, 67, 68syl2an 597 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐ต FallFac (๐‘˜ + 1)) โˆˆ โ„‚)
709, 69mulcld 11180 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1))) โˆˆ โ„‚)
715, 65, 70adddid 11184 . . . . 5 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐‘C๐‘˜) ยท (((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)) + ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1))))) = (((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) + ((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1))))))
7219, 54, 713eqtrd 2777 . . . 4 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) ยท ((๐ด + ๐ต) โˆ’ ๐‘)) = (((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) + ((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1))))))
7372sumeq2dv 15593 . . 3 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...๐‘)(((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) ยท ((๐ด + ๐ต) โˆ’ ๐‘)) = ฮฃ๐‘˜ โˆˆ (0...๐‘)(((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) + ((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1))))))
7473adantr 482 . 2 ((๐œ‘ โˆง ๐œ“) โ†’ ฮฃ๐‘˜ โˆˆ (0...๐‘)(((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) ยท ((๐ด + ๐ต) โˆ’ ๐‘)) = ฮฃ๐‘˜ โˆˆ (0...๐‘)(((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) + ((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1))))))
7515, 1fallfacp1d 15920 . . . 4 (๐œ‘ โ†’ ((๐ด + ๐ต) FallFac (๐‘ + 1)) = (((๐ด + ๐ต) FallFac ๐‘) ยท ((๐ด + ๐ต) โˆ’ ๐‘)))
76 binomfallfaclem.4 . . . . 5 (๐œ“ โ†’ ((๐ด + ๐ต) FallFac ๐‘) = ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))))
7776oveq1d 7373 . . . 4 (๐œ“ โ†’ (((๐ด + ๐ต) FallFac ๐‘) ยท ((๐ด + ๐ต) โˆ’ ๐‘)) = (ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) ยท ((๐ด + ๐ต) โˆ’ ๐‘)))
7875, 77sylan9eq 2793 . . 3 ((๐œ‘ โˆง ๐œ“) โ†’ ((๐ด + ๐ต) FallFac (๐‘ + 1)) = (ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) ยท ((๐ด + ๐ต) โˆ’ ๐‘)))
79 fzfid 13884 . . . . 5 (๐œ‘ โ†’ (0...๐‘) โˆˆ Fin)
805, 14mulcld 11180 . . . . 5 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) โˆˆ โ„‚)
8179, 17, 80fsummulc1 15675 . . . 4 (๐œ‘ โ†’ (ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) ยท ((๐ด + ๐ต) โˆ’ ๐‘)) = ฮฃ๐‘˜ โˆˆ (0...๐‘)(((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) ยท ((๐ด + ๐ต) โˆ’ ๐‘)))
8281adantr 482 . . 3 ((๐œ‘ โˆง ๐œ“) โ†’ (ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) ยท ((๐ด + ๐ต) โˆ’ ๐‘)) = ฮฃ๐‘˜ โˆˆ (0...๐‘)(((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) ยท ((๐ด + ๐ต) โˆ’ ๐‘)))
8378, 82eqtrd 2773 . 2 ((๐œ‘ โˆง ๐œ“) โ†’ ((๐ด + ๐ต) FallFac (๐‘ + 1)) = ฮฃ๐‘˜ โˆˆ (0...๐‘)(((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) ยท ((๐ด + ๐ต) โˆ’ ๐‘)))
84 elfzelz 13447 . . . . . . . 8 (๐‘˜ โˆˆ (0...(๐‘ + 1)) โ†’ ๐‘˜ โˆˆ โ„ค)
85 bcpasc 14227 . . . . . . . 8 ((๐‘ โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„ค) โ†’ ((๐‘C๐‘˜) + (๐‘C(๐‘˜ โˆ’ 1))) = ((๐‘ + 1)C๐‘˜))
861, 84, 85syl2an 597 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ ((๐‘C๐‘˜) + (๐‘C(๐‘˜ โˆ’ 1))) = ((๐‘ + 1)C๐‘˜))
8786oveq1d 7373 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (((๐‘C๐‘˜) + (๐‘C(๐‘˜ โˆ’ 1))) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) = (((๐‘ + 1)C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))))
881, 84, 3syl2an 597 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (๐‘C๐‘˜) โˆˆ โ„•0)
8988nn0cnd 12480 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (๐‘C๐‘˜) โˆˆ โ„‚)
90 peano2zm 12551 . . . . . . . . . 10 (๐‘˜ โˆˆ โ„ค โ†’ (๐‘˜ โˆ’ 1) โˆˆ โ„ค)
9184, 90syl 17 . . . . . . . . 9 (๐‘˜ โˆˆ (0...(๐‘ + 1)) โ†’ (๐‘˜ โˆ’ 1) โˆˆ โ„ค)
92 bccl 14228 . . . . . . . . 9 ((๐‘ โˆˆ โ„•0 โˆง (๐‘˜ โˆ’ 1) โˆˆ โ„ค) โ†’ (๐‘C(๐‘˜ โˆ’ 1)) โˆˆ โ„•0)
931, 91, 92syl2an 597 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (๐‘C(๐‘˜ โˆ’ 1)) โˆˆ โ„•0)
9493nn0cnd 12480 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (๐‘C(๐‘˜ โˆ’ 1)) โˆˆ โ„‚)
95 elfznn0 13540 . . . . . . . . 9 (๐‘˜ โˆˆ (0...(๐‘ + 1)) โ†’ ๐‘˜ โˆˆ โ„•0)
9610, 95, 12syl2an 597 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (๐ต FallFac ๐‘˜) โˆˆ โ„‚)
9763, 96mulcld 11180 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)) โˆˆ โ„‚)
9889, 94, 97adddird 11185 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (((๐‘C๐‘˜) + (๐‘C(๐‘˜ โˆ’ 1))) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) = (((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) + ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)))))
9987, 98eqtr3d 2775 . . . . 5 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (((๐‘ + 1)C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) = (((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) + ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)))))
10099sumeq2dv 15593 . . . 4 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))(((๐‘ + 1)C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) = ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))(((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) + ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)))))
101 nn0uz 12810 . . . . . . . . 9 โ„•0 = (โ„คโ‰ฅโ€˜0)
1021, 101eleqtrdi 2844 . . . . . . . 8 (๐œ‘ โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜0))
10389, 97mulcld 11180 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ ((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) โˆˆ โ„‚)
104 oveq2 7366 . . . . . . . . 9 (๐‘˜ = (๐‘ + 1) โ†’ (๐‘C๐‘˜) = (๐‘C(๐‘ + 1)))
105 oveq2 7366 . . . . . . . . . . 11 (๐‘˜ = (๐‘ + 1) โ†’ ((๐‘ + 1) โˆ’ ๐‘˜) = ((๐‘ + 1) โˆ’ (๐‘ + 1)))
106105oveq2d 7374 . . . . . . . . . 10 (๐‘˜ = (๐‘ + 1) โ†’ (๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) = (๐ด FallFac ((๐‘ + 1) โˆ’ (๐‘ + 1))))
107 oveq2 7366 . . . . . . . . . 10 (๐‘˜ = (๐‘ + 1) โ†’ (๐ต FallFac ๐‘˜) = (๐ต FallFac (๐‘ + 1)))
108106, 107oveq12d 7376 . . . . . . . . 9 (๐‘˜ = (๐‘ + 1) โ†’ ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)) = ((๐ด FallFac ((๐‘ + 1) โˆ’ (๐‘ + 1))) ยท (๐ต FallFac (๐‘ + 1))))
109104, 108oveq12d 7376 . . . . . . . 8 (๐‘˜ = (๐‘ + 1) โ†’ ((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) = ((๐‘C(๐‘ + 1)) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ (๐‘ + 1))) ยท (๐ต FallFac (๐‘ + 1)))))
110102, 103, 109fsump1 15646 . . . . . . 7 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) = (ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) + ((๐‘C(๐‘ + 1)) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ (๐‘ + 1))) ยท (๐ต FallFac (๐‘ + 1))))))
111 peano2nn0 12458 . . . . . . . . . . . . 13 (๐‘ โˆˆ โ„•0 โ†’ (๐‘ + 1) โˆˆ โ„•0)
1121, 111syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ + 1) โˆˆ โ„•0)
113112nn0zd 12530 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ + 1) โˆˆ โ„ค)
1141nn0red 12479 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘ โˆˆ โ„)
115114ltp1d 12090 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘ < (๐‘ + 1))
116115olcd 873 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐‘ + 1) < 0 โˆจ ๐‘ < (๐‘ + 1)))
117 bcval4 14213 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„•0 โˆง (๐‘ + 1) โˆˆ โ„ค โˆง ((๐‘ + 1) < 0 โˆจ ๐‘ < (๐‘ + 1))) โ†’ (๐‘C(๐‘ + 1)) = 0)
1181, 113, 116, 117syl3anc 1372 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘C(๐‘ + 1)) = 0)
119118oveq1d 7373 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘C(๐‘ + 1)) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ (๐‘ + 1))) ยท (๐ต FallFac (๐‘ + 1)))) = (0 ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ (๐‘ + 1))) ยท (๐ต FallFac (๐‘ + 1)))))
120112nn0cnd 12480 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘ + 1) โˆˆ โ„‚)
121120subidd 11505 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐‘ + 1) โˆ’ (๐‘ + 1)) = 0)
122121oveq2d 7374 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐ด FallFac ((๐‘ + 1) โˆ’ (๐‘ + 1))) = (๐ด FallFac 0))
123 0nn0 12433 . . . . . . . . . . . . 13 0 โˆˆ โ„•0
124 fallfaccl 15904 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„‚ โˆง 0 โˆˆ โ„•0) โ†’ (๐ด FallFac 0) โˆˆ โ„‚)
1256, 123, 124sylancl 587 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐ด FallFac 0) โˆˆ โ„‚)
126122, 125eqeltrd 2834 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ด FallFac ((๐‘ + 1) โˆ’ (๐‘ + 1))) โˆˆ โ„‚)
127 fallfaccl 15904 . . . . . . . . . . . 12 ((๐ต โˆˆ โ„‚ โˆง (๐‘ + 1) โˆˆ โ„•0) โ†’ (๐ต FallFac (๐‘ + 1)) โˆˆ โ„‚)
12810, 112, 127syl2anc 585 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ต FallFac (๐‘ + 1)) โˆˆ โ„‚)
129126, 128mulcld 11180 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ด FallFac ((๐‘ + 1) โˆ’ (๐‘ + 1))) ยท (๐ต FallFac (๐‘ + 1))) โˆˆ โ„‚)
130129mul02d 11358 . . . . . . . . 9 (๐œ‘ โ†’ (0 ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ (๐‘ + 1))) ยท (๐ต FallFac (๐‘ + 1)))) = 0)
131119, 130eqtrd 2773 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘C(๐‘ + 1)) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ (๐‘ + 1))) ยท (๐ต FallFac (๐‘ + 1)))) = 0)
132131oveq2d 7374 . . . . . . 7 (๐œ‘ โ†’ (ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) + ((๐‘C(๐‘ + 1)) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ (๐‘ + 1))) ยท (๐ต FallFac (๐‘ + 1))))) = (ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) + 0))
13360, 103syldan 592 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) โˆˆ โ„‚)
13479, 133fsumcl 15623 . . . . . . . 8 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) โˆˆ โ„‚)
135134addid1d 11360 . . . . . . 7 (๐œ‘ โ†’ (ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) + 0) = ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))))
136110, 132, 1353eqtrd 2777 . . . . . 6 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) = ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))))
137112, 101eleqtrdi 2844 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ + 1) โˆˆ (โ„คโ‰ฅโ€˜0))
13894, 97mulcld 11180 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) โˆˆ โ„‚)
139 oveq1 7365 . . . . . . . . . . 11 (๐‘˜ = 0 โ†’ (๐‘˜ โˆ’ 1) = (0 โˆ’ 1))
140 df-neg 11393 . . . . . . . . . . 11 -1 = (0 โˆ’ 1)
141139, 140eqtr4di 2791 . . . . . . . . . 10 (๐‘˜ = 0 โ†’ (๐‘˜ โˆ’ 1) = -1)
142141oveq2d 7374 . . . . . . . . 9 (๐‘˜ = 0 โ†’ (๐‘C(๐‘˜ โˆ’ 1)) = (๐‘C-1))
143 oveq2 7366 . . . . . . . . . . 11 (๐‘˜ = 0 โ†’ ((๐‘ + 1) โˆ’ ๐‘˜) = ((๐‘ + 1) โˆ’ 0))
144143oveq2d 7374 . . . . . . . . . 10 (๐‘˜ = 0 โ†’ (๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) = (๐ด FallFac ((๐‘ + 1) โˆ’ 0)))
145 oveq2 7366 . . . . . . . . . 10 (๐‘˜ = 0 โ†’ (๐ต FallFac ๐‘˜) = (๐ต FallFac 0))
146144, 145oveq12d 7376 . . . . . . . . 9 (๐‘˜ = 0 โ†’ ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)) = ((๐ด FallFac ((๐‘ + 1) โˆ’ 0)) ยท (๐ต FallFac 0)))
147142, 146oveq12d 7376 . . . . . . . 8 (๐‘˜ = 0 โ†’ ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) = ((๐‘C-1) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ 0)) ยท (๐ต FallFac 0))))
148137, 138, 147fsum1p 15643 . . . . . . 7 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) = (((๐‘C-1) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ 0)) ยท (๐ต FallFac 0))) + ฮฃ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)))))
149 neg1z 12544 . . . . . . . . . . . 12 -1 โˆˆ โ„ค
150 neg1lt0 12275 . . . . . . . . . . . . 13 -1 < 0
151150orci 864 . . . . . . . . . . . 12 (-1 < 0 โˆจ ๐‘ < -1)
152 bcval4 14213 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„•0 โˆง -1 โˆˆ โ„ค โˆง (-1 < 0 โˆจ ๐‘ < -1)) โ†’ (๐‘C-1) = 0)
153149, 151, 152mp3an23 1454 . . . . . . . . . . 11 (๐‘ โˆˆ โ„•0 โ†’ (๐‘C-1) = 0)
1541, 153syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘C-1) = 0)
155154oveq1d 7373 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘C-1) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ 0)) ยท (๐ต FallFac 0))) = (0 ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ 0)) ยท (๐ต FallFac 0))))
156120subid1d 11506 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐‘ + 1) โˆ’ 0) = (๐‘ + 1))
157156oveq2d 7374 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐ด FallFac ((๐‘ + 1) โˆ’ 0)) = (๐ด FallFac (๐‘ + 1)))
158 fallfaccl 15904 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„‚ โˆง (๐‘ + 1) โˆˆ โ„•0) โ†’ (๐ด FallFac (๐‘ + 1)) โˆˆ โ„‚)
1596, 112, 158syl2anc 585 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐ด FallFac (๐‘ + 1)) โˆˆ โ„‚)
160157, 159eqeltrd 2834 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ด FallFac ((๐‘ + 1) โˆ’ 0)) โˆˆ โ„‚)
161 fallfaccl 15904 . . . . . . . . . . . 12 ((๐ต โˆˆ โ„‚ โˆง 0 โˆˆ โ„•0) โ†’ (๐ต FallFac 0) โˆˆ โ„‚)
16210, 123, 161sylancl 587 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ต FallFac 0) โˆˆ โ„‚)
163160, 162mulcld 11180 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ด FallFac ((๐‘ + 1) โˆ’ 0)) ยท (๐ต FallFac 0)) โˆˆ โ„‚)
164163mul02d 11358 . . . . . . . . 9 (๐œ‘ โ†’ (0 ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ 0)) ยท (๐ต FallFac 0))) = 0)
165155, 164eqtrd 2773 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘C-1) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ 0)) ยท (๐ต FallFac 0))) = 0)
166 1zzd 12539 . . . . . . . . . . 11 (๐œ‘ โ†’ 1 โˆˆ โ„ค)
167 0zd 12516 . . . . . . . . . . 11 (๐œ‘ โ†’ 0 โˆˆ โ„ค)
1686, 10, 1binomfallfaclem1 15927 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘— โˆˆ (0...๐‘)) โ†’ ((๐‘C๐‘—) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘—)) ยท (๐ต FallFac (๐‘— + 1)))) โˆˆ โ„‚)
169 oveq2 7366 . . . . . . . . . . . 12 (๐‘— = (๐‘˜ โˆ’ 1) โ†’ (๐‘C๐‘—) = (๐‘C(๐‘˜ โˆ’ 1)))
170 oveq2 7366 . . . . . . . . . . . . . 14 (๐‘— = (๐‘˜ โˆ’ 1) โ†’ (๐‘ โˆ’ ๐‘—) = (๐‘ โˆ’ (๐‘˜ โˆ’ 1)))
171170oveq2d 7374 . . . . . . . . . . . . 13 (๐‘— = (๐‘˜ โˆ’ 1) โ†’ (๐ด FallFac (๐‘ โˆ’ ๐‘—)) = (๐ด FallFac (๐‘ โˆ’ (๐‘˜ โˆ’ 1))))
172 oveq1 7365 . . . . . . . . . . . . . 14 (๐‘— = (๐‘˜ โˆ’ 1) โ†’ (๐‘— + 1) = ((๐‘˜ โˆ’ 1) + 1))
173172oveq2d 7374 . . . . . . . . . . . . 13 (๐‘— = (๐‘˜ โˆ’ 1) โ†’ (๐ต FallFac (๐‘— + 1)) = (๐ต FallFac ((๐‘˜ โˆ’ 1) + 1)))
174171, 173oveq12d 7376 . . . . . . . . . . . 12 (๐‘— = (๐‘˜ โˆ’ 1) โ†’ ((๐ด FallFac (๐‘ โˆ’ ๐‘—)) ยท (๐ต FallFac (๐‘— + 1))) = ((๐ด FallFac (๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ต FallFac ((๐‘˜ โˆ’ 1) + 1))))
175169, 174oveq12d 7376 . . . . . . . . . . 11 (๐‘— = (๐‘˜ โˆ’ 1) โ†’ ((๐‘C๐‘—) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘—)) ยท (๐ต FallFac (๐‘— + 1)))) = ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ด FallFac (๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ต FallFac ((๐‘˜ โˆ’ 1) + 1)))))
176166, 167, 55, 168, 175fsumshft 15670 . . . . . . . . . 10 (๐œ‘ โ†’ ฮฃ๐‘— โˆˆ (0...๐‘)((๐‘C๐‘—) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘—)) ยท (๐ต FallFac (๐‘— + 1)))) = ฮฃ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ด FallFac (๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ต FallFac ((๐‘˜ โˆ’ 1) + 1)))))
17716adantr 482 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ๐‘ โˆˆ โ„‚)
178 elfzelz 13447 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1)) โ†’ ๐‘˜ โˆˆ โ„ค)
179178adantl 483 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ๐‘˜ โˆˆ โ„ค)
180179zcnd 12613 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ๐‘˜ โˆˆ โ„‚)
181 1cnd 11155 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ 1 โˆˆ โ„‚)
182177, 180, 181subsub3d 11547 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (๐‘ โˆ’ (๐‘˜ โˆ’ 1)) = ((๐‘ + 1) โˆ’ ๐‘˜))
183182oveq2d 7374 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (๐ด FallFac (๐‘ โˆ’ (๐‘˜ โˆ’ 1))) = (๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)))
184180, 181npcand 11521 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ((๐‘˜ โˆ’ 1) + 1) = ๐‘˜)
185184oveq2d 7374 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (๐ต FallFac ((๐‘˜ โˆ’ 1) + 1)) = (๐ต FallFac ๐‘˜))
186183, 185oveq12d 7376 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ((๐ด FallFac (๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ต FallFac ((๐‘˜ โˆ’ 1) + 1))) = ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)))
187186oveq2d 7374 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ด FallFac (๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ต FallFac ((๐‘˜ โˆ’ 1) + 1)))) = ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))))
188187sumeq2dv 15593 . . . . . . . . . 10 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ด FallFac (๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ต FallFac ((๐‘˜ โˆ’ 1) + 1)))) = ฮฃ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))))
189176, 188eqtr2d 2774 . . . . . . . . 9 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) = ฮฃ๐‘— โˆˆ (0...๐‘)((๐‘C๐‘—) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘—)) ยท (๐ต FallFac (๐‘— + 1)))))
190 oveq2 7366 . . . . . . . . . . 11 (๐‘˜ = ๐‘— โ†’ (๐‘C๐‘˜) = (๐‘C๐‘—))
191 oveq2 7366 . . . . . . . . . . . . 13 (๐‘˜ = ๐‘— โ†’ (๐‘ โˆ’ ๐‘˜) = (๐‘ โˆ’ ๐‘—))
192191oveq2d 7374 . . . . . . . . . . . 12 (๐‘˜ = ๐‘— โ†’ (๐ด FallFac (๐‘ โˆ’ ๐‘˜)) = (๐ด FallFac (๐‘ โˆ’ ๐‘—)))
193 oveq1 7365 . . . . . . . . . . . . 13 (๐‘˜ = ๐‘— โ†’ (๐‘˜ + 1) = (๐‘— + 1))
194193oveq2d 7374 . . . . . . . . . . . 12 (๐‘˜ = ๐‘— โ†’ (๐ต FallFac (๐‘˜ + 1)) = (๐ต FallFac (๐‘— + 1)))
195192, 194oveq12d 7376 . . . . . . . . . . 11 (๐‘˜ = ๐‘— โ†’ ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1))) = ((๐ด FallFac (๐‘ โˆ’ ๐‘—)) ยท (๐ต FallFac (๐‘— + 1))))
196190, 195oveq12d 7376 . . . . . . . . . 10 (๐‘˜ = ๐‘— โ†’ ((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1)))) = ((๐‘C๐‘—) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘—)) ยท (๐ต FallFac (๐‘— + 1)))))
197196cbvsumv 15586 . . . . . . . . 9 ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1)))) = ฮฃ๐‘— โˆˆ (0...๐‘)((๐‘C๐‘—) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘—)) ยท (๐ต FallFac (๐‘— + 1))))
198189, 197eqtr4di 2791 . . . . . . . 8 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) = ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1)))))
199165, 198oveq12d 7376 . . . . . . 7 (๐œ‘ โ†’ (((๐‘C-1) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ 0)) ยท (๐ต FallFac 0))) + ฮฃ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)))) = (0 + ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1))))))
2006, 10, 1binomfallfaclem1 15927 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1)))) โˆˆ โ„‚)
20179, 200fsumcl 15623 . . . . . . . 8 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1)))) โˆˆ โ„‚)
202201addid2d 11361 . . . . . . 7 (๐œ‘ โ†’ (0 + ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1))))) = ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1)))))
203148, 199, 2023eqtrd 2777 . . . . . 6 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) = ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1)))))
204136, 203oveq12d 7376 . . . . 5 (๐œ‘ โ†’ (ฮฃ๐‘˜ โˆˆ (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 13884 . . . . . 6 (๐œ‘ โ†’ (0...(๐‘ + 1)) โˆˆ Fin)
206205, 103, 138fsumadd 15630 . . . . 5 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))(((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) + ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)))) = (ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) + ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)))))
20779, 133, 200fsumadd 15630 . . . . 5 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...๐‘)(((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) + ((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1))))) = (ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) + ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1))))))
208204, 206, 2073eqtr4d 2783 . . . 4 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))(((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) + ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜)))) = ฮฃ๐‘˜ โˆˆ (0...๐‘)(((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) + ((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1))))))
209100, 208eqtrd 2773 . . 3 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))(((๐‘ + 1)C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) = ฮฃ๐‘˜ โˆˆ (0...๐‘)(((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) + ((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1))))))
210209adantr 482 . 2 ((๐œ‘ โˆง ๐œ“) โ†’ ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))(((๐‘ + 1)C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) = ฮฃ๐‘˜ โˆˆ (0...๐‘)(((๐‘C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))) + ((๐‘C๐‘˜) ยท ((๐ด FallFac (๐‘ โˆ’ ๐‘˜)) ยท (๐ต FallFac (๐‘˜ + 1))))))
21174, 83, 2103eqtr4d 2783 1 ((๐œ‘ โˆง ๐œ“) โ†’ ((๐ด + ๐ต) FallFac (๐‘ + 1)) = ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))(((๐‘ + 1)C๐‘˜) ยท ((๐ด FallFac ((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ต FallFac ๐‘˜))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 397   โˆจ wo 846   = wceq 1542   โˆˆ wcel 2107   โŠ† wss 3911   class class class wbr 5106  โ€˜cfv 6497  (class class class)co 7358  โ„‚cc 11054  0cc0 11056  1c1 11057   + caddc 11059   ยท cmul 11061   < clt 11194   โˆ’ cmin 11390  -cneg 11391  โ„•0cn0 12418  โ„คcz 12504  โ„คโ‰ฅcuz 12768  ...cfz 13430  Ccbc 14208  ฮฃcsu 15576   FallFac cfallfac 15892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-inf2 9582  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133  ax-pre-sup 11134
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-1st 7922  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-er 8651  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-sup 9383  df-oi 9451  df-card 9880  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-div 11818  df-nn 12159  df-2 12221  df-3 12222  df-n0 12419  df-z 12505  df-uz 12769  df-rp 12921  df-fz 13431  df-fzo 13574  df-seq 13913  df-exp 13974  df-fac 14180  df-bc 14209  df-hash 14237  df-cj 14990  df-re 14991  df-im 14992  df-sqrt 15126  df-abs 15127  df-clim 15376  df-sum 15577  df-prod 15794  df-fallfac 15895
This theorem is referenced by:  binomfallfac  15929
  Copyright terms: Public domain W3C validator