Step | Hyp | Ref
| Expression |
1 | | binomfallfaclem.3 |
. . . . . . . 8
โข (๐ โ ๐ โ
โ0) |
2 | | elfzelz 13447 |
. . . . . . . 8
โข (๐ โ (0...๐) โ ๐ โ โค) |
3 | | bccl 14228 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ โค)
โ (๐C๐) โ
โ0) |
4 | 1, 2, 3 | syl2an 597 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...๐)) โ (๐C๐) โ
โ0) |
5 | 4 | nn0cnd 12480 |
. . . . . 6
โข ((๐ โง ๐ โ (0...๐)) โ (๐C๐) โ โ) |
6 | | binomfallfaclem.1 |
. . . . . . . 8
โข (๐ โ ๐ด โ โ) |
7 | | fznn0sub 13479 |
. . . . . . . 8
โข (๐ โ (0...๐) โ (๐ โ ๐) โ
โ0) |
8 | | fallfaccl 15904 |
. . . . . . . 8
โข ((๐ด โ โ โง (๐ โ ๐) โ โ0) โ (๐ด FallFac (๐ โ ๐)) โ โ) |
9 | 6, 7, 8 | syl2an 597 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...๐)) โ (๐ด FallFac (๐ โ ๐)) โ โ) |
10 | | binomfallfaclem.2 |
. . . . . . . 8
โข (๐ โ ๐ต โ โ) |
11 | | elfznn0 13540 |
. . . . . . . 8
โข (๐ โ (0...๐) โ ๐ โ โ0) |
12 | | fallfaccl 15904 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐ โ โ0)
โ (๐ต FallFac ๐) โ
โ) |
13 | 10, 11, 12 | syl2an 597 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...๐)) โ (๐ต FallFac ๐) โ โ) |
14 | 9, 13 | mulcld 11180 |
. . . . . 6
โข ((๐ โง ๐ โ (0...๐)) โ ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)) โ โ) |
15 | 6, 10 | addcld 11179 |
. . . . . . . 8
โข (๐ โ (๐ด + ๐ต) โ โ) |
16 | 1 | nn0cnd 12480 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
17 | 15, 16 | subcld 11517 |
. . . . . . 7
โข (๐ โ ((๐ด + ๐ต) โ ๐) โ โ) |
18 | 17 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โ (0...๐)) โ ((๐ด + ๐ต) โ ๐) โ โ) |
19 | 5, 14, 18 | mulassd 11183 |
. . . . 5
โข ((๐ โง ๐ โ (0...๐)) โ (((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) ยท ((๐ด + ๐ต) โ ๐)) = ((๐C๐) ยท (((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)) ยท ((๐ด + ๐ต) โ ๐)))) |
20 | 7 | nn0cnd 12480 |
. . . . . . . . 9
โข (๐ โ (0...๐) โ (๐ โ ๐) โ โ) |
21 | | subcl 11405 |
. . . . . . . . 9
โข ((๐ด โ โ โง (๐ โ ๐) โ โ) โ (๐ด โ (๐ โ ๐)) โ โ) |
22 | 6, 20, 21 | syl2an 597 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...๐)) โ (๐ด โ (๐ โ ๐)) โ โ) |
23 | 11 | nn0cnd 12480 |
. . . . . . . . 9
โข (๐ โ (0...๐) โ ๐ โ โ) |
24 | | subcl 11405 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐ โ โ) โ (๐ต โ ๐) โ โ) |
25 | 10, 23, 24 | syl2an 597 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...๐)) โ (๐ต โ ๐) โ โ) |
26 | 14, 22, 25 | adddid 11184 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...๐)) โ (((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)) ยท ((๐ด โ (๐ โ ๐)) + (๐ต โ ๐))) = ((((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)) ยท (๐ด โ (๐ โ ๐))) + (((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)) ยท (๐ต โ ๐)))) |
27 | 6 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (0...๐)) โ ๐ด โ โ) |
28 | 16 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (0...๐)) โ ๐ โ โ) |
29 | 27, 28 | subcld 11517 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (0...๐)) โ (๐ด โ ๐) โ โ) |
30 | 23 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (0...๐)) โ ๐ โ โ) |
31 | 10 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (0...๐)) โ ๐ต โ โ) |
32 | 29, 30, 31 | ppncand 11557 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...๐)) โ (((๐ด โ ๐) + ๐) + (๐ต โ ๐)) = ((๐ด โ ๐) + ๐ต)) |
33 | 27, 28, 30 | subsubd 11545 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (0...๐)) โ (๐ด โ (๐ โ ๐)) = ((๐ด โ ๐) + ๐)) |
34 | 33 | oveq1d 7373 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...๐)) โ ((๐ด โ (๐ โ ๐)) + (๐ต โ ๐)) = (((๐ด โ ๐) + ๐) + (๐ต โ ๐))) |
35 | 27, 31, 28 | addsubd 11538 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...๐)) โ ((๐ด + ๐ต) โ ๐) = ((๐ด โ ๐) + ๐ต)) |
36 | 32, 34, 35 | 3eqtr4d 2783 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...๐)) โ ((๐ด โ (๐ โ ๐)) + (๐ต โ ๐)) = ((๐ด + ๐ต) โ ๐)) |
37 | 36 | oveq2d 7374 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...๐)) โ (((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)) ยท ((๐ด โ (๐ โ ๐)) + (๐ต โ ๐))) = (((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)) ยท ((๐ด + ๐ต) โ ๐))) |
38 | 9, 13, 22 | mul32d 11370 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...๐)) โ (((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)) ยท (๐ด โ (๐ โ ๐))) = (((๐ด FallFac (๐ โ ๐)) ยท (๐ด โ (๐ โ ๐))) ยท (๐ต FallFac ๐))) |
39 | | 1cnd 11155 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (0...๐)) โ 1 โ โ) |
40 | 28, 39, 30 | addsubd 11538 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (0...๐)) โ ((๐ + 1) โ ๐) = ((๐ โ ๐) + 1)) |
41 | 40 | oveq2d 7374 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (0...๐)) โ (๐ด FallFac ((๐ + 1) โ ๐)) = (๐ด FallFac ((๐ โ ๐) + 1))) |
42 | | fallfacp1 15918 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง (๐ โ ๐) โ โ0) โ (๐ด FallFac ((๐ โ ๐) + 1)) = ((๐ด FallFac (๐ โ ๐)) ยท (๐ด โ (๐ โ ๐)))) |
43 | 6, 7, 42 | syl2an 597 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (0...๐)) โ (๐ด FallFac ((๐ โ ๐) + 1)) = ((๐ด FallFac (๐ โ ๐)) ยท (๐ด โ (๐ โ ๐)))) |
44 | 41, 43 | eqtrd 2773 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (0...๐)) โ (๐ด FallFac ((๐ + 1) โ ๐)) = ((๐ด FallFac (๐ โ ๐)) ยท (๐ด โ (๐ โ ๐)))) |
45 | 44 | oveq1d 7373 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...๐)) โ ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)) = (((๐ด FallFac (๐ โ ๐)) ยท (๐ด โ (๐ โ ๐))) ยท (๐ต FallFac ๐))) |
46 | 38, 45 | eqtr4d 2776 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...๐)) โ (((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)) ยท (๐ด โ (๐ โ ๐))) = ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) |
47 | 9, 13, 25 | mulassd 11183 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...๐)) โ (((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)) ยท (๐ต โ ๐)) = ((๐ด FallFac (๐ โ ๐)) ยท ((๐ต FallFac ๐) ยท (๐ต โ ๐)))) |
48 | | fallfacp1 15918 |
. . . . . . . . . . 11
โข ((๐ต โ โ โง ๐ โ โ0)
โ (๐ต FallFac (๐ + 1)) = ((๐ต FallFac ๐) ยท (๐ต โ ๐))) |
49 | 10, 11, 48 | syl2an 597 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (0...๐)) โ (๐ต FallFac (๐ + 1)) = ((๐ต FallFac ๐) ยท (๐ต โ ๐))) |
50 | 49 | oveq2d 7374 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...๐)) โ ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1))) = ((๐ด FallFac (๐ โ ๐)) ยท ((๐ต FallFac ๐) ยท (๐ต โ ๐)))) |
51 | 47, 50 | eqtr4d 2776 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...๐)) โ (((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)) ยท (๐ต โ ๐)) = ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1)))) |
52 | 46, 51 | oveq12d 7376 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...๐)) โ ((((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)) ยท (๐ด โ (๐ โ ๐))) + (((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)) ยท (๐ต โ ๐))) = (((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)) + ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1))))) |
53 | 26, 37, 52 | 3eqtr3d 2781 |
. . . . . 6
โข ((๐ โง ๐ โ (0...๐)) โ (((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)) ยท ((๐ด + ๐ต) โ ๐)) = (((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)) + ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1))))) |
54 | 53 | oveq2d 7374 |
. . . . 5
โข ((๐ โง ๐ โ (0...๐)) โ ((๐C๐) ยท (((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)) ยท ((๐ด + ๐ต) โ ๐))) = ((๐C๐) ยท (((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)) + ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1)))))) |
55 | 1 | nn0zd 12530 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โค) |
56 | | uzid 12783 |
. . . . . . . . . 10
โข (๐ โ โค โ ๐ โ
(โคโฅโ๐)) |
57 | | peano2uz 12831 |
. . . . . . . . . 10
โข (๐ โ
(โคโฅโ๐) โ (๐ + 1) โ
(โคโฅโ๐)) |
58 | | fzss2 13487 |
. . . . . . . . . 10
โข ((๐ + 1) โ
(โคโฅโ๐) โ (0...๐) โ (0...(๐ + 1))) |
59 | 55, 56, 57, 58 | 4syl 19 |
. . . . . . . . 9
โข (๐ โ (0...๐) โ (0...(๐ + 1))) |
60 | 59 | sselda 3945 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...๐)) โ ๐ โ (0...(๐ + 1))) |
61 | | fznn0sub 13479 |
. . . . . . . . 9
โข (๐ โ (0...(๐ + 1)) โ ((๐ + 1) โ ๐) โ
โ0) |
62 | | fallfaccl 15904 |
. . . . . . . . 9
โข ((๐ด โ โ โง ((๐ + 1) โ ๐) โ โ0) โ (๐ด FallFac ((๐ + 1) โ ๐)) โ โ) |
63 | 6, 61, 62 | syl2an 597 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...(๐ + 1))) โ (๐ด FallFac ((๐ + 1) โ ๐)) โ โ) |
64 | 60, 63 | syldan 592 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...๐)) โ (๐ด FallFac ((๐ + 1) โ ๐)) โ โ) |
65 | 64, 13 | mulcld 11180 |
. . . . . 6
โข ((๐ โง ๐ โ (0...๐)) โ ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)) โ โ) |
66 | | peano2nn0 12458 |
. . . . . . . . 9
โข (๐ โ โ0
โ (๐ + 1) โ
โ0) |
67 | 11, 66 | syl 17 |
. . . . . . . 8
โข (๐ โ (0...๐) โ (๐ + 1) โ
โ0) |
68 | | fallfaccl 15904 |
. . . . . . . 8
โข ((๐ต โ โ โง (๐ + 1) โ
โ0) โ (๐ต FallFac (๐ + 1)) โ โ) |
69 | 10, 67, 68 | syl2an 597 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...๐)) โ (๐ต FallFac (๐ + 1)) โ โ) |
70 | 9, 69 | mulcld 11180 |
. . . . . 6
โข ((๐ โง ๐ โ (0...๐)) โ ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1))) โ โ) |
71 | 5, 65, 70 | adddid 11184 |
. . . . 5
โข ((๐ โง ๐ โ (0...๐)) โ ((๐C๐) ยท (((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)) + ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1))))) = (((๐C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) + ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1)))))) |
72 | 19, 54, 71 | 3eqtrd 2777 |
. . . 4
โข ((๐ โง ๐ โ (0...๐)) โ (((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) ยท ((๐ด + ๐ต) โ ๐)) = (((๐C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) + ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1)))))) |
73 | 72 | sumeq2dv 15593 |
. . 3
โข (๐ โ ฮฃ๐ โ (0...๐)(((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) ยท ((๐ด + ๐ต) โ ๐)) = ฮฃ๐ โ (0...๐)(((๐C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) + ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1)))))) |
74 | 73 | adantr 482 |
. 2
โข ((๐ โง ๐) โ ฮฃ๐ โ (0...๐)(((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) ยท ((๐ด + ๐ต) โ ๐)) = ฮฃ๐ โ (0...๐)(((๐C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) + ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1)))))) |
75 | 15, 1 | fallfacp1d 15920 |
. . . 4
โข (๐ โ ((๐ด + ๐ต) FallFac (๐ + 1)) = (((๐ด + ๐ต) FallFac ๐) ยท ((๐ด + ๐ต) โ ๐))) |
76 | | binomfallfaclem.4 |
. . . . 5
โข (๐ โ ((๐ด + ๐ต) FallFac ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)))) |
77 | 76 | oveq1d 7373 |
. . . 4
โข (๐ โ (((๐ด + ๐ต) FallFac ๐) ยท ((๐ด + ๐ต) โ ๐)) = (ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) ยท ((๐ด + ๐ต) โ ๐))) |
78 | 75, 77 | sylan9eq 2793 |
. . 3
โข ((๐ โง ๐) โ ((๐ด + ๐ต) FallFac (๐ + 1)) = (ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) ยท ((๐ด + ๐ต) โ ๐))) |
79 | | fzfid 13884 |
. . . . 5
โข (๐ โ (0...๐) โ Fin) |
80 | 5, 14 | mulcld 11180 |
. . . . 5
โข ((๐ โง ๐ โ (0...๐)) โ ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) โ โ) |
81 | 79, 17, 80 | fsummulc1 15675 |
. . . 4
โข (๐ โ (ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) ยท ((๐ด + ๐ต) โ ๐)) = ฮฃ๐ โ (0...๐)(((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) ยท ((๐ด + ๐ต) โ ๐))) |
82 | 81 | adantr 482 |
. . 3
โข ((๐ โง ๐) โ (ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) ยท ((๐ด + ๐ต) โ ๐)) = ฮฃ๐ โ (0...๐)(((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) ยท ((๐ด + ๐ต) โ ๐))) |
83 | 78, 82 | eqtrd 2773 |
. 2
โข ((๐ โง ๐) โ ((๐ด + ๐ต) FallFac (๐ + 1)) = ฮฃ๐ โ (0...๐)(((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐))) ยท ((๐ด + ๐ต) โ ๐))) |
84 | | elfzelz 13447 |
. . . . . . . 8
โข (๐ โ (0...(๐ + 1)) โ ๐ โ โค) |
85 | | bcpasc 14227 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ โค)
โ ((๐C๐) + (๐C(๐ โ 1))) = ((๐ + 1)C๐)) |
86 | 1, 84, 85 | syl2an 597 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ + 1))) โ ((๐C๐) + (๐C(๐ โ 1))) = ((๐ + 1)C๐)) |
87 | 86 | oveq1d 7373 |
. . . . . 6
โข ((๐ โง ๐ โ (0...(๐ + 1))) โ (((๐C๐) + (๐C(๐ โ 1))) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) = (((๐ + 1)C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)))) |
88 | 1, 84, 3 | syl2an 597 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...(๐ + 1))) โ (๐C๐) โ
โ0) |
89 | 88 | nn0cnd 12480 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ + 1))) โ (๐C๐) โ โ) |
90 | | peano2zm 12551 |
. . . . . . . . . 10
โข (๐ โ โค โ (๐ โ 1) โ
โค) |
91 | 84, 90 | syl 17 |
. . . . . . . . 9
โข (๐ โ (0...(๐ + 1)) โ (๐ โ 1) โ โค) |
92 | | bccl 14228 |
. . . . . . . . 9
โข ((๐ โ โ0
โง (๐ โ 1) โ
โค) โ (๐C(๐ โ 1)) โ
โ0) |
93 | 1, 91, 92 | syl2an 597 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...(๐ + 1))) โ (๐C(๐ โ 1)) โ
โ0) |
94 | 93 | nn0cnd 12480 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ + 1))) โ (๐C(๐ โ 1)) โ โ) |
95 | | elfznn0 13540 |
. . . . . . . . 9
โข (๐ โ (0...(๐ + 1)) โ ๐ โ โ0) |
96 | 10, 95, 12 | syl2an 597 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...(๐ + 1))) โ (๐ต FallFac ๐) โ โ) |
97 | 63, 96 | mulcld 11180 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ + 1))) โ ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)) โ โ) |
98 | 89, 94, 97 | adddird 11185 |
. . . . . 6
โข ((๐ โง ๐ โ (0...(๐ + 1))) โ (((๐C๐) + (๐C(๐ โ 1))) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) = (((๐C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) + ((๐C(๐ โ 1)) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))))) |
99 | 87, 98 | eqtr3d 2775 |
. . . . 5
โข ((๐ โง ๐ โ (0...(๐ + 1))) โ (((๐ + 1)C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) = (((๐C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) + ((๐C(๐ โ 1)) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))))) |
100 | 99 | sumeq2dv 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) |
102 | 1, 101 | eleqtrdi 2844 |
. . . . . . . 8
โข (๐ โ ๐ โ
(โคโฅโ0)) |
103 | 89, 97 | mulcld 11180 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...(๐ + 1))) โ ((๐C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) โ โ) |
104 | | oveq2 7366 |
. . . . . . . . 9
โข (๐ = (๐ + 1) โ (๐C๐) = (๐C(๐ + 1))) |
105 | | oveq2 7366 |
. . . . . . . . . . 11
โข (๐ = (๐ + 1) โ ((๐ + 1) โ ๐) = ((๐ + 1) โ (๐ + 1))) |
106 | 105 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ = (๐ + 1) โ (๐ด FallFac ((๐ + 1) โ ๐)) = (๐ด FallFac ((๐ + 1) โ (๐ + 1)))) |
107 | | oveq2 7366 |
. . . . . . . . . 10
โข (๐ = (๐ + 1) โ (๐ต FallFac ๐) = (๐ต FallFac (๐ + 1))) |
108 | 106, 107 | oveq12d 7376 |
. . . . . . . . 9
โข (๐ = (๐ + 1) โ ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)) = ((๐ด FallFac ((๐ + 1) โ (๐ + 1))) ยท (๐ต FallFac (๐ + 1)))) |
109 | 104, 108 | oveq12d 7376 |
. . . . . . . 8
โข (๐ = (๐ + 1) โ ((๐C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) = ((๐C(๐ + 1)) ยท ((๐ด FallFac ((๐ + 1) โ (๐ + 1))) ยท (๐ต FallFac (๐ + 1))))) |
110 | 102, 103,
109 | fsump1 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) |
112 | 1, 111 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ (๐ + 1) โ
โ0) |
113 | 112 | nn0zd 12530 |
. . . . . . . . . . 11
โข (๐ โ (๐ + 1) โ โค) |
114 | 1 | nn0red 12479 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
115 | 114 | ltp1d 12090 |
. . . . . . . . . . . 12
โข (๐ โ ๐ < (๐ + 1)) |
116 | 115 | olcd 873 |
. . . . . . . . . . 11
โข (๐ โ ((๐ + 1) < 0 โจ ๐ < (๐ + 1))) |
117 | | bcval4 14213 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง (๐ + 1) โ
โค โง ((๐ + 1) <
0 โจ ๐ < (๐ + 1))) โ (๐C(๐ + 1)) = 0) |
118 | 1, 113, 116, 117 | syl3anc 1372 |
. . . . . . . . . 10
โข (๐ โ (๐C(๐ + 1)) = 0) |
119 | 118 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ โ ((๐C(๐ + 1)) ยท ((๐ด FallFac ((๐ + 1) โ (๐ + 1))) ยท (๐ต FallFac (๐ + 1)))) = (0 ยท ((๐ด FallFac ((๐ + 1) โ (๐ + 1))) ยท (๐ต FallFac (๐ + 1))))) |
120 | 112 | nn0cnd 12480 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ + 1) โ โ) |
121 | 120 | subidd 11505 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ + 1) โ (๐ + 1)) = 0) |
122 | 121 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ โ (๐ด FallFac ((๐ + 1) โ (๐ + 1))) = (๐ด FallFac 0)) |
123 | | 0nn0 12433 |
. . . . . . . . . . . . 13
โข 0 โ
โ0 |
124 | | fallfaccl 15904 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง 0 โ
โ0) โ (๐ด FallFac 0) โ โ) |
125 | 6, 123, 124 | sylancl 587 |
. . . . . . . . . . . 12
โข (๐ โ (๐ด FallFac 0) โ โ) |
126 | 122, 125 | eqeltrd 2834 |
. . . . . . . . . . 11
โข (๐ โ (๐ด FallFac ((๐ + 1) โ (๐ + 1))) โ โ) |
127 | | fallfaccl 15904 |
. . . . . . . . . . . 12
โข ((๐ต โ โ โง (๐ + 1) โ
โ0) โ (๐ต FallFac (๐ + 1)) โ โ) |
128 | 10, 112, 127 | syl2anc 585 |
. . . . . . . . . . 11
โข (๐ โ (๐ต FallFac (๐ + 1)) โ โ) |
129 | 126, 128 | mulcld 11180 |
. . . . . . . . . 10
โข (๐ โ ((๐ด FallFac ((๐ + 1) โ (๐ + 1))) ยท (๐ต FallFac (๐ + 1))) โ โ) |
130 | 129 | mul02d 11358 |
. . . . . . . . 9
โข (๐ โ (0 ยท ((๐ด FallFac ((๐ + 1) โ (๐ + 1))) ยท (๐ต FallFac (๐ + 1)))) = 0) |
131 | 119, 130 | eqtrd 2773 |
. . . . . . . 8
โข (๐ โ ((๐C(๐ + 1)) ยท ((๐ด FallFac ((๐ + 1) โ (๐ + 1))) ยท (๐ต FallFac (๐ + 1)))) = 0) |
132 | 131 | oveq2d 7374 |
. . . . . . 7
โข (๐ โ (ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) + ((๐C(๐ + 1)) ยท ((๐ด FallFac ((๐ + 1) โ (๐ + 1))) ยท (๐ต FallFac (๐ + 1))))) = (ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) + 0)) |
133 | 60, 103 | syldan 592 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...๐)) โ ((๐C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) โ โ) |
134 | 79, 133 | fsumcl 15623 |
. . . . . . . 8
โข (๐ โ ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) โ โ) |
135 | 134 | addid1d 11360 |
. . . . . . 7
โข (๐ โ (ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) + 0) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)))) |
136 | 110, 132,
135 | 3eqtrd 2777 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ (0...(๐ + 1))((๐C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)))) |
137 | 112, 101 | eleqtrdi 2844 |
. . . . . . . 8
โข (๐ โ (๐ + 1) โ
(โคโฅโ0)) |
138 | 94, 97 | mulcld 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) |
141 | 139, 140 | eqtr4di 2791 |
. . . . . . . . . 10
โข (๐ = 0 โ (๐ โ 1) = -1) |
142 | 141 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ = 0 โ (๐C(๐ โ 1)) = (๐C-1)) |
143 | | oveq2 7366 |
. . . . . . . . . . 11
โข (๐ = 0 โ ((๐ + 1) โ ๐) = ((๐ + 1) โ 0)) |
144 | 143 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ = 0 โ (๐ด FallFac ((๐ + 1) โ ๐)) = (๐ด FallFac ((๐ + 1) โ 0))) |
145 | | oveq2 7366 |
. . . . . . . . . 10
โข (๐ = 0 โ (๐ต FallFac ๐) = (๐ต FallFac 0)) |
146 | 144, 145 | oveq12d 7376 |
. . . . . . . . 9
โข (๐ = 0 โ ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)) = ((๐ด FallFac ((๐ + 1) โ 0)) ยท (๐ต FallFac 0))) |
147 | 142, 146 | oveq12d 7376 |
. . . . . . . 8
โข (๐ = 0 โ ((๐C(๐ โ 1)) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) = ((๐C-1) ยท ((๐ด FallFac ((๐ + 1) โ 0)) ยท (๐ต FallFac 0)))) |
148 | 137, 138,
147 | fsum1p 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 |
151 | 150 | orci 864 |
. . . . . . . . . . . 12
โข (-1 <
0 โจ ๐ <
-1) |
152 | | bcval4 14213 |
. . . . . . . . . . . 12
โข ((๐ โ โ0
โง -1 โ โค โง (-1 < 0 โจ ๐ < -1)) โ (๐C-1) = 0) |
153 | 149, 151,
152 | mp3an23 1454 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ (๐C-1) =
0) |
154 | 1, 153 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (๐C-1) = 0) |
155 | 154 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ โ ((๐C-1) ยท ((๐ด FallFac ((๐ + 1) โ 0)) ยท (๐ต FallFac 0))) = (0 ยท
((๐ด FallFac ((๐ + 1) โ 0)) ยท
(๐ต FallFac
0)))) |
156 | 120 | subid1d 11506 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ + 1) โ 0) = (๐ + 1)) |
157 | 156 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ โ (๐ด FallFac ((๐ + 1) โ 0)) = (๐ด FallFac (๐ + 1))) |
158 | | fallfaccl 15904 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง (๐ + 1) โ
โ0) โ (๐ด FallFac (๐ + 1)) โ โ) |
159 | 6, 112, 158 | syl2anc 585 |
. . . . . . . . . . . 12
โข (๐ โ (๐ด FallFac (๐ + 1)) โ โ) |
160 | 157, 159 | eqeltrd 2834 |
. . . . . . . . . . 11
โข (๐ โ (๐ด FallFac ((๐ + 1) โ 0)) โ
โ) |
161 | | fallfaccl 15904 |
. . . . . . . . . . . 12
โข ((๐ต โ โ โง 0 โ
โ0) โ (๐ต FallFac 0) โ โ) |
162 | 10, 123, 161 | sylancl 587 |
. . . . . . . . . . 11
โข (๐ โ (๐ต FallFac 0) โ โ) |
163 | 160, 162 | mulcld 11180 |
. . . . . . . . . 10
โข (๐ โ ((๐ด FallFac ((๐ + 1) โ 0)) ยท (๐ต FallFac 0)) โ
โ) |
164 | 163 | mul02d 11358 |
. . . . . . . . 9
โข (๐ โ (0 ยท ((๐ด FallFac ((๐ + 1) โ 0)) ยท (๐ต FallFac 0))) =
0) |
165 | 155, 164 | eqtrd 2773 |
. . . . . . . 8
โข (๐ โ ((๐C-1) ยท ((๐ด FallFac ((๐ + 1) โ 0)) ยท (๐ต FallFac 0))) =
0) |
166 | | 1zzd 12539 |
. . . . . . . . . . 11
โข (๐ โ 1 โ
โค) |
167 | | 0zd 12516 |
. . . . . . . . . . 11
โข (๐ โ 0 โ
โค) |
168 | 6, 10, 1 | binomfallfaclem1 15927 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (0...๐)) โ ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1)))) โ โ) |
169 | | oveq2 7366 |
. . . . . . . . . . . 12
โข (๐ = (๐ โ 1) โ (๐C๐) = (๐C(๐ โ 1))) |
170 | | oveq2 7366 |
. . . . . . . . . . . . . 14
โข (๐ = (๐ โ 1) โ (๐ โ ๐) = (๐ โ (๐ โ 1))) |
171 | 170 | oveq2d 7374 |
. . . . . . . . . . . . 13
โข (๐ = (๐ โ 1) โ (๐ด FallFac (๐ โ ๐)) = (๐ด FallFac (๐ โ (๐ โ 1)))) |
172 | | oveq1 7365 |
. . . . . . . . . . . . . 14
โข (๐ = (๐ โ 1) โ (๐ + 1) = ((๐ โ 1) + 1)) |
173 | 172 | oveq2d 7374 |
. . . . . . . . . . . . 13
โข (๐ = (๐ โ 1) โ (๐ต FallFac (๐ + 1)) = (๐ต FallFac ((๐ โ 1) + 1))) |
174 | 171, 173 | oveq12d 7376 |
. . . . . . . . . . . 12
โข (๐ = (๐ โ 1) โ ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1))) = ((๐ด FallFac (๐ โ (๐ โ 1))) ยท (๐ต FallFac ((๐ โ 1) + 1)))) |
175 | 169, 174 | oveq12d 7376 |
. . . . . . . . . . 11
โข (๐ = (๐ โ 1) โ ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1)))) = ((๐C(๐ โ 1)) ยท ((๐ด FallFac (๐ โ (๐ โ 1))) ยท (๐ต FallFac ((๐ โ 1) + 1))))) |
176 | 166, 167,
55, 168, 175 | fsumshft 15670 |
. . . . . . . . . 10
โข (๐ โ ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1)))) = ฮฃ๐ โ ((0 + 1)...(๐ + 1))((๐C(๐ โ 1)) ยท ((๐ด FallFac (๐ โ (๐ โ 1))) ยท (๐ต FallFac ((๐ โ 1) + 1))))) |
177 | 16 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ ๐ โ โ) |
178 | | elfzelz 13447 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((0 + 1)...(๐ + 1)) โ ๐ โ โค) |
179 | 178 | adantl 483 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ ๐ โ โค) |
180 | 179 | zcnd 12613 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ ๐ โ โ) |
181 | | 1cnd 11155 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ 1 โ
โ) |
182 | 177, 180,
181 | subsub3d 11547 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ (๐ โ (๐ โ 1)) = ((๐ + 1) โ ๐)) |
183 | 182 | oveq2d 7374 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ (๐ด FallFac (๐ โ (๐ โ 1))) = (๐ด FallFac ((๐ + 1) โ ๐))) |
184 | 180, 181 | npcand 11521 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ ((๐ โ 1) + 1) = ๐) |
185 | 184 | oveq2d 7374 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ (๐ต FallFac ((๐ โ 1) + 1)) = (๐ต FallFac ๐)) |
186 | 183, 185 | oveq12d 7376 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ ((๐ด FallFac (๐ โ (๐ โ 1))) ยท (๐ต FallFac ((๐ โ 1) + 1))) = ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) |
187 | 186 | oveq2d 7374 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ((0 + 1)...(๐ + 1))) โ ((๐C(๐ โ 1)) ยท ((๐ด FallFac (๐ โ (๐ โ 1))) ยท (๐ต FallFac ((๐ โ 1) + 1)))) = ((๐C(๐ โ 1)) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)))) |
188 | 187 | sumeq2dv 15593 |
. . . . . . . . . 10
โข (๐ โ ฮฃ๐ โ ((0 + 1)...(๐ + 1))((๐C(๐ โ 1)) ยท ((๐ด FallFac (๐ โ (๐ โ 1))) ยท (๐ต FallFac ((๐ โ 1) + 1)))) = ฮฃ๐ โ ((0 + 1)...(๐ + 1))((๐C(๐ โ 1)) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)))) |
189 | 176, 188 | eqtr2d 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
โข (๐ = ๐ โ (๐ โ ๐) = (๐ โ ๐)) |
192 | 191 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ด FallFac (๐ โ ๐)) = (๐ด FallFac (๐ โ ๐))) |
193 | | oveq1 7365 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐ + 1) = (๐ + 1)) |
194 | 193 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ต FallFac (๐ + 1)) = (๐ต FallFac (๐ + 1))) |
195 | 192, 194 | oveq12d 7376 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1))) = ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1)))) |
196 | 190, 195 | oveq12d 7376 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1)))) = ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1))))) |
197 | 196 | cbvsumv 15586 |
. . . . . . . . 9
โข
ฮฃ๐ โ
(0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1)))) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1)))) |
198 | 189, 197 | eqtr4di 2791 |
. . . . . . . 8
โข (๐ โ ฮฃ๐ โ ((0 + 1)...(๐ + 1))((๐C(๐ โ 1)) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1))))) |
199 | 165, 198 | oveq12d 7376 |
. . . . . . 7
โข (๐ โ (((๐C-1) ยท ((๐ด FallFac ((๐ + 1) โ 0)) ยท (๐ต FallFac 0))) + ฮฃ๐ โ ((0 + 1)...(๐ + 1))((๐C(๐ โ 1)) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)))) = (0 + ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1)))))) |
200 | 6, 10, 1 | binomfallfaclem1 15927 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...๐)) โ ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1)))) โ โ) |
201 | 79, 200 | fsumcl 15623 |
. . . . . . . 8
โข (๐ โ ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1)))) โ โ) |
202 | 201 | addid2d 11361 |
. . . . . . 7
โข (๐ โ (0 + ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1))))) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1))))) |
203 | 148, 199,
202 | 3eqtrd 2777 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ (0...(๐ + 1))((๐C(๐ โ 1)) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1))))) |
204 | 136, 203 | oveq12d 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) |
206 | 205, 103,
138 | fsumadd 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 ๐))))) |
207 | 79, 133, 200 | fsumadd 15630 |
. . . . 5
โข (๐ โ ฮฃ๐ โ (0...๐)(((๐C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) + ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1))))) = (ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) + ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1)))))) |
208 | 204, 206,
207 | 3eqtr4d 2783 |
. . . 4
โข (๐ โ ฮฃ๐ โ (0...(๐ + 1))(((๐C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) + ((๐C(๐ โ 1)) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)))) = ฮฃ๐ โ (0...๐)(((๐C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) + ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1)))))) |
209 | 100, 208 | eqtrd 2773 |
. . 3
โข (๐ โ ฮฃ๐ โ (0...(๐ + 1))(((๐ + 1)C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) = ฮฃ๐ โ (0...๐)(((๐C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) + ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1)))))) |
210 | 209 | adantr 482 |
. 2
โข ((๐ โง ๐) โ ฮฃ๐ โ (0...(๐ + 1))(((๐ + 1)C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) = ฮฃ๐ โ (0...๐)(((๐C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐))) + ((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac (๐ + 1)))))) |
211 | 74, 83, 210 | 3eqtr4d 2783 |
1
โข ((๐ โง ๐) โ ((๐ด + ๐ต) FallFac (๐ + 1)) = ฮฃ๐ โ (0...(๐ + 1))(((๐ + 1)C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)))) |