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=BaseG
telgsumfz0s.g φGAbel
telgsumfz0s.m -˙=-G
telgsumfz0s.s φS0
telgsumfz0s.f φk0S+1CB
Assertion telgsumfz0s φGi=0Si/kC-˙i+1/kC=0/kC-˙S+1/kC

Proof

Step Hyp Ref Expression
1 telgsumfz0s.b B=BaseG
2 telgsumfz0s.g φGAbel
3 telgsumfz0s.m -˙=-G
4 telgsumfz0s.s φS0
5 telgsumfz0s.f φk0S+1CB
6 nn0uz 0=0
7 4 6 eleqtrdi φS0
8 1 2 3 7 5 telgsumfzs φGi=0Si/kC-˙i+1/kC=0/kC-˙S+1/kC