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={\mathrm{Base}}_G$$
	telgsumfz0s.g	$$⊢\phi \to G\in \mathrm{Abel}$$
	telgsumfz0s.m	$$⊢\underset{\dot{}}{-}={-}_G$$
	telgsumfz0s.s	$$⊢\phi \to S\in {\mathbb{N}}_0$$
	telgsumfz0s.f	$$⊢\phi \to \forall k\in \left(0\dots S+1\right)C\in B$$
Assertion	telgsumfz0s	$$⊢\phi \to \underset{i=0}{\overset{S}{{\sum }_G}}\left(⦋i/k⦌C\underset{\dot{}}{-}⦋\left(i+1\right)/k⦌C\right)=⦋0/k⦌C\underset{\dot{}}{-}⦋\left(S+1\right)/k⦌C$$

Proof

Step	Hyp	Ref	Expression
1		telgsumfz0s.b	$$⊢B={\mathrm{Base}}_G$$
2		telgsumfz0s.g	$$⊢\phi \to G\in \mathrm{Abel}$$
3		telgsumfz0s.m	$$⊢\underset{\dot{}}{-}={-}_G$$
4		telgsumfz0s.s	$$⊢\phi \to S\in {\mathbb{N}}_0$$
5		telgsumfz0s.f	$$⊢\phi \to \forall k\in \left(0\dots S+1\right)C\in B$$
6		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
7	4 6	eleqtrdi	$$⊢\phi \to S\in {\mathbb{Z}}_{\ge 0}$$
8	1 2 3 7 5	telgsumfzs	$$⊢\phi \to \underset{i=0}{\overset{S}{{\sum }_G}}\left(⦋i/k⦌C\underset{\dot{}}{-}⦋\left(i+1\right)/k⦌C\right)=⦋0/k⦌C\underset{\dot{}}{-}⦋\left(S+1\right)/k⦌C$$