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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	telgsum.g	⊢ ( 𝜑 → 𝐺 ∈ Abel )
	telgsum.m	⊢ − = ( -g ‘ 𝐺 )
	telgsum.0	⊢ 0 = ( 0g ‘ 𝐺 )
	telgsum.f	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐴 ∈ 𝐵 )
	telgsum.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
	telgsum.u	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( 𝑆 < 𝑘 → 𝐴 = 0 ) )
	telgsum.c	⊢ ( 𝑘 = 𝑖 → 𝐴 = 𝐶 )
	telgsum.d	⊢ ( 𝑘 = ( 𝑖 + 1 ) → 𝐴 = 𝐷 )
	telgsum.e	⊢ ( 𝑘 = 0 → 𝐴 = 𝐸 )
Assertion	telgsum	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ℕ0 ↦ ( 𝐶 − 𝐷 ) ) ) = 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		telgsum.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		telgsum.g	⊢ ( 𝜑 → 𝐺 ∈ Abel )
3		telgsum.m	⊢ − = ( -g ‘ 𝐺 )
4		telgsum.0	⊢ 0 = ( 0g ‘ 𝐺 )
5		telgsum.f	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐴 ∈ 𝐵 )
6		telgsum.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
7		telgsum.u	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( 𝑆 < 𝑘 → 𝐴 = 0 ) )
8		telgsum.c	⊢ ( 𝑘 = 𝑖 → 𝐴 = 𝐶 )
9		telgsum.d	⊢ ( 𝑘 = ( 𝑖 + 1 ) → 𝐴 = 𝐷 )
10		telgsum.e	⊢ ( 𝑘 = 0 → 𝐴 = 𝐸 )
11		simpr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑖 ∈ ℕ0 )
12	8	adantl	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑘 = 𝑖 ) → 𝐴 = 𝐶 )
13	11 12	csbied	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐴 = 𝐶 )
14	13	eqcomd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝐶 = ⦋ 𝑖 / 𝑘 ⦌ 𝐴 )
15		peano2nn0	⊢ ( 𝑖 ∈ ℕ0 → ( 𝑖 + 1 ) ∈ ℕ0 )
16	15	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑖 + 1 ) ∈ ℕ0 )
17	9	adantl	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑘 = ( 𝑖 + 1 ) ) → 𝐴 = 𝐷 )
18	16 17	csbied	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐴 = 𝐷 )
19	18	eqcomd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝐷 = ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐴 )
20	14 19	oveq12d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝐶 − 𝐷 ) = ( ⦋ 𝑖 / 𝑘 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐴 ) )
21	20	mpteq2dva	⊢ ( 𝜑 → ( 𝑖 ∈ ℕ0 ↦ ( 𝐶 − 𝐷 ) ) = ( 𝑖 ∈ ℕ0 ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐴 ) ) )
22	21	oveq2d	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ℕ0 ↦ ( 𝐶 − 𝐷 ) ) ) = ( 𝐺 Σg ( 𝑖 ∈ ℕ0 ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐴 ) ) ) )
23	1 2 3 4 5 6 7	telgsums	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ℕ0 ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐴 ) ) ) = ⦋ 0 / 𝑘 ⦌ 𝐴 )
24		c0ex	⊢ 0 ∈ V
25	24	a1i	⊢ ( 𝜑 → 0 ∈ V )
26	10	adantl	⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → 𝐴 = 𝐸 )
27	25 26	csbied	⊢ ( 𝜑 → ⦋ 0 / 𝑘 ⦌ 𝐴 = 𝐸 )
28	22 23 27	3eqtrd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ℕ0 ↦ ( 𝐶 − 𝐷 ) ) ) = 𝐸 )