Description: Telescoping finite group sum ranging over nonnegative integers, using explicit substitution. (Contributed by AV, 24-Oct-2019) (Proof shortened by AV, 25-Nov-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | telgsumfz0s.b | |
|
telgsumfz0s.g | |
||
telgsumfz0s.m | |
||
telgsumfz0s.s | |
||
telgsumfz0s.f | |
||
Assertion | telgsumfz0s | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | telgsumfz0s.b | |
|
2 | telgsumfz0s.g | |
|
3 | telgsumfz0s.m | |
|
4 | telgsumfz0s.s | |
|
5 | telgsumfz0s.f | |
|
6 | nn0uz | |
|
7 | 4 6 | eleqtrdi | |
8 | 1 2 3 7 5 | telgsumfzs | |