telgsumfz0

Description: Telescoping finite group sum ranging over nonnegative integers, using implicit substitution, analogous to telfsum . (Contributed by AV, 23-Nov-2019)

	Ref	Expression
Hypotheses	telgsumfz0.k	⊢ 𝐾 = ( Base ‘ 𝐺 )
	telgsumfz0.g	⊢ ( 𝜑 → 𝐺 ∈ Abel )
	telgsumfz0.m	⊢ − = ( -_g ‘ 𝐺 )
	telgsumfz0.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ₀ )
	telgsumfz0.f	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( 𝑆 + 1 ) ) 𝐴 ∈ 𝐾 )
	telgsumfz0.a	⊢ ( 𝑘 = 𝑖 → 𝐴 = 𝐵 )
	telgsumfz0.c	⊢ ( 𝑘 = ( 𝑖 + 1 ) → 𝐴 = 𝐶 )
	telgsumfz0.d	⊢ ( 𝑘 = 0 → 𝐴 = 𝐷 )
	telgsumfz0.e	⊢ ( 𝑘 = ( 𝑆 + 1 ) → 𝐴 = 𝐸 )
Assertion	telgsumfz0	⊢ ( 𝜑 → ( 𝐺 Σ_g ( 𝑖 ∈ ( 0 ... 𝑆 ) ↦ ( 𝐵 − 𝐶 ) ) ) = ( 𝐷 − 𝐸 ) )

Proof

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

Metamath Proof Explorer

Theorem telgsumfz0

Proof