Metamath Proof Explorer

Theorem telgsumfzs

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

Ref Expression
Hypotheses telgsumfzs.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
telgsumfzs.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
telgsumfzs.m ⊢ − = ( -g ‘ 𝐺 )
telgsumfzs.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
telgsumfzs.f ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐶 ∈ 𝐵 )
Assertion telgsumfzs ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑁 + 1 ) / 𝑘 ⦌ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 telgsumfzs.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 telgsumfzs.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
3 telgsumfzs.m ⊢ − = ( -g ‘ 𝐺 )
4 telgsumfzs.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
5 telgsumfzs.f ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐶 ∈ 𝐵 )
6 oveq1 ⊢ ( 𝑥 = 𝑀 → ( 𝑥 + 1 ) = ( 𝑀 + 1 ) )
7 6 oveq2d ⊢ ( 𝑥 = 𝑀 → ( 𝑀 ... ( 𝑥 + 1 ) ) = ( 𝑀 ... ( 𝑀 + 1 ) ) )
8 7 raleqdv ⊢ ( 𝑥 = 𝑀 → ( ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑥 + 1 ) ) 𝐶 ∈ 𝐵 ↔ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) )
9 8 anbi2d ⊢ ( 𝑥 = 𝑀 → ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑥 + 1 ) ) 𝐶 ∈ 𝐵 ) ↔ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) ) )
10 oveq2 ⊢ ( 𝑥 = 𝑀 → ( 𝑀 ... 𝑥 ) = ( 𝑀 ... 𝑀 ) )
11 10 mpteq1d ⊢ ( 𝑥 = 𝑀 → ( 𝑖 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) = ( 𝑖 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) )
12 11 oveq2d ⊢ ( 𝑥 = 𝑀 → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) )
13 6 csbeq1d ⊢ ( 𝑥 = 𝑀 → ⦋ ( 𝑥 + 1 ) / 𝑘 ⦌ 𝐶 = ⦋ ( 𝑀 + 1 ) / 𝑘 ⦌ 𝐶 )
14 13 oveq2d ⊢ ( 𝑥 = 𝑀 → ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑥 + 1 ) / 𝑘 ⦌ 𝐶 ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑀 + 1 ) / 𝑘 ⦌ 𝐶 ) )
15 12 14 eqeq12d ⊢ ( 𝑥 = 𝑀 → ( ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑥 + 1 ) / 𝑘 ⦌ 𝐶 ) ↔ ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑀 + 1 ) / 𝑘 ⦌ 𝐶 ) ) )
16 9 15 imbi12d ⊢ ( 𝑥 = 𝑀 → ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑥 + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑥 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ↔ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑀 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) )
17 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 + 1 ) = ( 𝑦 + 1 ) )
18 17 oveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑀 ... ( 𝑥 + 1 ) ) = ( 𝑀 ... ( 𝑦 + 1 ) ) )
19 18 raleqdv ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑥 + 1 ) ) 𝐶 ∈ 𝐵 ↔ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) 𝐶 ∈ 𝐵 ) )
20 19 anbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑥 + 1 ) ) 𝐶 ∈ 𝐵 ) ↔ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) 𝐶 ∈ 𝐵 ) ) )
21 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑀 ... 𝑥 ) = ( 𝑀 ... 𝑦 ) )
22 21 mpteq1d ⊢ ( 𝑥 = 𝑦 → ( 𝑖 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) = ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) )
23 22 oveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) )
24 17 csbeq1d ⊢ ( 𝑥 = 𝑦 → ⦋ ( 𝑥 + 1 ) / 𝑘 ⦌ 𝐶 = ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 )
25 24 oveq2d ⊢ ( 𝑥 = 𝑦 → ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑥 + 1 ) / 𝑘 ⦌ 𝐶 ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) )
26 23 25 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑥 + 1 ) / 𝑘 ⦌ 𝐶 ) ↔ ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) ) )
27 20 26 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑥 + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑥 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ↔ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) )
28 oveq1 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 + 1 ) = ( ( 𝑦 + 1 ) + 1 ) )
29 28 oveq2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑀 ... ( 𝑥 + 1 ) ) = ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) )
30 29 raleqdv ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑥 + 1 ) ) 𝐶 ∈ 𝐵 ↔ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) )
31 30 anbi2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑥 + 1 ) ) 𝐶 ∈ 𝐵 ) ↔ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) )
32 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑀 ... 𝑥 ) = ( 𝑀 ... ( 𝑦 + 1 ) ) )
33 32 mpteq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑖 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) = ( 𝑖 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) )
34 33 oveq2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) )
35 28 csbeq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ⦋ ( 𝑥 + 1 ) / 𝑘 ⦌ 𝐶 = ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 )
36 35 oveq2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑥 + 1 ) / 𝑘 ⦌ 𝐶 ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) )
37 34 36 eqeq12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑥 + 1 ) / 𝑘 ⦌ 𝐶 ) ↔ ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) ) )
38 31 37 imbi12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑥 + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑥 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ↔ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) )
39 oveq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 + 1 ) = ( 𝑁 + 1 ) )
40 39 oveq2d ⊢ ( 𝑥 = 𝑁 → ( 𝑀 ... ( 𝑥 + 1 ) ) = ( 𝑀 ... ( 𝑁 + 1 ) ) )
41 40 raleqdv ⊢ ( 𝑥 = 𝑁 → ( ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑥 + 1 ) ) 𝐶 ∈ 𝐵 ↔ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐶 ∈ 𝐵 ) )
42 41 anbi2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑥 + 1 ) ) 𝐶 ∈ 𝐵 ) ↔ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐶 ∈ 𝐵 ) ) )
43 oveq2 ⊢ ( 𝑥 = 𝑁 → ( 𝑀 ... 𝑥 ) = ( 𝑀 ... 𝑁 ) )
44 43 mpteq1d ⊢ ( 𝑥 = 𝑁 → ( 𝑖 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) = ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) )
45 44 oveq2d ⊢ ( 𝑥 = 𝑁 → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) )
46 39 csbeq1d ⊢ ( 𝑥 = 𝑁 → ⦋ ( 𝑥 + 1 ) / 𝑘 ⦌ 𝐶 = ⦋ ( 𝑁 + 1 ) / 𝑘 ⦌ 𝐶 )
47 46 oveq2d ⊢ ( 𝑥 = 𝑁 → ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑥 + 1 ) / 𝑘 ⦌ 𝐶 ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑁 + 1 ) / 𝑘 ⦌ 𝐶 ) )
48 45 47 eqeq12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑥 + 1 ) / 𝑘 ⦌ 𝐶 ) ↔ ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑁 + 1 ) / 𝑘 ⦌ 𝐶 ) ) )
49 42 48 imbi12d ⊢ ( 𝑥 = 𝑁 → ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑥 + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑥 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ↔ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑁 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) )
50 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
51 4 50 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
52 51 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → 𝑀 ∈ ℤ )
53 fzsn ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
54 52 53 syl ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
55 54 mpteq1d ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝑖 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) = ( 𝑖 ∈ { 𝑀 } ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) )
56 55 oveq2d ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( 𝐺 Σg ( 𝑖 ∈ { 𝑀 } ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) )
57 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
58 2 57 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
59 grpmnd ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
60 58 59 syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
61 60 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → 𝐺 ∈ Mnd )
62 58 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → 𝐺 ∈ Grp )
63 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
64 52 63 syl ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
65 peano2uz ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
66 64 65 syl ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
67 eluzfz1 ⊢ ( ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) )
68 66 67 syl ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → 𝑀 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) )
69 rspcsbela ⊢ ( ( 𝑀 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → ⦋ 𝑀 / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
70 68 69 sylancom ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → ⦋ 𝑀 / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
71 eluzfz2 ⊢ ( ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 + 1 ) ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) )
72 66 71 syl ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝑀 + 1 ) ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) )
73 rspcsbela ⊢ ( ( ( 𝑀 + 1 ) ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → ⦋ ( 𝑀 + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
74 72 73 sylancom ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → ⦋ ( 𝑀 + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
75 1 3 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ ⦋ 𝑀 / 𝑘 ⦌ 𝐶 ∈ 𝐵 ∧ ⦋ ( 𝑀 + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 ) → ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑀 + 1 ) / 𝑘 ⦌ 𝐶 ) ∈ 𝐵 )
76 62 70 74 75 syl3anc ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑀 + 1 ) / 𝑘 ⦌ 𝐶 ) ∈ 𝐵 )
77 csbeq1 ⊢ ( 𝑖 = 𝑀 → ⦋ 𝑖 / 𝑘 ⦌ 𝐶 = ⦋ 𝑀 / 𝑘 ⦌ 𝐶 )
78 oveq1 ⊢ ( 𝑖 = 𝑀 → ( 𝑖 + 1 ) = ( 𝑀 + 1 ) )
79 78 csbeq1d ⊢ ( 𝑖 = 𝑀 → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 = ⦋ ( 𝑀 + 1 ) / 𝑘 ⦌ 𝐶 )
80 77 79 oveq12d ⊢ ( 𝑖 = 𝑀 → ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑀 + 1 ) / 𝑘 ⦌ 𝐶 ) )
81 80 adantl ⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) ∧ 𝑖 = 𝑀 ) → ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑀 + 1 ) / 𝑘 ⦌ 𝐶 ) )
82 1 61 52 76 81 gsumsnd ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑖 ∈ { 𝑀 } ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑀 + 1 ) / 𝑘 ⦌ 𝐶 ) )
83 56 82 eqtrd ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑀 + 1 ) / 𝑘 ⦌ 𝐶 ) )
84 1 2 3 telgsumfzslem ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → ( ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) ) )
85 84 ex ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) → ( ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) )
86 eluzelz ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑦 ∈ ℤ )
87 86 peano2zd ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑦 + 1 ) ∈ ℤ )
88 87 peano2zd ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑦 + 1 ) + 1 ) ∈ ℤ )
89 peano2z ⊢ ( 𝑦 ∈ ℤ → ( 𝑦 + 1 ) ∈ ℤ )
90 89 zred ⊢ ( 𝑦 ∈ ℤ → ( 𝑦 + 1 ) ∈ ℝ )
91 86 90 syl ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑦 + 1 ) ∈ ℝ )
92 91 lep1d ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑦 + 1 ) ≤ ( ( 𝑦 + 1 ) + 1 ) )
93 eluz2 ⊢ ( ( ( 𝑦 + 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑦 + 1 ) ) ↔ ( ( 𝑦 + 1 ) ∈ ℤ ∧ ( ( 𝑦 + 1 ) + 1 ) ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ ( ( 𝑦 + 1 ) + 1 ) ) )
94 87 88 92 93 syl3anbrc ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑦 + 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑦 + 1 ) ) )
95 fzss2 ⊢ ( ( ( 𝑦 + 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑦 + 1 ) ) → ( 𝑀 ... ( 𝑦 + 1 ) ) ⊆ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) )
96 94 95 syl ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... ( 𝑦 + 1 ) ) ⊆ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) )
97 ssralv ⊢ ( ( 𝑀 ... ( 𝑦 + 1 ) ) ⊆ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) → ( ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 → ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) 𝐶 ∈ 𝐵 ) )
98 96 97 syl ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 → ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) 𝐶 ∈ 𝐵 ) )
99 98 adantld ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) → ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) 𝐶 ∈ 𝐵 ) )
100 85 99 a2and ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) ) → ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) )
101 16 27 38 49 83 100 uzind4i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑁 + 1 ) / 𝑘 ⦌ 𝐶 ) ) )
102 101 expd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ( ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐶 ∈ 𝐵 → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑁 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) )
103 4 102 mpcom ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐶 ∈ 𝐵 → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑁 + 1 ) / 𝑘 ⦌ 𝐶 ) ) )
104 5 103 mpd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑁 + 1 ) / 𝑘 ⦌ 𝐶 ) )