Metamath Proof Explorer

Theorem telgsumfzslem

Description: Lemma for telgsumfzs (induction step). (Contributed by AV, 23-Nov-2019)

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

Proof

Step Hyp Ref Expression
1 telgsumfzs.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 telgsumfzs.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
3 telgsumfzs.m ⊢ − = ( -g ‘ 𝐺 )
4 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
5 2 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) → 𝐺 ∈ Abel )
6 ablcmn ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ CMnd )
7 5 6 syl ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) → 𝐺 ∈ CMnd )
8 7 adantl ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → 𝐺 ∈ CMnd )
9 fzfid ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → ( 𝑀 ... ( 𝑦 + 1 ) ) ∈ Fin )
10 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
11 2 10 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
12 11 ad2antrl ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → 𝐺 ∈ Grp )
13 12 adantr ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) ) → 𝐺 ∈ Grp )
14 fzelp1 ⊢ ( 𝑖 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) → 𝑖 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) )
15 simpr ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) → ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 )
16 15 adantl ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 )
17 rspcsbela ⊢ ( ( 𝑖 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
18 14 16 17 syl2anr ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
19 fzp1elp1 ⊢ ( 𝑖 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) → ( 𝑖 + 1 ) ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) )
20 rspcsbela ⊢ ( ( ( 𝑖 + 1 ) ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
21 19 16 20 syl2anr ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) ) → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
22 1 3 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ ⦋ 𝑖 / 𝑘 ⦌ 𝐶 ∈ 𝐵 ∧ ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 ) → ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ∈ 𝐵 )
23 13 18 21 22 syl3anc ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) ) → ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ∈ 𝐵 )
24 fzp1disj ⊢ ( ( 𝑀 ... 𝑦 ) ∩ { ( 𝑦 + 1 ) } ) = ∅
25 24 a1i ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → ( ( 𝑀 ... 𝑦 ) ∩ { ( 𝑦 + 1 ) } ) = ∅ )
26 fzsuc ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... ( 𝑦 + 1 ) ) = ( ( 𝑀 ... 𝑦 ) ∪ { ( 𝑦 + 1 ) } ) )
27 26 adantr ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → ( 𝑀 ... ( 𝑦 + 1 ) ) = ( ( 𝑀 ... 𝑦 ) ∪ { ( 𝑦 + 1 ) } ) )
28 1 4 8 9 23 25 27 gsummptfidmsplit ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝑖 ∈ { ( 𝑦 + 1 ) } ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) ) )
29 28 adantr ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) ∧ ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝑖 ∈ { ( 𝑦 + 1 ) } ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) ) )
30 simpr ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) ∧ ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) )
31 grpmnd ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
32 11 31 syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
33 32 ad2antrl ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → 𝐺 ∈ Mnd )
34 ovexd ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → ( 𝑦 + 1 ) ∈ V )
35 peano2uz ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑦 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
36 eluzfz2 ⊢ ( ( 𝑦 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑦 + 1 ) ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) )
37 35 36 syl ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑦 + 1 ) ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) )
38 fzelp1 ⊢ ( ( 𝑦 + 1 ) ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) → ( 𝑦 + 1 ) ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) )
39 37 38 syl ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑦 + 1 ) ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) )
40 rspcsbela ⊢ ( ( ( 𝑦 + 1 ) ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) → ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
41 39 15 40 syl2an ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
42 peano2uz ⊢ ( ( 𝑦 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑦 + 1 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
43 35 42 syl ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑦 + 1 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
44 eluzfz2 ⊢ ( ( ( 𝑦 + 1 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑦 + 1 ) + 1 ) ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) )
45 43 44 syl ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑦 + 1 ) + 1 ) ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) )
46 rspcsbela ⊢ ( ( ( ( 𝑦 + 1 ) + 1 ) ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) → ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
47 45 15 46 syl2an ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
48 1 3 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 ∧ ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 ) → ( ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) ∈ 𝐵 )
49 12 41 47 48 syl3anc ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → ( ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) ∈ 𝐵 )
50 csbeq1 ⊢ ( 𝑖 = ( 𝑦 + 1 ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐶 = ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 )
51 oveq1 ⊢ ( 𝑖 = ( 𝑦 + 1 ) → ( 𝑖 + 1 ) = ( ( 𝑦 + 1 ) + 1 ) )
52 51 csbeq1d ⊢ ( 𝑖 = ( 𝑦 + 1 ) → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 = ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 )
53 50 52 oveq12d ⊢ ( 𝑖 = ( 𝑦 + 1 ) → ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) = ( ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) )
54 53 adantl ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) ∧ 𝑖 = ( 𝑦 + 1 ) ) → ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) = ( ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) )
55 1 33 34 49 54 gsumsnd ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → ( 𝐺 Σg ( 𝑖 ∈ { ( 𝑦 + 1 ) } ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) )
56 55 adantr ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) ∧ ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) ) → ( 𝐺 Σg ( 𝑖 ∈ { ( 𝑦 + 1 ) } ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) )
57 30 56 oveq12d ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) ∧ ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) ) → ( ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝑖 ∈ { ( 𝑦 + 1 ) } ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) ) = ( ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) ( +g ‘ 𝐺 ) ( ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) ) )
58 eluzfz1 ⊢ ( ( ( 𝑦 + 1 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) )
59 43 58 syl ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) )
60 rspcsbela ⊢ ( ( 𝑀 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) → ⦋ 𝑀 / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
61 59 15 60 syl2an ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → ⦋ 𝑀 / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
62 1 4 3 grpnpncan ⊢ ( ( 𝐺 ∈ Grp ∧ ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 ∈ 𝐵 ∧ ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 ∧ ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 ) ) → ( ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) ( +g ‘ 𝐺 ) ( ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) )
63 12 61 41 47 62 syl13anc ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → ( ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) ( +g ‘ 𝐺 ) ( ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) )
64 63 adantr ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) ∧ ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) ) → ( ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) ( +g ‘ 𝐺 ) ( ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) )
65 29 57 64 3eqtrd ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) ∧ ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) )
66 65 ex ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → ( ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) ) )