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 | |- B = ( Base ` G ) |
|
| telgsumfz0s.g | |- ( ph -> G e. Abel ) |
||
| telgsumfz0s.m | |- .- = ( -g ` G ) |
||
| telgsumfz0s.s | |- ( ph -> S e. NN0 ) |
||
| telgsumfz0s.f | |- ( ph -> A. k e. ( 0 ... ( S + 1 ) ) C e. B ) |
||
| Assertion | telgsumfz0s | |- ( ph -> ( G gsum ( i e. ( 0 ... S ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ 0 / k ]_ C .- [_ ( S + 1 ) / k ]_ C ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | telgsumfz0s.b | |- B = ( Base ` G ) |
|
| 2 | telgsumfz0s.g | |- ( ph -> G e. Abel ) |
|
| 3 | telgsumfz0s.m | |- .- = ( -g ` G ) |
|
| 4 | telgsumfz0s.s | |- ( ph -> S e. NN0 ) |
|
| 5 | telgsumfz0s.f | |- ( ph -> A. k e. ( 0 ... ( S + 1 ) ) C e. B ) |
|
| 6 | nn0uz | |- NN0 = ( ZZ>= ` 0 ) |
|
| 7 | 4 6 | eleqtrdi | |- ( ph -> S e. ( ZZ>= ` 0 ) ) |
| 8 | 1 2 3 7 5 | telgsumfzs | |- ( ph -> ( G gsum ( i e. ( 0 ... S ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ 0 / k ]_ C .- [_ ( S + 1 ) / k ]_ C ) ) |