Step | Hyp | Ref
| Expression |
1 | | fzfid 13885 |
. . 3
โข ((๐ด โ โ โง ๐ โ โ0)
โ (0...(๐ โ 1))
โ Fin) |
2 | | fzssp1 13491 |
. . . . . 6
โข
(0...(๐ โ 1))
โ (0...((๐ โ 1)
+ 1)) |
3 | | nn0cn 12430 |
. . . . . . . . 9
โข (๐ โ โ0
โ ๐ โ
โ) |
4 | 3 | adantl 483 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ0)
โ ๐ โ
โ) |
5 | | ax-1cn 11116 |
. . . . . . . 8
โข 1 โ
โ |
6 | | npcan 11417 |
. . . . . . . 8
โข ((๐ โ โ โง 1 โ
โ) โ ((๐ โ
1) + 1) = ๐) |
7 | 4, 5, 6 | sylancl 587 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ0)
โ ((๐ โ 1) + 1)
= ๐) |
8 | 7 | oveq2d 7378 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ0)
โ (0...((๐ โ 1)
+ 1)) = (0...๐)) |
9 | 2, 8 | sseqtrid 4001 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ0)
โ (0...(๐ โ 1))
โ (0...๐)) |
10 | 9 | sselda 3949 |
. . . 4
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ (0...(๐ โ 1))) โ ๐ โ (0...๐)) |
11 | | bccl2 14230 |
. . . . . . 7
โข (๐ โ (0...๐) โ (๐C๐) โ โ) |
12 | 11 | adantl 483 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ (0...๐)) โ (๐C๐) โ โ) |
13 | 12 | nncnd 12176 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ (0...๐)) โ (๐C๐) โ โ) |
14 | | simpl 484 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ0)
โ ๐ด โ
โ) |
15 | | elfznn0 13541 |
. . . . . 6
โข (๐ โ (0...๐) โ ๐ โ โ0) |
16 | | expcl 13992 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
17 | 14, 15, 16 | syl2an 597 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ (0...๐)) โ (๐ดโ๐) โ โ) |
18 | 13, 17 | mulcld 11182 |
. . . 4
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ (0...๐)) โ ((๐C๐) ยท (๐ดโ๐)) โ โ) |
19 | 10, 18 | syldan 592 |
. . 3
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ (0...(๐ โ 1))) โ ((๐C๐) ยท (๐ดโ๐)) โ โ) |
20 | 1, 19 | fsumcl 15625 |
. 2
โข ((๐ด โ โ โง ๐ โ โ0)
โ ฮฃ๐ โ
(0...(๐ โ 1))((๐C๐) ยท (๐ดโ๐)) โ โ) |
21 | | expcl 13992 |
. 2
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
22 | | addcom 11348 |
. . . . 5
โข ((๐ด โ โ โง 1 โ
โ) โ (๐ด + 1) =
(1 + ๐ด)) |
23 | 14, 5, 22 | sylancl 587 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ด + 1) = (1 + ๐ด)) |
24 | 23 | oveq1d 7377 |
. . 3
โข ((๐ด โ โ โง ๐ โ โ0)
โ ((๐ด + 1)โ๐) = ((1 + ๐ด)โ๐)) |
25 | | binom1p 15723 |
. . 3
โข ((๐ด โ โ โง ๐ โ โ0)
โ ((1 + ๐ด)โ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท (๐ดโ๐))) |
26 | | simpr 486 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ0)
โ ๐ โ
โ0) |
27 | | nn0uz 12812 |
. . . . . 6
โข
โ0 = (โคโฅโ0) |
28 | 26, 27 | eleqtrdi 2848 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ0)
โ ๐ โ
(โคโฅโ0)) |
29 | | oveq2 7370 |
. . . . . 6
โข (๐ = ๐ โ (๐C๐) = (๐C๐)) |
30 | | oveq2 7370 |
. . . . . 6
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
31 | 29, 30 | oveq12d 7380 |
. . . . 5
โข (๐ = ๐ โ ((๐C๐) ยท (๐ดโ๐)) = ((๐C๐) ยท (๐ดโ๐))) |
32 | 28, 18, 31 | fsumm1 15643 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ0)
โ ฮฃ๐ โ
(0...๐)((๐C๐) ยท (๐ดโ๐)) = (ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท (๐ดโ๐)) + ((๐C๐) ยท (๐ดโ๐)))) |
33 | | bcnn 14219 |
. . . . . . . 8
โข (๐ โ โ0
โ (๐C๐) = 1) |
34 | 33 | adantl 483 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐C๐) = 1) |
35 | 34 | oveq1d 7377 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ0)
โ ((๐C๐) ยท (๐ดโ๐)) = (1 ยท (๐ดโ๐))) |
36 | 21 | mulid2d 11180 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ0)
โ (1 ยท (๐ดโ๐)) = (๐ดโ๐)) |
37 | 35, 36 | eqtrd 2777 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ0)
โ ((๐C๐) ยท (๐ดโ๐)) = (๐ดโ๐)) |
38 | 37 | oveq2d 7378 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ0)
โ (ฮฃ๐ โ
(0...(๐ โ 1))((๐C๐) ยท (๐ดโ๐)) + ((๐C๐) ยท (๐ดโ๐))) = (ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท (๐ดโ๐)) + (๐ดโ๐))) |
39 | 32, 38 | eqtrd 2777 |
. . 3
โข ((๐ด โ โ โง ๐ โ โ0)
โ ฮฃ๐ โ
(0...๐)((๐C๐) ยท (๐ดโ๐)) = (ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท (๐ดโ๐)) + (๐ดโ๐))) |
40 | 24, 25, 39 | 3eqtrd 2781 |
. 2
โข ((๐ด โ โ โง ๐ โ โ0)
โ ((๐ด + 1)โ๐) = (ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท (๐ดโ๐)) + (๐ดโ๐))) |
41 | 20, 21, 40 | mvrraddd 11574 |
1
โข ((๐ด โ โ โง ๐ โ โ0)
โ (((๐ด + 1)โ๐) โ (๐ดโ๐)) = ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท (๐ดโ๐))) |