Metamath Proof Explorer


Theorem telgsumfz0s

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 φ G Abel
telgsumfz0s.m - ˙ = - G
telgsumfz0s.s φ S 0
telgsumfz0s.f φ k 0 S + 1 C B
Assertion telgsumfz0s φ G i = 0 S i / k C - ˙ i + 1 / k C = 0 / k C - ˙ S + 1 / k C

Proof

Step Hyp Ref Expression
1 telgsumfz0s.b B = Base G
2 telgsumfz0s.g φ G Abel
3 telgsumfz0s.m - ˙ = - G
4 telgsumfz0s.s φ S 0
5 telgsumfz0s.f φ k 0 S + 1 C B
6 nn0uz 0 = 0
7 4 6 eleqtrdi φ S 0
8 1 2 3 7 5 telgsumfzs φ G i = 0 S i / k C - ˙ i + 1 / k C = 0 / k C - ˙ S + 1 / k C