Step | Hyp | Ref
| Expression |
1 | | 1cnd 11158 |
. . . 4
โข (๐ โ โ โ 1 โ
โ) |
2 | | negid 11456 |
. . . . 5
โข (1 โ
โ โ (1 + -1) = 0) |
3 | 2 | eqcomd 2739 |
. . . 4
โข (1 โ
โ โ 0 = (1 + -1)) |
4 | 1, 3 | syl 17 |
. . 3
โข (๐ โ โ โ 0 = (1 +
-1)) |
5 | 4 | oveq1d 7376 |
. 2
โข (๐ โ โ โ
(0โ๐) = ((1 +
-1)โ๐)) |
6 | | 0exp 14012 |
. 2
โข (๐ โ โ โ
(0โ๐) =
0) |
7 | 1 | negcld 11507 |
. . . 4
โข (๐ โ โ โ -1 โ
โ) |
8 | | nnnn0 12428 |
. . . 4
โข (๐ โ โ โ ๐ โ
โ0) |
9 | | binom 15723 |
. . . 4
โข ((1
โ โ โง -1 โ โ โง ๐ โ โ0) โ ((1 +
-1)โ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((1โ(๐ โ ๐)) ยท (-1โ๐)))) |
10 | 1, 7, 8, 9 | syl3anc 1372 |
. . 3
โข (๐ โ โ โ ((1 +
-1)โ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((1โ(๐ โ ๐)) ยท (-1โ๐)))) |
11 | | nnz 12528 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โค) |
12 | | elfzelz 13450 |
. . . . . . . . . 10
โข (๐ โ (0...๐) โ ๐ โ โค) |
13 | | zsubcl 12553 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โ ๐) โ โค) |
14 | 11, 12, 13 | syl2an 597 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (0...๐)) โ (๐ โ ๐) โ โค) |
15 | | 1exp 14006 |
. . . . . . . . 9
โข ((๐ โ ๐) โ โค โ (1โ(๐ โ ๐)) = 1) |
16 | 14, 15 | syl 17 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (0...๐)) โ (1โ(๐ โ ๐)) = 1) |
17 | 16 | oveq1d 7376 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (0...๐)) โ ((1โ(๐ โ ๐)) ยท (-1โ๐)) = (1 ยท (-1โ๐))) |
18 | | neg1cn 12275 |
. . . . . . . . . 10
โข -1 โ
โ |
19 | 18 | a1i 11 |
. . . . . . . . 9
โข (๐ โ โ โ -1 โ
โ) |
20 | | elfznn0 13543 |
. . . . . . . . 9
โข (๐ โ (0...๐) โ ๐ โ โ0) |
21 | | expcl 13994 |
. . . . . . . . 9
โข ((-1
โ โ โง ๐
โ โ0) โ (-1โ๐) โ โ) |
22 | 19, 20, 21 | syl2an 597 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (0...๐)) โ (-1โ๐) โ โ) |
23 | 22 | mullidd 11181 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (0...๐)) โ (1 ยท (-1โ๐)) = (-1โ๐)) |
24 | 17, 23 | eqtrd 2773 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (0...๐)) โ ((1โ(๐ โ ๐)) ยท (-1โ๐)) = (-1โ๐)) |
25 | 24 | oveq2d 7377 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (0...๐)) โ ((๐C๐) ยท ((1โ(๐ โ ๐)) ยท (-1โ๐))) = ((๐C๐) ยท (-1โ๐))) |
26 | | bccl 14231 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ โค)
โ (๐C๐) โ
โ0) |
27 | 8, 12, 26 | syl2an 597 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (0...๐)) โ (๐C๐) โ
โ0) |
28 | 27 | nn0cnd 12483 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (0...๐)) โ (๐C๐) โ โ) |
29 | 28, 22 | mulcomd 11184 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (0...๐)) โ ((๐C๐) ยท (-1โ๐)) = ((-1โ๐) ยท (๐C๐))) |
30 | 25, 29 | eqtrd 2773 |
. . . 4
โข ((๐ โ โ โง ๐ โ (0...๐)) โ ((๐C๐) ยท ((1โ(๐ โ ๐)) ยท (-1โ๐))) = ((-1โ๐) ยท (๐C๐))) |
31 | 30 | sumeq2dv 15596 |
. . 3
โข (๐ โ โ โ
ฮฃ๐ โ (0...๐)((๐C๐) ยท ((1โ(๐ โ ๐)) ยท (-1โ๐))) = ฮฃ๐ โ (0...๐)((-1โ๐) ยท (๐C๐))) |
32 | 10, 31 | eqtrd 2773 |
. 2
โข (๐ โ โ โ ((1 +
-1)โ๐) = ฮฃ๐ โ (0...๐)((-1โ๐) ยท (๐C๐))) |
33 | 5, 6, 32 | 3eqtr3rd 2782 |
1
โข (๐ โ โ โ
ฮฃ๐ โ (0...๐)((-1โ๐) ยท (๐C๐)) = 0) |