Step | Hyp | Ref
| Expression |
1 | | sum0 15613 |
. . . 4
โข
ฮฃ๐ โ
โ
(๐ต ยท (๐ โ ๐)) = 0 |
2 | | 0m0e0 12280 |
. . . 4
โข (0
โ 0) = 0 |
3 | 1, 2 | eqtr4i 2768 |
. . 3
โข
ฮฃ๐ โ
โ
(๐ต ยท (๐ โ ๐)) = (0 โ 0) |
4 | | simpr 486 |
. . . . . 6
โข ((๐ โง ๐ = ๐) โ ๐ = ๐) |
5 | 4 | oveq2d 7378 |
. . . . 5
โข ((๐ โง ๐ = ๐) โ (๐..^๐) = (๐..^๐)) |
6 | | fzo0 13603 |
. . . . 5
โข (๐..^๐) = โ
|
7 | 5, 6 | eqtrdi 2793 |
. . . 4
โข ((๐ โง ๐ = ๐) โ (๐..^๐) = โ
) |
8 | 7 | sumeq1d 15593 |
. . 3
โข ((๐ โง ๐ = ๐) โ ฮฃ๐ โ (๐..^๐)(๐ต ยท (๐ โ ๐)) = ฮฃ๐ โ โ
(๐ต ยท (๐ โ ๐))) |
9 | | fsumparts.1 |
. . . . . . . 8
โข (๐ โ ๐ โ (โคโฅโ๐)) |
10 | | eluzfz1 13455 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ๐) โ ๐ โ (๐...๐)) |
11 | 9, 10 | syl 17 |
. . . . . . 7
โข (๐ โ ๐ โ (๐...๐)) |
12 | | eqtr3 2763 |
. . . . . . . . . . . 12
โข ((๐ = ๐ โง ๐ = ๐) โ ๐ = ๐) |
13 | | fsumparts.e |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ด = ๐ธ โง ๐ = ๐)) |
14 | | oveq12 7371 |
. . . . . . . . . . . 12
โข ((๐ด = ๐ธ โง ๐ = ๐) โ (๐ด ยท ๐) = (๐ธ ยท ๐)) |
15 | 12, 13, 14 | 3syl 18 |
. . . . . . . . . . 11
โข ((๐ = ๐ โง ๐ = ๐) โ (๐ด ยท ๐) = (๐ธ ยท ๐)) |
16 | | fsumparts.d |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐ด = ๐ท โง ๐ = ๐)) |
17 | | oveq12 7371 |
. . . . . . . . . . . . 13
โข ((๐ด = ๐ท โง ๐ = ๐) โ (๐ด ยท ๐) = (๐ท ยท ๐)) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ด ยท ๐) = (๐ท ยท ๐)) |
19 | 18 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ = ๐ โง ๐ = ๐) โ (๐ด ยท ๐) = (๐ท ยท ๐)) |
20 | 15, 19 | eqeq12d 2753 |
. . . . . . . . . 10
โข ((๐ = ๐ โง ๐ = ๐) โ ((๐ด ยท ๐) = (๐ด ยท ๐) โ (๐ธ ยท ๐) = (๐ท ยท ๐))) |
21 | 20 | pm5.74da 803 |
. . . . . . . . 9
โข (๐ = ๐ โ ((๐ = ๐ โ (๐ด ยท ๐) = (๐ด ยท ๐)) โ (๐ = ๐ โ (๐ธ ยท ๐) = (๐ท ยท ๐)))) |
22 | | eqidd 2738 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ด ยท ๐) = (๐ด ยท ๐)) |
23 | 21, 22 | vtoclg 3528 |
. . . . . . . 8
โข (๐ โ (๐...๐) โ (๐ = ๐ โ (๐ธ ยท ๐) = (๐ท ยท ๐))) |
24 | 23 | imp 408 |
. . . . . . 7
โข ((๐ โ (๐...๐) โง ๐ = ๐) โ (๐ธ ยท ๐) = (๐ท ยท ๐)) |
25 | 11, 24 | sylan 581 |
. . . . . 6
โข ((๐ โง ๐ = ๐) โ (๐ธ ยท ๐) = (๐ท ยท ๐)) |
26 | 25 | oveq1d 7377 |
. . . . 5
โข ((๐ โง ๐ = ๐) โ ((๐ธ ยท ๐) โ (๐ท ยท ๐)) = ((๐ท ยท ๐) โ (๐ท ยท ๐))) |
27 | 16 | simpld 496 |
. . . . . . . . . 10
โข (๐ = ๐ โ ๐ด = ๐ท) |
28 | 27 | eleq1d 2823 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ด โ โ โ ๐ท โ โ)) |
29 | | fsumparts.2 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) |
30 | 29 | ralrimiva 3144 |
. . . . . . . . 9
โข (๐ โ โ๐ โ (๐...๐)๐ด โ โ) |
31 | 28, 30, 11 | rspcdva 3585 |
. . . . . . . 8
โข (๐ โ ๐ท โ โ) |
32 | 16 | simprd 497 |
. . . . . . . . . 10
โข (๐ = ๐ โ ๐ = ๐) |
33 | 32 | eleq1d 2823 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ โ โ โ ๐ โ โ)) |
34 | | fsumparts.3 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (๐...๐)) โ ๐ โ โ) |
35 | 34 | ralrimiva 3144 |
. . . . . . . . 9
โข (๐ โ โ๐ โ (๐...๐)๐ โ โ) |
36 | 33, 35, 11 | rspcdva 3585 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
37 | 31, 36 | mulcld 11182 |
. . . . . . 7
โข (๐ โ (๐ท ยท ๐) โ โ) |
38 | 37 | subidd 11507 |
. . . . . 6
โข (๐ โ ((๐ท ยท ๐) โ (๐ท ยท ๐)) = 0) |
39 | 38 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ = ๐) โ ((๐ท ยท ๐) โ (๐ท ยท ๐)) = 0) |
40 | 26, 39 | eqtrd 2777 |
. . . 4
โข ((๐ โง ๐ = ๐) โ ((๐ธ ยท ๐) โ (๐ท ยท ๐)) = 0) |
41 | 7 | sumeq1d 15593 |
. . . . 5
โข ((๐ โง ๐ = ๐) โ ฮฃ๐ โ (๐..^๐)((๐ถ โ ๐ต) ยท ๐) = ฮฃ๐ โ โ
((๐ถ โ ๐ต) ยท ๐)) |
42 | | sum0 15613 |
. . . . 5
โข
ฮฃ๐ โ
โ
((๐ถ โ ๐ต) ยท ๐) = 0 |
43 | 41, 42 | eqtrdi 2793 |
. . . 4
โข ((๐ โง ๐ = ๐) โ ฮฃ๐ โ (๐..^๐)((๐ถ โ ๐ต) ยท ๐) = 0) |
44 | 40, 43 | oveq12d 7380 |
. . 3
โข ((๐ โง ๐ = ๐) โ (((๐ธ ยท ๐) โ (๐ท ยท ๐)) โ ฮฃ๐ โ (๐..^๐)((๐ถ โ ๐ต) ยท ๐)) = (0 โ 0)) |
45 | 3, 8, 44 | 3eqtr4a 2803 |
. 2
โข ((๐ โง ๐ = ๐) โ ฮฃ๐ โ (๐..^๐)(๐ต ยท (๐ โ ๐)) = (((๐ธ ยท ๐) โ (๐ท ยท ๐)) โ ฮฃ๐ โ (๐..^๐)((๐ถ โ ๐ต) ยท ๐))) |
46 | | fzofi 13886 |
. . . . . . . . 9
โข ((๐ + 1)..^๐) โ Fin |
47 | 46 | a1i 11 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ((๐ + 1)..^๐) โ Fin) |
48 | | eluzel2 12775 |
. . . . . . . . . . . . 13
โข (๐ โ
(โคโฅโ๐) โ ๐ โ โค) |
49 | 9, 48 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โค) |
50 | 49 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ๐ โ โค) |
51 | | uzid 12785 |
. . . . . . . . . . 11
โข (๐ โ โค โ ๐ โ
(โคโฅโ๐)) |
52 | | peano2uz 12833 |
. . . . . . . . . . 11
โข (๐ โ
(โคโฅโ๐) โ (๐ + 1) โ
(โคโฅโ๐)) |
53 | | fzoss1 13606 |
. . . . . . . . . . 11
โข ((๐ + 1) โ
(โคโฅโ๐) โ ((๐ + 1)..^๐) โ (๐..^๐)) |
54 | 50, 51, 52, 53 | 4syl 19 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ((๐ + 1)..^๐) โ (๐..^๐)) |
55 | 54 | sselda 3949 |
. . . . . . . . 9
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)..^๐)) โ ๐ โ (๐..^๐)) |
56 | | elfzofz 13595 |
. . . . . . . . . . 11
โข (๐ โ (๐..^๐) โ ๐ โ (๐...๐)) |
57 | 29, 34 | mulcld 11182 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (๐...๐)) โ (๐ด ยท ๐) โ โ) |
58 | 56, 57 | sylan2 594 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (๐..^๐)) โ (๐ด ยท ๐) โ โ) |
59 | 58 | adantlr 714 |
. . . . . . . . 9
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ (๐..^๐)) โ (๐ด ยท ๐) โ โ) |
60 | 55, 59 | syldan 592 |
. . . . . . . 8
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)..^๐)) โ (๐ด ยท ๐) โ โ) |
61 | 47, 60 | fsumcl 15625 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ฮฃ๐ โ ((๐ + 1)..^๐)(๐ด ยท ๐) โ โ) |
62 | 13 | simpld 496 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ๐ด = ๐ธ) |
63 | 62 | eleq1d 2823 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ด โ โ โ ๐ธ โ โ)) |
64 | | eluzfz2 13456 |
. . . . . . . . . . 11
โข (๐ โ
(โคโฅโ๐) โ ๐ โ (๐...๐)) |
65 | 9, 64 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ๐ โ (๐...๐)) |
66 | 63, 30, 65 | rspcdva 3585 |
. . . . . . . . 9
โข (๐ โ ๐ธ โ โ) |
67 | 13 | simprd 497 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ๐ = ๐) |
68 | 67 | eleq1d 2823 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ โ โ โ ๐ โ โ)) |
69 | 68, 35, 65 | rspcdva 3585 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
70 | 66, 69 | mulcld 11182 |
. . . . . . . 8
โข (๐ โ (๐ธ ยท ๐) โ โ) |
71 | 70 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ (๐ธ ยท ๐) โ โ) |
72 | | simpr 486 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ๐ โ (โคโฅโ(๐ + 1))) |
73 | | fzp1ss 13499 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ((๐ + 1)...๐) โ (๐...๐)) |
74 | 50, 73 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ((๐ + 1)...๐) โ (๐...๐)) |
75 | 74 | sselda 3949 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ ๐ โ (๐...๐)) |
76 | 57 | adantlr 714 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ (๐...๐)) โ (๐ด ยท ๐) โ โ) |
77 | 75, 76 | syldan 592 |
. . . . . . . . 9
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ (๐ด ยท ๐) โ โ) |
78 | 13, 14 | syl 17 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ด ยท ๐) = (๐ธ ยท ๐)) |
79 | 72, 77, 78 | fsumm1 15643 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ฮฃ๐ โ ((๐ + 1)...๐)(๐ด ยท ๐) = (ฮฃ๐ โ ((๐ + 1)...(๐ โ 1))(๐ด ยท ๐) + (๐ธ ยท ๐))) |
80 | | eluzelz 12780 |
. . . . . . . . . . . . . 14
โข (๐ โ
(โคโฅโ๐) โ ๐ โ โค) |
81 | 9, 80 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โค) |
82 | 81 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ๐ โ โค) |
83 | | fzoval 13580 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (๐..^๐) = (๐...(๐ โ 1))) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ (๐..^๐) = (๐...(๐ โ 1))) |
85 | 50 | zcnd 12615 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ๐ โ โ) |
86 | | ax-1cn 11116 |
. . . . . . . . . . . . 13
โข 1 โ
โ |
87 | | pncan 11414 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง 1 โ
โ) โ ((๐ + 1)
โ 1) = ๐) |
88 | 85, 86, 87 | sylancl 587 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ((๐ + 1) โ 1) = ๐) |
89 | 88 | oveq1d 7377 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ (((๐ + 1) โ 1)...(๐ โ 1)) = (๐...(๐ โ 1))) |
90 | 84, 89 | eqtr4d 2780 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ (๐..^๐) = (((๐ + 1) โ 1)...(๐ โ 1))) |
91 | 90 | sumeq1d 15593 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ฮฃ๐ โ (๐..^๐)(๐ถ ยท ๐) = ฮฃ๐ โ (((๐ + 1) โ 1)...(๐ โ 1))(๐ถ ยท ๐)) |
92 | | 1zzd 12541 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ 1 โ
โค) |
93 | 50 | peano2zd 12617 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ (๐ + 1) โ
โค) |
94 | | fsumparts.c |
. . . . . . . . . . 11
โข (๐ = (๐ + 1) โ (๐ด = ๐ถ โง ๐ = ๐)) |
95 | | oveq12 7371 |
. . . . . . . . . . 11
โข ((๐ด = ๐ถ โง ๐ = ๐) โ (๐ด ยท ๐) = (๐ถ ยท ๐)) |
96 | 94, 95 | syl 17 |
. . . . . . . . . 10
โข (๐ = (๐ + 1) โ (๐ด ยท ๐) = (๐ถ ยท ๐)) |
97 | 92, 93, 82, 77, 96 | fsumshftm 15673 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ฮฃ๐ โ ((๐ + 1)...๐)(๐ด ยท ๐) = ฮฃ๐ โ (((๐ + 1) โ 1)...(๐ โ 1))(๐ถ ยท ๐)) |
98 | 91, 97 | eqtr4d 2780 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ฮฃ๐ โ (๐..^๐)(๐ถ ยท ๐) = ฮฃ๐ โ ((๐ + 1)...๐)(๐ด ยท ๐)) |
99 | | fzoval 13580 |
. . . . . . . . . . 11
โข (๐ โ โค โ ((๐ + 1)..^๐) = ((๐ + 1)...(๐ โ 1))) |
100 | 82, 99 | syl 17 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ((๐ + 1)..^๐) = ((๐ + 1)...(๐ โ 1))) |
101 | 100 | sumeq1d 15593 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ฮฃ๐ โ ((๐ + 1)..^๐)(๐ด ยท ๐) = ฮฃ๐ โ ((๐ + 1)...(๐ โ 1))(๐ด ยท ๐)) |
102 | 101 | oveq1d 7377 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ (ฮฃ๐ โ ((๐ + 1)..^๐)(๐ด ยท ๐) + (๐ธ ยท ๐)) = (ฮฃ๐ โ ((๐ + 1)...(๐ โ 1))(๐ด ยท ๐) + (๐ธ ยท ๐))) |
103 | 79, 98, 102 | 3eqtr4d 2787 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ฮฃ๐ โ (๐..^๐)(๐ถ ยท ๐) = (ฮฃ๐ โ ((๐ + 1)..^๐)(๐ด ยท ๐) + (๐ธ ยท ๐))) |
104 | 61, 71, 103 | comraddd 11376 |
. . . . . 6
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ฮฃ๐ โ (๐..^๐)(๐ถ ยท ๐) = ((๐ธ ยท ๐) + ฮฃ๐ โ ((๐ + 1)..^๐)(๐ด ยท ๐))) |
105 | 104 | oveq1d 7377 |
. . . . 5
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ (ฮฃ๐ โ (๐..^๐)(๐ถ ยท ๐) โ ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐)) = (((๐ธ ยท ๐) + ฮฃ๐ โ ((๐ + 1)..^๐)(๐ด ยท ๐)) โ ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐))) |
106 | | fzofzp1 13676 |
. . . . . . . . . 10
โข (๐ โ (๐..^๐) โ (๐ + 1) โ (๐...๐)) |
107 | 94 | simpld 496 |
. . . . . . . . . . . 12
โข (๐ = (๐ + 1) โ ๐ด = ๐ถ) |
108 | 107 | eleq1d 2823 |
. . . . . . . . . . 11
โข (๐ = (๐ + 1) โ (๐ด โ โ โ ๐ถ โ โ)) |
109 | 108 | rspccva 3583 |
. . . . . . . . . 10
โข
((โ๐ โ
(๐...๐)๐ด โ โ โง (๐ + 1) โ (๐...๐)) โ ๐ถ โ โ) |
110 | 30, 106, 109 | syl2an 597 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (๐..^๐)) โ ๐ถ โ โ) |
111 | | elfzofz 13595 |
. . . . . . . . . 10
โข (๐ โ (๐..^๐) โ ๐ โ (๐...๐)) |
112 | | fsumparts.b |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐ด = ๐ต โง ๐ = ๐)) |
113 | 112 | simpld 496 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ๐ด = ๐ต) |
114 | 113 | eleq1d 2823 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐ด โ โ โ ๐ต โ โ)) |
115 | 114 | rspccva 3583 |
. . . . . . . . . 10
โข
((โ๐ โ
(๐...๐)๐ด โ โ โง ๐ โ (๐...๐)) โ ๐ต โ โ) |
116 | 30, 111, 115 | syl2an 597 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (๐..^๐)) โ ๐ต โ โ) |
117 | 94 | simprd 497 |
. . . . . . . . . . . 12
โข (๐ = (๐ + 1) โ ๐ = ๐) |
118 | 117 | eleq1d 2823 |
. . . . . . . . . . 11
โข (๐ = (๐ + 1) โ (๐ โ โ โ ๐ โ โ)) |
119 | 118 | rspccva 3583 |
. . . . . . . . . 10
โข
((โ๐ โ
(๐...๐)๐ โ โ โง (๐ + 1) โ (๐...๐)) โ ๐ โ โ) |
120 | 35, 106, 119 | syl2an 597 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (๐..^๐)) โ ๐ โ โ) |
121 | 110, 116,
120 | subdird 11619 |
. . . . . . . 8
โข ((๐ โง ๐ โ (๐..^๐)) โ ((๐ถ โ ๐ต) ยท ๐) = ((๐ถ ยท ๐) โ (๐ต ยท ๐))) |
122 | 121 | sumeq2dv 15595 |
. . . . . . 7
โข (๐ โ ฮฃ๐ โ (๐..^๐)((๐ถ โ ๐ต) ยท ๐) = ฮฃ๐ โ (๐..^๐)((๐ถ ยท ๐) โ (๐ต ยท ๐))) |
123 | | fzofi 13886 |
. . . . . . . . 9
โข (๐..^๐) โ Fin |
124 | 123 | a1i 11 |
. . . . . . . 8
โข (๐ โ (๐..^๐) โ Fin) |
125 | 110, 120 | mulcld 11182 |
. . . . . . . 8
โข ((๐ โง ๐ โ (๐..^๐)) โ (๐ถ ยท ๐) โ โ) |
126 | 116, 120 | mulcld 11182 |
. . . . . . . 8
โข ((๐ โง ๐ โ (๐..^๐)) โ (๐ต ยท ๐) โ โ) |
127 | 124, 125,
126 | fsumsub 15680 |
. . . . . . 7
โข (๐ โ ฮฃ๐ โ (๐..^๐)((๐ถ ยท ๐) โ (๐ต ยท ๐)) = (ฮฃ๐ โ (๐..^๐)(๐ถ ยท ๐) โ ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐))) |
128 | 122, 127 | eqtrd 2777 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ (๐..^๐)((๐ถ โ ๐ต) ยท ๐) = (ฮฃ๐ โ (๐..^๐)(๐ถ ยท ๐) โ ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐))) |
129 | 128 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ฮฃ๐ โ (๐..^๐)((๐ถ โ ๐ต) ยท ๐) = (ฮฃ๐ โ (๐..^๐)(๐ถ ยท ๐) โ ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐))) |
130 | 124, 126 | fsumcl 15625 |
. . . . . . 7
โข (๐ โ ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐) โ โ) |
131 | 130 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐) โ โ) |
132 | 71, 131, 61 | subsub3d 11549 |
. . . . 5
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ((๐ธ ยท ๐) โ (ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐) โ ฮฃ๐ โ ((๐ + 1)..^๐)(๐ด ยท ๐))) = (((๐ธ ยท ๐) + ฮฃ๐ โ ((๐ + 1)..^๐)(๐ด ยท ๐)) โ ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐))) |
133 | 105, 129,
132 | 3eqtr4d 2787 |
. . . 4
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ฮฃ๐ โ (๐..^๐)((๐ถ โ ๐ต) ยท ๐) = ((๐ธ ยท ๐) โ (ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐) โ ฮฃ๐ โ ((๐ + 1)..^๐)(๐ด ยท ๐)))) |
134 | 133 | oveq2d 7378 |
. . 3
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ (((๐ธ ยท ๐) โ (๐ท ยท ๐)) โ ฮฃ๐ โ (๐..^๐)((๐ถ โ ๐ต) ยท ๐)) = (((๐ธ ยท ๐) โ (๐ท ยท ๐)) โ ((๐ธ ยท ๐) โ (ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐) โ ฮฃ๐ โ ((๐ + 1)..^๐)(๐ด ยท ๐))))) |
135 | 37 | adantr 482 |
. . . 4
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ (๐ท ยท ๐) โ โ) |
136 | 131, 61 | subcld 11519 |
. . . 4
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ (ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐) โ ฮฃ๐ โ ((๐ + 1)..^๐)(๐ด ยท ๐)) โ โ) |
137 | 71, 135, 136 | nnncan1d 11553 |
. . 3
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ (((๐ธ ยท ๐) โ (๐ท ยท ๐)) โ ((๐ธ ยท ๐) โ (ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐) โ ฮฃ๐ โ ((๐ + 1)..^๐)(๐ด ยท ๐)))) = ((ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐) โ ฮฃ๐ โ ((๐ + 1)..^๐)(๐ด ยท ๐)) โ (๐ท ยท ๐))) |
138 | 61, 135 | addcomd 11364 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ (ฮฃ๐ โ ((๐ + 1)..^๐)(๐ด ยท ๐) + (๐ท ยท ๐)) = ((๐ท ยท ๐) + ฮฃ๐ โ ((๐ + 1)..^๐)(๐ด ยท ๐))) |
139 | | eluzp1m1 12796 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ โ 1) โ
(โคโฅโ๐)) |
140 | 49, 139 | sylan 581 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ (๐ โ 1) โ
(โคโฅโ๐)) |
141 | 84 | eleq2d 2824 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ (๐ โ (๐..^๐) โ ๐ โ (๐...(๐ โ 1)))) |
142 | 141 | biimpar 479 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ (๐...(๐ โ 1))) โ ๐ โ (๐..^๐)) |
143 | 142, 59 | syldan 592 |
. . . . . . . . 9
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ (๐...(๐ โ 1))) โ (๐ด ยท ๐) โ โ) |
144 | 140, 143,
18 | fsum1p 15645 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ฮฃ๐ โ (๐...(๐ โ 1))(๐ด ยท ๐) = ((๐ท ยท ๐) + ฮฃ๐ โ ((๐ + 1)...(๐ โ 1))(๐ด ยท ๐))) |
145 | 84 | sumeq1d 15593 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ฮฃ๐ โ (๐..^๐)(๐ด ยท ๐) = ฮฃ๐ โ (๐...(๐ โ 1))(๐ด ยท ๐)) |
146 | 101 | oveq2d 7378 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ((๐ท ยท ๐) + ฮฃ๐ โ ((๐ + 1)..^๐)(๐ด ยท ๐)) = ((๐ท ยท ๐) + ฮฃ๐ โ ((๐ + 1)...(๐ โ 1))(๐ด ยท ๐))) |
147 | 144, 145,
146 | 3eqtr4d 2787 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ฮฃ๐ โ (๐..^๐)(๐ด ยท ๐) = ((๐ท ยท ๐) + ฮฃ๐ โ ((๐ + 1)..^๐)(๐ด ยท ๐))) |
148 | 138, 147 | eqtr4d 2780 |
. . . . . 6
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ (ฮฃ๐ โ ((๐ + 1)..^๐)(๐ด ยท ๐) + (๐ท ยท ๐)) = ฮฃ๐ โ (๐..^๐)(๐ด ยท ๐)) |
149 | | oveq12 7371 |
. . . . . . . 8
โข ((๐ด = ๐ต โง ๐ = ๐) โ (๐ด ยท ๐) = (๐ต ยท ๐)) |
150 | 112, 149 | syl 17 |
. . . . . . 7
โข (๐ = ๐ โ (๐ด ยท ๐) = (๐ต ยท ๐)) |
151 | 150 | cbvsumv 15588 |
. . . . . 6
โข
ฮฃ๐ โ
(๐..^๐)(๐ด ยท ๐) = ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐) |
152 | 148, 151 | eqtrdi 2793 |
. . . . 5
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ (ฮฃ๐ โ ((๐ + 1)..^๐)(๐ด ยท ๐) + (๐ท ยท ๐)) = ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐)) |
153 | 152 | oveq2d 7378 |
. . . 4
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ (ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐) โ (ฮฃ๐ โ ((๐ + 1)..^๐)(๐ด ยท ๐) + (๐ท ยท ๐))) = (ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐) โ ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐))) |
154 | 131, 61, 135 | subsub4d 11550 |
. . . 4
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ((ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐) โ ฮฃ๐ โ ((๐ + 1)..^๐)(๐ด ยท ๐)) โ (๐ท ยท ๐)) = (ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐) โ (ฮฃ๐ โ ((๐ + 1)..^๐)(๐ด ยท ๐) + (๐ท ยท ๐)))) |
155 | 112 | simprd 497 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ๐ = ๐) |
156 | 155 | eleq1d 2823 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ โ โ โ ๐ โ โ)) |
157 | 156 | rspccva 3583 |
. . . . . . . . 9
โข
((โ๐ โ
(๐...๐)๐ โ โ โง ๐ โ (๐...๐)) โ ๐ โ โ) |
158 | 35, 111, 157 | syl2an 597 |
. . . . . . . 8
โข ((๐ โง ๐ โ (๐..^๐)) โ ๐ โ โ) |
159 | 116, 120,
158 | subdid 11618 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐..^๐)) โ (๐ต ยท (๐ โ ๐)) = ((๐ต ยท ๐) โ (๐ต ยท ๐))) |
160 | 159 | sumeq2dv 15595 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ (๐..^๐)(๐ต ยท (๐ โ ๐)) = ฮฃ๐ โ (๐..^๐)((๐ต ยท ๐) โ (๐ต ยท ๐))) |
161 | 116, 158 | mulcld 11182 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐..^๐)) โ (๐ต ยท ๐) โ โ) |
162 | 124, 126,
161 | fsumsub 15680 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ (๐..^๐)((๐ต ยท ๐) โ (๐ต ยท ๐)) = (ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐) โ ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐))) |
163 | 160, 162 | eqtrd 2777 |
. . . . 5
โข (๐ โ ฮฃ๐ โ (๐..^๐)(๐ต ยท (๐ โ ๐)) = (ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐) โ ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐))) |
164 | 163 | adantr 482 |
. . . 4
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ฮฃ๐ โ (๐..^๐)(๐ต ยท (๐ โ ๐)) = (ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐) โ ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐))) |
165 | 153, 154,
164 | 3eqtr4d 2787 |
. . 3
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ((ฮฃ๐ โ (๐..^๐)(๐ต ยท ๐) โ ฮฃ๐ โ ((๐ + 1)..^๐)(๐ด ยท ๐)) โ (๐ท ยท ๐)) = ฮฃ๐ โ (๐..^๐)(๐ต ยท (๐ โ ๐))) |
166 | 134, 137,
165 | 3eqtrrd 2782 |
. 2
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ฮฃ๐ โ (๐..^๐)(๐ต ยท (๐ โ ๐)) = (((๐ธ ยท ๐) โ (๐ท ยท ๐)) โ ฮฃ๐ โ (๐..^๐)((๐ถ โ ๐ต) ยท ๐))) |
167 | | uzp1 12811 |
. . 3
โข (๐ โ
(โคโฅโ๐) โ (๐ = ๐ โจ ๐ โ (โคโฅโ(๐ + 1)))) |
168 | 9, 167 | syl 17 |
. 2
โข (๐ โ (๐ = ๐ โจ ๐ โ (โคโฅโ(๐ + 1)))) |
169 | 45, 166, 168 | mpjaodan 958 |
1
โข (๐ โ ฮฃ๐ โ (๐..^๐)(๐ต ยท (๐ โ ๐)) = (((๐ธ ยท ๐) โ (๐ท ยท ๐)) โ ฮฃ๐ โ (๐..^๐)((๐ถ โ ๐ต) ยท ๐))) |