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 ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐿 𝐶 ) ) ) = ( 𝐷 𝐸 ) )