Step | Hyp | Ref
| Expression |
1 | | elfzelz 13447 |
. . . . . . 7
โข (๐ โ (0...๐) โ ๐ โ โค) |
2 | | bcpascm1 46513 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โค) โ (((๐ โ 1)C๐) + ((๐ โ 1)C(๐ โ 1))) = (๐C๐)) |
3 | 1, 2 | sylan2 594 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (0...๐)) โ (((๐ โ 1)C๐) + ((๐ โ 1)C(๐ โ 1))) = (๐C๐)) |
4 | 3 | eqcomd 2739 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (0...๐)) โ (๐C๐) = (((๐ โ 1)C๐) + ((๐ โ 1)C(๐ โ 1)))) |
5 | 4 | oveq2d 7374 |
. . . 4
โข ((๐ โ โ โง ๐ โ (0...๐)) โ ((-1โ๐) ยท (๐C๐)) = ((-1โ๐) ยท (((๐ โ 1)C๐) + ((๐ โ 1)C(๐ โ 1))))) |
6 | | ax-1cn 11114 |
. . . . . . 7
โข 1 โ
โ |
7 | | negcl 11406 |
. . . . . . . 8
โข (1 โ
โ โ -1 โ โ) |
8 | | elfznn0 13540 |
. . . . . . . 8
โข (๐ โ (0...๐) โ ๐ โ โ0) |
9 | | expcl 13991 |
. . . . . . . 8
โข ((-1
โ โ โง ๐
โ โ0) โ (-1โ๐) โ โ) |
10 | 7, 8, 9 | syl2an 597 |
. . . . . . 7
โข ((1
โ โ โง ๐
โ (0...๐)) โ
(-1โ๐) โ
โ) |
11 | 6, 10 | mpan 689 |
. . . . . 6
โข (๐ โ (0...๐) โ (-1โ๐) โ โ) |
12 | 11 | adantl 483 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (0...๐)) โ (-1โ๐) โ โ) |
13 | | nnm1nn0 12459 |
. . . . . 6
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
14 | | bccl 14228 |
. . . . . . 7
โข (((๐ โ 1) โ
โ0 โง ๐
โ โค) โ ((๐
โ 1)C๐) โ
โ0) |
15 | 14 | nn0cnd 12480 |
. . . . . 6
โข (((๐ โ 1) โ
โ0 โง ๐
โ โค) โ ((๐
โ 1)C๐) โ
โ) |
16 | 13, 1, 15 | syl2an 597 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (0...๐)) โ ((๐ โ 1)C๐) โ โ) |
17 | | peano2zm 12551 |
. . . . . . 7
โข (๐ โ โค โ (๐ โ 1) โ
โค) |
18 | 1, 17 | syl 17 |
. . . . . 6
โข (๐ โ (0...๐) โ (๐ โ 1) โ โค) |
19 | | bccl 14228 |
. . . . . . 7
โข (((๐ โ 1) โ
โ0 โง (๐ โ 1) โ โค) โ ((๐ โ 1)C(๐ โ 1)) โ
โ0) |
20 | 19 | nn0cnd 12480 |
. . . . . 6
โข (((๐ โ 1) โ
โ0 โง (๐ โ 1) โ โค) โ ((๐ โ 1)C(๐ โ 1)) โ โ) |
21 | 13, 18, 20 | syl2an 597 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (0...๐)) โ ((๐ โ 1)C(๐ โ 1)) โ โ) |
22 | 12, 16, 21 | adddid 11184 |
. . . 4
โข ((๐ โ โ โง ๐ โ (0...๐)) โ ((-1โ๐) ยท (((๐ โ 1)C๐) + ((๐ โ 1)C(๐ โ 1)))) = (((-1โ๐) ยท ((๐ โ 1)C๐)) + ((-1โ๐) ยท ((๐ โ 1)C(๐ โ 1))))) |
23 | 5, 22 | eqtrd 2773 |
. . 3
โข ((๐ โ โ โง ๐ โ (0...๐)) โ ((-1โ๐) ยท (๐C๐)) = (((-1โ๐) ยท ((๐ โ 1)C๐)) + ((-1โ๐) ยท ((๐ โ 1)C(๐ โ 1))))) |
24 | 23 | sumeq2dv 15593 |
. 2
โข (๐ โ โ โ
ฮฃ๐ โ (0...๐)((-1โ๐) ยท (๐C๐)) = ฮฃ๐ โ (0...๐)(((-1โ๐) ยท ((๐ โ 1)C๐)) + ((-1โ๐) ยท ((๐ โ 1)C(๐ โ 1))))) |
25 | | fzfid 13884 |
. . . 4
โข (๐ โ โ โ
(0...๐) โ
Fin) |
26 | | neg1cn 12272 |
. . . . . . 7
โข -1 โ
โ |
27 | 26 | a1i 11 |
. . . . . 6
โข (๐ โ โ โ -1 โ
โ) |
28 | 27, 8, 9 | syl2an 597 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (0...๐)) โ (-1โ๐) โ โ) |
29 | 28, 16 | mulcld 11180 |
. . . 4
โข ((๐ โ โ โง ๐ โ (0...๐)) โ ((-1โ๐) ยท ((๐ โ 1)C๐)) โ โ) |
30 | | 1z 12538 |
. . . . . . . 8
โข 1 โ
โค |
31 | 30 | a1i 11 |
. . . . . . 7
โข (๐ โ (0...๐) โ 1 โ โค) |
32 | 1, 31 | zsubcld 12617 |
. . . . . 6
โข (๐ โ (0...๐) โ (๐ โ 1) โ โค) |
33 | 13, 32, 20 | syl2an 597 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (0...๐)) โ ((๐ โ 1)C(๐ โ 1)) โ โ) |
34 | 28, 33 | mulcld 11180 |
. . . 4
โข ((๐ โ โ โง ๐ โ (0...๐)) โ ((-1โ๐) ยท ((๐ โ 1)C(๐ โ 1))) โ
โ) |
35 | 25, 29, 34 | fsumadd 15630 |
. . 3
โข (๐ โ โ โ
ฮฃ๐ โ (0...๐)(((-1โ๐) ยท ((๐ โ 1)C๐)) + ((-1โ๐) ยท ((๐ โ 1)C(๐ โ 1)))) = (ฮฃ๐ โ (0...๐)((-1โ๐) ยท ((๐ โ 1)C๐)) + ฮฃ๐ โ (0...๐)((-1โ๐) ยท ((๐ โ 1)C(๐ โ 1))))) |
36 | 30 | a1i 11 |
. . . . . 6
โข (๐ โ โ โ 1 โ
โค) |
37 | | 0zd 12516 |
. . . . . 6
โข (๐ โ โ โ 0 โ
โค) |
38 | | nnz 12525 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โค) |
39 | | oveq2 7366 |
. . . . . . 7
โข (๐ = (๐ โ 1) โ (-1โ๐) = (-1โ(๐ โ 1))) |
40 | | oveq2 7366 |
. . . . . . 7
โข (๐ = (๐ โ 1) โ ((๐ โ 1)C๐) = ((๐ โ 1)C(๐ โ 1))) |
41 | 39, 40 | oveq12d 7376 |
. . . . . 6
โข (๐ = (๐ โ 1) โ ((-1โ๐) ยท ((๐ โ 1)C๐)) = ((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1)))) |
42 | 36, 37, 38, 29, 41 | fsumshft 15670 |
. . . . 5
โข (๐ โ โ โ
ฮฃ๐ โ (0...๐)((-1โ๐) ยท ((๐ โ 1)C๐)) = ฮฃ๐ โ ((0 + 1)...(๐ + 1))((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1)))) |
43 | | 0p1e1 12280 |
. . . . . . . 8
โข (0 + 1) =
1 |
44 | 43 | oveq1i 7368 |
. . . . . . 7
โข ((0 +
1)...(๐ + 1)) = (1...(๐ + 1)) |
45 | 44 | a1i 11 |
. . . . . 6
โข (๐ โ โ โ ((0 +
1)...(๐ + 1)) = (1...(๐ + 1))) |
46 | 45 | sumeq1d 15591 |
. . . . 5
โข (๐ โ โ โ
ฮฃ๐ โ ((0 +
1)...(๐ +
1))((-1โ(๐ โ 1))
ยท ((๐ โ
1)C(๐ โ 1))) =
ฮฃ๐ โ (1...(๐ + 1))((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1)))) |
47 | | elnnuz 12812 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
(โคโฅโ1)) |
48 | 47 | biimpi 215 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
(โคโฅโ1)) |
49 | 26 | a1i 11 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1...(๐ + 1))) โ -1 โ
โ) |
50 | | elfznn 13476 |
. . . . . . . . . . 11
โข (๐ โ (1...(๐ + 1)) โ ๐ โ โ) |
51 | | nnm1nn0 12459 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (1...(๐ + 1)) โ (๐ โ 1) โ
โ0) |
53 | 52 | adantl 483 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1...(๐ + 1))) โ (๐ โ 1) โ
โ0) |
54 | 49, 53 | expcld 14057 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1...(๐ + 1))) โ (-1โ(๐ โ 1)) โ โ) |
55 | | elfzelz 13447 |
. . . . . . . . . 10
โข (๐ โ (1...(๐ + 1)) โ ๐ โ โค) |
56 | | elfzel1 13446 |
. . . . . . . . . 10
โข (๐ โ (1...(๐ + 1)) โ 1 โ
โค) |
57 | 55, 56 | zsubcld 12617 |
. . . . . . . . 9
โข (๐ โ (1...(๐ + 1)) โ (๐ โ 1) โ โค) |
58 | | bccl 14228 |
. . . . . . . . . 10
โข (((๐ โ 1) โ
โ0 โง (๐ โ 1) โ โค) โ ((๐ โ 1)C(๐ โ 1)) โ
โ0) |
59 | 58 | nn0cnd 12480 |
. . . . . . . . 9
โข (((๐ โ 1) โ
โ0 โง (๐ โ 1) โ โค) โ ((๐ โ 1)C(๐ โ 1)) โ โ) |
60 | 13, 57, 59 | syl2an 597 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1...(๐ + 1))) โ ((๐ โ 1)C(๐ โ 1)) โ โ) |
61 | 54, 60 | mulcld 11180 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...(๐ + 1))) โ ((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))) โ
โ) |
62 | | oveq1 7365 |
. . . . . . . . 9
โข (๐ = (๐ + 1) โ (๐ โ 1) = ((๐ + 1) โ 1)) |
63 | 62 | oveq2d 7374 |
. . . . . . . 8
โข (๐ = (๐ + 1) โ (-1โ(๐ โ 1)) = (-1โ((๐ + 1) โ 1))) |
64 | 62 | oveq2d 7374 |
. . . . . . . 8
โข (๐ = (๐ + 1) โ ((๐ โ 1)C(๐ โ 1)) = ((๐ โ 1)C((๐ + 1) โ 1))) |
65 | 63, 64 | oveq12d 7376 |
. . . . . . 7
โข (๐ = (๐ + 1) โ ((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))) = ((-1โ((๐ + 1) โ 1)) ยท ((๐ โ 1)C((๐ + 1) โ 1)))) |
66 | 48, 61, 65 | fsump1 15646 |
. . . . . 6
โข (๐ โ โ โ
ฮฃ๐ โ (1...(๐ + 1))((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))) = (ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))) + ((-1โ((๐ + 1) โ 1)) ยท ((๐ โ 1)C((๐ + 1) โ 1))))) |
67 | | nncn 12166 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ) |
68 | | pncan1 11584 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((๐ + 1) โ 1) = ๐) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((๐ + 1) โ 1) = ๐) |
70 | | nnnn0 12425 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ0) |
71 | 69, 70 | eqeltrd 2834 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((๐ + 1) โ 1) โ
โ0) |
72 | 71 | nn0zd 12530 |
. . . . . . . . . 10
โข (๐ โ โ โ ((๐ + 1) โ 1) โ
โค) |
73 | | nnre 12165 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ) |
74 | | ltm1 12002 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐ โ 1) < ๐) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (๐ โ 1) < ๐) |
76 | 75, 69 | breqtrrd 5134 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ โ 1) < ((๐ + 1) โ
1)) |
77 | 76 | olcd 873 |
. . . . . . . . . 10
โข (๐ โ โ โ (((๐ + 1) โ 1) < 0 โจ
(๐ โ 1) < ((๐ + 1) โ
1))) |
78 | | bcval4 14213 |
. . . . . . . . . 10
โข (((๐ โ 1) โ
โ0 โง ((๐ + 1) โ 1) โ โค โง
(((๐ + 1) โ 1) < 0
โจ (๐ โ 1) <
((๐ + 1) โ 1)))
โ ((๐ โ
1)C((๐ + 1) โ 1)) =
0) |
79 | 13, 72, 77, 78 | syl3anc 1372 |
. . . . . . . . 9
โข (๐ โ โ โ ((๐ โ 1)C((๐ + 1) โ 1)) = 0) |
80 | 79 | oveq2d 7374 |
. . . . . . . 8
โข (๐ โ โ โ
((-1โ((๐ + 1) โ
1)) ยท ((๐ โ
1)C((๐ + 1) โ 1))) =
((-1โ((๐ + 1) โ
1)) ยท 0)) |
81 | 27, 71 | expcld 14057 |
. . . . . . . . 9
โข (๐ โ โ โ
(-1โ((๐ + 1) โ
1)) โ โ) |
82 | 81 | mul01d 11359 |
. . . . . . . 8
โข (๐ โ โ โ
((-1โ((๐ + 1) โ
1)) ยท 0) = 0) |
83 | 80, 82 | eqtrd 2773 |
. . . . . . 7
โข (๐ โ โ โ
((-1โ((๐ + 1) โ
1)) ยท ((๐ โ
1)C((๐ + 1) โ 1))) =
0) |
84 | 83 | oveq2d 7374 |
. . . . . 6
โข (๐ โ โ โ
(ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))) + ((-1โ((๐ + 1) โ 1)) ยท ((๐ โ 1)C((๐ + 1) โ 1)))) = (ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))) + 0)) |
85 | | oveq1 7365 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ โ 1) = (๐ โ 1)) |
86 | 85 | oveq2d 7374 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (-1โ(๐ โ 1)) = (-1โ(๐ โ 1))) |
87 | 85 | oveq2d 7374 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((๐ โ 1)C(๐ โ 1)) = ((๐ โ 1)C(๐ โ 1))) |
88 | 86, 87 | oveq12d 7376 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))) = ((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1)))) |
89 | 88 | cbvsumv 15586 |
. . . . . . . . 9
โข
ฮฃ๐ โ
(1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))) = ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))) |
90 | 89 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ โ
ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))) = ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1)))) |
91 | 90 | oveq1d 7373 |
. . . . . . 7
โข (๐ โ โ โ
(ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))) + 0) = (ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))) + 0)) |
92 | | fzfid 13884 |
. . . . . . . . 9
โข (๐ โ โ โ
(1...๐) โ
Fin) |
93 | 26 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ (1...๐)) โ -1 โ
โ) |
94 | | elfznn 13476 |
. . . . . . . . . . . . 13
โข (๐ โ (1...๐) โ ๐ โ โ) |
95 | | nnm1nn0 12459 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ (1...๐) โ (๐ โ 1) โ
โ0) |
97 | 96 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (๐ โ 1) โ
โ0) |
98 | 93, 97 | expcld 14057 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (-1โ(๐ โ 1)) โ โ) |
99 | | elfzelz 13447 |
. . . . . . . . . . . . 13
โข (๐ โ (1...๐) โ ๐ โ โค) |
100 | | elfzel1 13446 |
. . . . . . . . . . . . 13
โข (๐ โ (1...๐) โ 1 โ โค) |
101 | 99, 100 | zsubcld 12617 |
. . . . . . . . . . . 12
โข (๐ โ (1...๐) โ (๐ โ 1) โ โค) |
102 | 13, 101, 19 | syl2an 597 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((๐ โ 1)C(๐ โ 1)) โ
โ0) |
103 | 102 | nn0cnd 12480 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((๐ โ 1)C(๐ โ 1)) โ โ) |
104 | 98, 103 | mulcld 11180 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))) โ
โ) |
105 | 92, 104 | fsumcl 15623 |
. . . . . . . 8
โข (๐ โ โ โ
ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))) โ
โ) |
106 | 105 | addid1d 11360 |
. . . . . . 7
โข (๐ โ โ โ
(ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))) + 0) = ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1)))) |
107 | 91, 106 | eqtrd 2773 |
. . . . . 6
โข (๐ โ โ โ
(ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))) + 0) = ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1)))) |
108 | 66, 84, 107 | 3eqtrd 2777 |
. . . . 5
โข (๐ โ โ โ
ฮฃ๐ โ (1...(๐ + 1))((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))) = ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1)))) |
109 | 42, 46, 108 | 3eqtrd 2777 |
. . . 4
โข (๐ โ โ โ
ฮฃ๐ โ (0...๐)((-1โ๐) ยท ((๐ โ 1)C๐)) = ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1)))) |
110 | | elnn0uz 12813 |
. . . . . . 7
โข (๐ โ โ0
โ ๐ โ
(โคโฅโ0)) |
111 | 70, 110 | sylib 217 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
(โคโฅโ0)) |
112 | | oveq2 7366 |
. . . . . . 7
โข (๐ = 0 โ (-1โ๐) =
(-1โ0)) |
113 | | oveq1 7365 |
. . . . . . . 8
โข (๐ = 0 โ (๐ โ 1) = (0 โ 1)) |
114 | 113 | oveq2d 7374 |
. . . . . . 7
โข (๐ = 0 โ ((๐ โ 1)C(๐ โ 1)) = ((๐ โ 1)C(0 โ 1))) |
115 | 112, 114 | oveq12d 7376 |
. . . . . 6
โข (๐ = 0 โ ((-1โ๐) ยท ((๐ โ 1)C(๐ โ 1))) = ((-1โ0) ยท ((๐ โ 1)C(0 โ
1)))) |
116 | 111, 34, 115 | fsum1p 15643 |
. . . . 5
โข (๐ โ โ โ
ฮฃ๐ โ (0...๐)((-1โ๐) ยท ((๐ โ 1)C(๐ โ 1))) = (((-1โ0) ยท
((๐ โ 1)C(0 โ
1))) + ฮฃ๐ โ ((0
+ 1)...๐)((-1โ๐) ยท ((๐ โ 1)C(๐ โ 1))))) |
117 | 27 | exp0d 14051 |
. . . . . . . 8
โข (๐ โ โ โ
(-1โ0) = 1) |
118 | | 0z 12515 |
. . . . . . . . . . 11
โข 0 โ
โค |
119 | | zsubcl 12550 |
. . . . . . . . . . 11
โข ((0
โ โค โง 1 โ โค) โ (0 โ 1) โ
โค) |
120 | 118, 30, 119 | mp2an 691 |
. . . . . . . . . 10
โข (0
โ 1) โ โค |
121 | 120 | a1i 11 |
. . . . . . . . 9
โข (๐ โ โ โ (0
โ 1) โ โค) |
122 | | 0re 11162 |
. . . . . . . . . . 11
โข 0 โ
โ |
123 | | ltm1 12002 |
. . . . . . . . . . 11
โข (0 โ
โ โ (0 โ 1) < 0) |
124 | 122, 123 | mp1i 13 |
. . . . . . . . . 10
โข (๐ โ โ โ (0
โ 1) < 0) |
125 | 124 | orcd 872 |
. . . . . . . . 9
โข (๐ โ โ โ ((0
โ 1) < 0 โจ (๐
โ 1) < (0 โ 1))) |
126 | | bcval4 14213 |
. . . . . . . . 9
โข (((๐ โ 1) โ
โ0 โง (0 โ 1) โ โค โง ((0 โ 1)
< 0 โจ (๐ โ 1)
< (0 โ 1))) โ ((๐ โ 1)C(0 โ 1)) =
0) |
127 | 13, 121, 125, 126 | syl3anc 1372 |
. . . . . . . 8
โข (๐ โ โ โ ((๐ โ 1)C(0 โ 1)) =
0) |
128 | 117, 127 | oveq12d 7376 |
. . . . . . 7
โข (๐ โ โ โ
((-1โ0) ยท ((๐
โ 1)C(0 โ 1))) = (1 ยท 0)) |
129 | 6 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ โ 1 โ
โ) |
130 | 129 | mul01d 11359 |
. . . . . . 7
โข (๐ โ โ โ (1
ยท 0) = 0) |
131 | 128, 130 | eqtrd 2773 |
. . . . . 6
โข (๐ โ โ โ
((-1โ0) ยท ((๐
โ 1)C(0 โ 1))) = 0) |
132 | 43 | a1i 11 |
. . . . . . . . 9
โข (๐ โ โ โ (0 + 1) =
1) |
133 | 132 | oveq1d 7373 |
. . . . . . . 8
โข (๐ โ โ โ ((0 +
1)...๐) = (1...๐)) |
134 | 99 | zcnd 12613 |
. . . . . . . . . . . . . 14
โข (๐ โ (1...๐) โ ๐ โ โ) |
135 | | npcan1 11585 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ((๐ โ 1) + 1) = ๐) |
136 | 135 | eqcomd 2739 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ = ((๐ โ 1) + 1)) |
137 | 134, 136 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ (1...๐) โ ๐ = ((๐ โ 1) + 1)) |
138 | 137 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ๐ = ((๐ โ 1) + 1)) |
139 | 138 | oveq2d 7374 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (-1โ๐) = (-1โ((๐ โ 1) + 1))) |
140 | | expp1 13980 |
. . . . . . . . . . . 12
โข ((-1
โ โ โง (๐
โ 1) โ โ0) โ (-1โ((๐ โ 1) + 1)) = ((-1โ(๐ โ 1)) ยท
-1)) |
141 | 27, 96, 140 | syl2an 597 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (-1โ((๐ โ 1) + 1)) = ((-1โ(๐ โ 1)) ยท
-1)) |
142 | 139, 141 | eqtrd 2773 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (-1โ๐) = ((-1โ(๐ โ 1)) ยท -1)) |
143 | 142 | oveq1d 7373 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((-1โ๐) ยท ((๐ โ 1)C(๐ โ 1))) = (((-1โ(๐ โ 1)) ยท -1)
ยท ((๐ โ
1)C(๐ โ
1)))) |
144 | 98, 93 | mulcomd 11181 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((-1โ(๐ โ 1)) ยท -1) = (-1 ยท
(-1โ(๐ โ
1)))) |
145 | 144 | oveq1d 7373 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (((-1โ(๐ โ 1)) ยท -1) ยท ((๐ โ 1)C(๐ โ 1))) = ((-1 ยท (-1โ(๐ โ 1))) ยท ((๐ โ 1)C(๐ โ 1)))) |
146 | 93, 98, 103 | mulassd 11183 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((-1 ยท (-1โ(๐ โ 1))) ยท ((๐ โ 1)C(๐ โ 1))) = (-1 ยท ((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))))) |
147 | 143, 145,
146 | 3eqtrd 2777 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((-1โ๐) ยท ((๐ โ 1)C(๐ โ 1))) = (-1 ยท ((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))))) |
148 | 133, 147 | sumeq12rdv 15597 |
. . . . . . 7
โข (๐ โ โ โ
ฮฃ๐ โ ((0 +
1)...๐)((-1โ๐) ยท ((๐ โ 1)C(๐ โ 1))) = ฮฃ๐ โ (1...๐)(-1 ยท ((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))))) |
149 | 92, 27, 104 | fsummulc2 15674 |
. . . . . . 7
โข (๐ โ โ โ (-1
ยท ฮฃ๐ โ
(1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1)))) = ฮฃ๐ โ (1...๐)(-1 ยท ((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))))) |
150 | 148, 149 | eqtr4d 2776 |
. . . . . 6
โข (๐ โ โ โ
ฮฃ๐ โ ((0 +
1)...๐)((-1โ๐) ยท ((๐ โ 1)C(๐ โ 1))) = (-1 ยท ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))))) |
151 | 131, 150 | oveq12d 7376 |
. . . . 5
โข (๐ โ โ โ
(((-1โ0) ยท ((๐
โ 1)C(0 โ 1))) + ฮฃ๐ โ ((0 + 1)...๐)((-1โ๐) ยท ((๐ โ 1)C(๐ โ 1)))) = (0 + (-1 ยท
ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1)))))) |
152 | 27, 105 | mulcld 11180 |
. . . . . 6
โข (๐ โ โ โ (-1
ยท ฮฃ๐ โ
(1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1)))) โ
โ) |
153 | 152 | addid2d 11361 |
. . . . 5
โข (๐ โ โ โ (0 + (-1
ยท ฮฃ๐ โ
(1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))))) = (-1 ยท ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))))) |
154 | 116, 151,
153 | 3eqtrd 2777 |
. . . 4
โข (๐ โ โ โ
ฮฃ๐ โ (0...๐)((-1โ๐) ยท ((๐ โ 1)C(๐ โ 1))) = (-1 ยท ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))))) |
155 | 109, 154 | oveq12d 7376 |
. . 3
โข (๐ โ โ โ
(ฮฃ๐ โ (0...๐)((-1โ๐) ยท ((๐ โ 1)C๐)) + ฮฃ๐ โ (0...๐)((-1โ๐) ยท ((๐ โ 1)C(๐ โ 1)))) = (ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))) + (-1 ยท ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1)))))) |
156 | 35, 155 | eqtrd 2773 |
. 2
โข (๐ โ โ โ
ฮฃ๐ โ (0...๐)(((-1โ๐) ยท ((๐ โ 1)C๐)) + ((-1โ๐) ยท ((๐ โ 1)C(๐ โ 1)))) = (ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))) + (-1 ยท ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1)))))) |
157 | 105 | mulm1d 11612 |
. . . 4
โข (๐ โ โ โ (-1
ยท ฮฃ๐ โ
(1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1)))) = -ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1)))) |
158 | 157 | oveq2d 7374 |
. . 3
โข (๐ โ โ โ
(ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))) + (-1 ยท ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))))) = (ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))) + -ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))))) |
159 | 105 | negidd 11507 |
. . 3
โข (๐ โ โ โ
(ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))) + -ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1)))) = 0) |
160 | 158, 159 | eqtrd 2773 |
. 2
โข (๐ โ โ โ
(ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))) + (-1 ยท ฮฃ๐ โ (1...๐)((-1โ(๐ โ 1)) ยท ((๐ โ 1)C(๐ โ 1))))) = 0) |
161 | 24, 156, 160 | 3eqtrd 2777 |
1
โข (๐ โ โ โ
ฮฃ๐ โ (0...๐)((-1โ๐) ยท (๐C๐)) = 0) |