This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem telgsumfz

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

Ref Expression
Hypotheses telgsumfz.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
telgsumfz.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
telgsumfz.m ⊢ − = ( -g ‘ 𝐺 )
telgsumfz.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
telgsumfz.f ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐴 ∈ 𝐵 )
telgsumfz.l ⊢ ( 𝑘 = 𝑖 → 𝐴 = 𝐿 )
telgsumfz.c ⊢ ( 𝑘 = ( 𝑖 + 1 ) → 𝐴 = 𝐶 )
telgsumfz.d ⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐷 )
telgsumfz.e ⊢ ( 𝑘 = ( 𝑁 + 1 ) → 𝐴 = 𝐸 )
Assertion telgsumfz ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐿 − 𝐶 ) ) ) = ( 𝐷 − 𝐸 ) )

Proof

Step Hyp Ref Expression
1 telgsumfz.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 telgsumfz.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
3 telgsumfz.m ⊢ − = ( -g ‘ 𝐺 )
4 telgsumfz.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
5 telgsumfz.f ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐴 ∈ 𝐵 )
6 telgsumfz.l ⊢ ( 𝑘 = 𝑖 → 𝐴 = 𝐿 )
7 telgsumfz.c ⊢ ( 𝑘 = ( 𝑖 + 1 ) → 𝐴 = 𝐶 )
8 telgsumfz.d ⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐷 )
9 telgsumfz.e ⊢ ( 𝑘 = ( 𝑁 + 1 ) → 𝐴 = 𝐸 )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑖 ∈ ( 𝑀 ... 𝑁 ) )
11 6 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑘 = 𝑖 ) → 𝐴 = 𝐿 )
12 10 11 csbied ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑁 ) ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐴 = 𝐿 )
13 12 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐿 = ⦋ 𝑖 / 𝑘 ⦌ 𝐴 )
14 ovexd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑖 + 1 ) ∈ V )
15 7 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑘 = ( 𝑖 + 1 ) ) → 𝐴 = 𝐶 )
16 14 15 csbied ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑁 ) ) → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐴 = 𝐶 )
17 16 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐶 = ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐴 )
18 13 17 oveq12d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐿 − 𝐶 ) = ( ⦋ 𝑖 / 𝑘 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐴 ) )
19 18 mpteq2dva ⊢ ( 𝜑 → ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐿 − 𝐶 ) ) = ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐴 ) ) )
20 19 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐿 − 𝐶 ) ) ) = ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐴 ) ) ) )
21 1 2 3 4 5 telgsumfzs ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐴 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐴 − ⦋ ( 𝑁 + 1 ) / 𝑘 ⦌ 𝐴 ) )
22 4 elfvexd ⊢ ( 𝜑 → 𝑀 ∈ V )
23 8 adantl ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝐴 = 𝐷 )
24 22 23 csbied ⊢ ( 𝜑 → ⦋ 𝑀 / 𝑘 ⦌ 𝐴 = 𝐷 )
25 ovexd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ V )
26 9 adantl ⊢ ( ( 𝜑 ∧ 𝑘 = ( 𝑁 + 1 ) ) → 𝐴 = 𝐸 )
27 25 26 csbied ⊢ ( 𝜑 → ⦋ ( 𝑁 + 1 ) / 𝑘 ⦌ 𝐴 = 𝐸 )
28 24 27 oveq12d ⊢ ( 𝜑 → ( ⦋ 𝑀 / 𝑘 ⦌ 𝐴 − ⦋ ( 𝑁 + 1 ) / 𝑘 ⦌ 𝐴 ) = ( 𝐷 − 𝐸 ) )
29 20 21 28 3eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐿 − 𝐶 ) ) ) = ( 𝐷 − 𝐸 ) )