Theorem telgsum

Description: Telescoping finitely supported group sum ranging over nonnegative integers, using implicit substitution. (Contributed by AV, 31-Dec-2019)

	Ref	Expression
Hypotheses	telgsum.b	$$⊢B={\mathrm{Base}}_G$$
	telgsum.g	$$⊢\phi \to G\in \mathrm{Abel}$$
	telgsum.m	$$⊢\underset{\dot{}}{-}={-}_G$$
	telgsum.0	$$⊢\underset{\dot{}}{0}=0_G$$
	telgsum.f	$$⊢\phi \to \forall k\in {\mathbb{N}}_{0}A\in B$$
	telgsum.s	$$⊢\phi \to S\in {\mathbb{N}}_0$$
	telgsum.u	$$⊢\phi \to \forall k\in {\mathbb{N}}_0\left(S<k\to A=\underset{\dot{}}{0}\right)$$
	telgsum.c	$$⊢k=i\to A=C$$
	telgsum.d	$$⊢k=i+1\to A=D$$
	telgsum.e	$$⊢k=0\to A=E$$
Assertion	telgsum	$$⊢\phi \to \underset{i\in {\mathbb{N}}_0}{{\sum }_G}\left(C\underset{\dot{}}{-}D\right)=E$$

Proof

Step	Hyp	Ref	Expression
1		telgsum.b	$$⊢B={\mathrm{Base}}_G$$
2		telgsum.g	$$⊢\phi \to G\in \mathrm{Abel}$$
3		telgsum.m	$$⊢\underset{\dot{}}{-}={-}_G$$
4		telgsum.0	$$⊢\underset{\dot{}}{0}=0_G$$
5		telgsum.f	$$⊢\phi \to \forall k\in {\mathbb{N}}_{0}A\in B$$
6		telgsum.s	$$⊢\phi \to S\in {\mathbb{N}}_0$$
7		telgsum.u	$$⊢\phi \to \forall k\in {\mathbb{N}}_0\left(S<k\to A=\underset{\dot{}}{0}\right)$$
8		telgsum.c	$$⊢k=i\to A=C$$
9		telgsum.d	$$⊢k=i+1\to A=D$$
10		telgsum.e	$$⊢k=0\to A=E$$
11		simpr	$$⊢\left(\phi \wedge i\in {\mathbb{N}}_0\right)\to i\in {\mathbb{N}}_0$$
12	8	adantl	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge k=i\right)\to A=C$$
13	11 12	csbied	$$⊢\left(\phi \wedge i\in {\mathbb{N}}_0\right)\to ⦋i/k⦌A=C$$
14	13	eqcomd	$$⊢\left(\phi \wedge i\in {\mathbb{N}}_0\right)\to C=⦋i/k⦌A$$
15		peano2nn0	$$⊢i\in {\mathbb{N}}_0\to i+1\in {\mathbb{N}}_0$$
16	15	adantl	$$⊢\left(\phi \wedge i\in {\mathbb{N}}_0\right)\to i+1\in {\mathbb{N}}_0$$
17	9	adantl	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge k=i+1\right)\to A=D$$
18	16 17	csbied	$$⊢\left(\phi \wedge i\in {\mathbb{N}}_0\right)\to ⦋\left(i+1\right)/k⦌A=D$$
19	18	eqcomd	$$⊢\left(\phi \wedge i\in {\mathbb{N}}_0\right)\to D=⦋\left(i+1\right)/k⦌A$$
20	14 19	oveq12d	$$⊢\left(\phi \wedge i\in {\mathbb{N}}_0\right)\to C\underset{\dot{}}{-}D=⦋i/k⦌A\underset{\dot{}}{-}⦋\left(i+1\right)/k⦌A$$
21	20	mpteq2dva	$$⊢\phi \to \left(i\in {\mathbb{N}}_0⟼C\underset{\dot{}}{-}D\right)=\left(i\in {\mathbb{N}}_0⟼⦋i/k⦌A\underset{\dot{}}{-}⦋\left(i+1\right)/k⦌A\right)$$
22	21	oveq2d	$$⊢\phi \to \underset{i\in {\mathbb{N}}_0}{{\sum }_G}\left(C\underset{\dot{}}{-}D\right)=\underset{i\in {\mathbb{N}}_0}{{\sum }_G}\left(⦋i/k⦌A\underset{\dot{}}{-}⦋\left(i+1\right)/k⦌A\right)$$
23	1 2 3 4 5 6 7	telgsums	$$⊢\phi \to \underset{i\in {\mathbb{N}}_0}{{\sum }_G}\left(⦋i/k⦌A\underset{\dot{}}{-}⦋\left(i+1\right)/k⦌A\right)=⦋0/k⦌A$$
24		c0ex	$$⊢0\in \mathrm{V}$$
25	24	a1i	$$⊢\phi \to 0\in \mathrm{V}$$
26	10	adantl	$$⊢\left(\phi \wedge k=0\right)\to A=E$$
27	25 26	csbied	$$⊢\phi \to ⦋0/k⦌A=E$$
28	22 23 27	3eqtrd	$$⊢\phi \to \underset{i\in {\mathbb{N}}_0}{{\sum }_G}\left(C\underset{\dot{}}{-}D\right)=E$$