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 58 grpmndd ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
60 59 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → 𝐺 ∈ Mnd )
61 58 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → 𝐺 ∈ Grp )
62 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
63 52 62 syl ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
64 peano2uz ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
65 63 64 syl ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
66 eluzfz1 ⊢ ( ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) )
67 65 66 syl ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → 𝑀 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) )
68 rspcsbela ⊢ ( ( 𝑀 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → ⦋ 𝑀 / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
69 67 68 sylancom ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → ⦋ 𝑀 / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
70 eluzfz2 ⊢ ( ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 + 1 ) ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) )
71 65 70 syl ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝑀 + 1 ) ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) )
72 rspcsbela ⊢ ( ( ( 𝑀 + 1 ) ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → ⦋ ( 𝑀 + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
73 71 72 sylancom ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → ⦋ ( 𝑀 + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
74 1 3 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ ⦋ 𝑀 / 𝑘 ⦌ 𝐶 ∈ 𝐵 ∧ ⦋ ( 𝑀 + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 ) → ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑀 + 1 ) / 𝑘 ⦌ 𝐶 ) ∈ 𝐵 )
75 61 69 73 74 syl3anc ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑀 + 1 ) / 𝑘 ⦌ 𝐶 ) ∈ 𝐵 )
76 csbeq1 ⊢ ( 𝑖 = 𝑀 → ⦋ 𝑖 / 𝑘 ⦌ 𝐶 = ⦋ 𝑀 / 𝑘 ⦌ 𝐶 )
77 oveq1 ⊢ ( 𝑖 = 𝑀 → ( 𝑖 + 1 ) = ( 𝑀 + 1 ) )
78 77 csbeq1d ⊢ ( 𝑖 = 𝑀 → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 = ⦋ ( 𝑀 + 1 ) / 𝑘 ⦌ 𝐶 )
79 76 78 oveq12d ⊢ ( 𝑖 = 𝑀 → ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑀 + 1 ) / 𝑘 ⦌ 𝐶 ) )
80 79 adantl ⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) ∧ 𝑖 = 𝑀 ) → ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑀 + 1 ) / 𝑘 ⦌ 𝐶 ) )
81 1 60 52 75 80 gsumsnd ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑖 ∈ { 𝑀 } ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑀 + 1 ) / 𝑘 ⦌ 𝐶 ) )
82 56 81 eqtrd ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑀 + 1 ) / 𝑘 ⦌ 𝐶 ) )
83 1 2 3 telgsumfzslem ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → ( ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) ) )
84 83 ex ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) → ( ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) )
85 eluzelz ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑦 ∈ ℤ )
86 85 peano2zd ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑦 + 1 ) ∈ ℤ )
87 86 peano2zd ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑦 + 1 ) + 1 ) ∈ ℤ )
88 peano2z ⊢ ( 𝑦 ∈ ℤ → ( 𝑦 + 1 ) ∈ ℤ )
89 88 zred ⊢ ( 𝑦 ∈ ℤ → ( 𝑦 + 1 ) ∈ ℝ )
90 85 89 syl ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑦 + 1 ) ∈ ℝ )
91 90 lep1d ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑦 + 1 ) ≤ ( ( 𝑦 + 1 ) + 1 ) )
92 eluz2 ⊢ ( ( ( 𝑦 + 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑦 + 1 ) ) ↔ ( ( 𝑦 + 1 ) ∈ ℤ ∧ ( ( 𝑦 + 1 ) + 1 ) ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ ( ( 𝑦 + 1 ) + 1 ) ) )
93 86 87 91 92 syl3anbrc ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑦 + 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑦 + 1 ) ) )
94 fzss2 ⊢ ( ( ( 𝑦 + 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑦 + 1 ) ) → ( 𝑀 ... ( 𝑦 + 1 ) ) ⊆ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) )
95 93 94 syl ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... ( 𝑦 + 1 ) ) ⊆ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) )
96 ssralv ⊢ ( ( 𝑀 ... ( 𝑦 + 1 ) ) ⊆ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) → ( ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 → ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) 𝐶 ∈ 𝐵 ) )
97 95 96 syl ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 → ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) 𝐶 ∈ 𝐵 ) )
98 97 adantld ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) → ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) 𝐶 ∈ 𝐵 ) )
99 84 98 a2and ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) ) → ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) )
100 16 27 38 49 82 99 uzind4i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑁 + 1 ) / 𝑘 ⦌ 𝐶 ) ) )
101 100 expd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ( ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐶 ∈ 𝐵 → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑁 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) )
102 4 101 mpcom ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐶 ∈ 𝐵 → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑁 + 1 ) / 𝑘 ⦌ 𝐶 ) ) )
103 5 102 mpd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑁 + 1 ) / 𝑘 ⦌ 𝐶 ) )