Step | Hyp | Ref
| Expression |
1 | | pwp1fsum.a |
. . . 4
โข (๐ โ ๐ด โ โ) |
2 | | 1cnd 11155 |
. . . 4
โข (๐ โ 1 โ
โ) |
3 | | fzfid 13884 |
. . . . 5
โข (๐ โ (0...(๐ โ 1)) โ Fin) |
4 | | neg1cn 12272 |
. . . . . . . 8
โข -1 โ
โ |
5 | 4 | a1i 11 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ โ 1))) โ -1 โ
โ) |
6 | | elfznn0 13540 |
. . . . . . . 8
โข (๐ โ (0...(๐ โ 1)) โ ๐ โ โ0) |
7 | 6 | adantl 483 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ โ 1))) โ ๐ โ โ0) |
8 | 5, 7 | expcld 14057 |
. . . . . 6
โข ((๐ โง ๐ โ (0...(๐ โ 1))) โ (-1โ๐) โ
โ) |
9 | 1 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ โ 1))) โ ๐ด โ โ) |
10 | 9, 7 | expcld 14057 |
. . . . . 6
โข ((๐ โง ๐ โ (0...(๐ โ 1))) โ (๐ดโ๐) โ โ) |
11 | 8, 10 | mulcld 11180 |
. . . . 5
โข ((๐ โง ๐ โ (0...(๐ โ 1))) โ ((-1โ๐) ยท (๐ดโ๐)) โ โ) |
12 | 3, 11 | fsumcl 15623 |
. . . 4
โข (๐ โ ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐)) โ โ) |
13 | 1, 2, 12 | adddird 11185 |
. . 3
โข (๐ โ ((๐ด + 1) ยท ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐))) = ((๐ด ยท ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐))) + (1 ยท ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐))))) |
14 | 3, 1, 11 | fsummulc2 15674 |
. . . . 5
โข (๐ โ (๐ด ยท ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐))) = ฮฃ๐ โ (0...(๐ โ 1))(๐ด ยท ((-1โ๐) ยท (๐ดโ๐)))) |
15 | 9, 11 | mulcomd 11181 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ โ 1))) โ (๐ด ยท ((-1โ๐) ยท (๐ดโ๐))) = (((-1โ๐) ยท (๐ดโ๐)) ยท ๐ด)) |
16 | 8, 10, 9 | mulassd 11183 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ โ 1))) โ (((-1โ๐) ยท (๐ดโ๐)) ยท ๐ด) = ((-1โ๐) ยท ((๐ดโ๐) ยท ๐ด))) |
17 | | expp1 13980 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
18 | 1, 6, 17 | syl2an 597 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...(๐ โ 1))) โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
19 | 18 | eqcomd 2739 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...(๐ โ 1))) โ ((๐ดโ๐) ยท ๐ด) = (๐ดโ(๐ + 1))) |
20 | 19 | oveq2d 7374 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ โ 1))) โ ((-1โ๐) ยท ((๐ดโ๐) ยท ๐ด)) = ((-1โ๐) ยท (๐ดโ(๐ + 1)))) |
21 | 15, 16, 20 | 3eqtrd 2777 |
. . . . . 6
โข ((๐ โง ๐ โ (0...(๐ โ 1))) โ (๐ด ยท ((-1โ๐) ยท (๐ดโ๐))) = ((-1โ๐) ยท (๐ดโ(๐ + 1)))) |
22 | 21 | sumeq2dv 15593 |
. . . . 5
โข (๐ โ ฮฃ๐ โ (0...(๐ โ 1))(๐ด ยท ((-1โ๐) ยท (๐ดโ๐))) = ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ(๐ + 1)))) |
23 | 14, 22 | eqtrd 2773 |
. . . 4
โข (๐ โ (๐ด ยท ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐))) = ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ(๐ + 1)))) |
24 | 12 | mulid2d 11178 |
. . . 4
โข (๐ โ (1 ยท ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐))) = ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐))) |
25 | 23, 24 | oveq12d 7376 |
. . 3
โข (๐ โ ((๐ด ยท ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐))) + (1 ยท ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐)))) = (ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ(๐ + 1))) + ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐)))) |
26 | | 1zzd 12539 |
. . . . . . 7
โข (๐ โ 1 โ
โค) |
27 | | 0zd 12516 |
. . . . . . 7
โข (๐ โ 0 โ
โค) |
28 | | pwp1fsum.n |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
29 | | nnz 12525 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โค) |
30 | | peano2zm 12551 |
. . . . . . . . 9
โข (๐ โ โค โ (๐ โ 1) โ
โค) |
31 | 29, 30 | syl 17 |
. . . . . . . 8
โข (๐ โ โ โ (๐ โ 1) โ
โค) |
32 | 28, 31 | syl 17 |
. . . . . . 7
โข (๐ โ (๐ โ 1) โ โค) |
33 | | peano2nn0 12458 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ (๐ + 1) โ
โ0) |
34 | 6, 33 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (0...(๐ โ 1)) โ (๐ + 1) โ
โ0) |
35 | 34 | adantl 483 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...(๐ โ 1))) โ (๐ + 1) โ
โ0) |
36 | 9, 35 | expcld 14057 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...(๐ โ 1))) โ (๐ดโ(๐ + 1)) โ โ) |
37 | 8, 36 | mulcld 11180 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ โ 1))) โ ((-1โ๐) ยท (๐ดโ(๐ + 1))) โ โ) |
38 | | oveq2 7366 |
. . . . . . . 8
โข (๐ = (๐ โ 1) โ (-1โ๐) = (-1โ(๐ โ 1))) |
39 | | oveq1 7365 |
. . . . . . . . 9
โข (๐ = (๐ โ 1) โ (๐ + 1) = ((๐ โ 1) + 1)) |
40 | 39 | oveq2d 7374 |
. . . . . . . 8
โข (๐ = (๐ โ 1) โ (๐ดโ(๐ + 1)) = (๐ดโ((๐ โ 1) + 1))) |
41 | 38, 40 | oveq12d 7376 |
. . . . . . 7
โข (๐ = (๐ โ 1) โ ((-1โ๐) ยท (๐ดโ(๐ + 1))) = ((-1โ(๐ โ 1)) ยท (๐ดโ((๐ โ 1) + 1)))) |
42 | 26, 27, 32, 37, 41 | fsumshft 15670 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ(๐ + 1))) = ฮฃ๐ โ ((0 + 1)...((๐ โ 1) + 1))((-1โ(๐ โ 1)) ยท (๐ดโ((๐ โ 1) + 1)))) |
43 | | elfzelz 13447 |
. . . . . . . . . . . 12
โข (๐ โ ((0 + 1)...((๐ โ 1) + 1)) โ ๐ โ
โค) |
44 | 43 | zcnd 12613 |
. . . . . . . . . . 11
โข (๐ โ ((0 + 1)...((๐ โ 1) + 1)) โ ๐ โ
โ) |
45 | 44 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ((0 + 1)...((๐ โ 1) + 1))) โ ๐ โ โ) |
46 | | npcan1 11585 |
. . . . . . . . . 10
โข (๐ โ โ โ ((๐ โ 1) + 1) = ๐) |
47 | 45, 46 | syl 17 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ((0 + 1)...((๐ โ 1) + 1))) โ ((๐ โ 1) + 1) = ๐) |
48 | 47 | oveq2d 7374 |
. . . . . . . 8
โข ((๐ โง ๐ โ ((0 + 1)...((๐ โ 1) + 1))) โ (๐ดโ((๐ โ 1) + 1)) = (๐ดโ๐)) |
49 | 48 | oveq2d 7374 |
. . . . . . 7
โข ((๐ โง ๐ โ ((0 + 1)...((๐ โ 1) + 1))) โ ((-1โ(๐ โ 1)) ยท (๐ดโ((๐ โ 1) + 1))) = ((-1โ(๐ โ 1)) ยท (๐ดโ๐))) |
50 | 49 | sumeq2dv 15593 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ ((0 + 1)...((๐ โ 1) + 1))((-1โ(๐ โ 1)) ยท (๐ดโ((๐ โ 1) + 1))) = ฮฃ๐ โ ((0 + 1)...((๐ โ 1) +
1))((-1โ(๐ โ 1))
ยท (๐ดโ๐))) |
51 | 28 | nncnd 12174 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
52 | | npcan1 11585 |
. . . . . . . . . 10
โข (๐ โ โ โ ((๐ โ 1) + 1) = ๐) |
53 | 51, 52 | syl 17 |
. . . . . . . . 9
โข (๐ โ ((๐ โ 1) + 1) = ๐) |
54 | | 0p1e1 12280 |
. . . . . . . . . . . 12
โข (0 + 1) =
1 |
55 | 54 | fveq2i 6846 |
. . . . . . . . . . 11
โข
(โคโฅโ(0 + 1)) =
(โคโฅโ1) |
56 | | nnuz 12811 |
. . . . . . . . . . 11
โข โ =
(โคโฅโ1) |
57 | 55, 56 | eqtr4i 2764 |
. . . . . . . . . 10
โข
(โคโฅโ(0 + 1)) = โ |
58 | 57 | a1i 11 |
. . . . . . . . 9
โข (๐ โ
(โคโฅโ(0 + 1)) = โ) |
59 | 28, 53, 58 | 3eltr4d 2849 |
. . . . . . . 8
โข (๐ โ ((๐ โ 1) + 1) โ
(โคโฅโ(0 + 1))) |
60 | 54 | oveq1i 7368 |
. . . . . . . . . . 11
โข ((0 +
1)...((๐ โ 1) + 1)) =
(1...((๐ โ 1) +
1)) |
61 | 60 | eleq2i 2826 |
. . . . . . . . . 10
โข (๐ โ ((0 + 1)...((๐ โ 1) + 1)) โ ๐ โ (1...((๐ โ 1) + 1))) |
62 | 4 | a1i 11 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ โ) โ -1 โ
โ) |
63 | | nnm1nn0 12459 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
64 | 63 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ โ) โ (๐ โ 1) โ
โ0) |
65 | 62, 64 | expcld 14057 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ โ) โ (-1โ(๐ โ 1)) โ
โ) |
66 | 1 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ โ) โ ๐ด โ โ) |
67 | | nnnn0 12425 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ
โ0) |
68 | 67 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ โ) โ ๐ โ โ0) |
69 | 66, 68 | expcld 14057 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ โ) โ (๐ดโ๐) โ โ) |
70 | 65, 69 | mulcld 11180 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ โ) โ ((-1โ(๐ โ 1)) ยท (๐ดโ๐)) โ โ) |
71 | 70 | expcom 415 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ โ ((-1โ(๐ โ 1)) ยท (๐ดโ๐)) โ โ)) |
72 | | elfznn 13476 |
. . . . . . . . . . 11
โข (๐ โ (1...((๐ โ 1) + 1)) โ ๐ โ โ) |
73 | 71, 72 | syl11 33 |
. . . . . . . . . 10
โข (๐ โ (๐ โ (1...((๐ โ 1) + 1)) โ ((-1โ(๐ โ 1)) ยท (๐ดโ๐)) โ โ)) |
74 | 61, 73 | biimtrid 241 |
. . . . . . . . 9
โข (๐ โ (๐ โ ((0 + 1)...((๐ โ 1) + 1)) โ ((-1โ(๐ โ 1)) ยท (๐ดโ๐)) โ โ)) |
75 | 74 | imp 408 |
. . . . . . . 8
โข ((๐ โง ๐ โ ((0 + 1)...((๐ โ 1) + 1))) โ ((-1โ(๐ โ 1)) ยท (๐ดโ๐)) โ โ) |
76 | | oveq1 7365 |
. . . . . . . . . 10
โข (๐ = ((๐ โ 1) + 1) โ (๐ โ 1) = (((๐ โ 1) + 1) โ
1)) |
77 | 76 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ = ((๐ โ 1) + 1) โ (-1โ(๐ โ 1)) = (-1โ(((๐ โ 1) + 1) โ
1))) |
78 | | oveq2 7366 |
. . . . . . . . 9
โข (๐ = ((๐ โ 1) + 1) โ (๐ดโ๐) = (๐ดโ((๐ โ 1) + 1))) |
79 | 77, 78 | oveq12d 7376 |
. . . . . . . 8
โข (๐ = ((๐ โ 1) + 1) โ ((-1โ(๐ โ 1)) ยท (๐ดโ๐)) = ((-1โ(((๐ โ 1) + 1) โ 1)) ยท (๐ดโ((๐ โ 1) + 1)))) |
80 | 59, 75, 79 | fsumm1 15641 |
. . . . . . 7
โข (๐ โ ฮฃ๐ โ ((0 + 1)...((๐ โ 1) + 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)) = (ฮฃ๐ โ ((0 + 1)...(((๐ โ 1) + 1) โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ((-1โ(((๐ โ 1) + 1) โ 1)) ยท (๐ดโ((๐ โ 1) + 1))))) |
81 | 32 | zcnd 12613 |
. . . . . . . . . . . 12
โข (๐ โ (๐ โ 1) โ โ) |
82 | | pncan1 11584 |
. . . . . . . . . . . 12
โข ((๐ โ 1) โ โ
โ (((๐ โ 1) + 1)
โ 1) = (๐ โ
1)) |
83 | 81, 82 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (((๐ โ 1) + 1) โ 1) = (๐ โ 1)) |
84 | 83 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ โ ((0 + 1)...(((๐ โ 1) + 1) โ 1)) =
((0 + 1)...(๐ โ
1))) |
85 | 84 | sumeq1d 15591 |
. . . . . . . . 9
โข (๐ โ ฮฃ๐ โ ((0 + 1)...(((๐ โ 1) + 1) โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)) = ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐))) |
86 | | oveq1 7365 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ โ 1) = (๐ โ 1)) |
87 | 86 | oveq2d 7374 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (-1โ(๐ โ 1)) = (-1โ(๐ โ 1))) |
88 | | oveq2 7366 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
89 | 87, 88 | oveq12d 7376 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((-1โ(๐ โ 1)) ยท (๐ดโ๐)) = ((-1โ(๐ โ 1)) ยท (๐ดโ๐))) |
90 | 89 | cbvsumv 15586 |
. . . . . . . . 9
โข
ฮฃ๐ โ ((0
+ 1)...(๐ โ
1))((-1โ(๐ โ 1))
ยท (๐ดโ๐)) = ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)) |
91 | 85, 90 | eqtrdi 2789 |
. . . . . . . 8
โข (๐ โ ฮฃ๐ โ ((0 + 1)...(((๐ โ 1) + 1) โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)) = ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐))) |
92 | 83 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ โ (-1โ(((๐ โ 1) + 1) โ 1)) =
(-1โ(๐ โ
1))) |
93 | 53 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ โ (๐ดโ((๐ โ 1) + 1)) = (๐ดโ๐)) |
94 | 92, 93 | oveq12d 7376 |
. . . . . . . 8
โข (๐ โ ((-1โ(((๐ โ 1) + 1) โ 1))
ยท (๐ดโ((๐ โ 1) + 1))) =
((-1โ(๐ โ 1))
ยท (๐ดโ๐))) |
95 | 91, 94 | oveq12d 7376 |
. . . . . . 7
โข (๐ โ (ฮฃ๐ โ ((0 + 1)...(((๐ โ 1) + 1) โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ((-1โ(((๐ โ 1) + 1) โ 1)) ยท (๐ดโ((๐ โ 1) + 1)))) = (ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ((-1โ(๐ โ 1)) ยท (๐ดโ๐)))) |
96 | 80, 95 | eqtrd 2773 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ ((0 + 1)...((๐ โ 1) + 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)) = (ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ((-1โ(๐ โ 1)) ยท (๐ดโ๐)))) |
97 | 42, 50, 96 | 3eqtrd 2777 |
. . . . 5
โข (๐ โ ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ(๐ + 1))) = (ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ((-1โ(๐ โ 1)) ยท (๐ดโ๐)))) |
98 | | nnm1nn0 12459 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
99 | | elnn0uz 12813 |
. . . . . . . . 9
โข ((๐ โ 1) โ
โ0 โ (๐ โ 1) โ
(โคโฅโ0)) |
100 | 98, 99 | sylib 217 |
. . . . . . . 8
โข (๐ โ โ โ (๐ โ 1) โ
(โคโฅโ0)) |
101 | 28, 100 | syl 17 |
. . . . . . 7
โข (๐ โ (๐ โ 1) โ
(โคโฅโ0)) |
102 | | oveq2 7366 |
. . . . . . . . 9
โข (๐ = 0 โ (-1โ๐) =
(-1โ0)) |
103 | | exp0 13977 |
. . . . . . . . . 10
โข (-1
โ โ โ (-1โ0) = 1) |
104 | 4, 103 | ax-mp 5 |
. . . . . . . . 9
โข
(-1โ0) = 1 |
105 | 102, 104 | eqtrdi 2789 |
. . . . . . . 8
โข (๐ = 0 โ (-1โ๐) = 1) |
106 | | oveq2 7366 |
. . . . . . . 8
โข (๐ = 0 โ (๐ดโ๐) = (๐ดโ0)) |
107 | 105, 106 | oveq12d 7376 |
. . . . . . 7
โข (๐ = 0 โ ((-1โ๐) ยท (๐ดโ๐)) = (1 ยท (๐ดโ0))) |
108 | 101, 11, 107 | fsum1p 15643 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐)) = ((1 ยท (๐ดโ0)) + ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐)))) |
109 | 1 | exp0d 14051 |
. . . . . . . . 9
โข (๐ โ (๐ดโ0) = 1) |
110 | 109 | oveq2d 7374 |
. . . . . . . 8
โข (๐ โ (1 ยท (๐ดโ0)) = (1 ยท
1)) |
111 | | 1t1e1 12320 |
. . . . . . . 8
โข (1
ยท 1) = 1 |
112 | 110, 111 | eqtrdi 2789 |
. . . . . . 7
โข (๐ โ (1 ยท (๐ดโ0)) = 1) |
113 | 112 | oveq1d 7373 |
. . . . . 6
โข (๐ โ ((1 ยท (๐ดโ0)) + ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐))) = (1 + ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐)))) |
114 | | fzfid 13884 |
. . . . . . . 8
โข (๐ โ ((0 + 1)...(๐ โ 1)) โ
Fin) |
115 | | elfznn 13476 |
. . . . . . . . . . 11
โข (๐ โ (1...(๐ โ 1)) โ ๐ โ โ) |
116 | 4 | a1i 11 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ โ) โ -1 โ
โ) |
117 | | nnnn0 12425 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ
โ0) |
118 | 117 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ โ) โ ๐ โ โ0) |
119 | 116, 118 | expcld 14057 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ โ) โ (-1โ๐) โ
โ) |
120 | 1 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ โ) โ ๐ด โ โ) |
121 | 120, 118 | expcld 14057 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ โ) โ (๐ดโ๐) โ โ) |
122 | 119, 121 | mulcld 11180 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ โ) โ ((-1โ๐) ยท (๐ดโ๐)) โ โ) |
123 | 122 | expcom 415 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ โ ((-1โ๐) ยท (๐ดโ๐)) โ โ)) |
124 | 115, 123 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (1...(๐ โ 1)) โ (๐ โ ((-1โ๐) ยท (๐ดโ๐)) โ โ)) |
125 | 54 | oveq1i 7368 |
. . . . . . . . . 10
โข ((0 +
1)...(๐ โ 1)) =
(1...(๐ โ
1)) |
126 | 124, 125 | eleq2s 2852 |
. . . . . . . . 9
โข (๐ โ ((0 + 1)...(๐ โ 1)) โ (๐ โ ((-1โ๐) ยท (๐ดโ๐)) โ โ)) |
127 | 126 | impcom 409 |
. . . . . . . 8
โข ((๐ โง ๐ โ ((0 + 1)...(๐ โ 1))) โ ((-1โ๐) ยท (๐ดโ๐)) โ โ) |
128 | 114, 127 | fsumcl 15623 |
. . . . . . 7
โข (๐ โ ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐)) โ โ) |
129 | 2, 128 | addcomd 11362 |
. . . . . 6
โข (๐ โ (1 + ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐))) = (ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐)) + 1)) |
130 | 108, 113,
129 | 3eqtrd 2777 |
. . . . 5
โข (๐ โ ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐)) = (ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐)) + 1)) |
131 | 97, 130 | oveq12d 7376 |
. . . 4
โข (๐ โ (ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ(๐ + 1))) + ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐))) = ((ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ((-1โ(๐ โ 1)) ยท (๐ดโ๐))) + (ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐)) + 1))) |
132 | | nnm1nn0 12459 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
133 | 132 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ โ) โ (๐ โ 1) โ
โ0) |
134 | 116, 133 | expcld 14057 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ โ) โ (-1โ(๐ โ 1)) โ
โ) |
135 | 134, 121 | mulcld 11180 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ) โ ((-1โ(๐ โ 1)) ยท (๐ดโ๐)) โ โ) |
136 | 135 | expcom 415 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ โ ((-1โ(๐ โ 1)) ยท (๐ดโ๐)) โ โ)) |
137 | 115, 136 | syl 17 |
. . . . . . . . 9
โข (๐ โ (1...(๐ โ 1)) โ (๐ โ ((-1โ(๐ โ 1)) ยท (๐ดโ๐)) โ โ)) |
138 | 137, 125 | eleq2s 2852 |
. . . . . . . 8
โข (๐ โ ((0 + 1)...(๐ โ 1)) โ (๐ โ ((-1โ(๐ โ 1)) ยท (๐ดโ๐)) โ โ)) |
139 | 138 | impcom 409 |
. . . . . . 7
โข ((๐ โง ๐ โ ((0 + 1)...(๐ โ 1))) โ ((-1โ(๐ โ 1)) ยท (๐ดโ๐)) โ โ) |
140 | 114, 139 | fsumcl 15623 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)) โ โ) |
141 | 4 | a1i 11 |
. . . . . . . 8
โข (๐ โ -1 โ
โ) |
142 | 28, 98 | syl 17 |
. . . . . . . 8
โข (๐ โ (๐ โ 1) โ
โ0) |
143 | 141, 142 | expcld 14057 |
. . . . . . 7
โข (๐ โ (-1โ(๐ โ 1)) โ
โ) |
144 | 28 | nnnn0d 12478 |
. . . . . . . 8
โข (๐ โ ๐ โ
โ0) |
145 | 1, 144 | expcld 14057 |
. . . . . . 7
โข (๐ โ (๐ดโ๐) โ โ) |
146 | 143, 145 | mulcld 11180 |
. . . . . 6
โข (๐ โ ((-1โ(๐ โ 1)) ยท (๐ดโ๐)) โ โ) |
147 | 140, 146 | addcld 11179 |
. . . . 5
โข (๐ โ (ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ((-1โ(๐ โ 1)) ยท (๐ดโ๐))) โ โ) |
148 | 147, 128,
2 | addassd 11182 |
. . . 4
โข (๐ โ (((ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ((-1โ(๐ โ 1)) ยท (๐ดโ๐))) + ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐))) + 1) = ((ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ((-1โ(๐ โ 1)) ยท (๐ดโ๐))) + (ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐)) + 1))) |
149 | 140, 146 | addcomd 11362 |
. . . . . . 7
โข (๐ โ (ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ((-1โ(๐ โ 1)) ยท (๐ดโ๐))) = (((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)))) |
150 | 149 | oveq1d 7373 |
. . . . . 6
โข (๐ โ ((ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ((-1โ(๐ โ 1)) ยท (๐ดโ๐))) + ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐))) = ((((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐))) + ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐)))) |
151 | 146, 140,
128 | addassd 11182 |
. . . . . 6
โข (๐ โ ((((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐))) + ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐))) = (((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + (ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐))))) |
152 | | nncn 12166 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ ๐ โ
โ) |
153 | | npcan1 11585 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ ((๐ โ 1) + 1) = ๐) |
154 | 152, 153 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ ((๐ โ 1) + 1) = ๐) |
155 | 154 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ ๐ = ((๐ โ 1) + 1)) |
156 | 155 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ
(-1โ๐) =
(-1โ((๐ โ 1) +
1))) |
157 | 4 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ -1 โ
โ) |
158 | 157, 132 | expp1d 14058 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ
(-1โ((๐ โ 1) +
1)) = ((-1โ(๐ โ
1)) ยท -1)) |
159 | 157, 132 | expcld 14057 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ
(-1โ(๐ โ 1))
โ โ) |
160 | 159, 157 | mulcomd 11181 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ
((-1โ(๐ โ 1))
ยท -1) = (-1 ยท (-1โ(๐ โ 1)))) |
161 | 156, 158,
160 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ
(-1โ๐) = (-1 ยท
(-1โ(๐ โ
1)))) |
162 | 161 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ
((-1โ(๐ โ 1)) +
(-1โ๐)) =
((-1โ(๐ โ 1)) +
(-1 ยท (-1โ(๐
โ 1))))) |
163 | 159 | mulm1d 11612 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ (-1
ยท (-1โ(๐
โ 1))) = -(-1โ(๐
โ 1))) |
164 | 163 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ
((-1โ(๐ โ 1)) +
(-1 ยท (-1โ(๐
โ 1)))) = ((-1โ(๐ โ 1)) + -(-1โ(๐ โ 1)))) |
165 | 159 | negidd 11507 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ
((-1โ(๐ โ 1)) +
-(-1โ(๐ โ 1))) =
0) |
166 | 162, 164,
165 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ
((-1โ(๐ โ 1)) +
(-1โ๐)) =
0) |
167 | 166 | adantl 483 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ โ) โ ((-1โ(๐ โ 1)) + (-1โ๐)) = 0) |
168 | 167 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ โ) โ (((-1โ(๐ โ 1)) + (-1โ๐)) ยท (๐ดโ๐)) = (0 ยท (๐ดโ๐))) |
169 | 134, 119,
121 | adddird 11185 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ โ) โ (((-1โ(๐ โ 1)) + (-1โ๐)) ยท (๐ดโ๐)) = (((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ((-1โ๐) ยท (๐ดโ๐)))) |
170 | 121 | mul02d 11358 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ โ) โ (0 ยท (๐ดโ๐)) = 0) |
171 | 168, 169,
170 | 3eqtr3d 2781 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ โ) โ (((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ((-1โ๐) ยท (๐ดโ๐))) = 0) |
172 | 171 | expcom 415 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐ โ (((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ((-1โ๐) ยท (๐ดโ๐))) = 0)) |
173 | 115, 172 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ (1...(๐ โ 1)) โ (๐ โ (((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ((-1โ๐) ยท (๐ดโ๐))) = 0)) |
174 | 173, 125 | eleq2s 2852 |
. . . . . . . . . . 11
โข (๐ โ ((0 + 1)...(๐ โ 1)) โ (๐ โ (((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ((-1โ๐) ยท (๐ดโ๐))) = 0)) |
175 | 174 | impcom 409 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ((0 + 1)...(๐ โ 1))) โ (((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ((-1โ๐) ยท (๐ดโ๐))) = 0) |
176 | 175 | sumeq2dv 15593 |
. . . . . . . . 9
โข (๐ โ ฮฃ๐ โ ((0 + 1)...(๐ โ 1))(((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ((-1โ๐) ยท (๐ดโ๐))) = ฮฃ๐ โ ((0 + 1)...(๐ โ 1))0) |
177 | 114, 139,
127 | fsumadd 15630 |
. . . . . . . . 9
โข (๐ โ ฮฃ๐ โ ((0 + 1)...(๐ โ 1))(((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ((-1โ๐) ยท (๐ดโ๐))) = (ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐)))) |
178 | 114 | olcd 873 |
. . . . . . . . . 10
โข (๐ โ (((0 + 1)...(๐ โ 1)) โ
(โคโฅโ1) โจ ((0 + 1)...(๐ โ 1)) โ Fin)) |
179 | | sumz 15612 |
. . . . . . . . . 10
โข ((((0 +
1)...(๐ โ 1)) โ
(โคโฅโ1) โจ ((0 + 1)...(๐ โ 1)) โ Fin) โ ฮฃ๐ โ ((0 + 1)...(๐ โ 1))0 =
0) |
180 | 178, 179 | syl 17 |
. . . . . . . . 9
โข (๐ โ ฮฃ๐ โ ((0 + 1)...(๐ โ 1))0 = 0) |
181 | 176, 177,
180 | 3eqtr3d 2781 |
. . . . . . . 8
โข (๐ โ (ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐))) = 0) |
182 | 181 | oveq2d 7374 |
. . . . . . 7
โข (๐ โ (((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + (ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐)))) = (((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + 0)) |
183 | 146 | addid1d 11360 |
. . . . . . 7
โข (๐ โ (((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + 0) = ((-1โ(๐ โ 1)) ยท (๐ดโ๐))) |
184 | 182, 183 | eqtrd 2773 |
. . . . . 6
โข (๐ โ (((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + (ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐)))) = ((-1โ(๐ โ 1)) ยท (๐ดโ๐))) |
185 | 150, 151,
184 | 3eqtrd 2777 |
. . . . 5
โข (๐ โ ((ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ((-1โ(๐ โ 1)) ยท (๐ดโ๐))) + ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐))) = ((-1โ(๐ โ 1)) ยท (๐ดโ๐))) |
186 | 185 | oveq1d 7373 |
. . . 4
โข (๐ โ (((ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + ((-1โ(๐ โ 1)) ยท (๐ดโ๐))) + ฮฃ๐ โ ((0 + 1)...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐))) + 1) = (((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + 1)) |
187 | 131, 148,
186 | 3eqtr2d 2779 |
. . 3
โข (๐ โ (ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ(๐ + 1))) + ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐))) = (((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + 1)) |
188 | 13, 25, 187 | 3eqtrd 2777 |
. 2
โข (๐ โ ((๐ด + 1) ยท ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐))) = (((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + 1)) |
189 | 188 | eqcomd 2739 |
1
โข (๐ โ (((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + 1) = ((๐ด + 1) ยท ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐)))) |