Description: Index shift of a finite group sum over a finite set of sequential integers. (Contributed by AV, 24-Aug-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | gsummptshft.b | |
|
gsummptshft.z | |
||
gsummptshft.g | |
||
gsummptshft.k | |
||
gsummptshft.m | |
||
gsummptshft.n | |
||
gsummptshft.a | |
||
gsummptshft.c | |
||
Assertion | gsummptshft | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | gsummptshft.b | |
|
2 | gsummptshft.z | |
|
3 | gsummptshft.g | |
|
4 | gsummptshft.k | |
|
5 | gsummptshft.m | |
|
6 | gsummptshft.n | |
|
7 | gsummptshft.a | |
|
8 | gsummptshft.c | |
|
9 | ovexd | |
|
10 | 7 | fmpttd | |
11 | eqid | |
|
12 | fzfid | |
|
13 | 2 | fvexi | |
14 | 13 | a1i | |
15 | 11 12 7 14 | fsuppmptdm | |
16 | 4 5 6 | mptfzshft | |
17 | 1 2 3 9 10 15 16 | gsumf1o | |
18 | elfzelz | |
|
19 | 18 | zcnd | |
20 | 4 | zcnd | |
21 | npcan | |
|
22 | 19 20 21 | syl2anr | |
23 | simpr | |
|
24 | 22 23 | eqeltrd | |
25 | 5 6 | jca | |
26 | 25 | adantr | |
27 | 18 | adantl | |
28 | 4 | adantr | |
29 | 27 28 | zsubcld | |
30 | fzaddel | |
|
31 | 26 29 28 30 | syl12anc | |
32 | 24 31 | mpbird | |
33 | eqidd | |
|
34 | eqidd | |
|
35 | 32 33 34 8 | fmptco | |
36 | 35 | oveq2d | |
37 | 17 36 | eqtrd | |