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 11 grpmndd ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
32 31 ad2antrl ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → 𝐺 ∈ Mnd )
33 ovexd ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → ( 𝑦 + 1 ) ∈ V )
34 peano2uz ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑦 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
35 eluzfz2 ⊢ ( ( 𝑦 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑦 + 1 ) ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) )
36 34 35 syl ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑦 + 1 ) ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) )
37 fzelp1 ⊢ ( ( 𝑦 + 1 ) ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) → ( 𝑦 + 1 ) ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) )
38 36 37 syl ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑦 + 1 ) ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) )
39 rspcsbela ⊢ ( ( ( 𝑦 + 1 ) ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) → ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
40 38 15 39 syl2an ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
41 peano2uz ⊢ ( ( 𝑦 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑦 + 1 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
42 34 41 syl ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑦 + 1 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
43 eluzfz2 ⊢ ( ( ( 𝑦 + 1 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑦 + 1 ) + 1 ) ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) )
44 42 43 syl ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑦 + 1 ) + 1 ) ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) )
45 rspcsbela ⊢ ( ( ( ( 𝑦 + 1 ) + 1 ) ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) → ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
46 44 15 45 syl2an ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
47 1 3 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 ∧ ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 ) → ( ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) ∈ 𝐵 )
48 12 40 46 47 syl3anc ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → ( ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) ∈ 𝐵 )
49 csbeq1 ⊢ ( 𝑖 = ( 𝑦 + 1 ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐶 = ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 )
50 oveq1 ⊢ ( 𝑖 = ( 𝑦 + 1 ) → ( 𝑖 + 1 ) = ( ( 𝑦 + 1 ) + 1 ) )
51 50 csbeq1d ⊢ ( 𝑖 = ( 𝑦 + 1 ) → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 = ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 )
52 49 51 oveq12d ⊢ ( 𝑖 = ( 𝑦 + 1 ) → ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) = ( ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) )
53 52 adantl ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) ∧ 𝑖 = ( 𝑦 + 1 ) ) → ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) = ( ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) )
54 1 32 33 48 53 gsumsnd ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → ( 𝐺 Σg ( 𝑖 ∈ { ( 𝑦 + 1 ) } ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) )
55 54 adantr ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) ∧ ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) ) → ( 𝐺 Σg ( 𝑖 ∈ { ( 𝑦 + 1 ) } ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) )
56 30 55 oveq12d ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) ∧ ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) ) → ( ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝑖 ∈ { ( 𝑦 + 1 ) } ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) ) = ( ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) ( +g ‘ 𝐺 ) ( ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) ) )
57 eluzfz1 ⊢ ( ( ( 𝑦 + 1 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) )
58 42 57 syl ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) )
59 rspcsbela ⊢ ( ( 𝑀 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) → ⦋ 𝑀 / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
60 58 15 59 syl2an ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → ⦋ 𝑀 / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
61 1 4 3 grpnpncan ⊢ ( ( 𝐺 ∈ Grp ∧ ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 ∈ 𝐵 ∧ ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 ∧ ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 ) ) → ( ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) ( +g ‘ 𝐺 ) ( ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) )
62 12 60 40 46 61 syl13anc ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → ( ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) ( +g ‘ 𝐺 ) ( ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) )
63 62 adantr ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) ∧ ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) ) → ( ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) ( +g ‘ 𝐺 ) ( ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) )
64 29 56 63 3eqtrd ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) ∧ ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) )
65 64 ex ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑀 ... ( ( 𝑦 + 1 ) + 1 ) ) 𝐶 ∈ 𝐵 ) ) → ( ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... 𝑦 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑦 + 1 ) / 𝑘 ⦌ 𝐶 ) → ( 𝐺 Σg ( 𝑖 ∈ ( 𝑀 ... ( 𝑦 + 1 ) ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 𝑀 / 𝑘 ⦌ 𝐶 − ⦋ ( ( 𝑦 + 1 ) + 1 ) / 𝑘 ⦌ 𝐶 ) ) )