This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem telgsums

Description: Telescoping finitely supported group sum ranging over nonnegative integers, using explicit substitution. (Contributed by AV, 24-Oct-2019)

Ref Expression
Hypotheses telgsums.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
telgsums.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
telgsums.m ⊢ − = ( -g ‘ 𝐺 )
telgsums.0 ⊢ 0 = ( 0g ‘ 𝐺 )
telgsums.f ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 )
telgsums.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
telgsums.u ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( 𝑆 < 𝑘 → 𝐶 = 0 ) )
Assertion telgsums ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ℕ0 ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ⦋ 0 / 𝑘 ⦌ 𝐶 )

Proof

Step Hyp Ref Expression
1 telgsums.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 telgsums.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
3 telgsums.m ⊢ − = ( -g ‘ 𝐺 )
4 telgsums.0 ⊢ 0 = ( 0g ‘ 𝐺 )
5 telgsums.f ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 )
6 telgsums.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
7 telgsums.u ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( 𝑆 < 𝑘 → 𝐶 = 0 ) )
8 ablcmn ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ CMnd )
9 2 8 syl ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
10 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
11 2 10 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝐺 ∈ Grp )
13 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑖 ∈ ℕ0 )
14 5 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 )
15 rspcsbela ⊢ ( ( 𝑖 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
16 13 14 15 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
17 peano2nn0 ⊢ ( 𝑖 ∈ ℕ0 → ( 𝑖 + 1 ) ∈ ℕ0 )
18 rspcsbela ⊢ ( ( ( 𝑖 + 1 ) ∈ ℕ0 ∧ ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 ) → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
19 17 5 18 syl2anr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
20 1 3 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ ⦋ 𝑖 / 𝑘 ⦌ 𝐶 ∈ 𝐵 ∧ ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ∈ 𝐵 ) → ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ∈ 𝐵 )
21 12 16 19 20 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ∈ 𝐵 )
22 21 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ℕ0 ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ∈ 𝐵 )
23 rspsbca ⊢ ( ( 𝑖 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ℕ0 ( 𝑆 < 𝑘 → 𝐶 = 0 ) ) → [ 𝑖 / 𝑘 ] ( 𝑆 < 𝑘 → 𝐶 = 0 ) )
24 sbcimg ⊢ ( 𝑖 ∈ V → ( [ 𝑖 / 𝑘 ] ( 𝑆 < 𝑘 → 𝐶 = 0 ) ↔ ( [ 𝑖 / 𝑘 ] 𝑆 < 𝑘 → [ 𝑖 / 𝑘 ] 𝐶 = 0 ) ) )
25 sbcbr2g ⊢ ( 𝑖 ∈ V → ( [ 𝑖 / 𝑘 ] 𝑆 < 𝑘 ↔ 𝑆 < ⦋ 𝑖 / 𝑘 ⦌ 𝑘 ) )
26 csbvarg ⊢ ( 𝑖 ∈ V → ⦋ 𝑖 / 𝑘 ⦌ 𝑘 = 𝑖 )
27 26 breq2d ⊢ ( 𝑖 ∈ V → ( 𝑆 < ⦋ 𝑖 / 𝑘 ⦌ 𝑘 ↔ 𝑆 < 𝑖 ) )
28 25 27 bitrd ⊢ ( 𝑖 ∈ V → ( [ 𝑖 / 𝑘 ] 𝑆 < 𝑘 ↔ 𝑆 < 𝑖 ) )
29 sbceq1g ⊢ ( 𝑖 ∈ V → ( [ 𝑖 / 𝑘 ] 𝐶 = 0 ↔ ⦋ 𝑖 / 𝑘 ⦌ 𝐶 = 0 ) )
30 28 29 imbi12d ⊢ ( 𝑖 ∈ V → ( ( [ 𝑖 / 𝑘 ] 𝑆 < 𝑘 → [ 𝑖 / 𝑘 ] 𝐶 = 0 ) ↔ ( 𝑆 < 𝑖 → ⦋ 𝑖 / 𝑘 ⦌ 𝐶 = 0 ) ) )
31 24 30 bitrd ⊢ ( 𝑖 ∈ V → ( [ 𝑖 / 𝑘 ] ( 𝑆 < 𝑘 → 𝐶 = 0 ) ↔ ( 𝑆 < 𝑖 → ⦋ 𝑖 / 𝑘 ⦌ 𝐶 = 0 ) ) )
32 31 elv ⊢ ( [ 𝑖 / 𝑘 ] ( 𝑆 < 𝑘 → 𝐶 = 0 ) ↔ ( 𝑆 < 𝑖 → ⦋ 𝑖 / 𝑘 ⦌ 𝐶 = 0 ) )
33 23 32 sylib ⊢ ( ( 𝑖 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ℕ0 ( 𝑆 < 𝑘 → 𝐶 = 0 ) ) → ( 𝑆 < 𝑖 → ⦋ 𝑖 / 𝑘 ⦌ 𝐶 = 0 ) )
34 33 expcom ⊢ ( ∀ 𝑘 ∈ ℕ0 ( 𝑆 < 𝑘 → 𝐶 = 0 ) → ( 𝑖 ∈ ℕ0 → ( 𝑆 < 𝑖 → ⦋ 𝑖 / 𝑘 ⦌ 𝐶 = 0 ) ) )
35 7 34 syl ⊢ ( 𝜑 → ( 𝑖 ∈ ℕ0 → ( 𝑆 < 𝑖 → ⦋ 𝑖 / 𝑘 ⦌ 𝐶 = 0 ) ) )
36 35 imp31 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑆 < 𝑖 ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐶 = 0 )
37 6 nn0red ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑆 ∈ ℝ )
39 38 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑆 < 𝑖 ) → 𝑆 ∈ ℝ )
40 nn0re ⊢ ( 𝑖 ∈ ℕ0 → 𝑖 ∈ ℝ )
41 40 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑆 < 𝑖 ) → 𝑖 ∈ ℝ )
42 17 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑆 < 𝑖 ) → ( 𝑖 + 1 ) ∈ ℕ0 )
43 42 nn0red ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑆 < 𝑖 ) → ( 𝑖 + 1 ) ∈ ℝ )
44 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑆 < 𝑖 ) → 𝑆 < 𝑖 )
45 41 ltp1d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑆 < 𝑖 ) → 𝑖 < ( 𝑖 + 1 ) )
46 39 41 43 44 45 lttrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑆 < 𝑖 ) → 𝑆 < ( 𝑖 + 1 ) )
47 46 ex ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑆 < 𝑖 → 𝑆 < ( 𝑖 + 1 ) ) )
48 rspsbca ⊢ ( ( ( 𝑖 + 1 ) ∈ ℕ0 ∧ ∀ 𝑘 ∈ ℕ0 ( 𝑆 < 𝑘 → 𝐶 = 0 ) ) → [ ( 𝑖 + 1 ) / 𝑘 ] ( 𝑆 < 𝑘 → 𝐶 = 0 ) )
49 ovex ⊢ ( 𝑖 + 1 ) ∈ V
50 sbcimg ⊢ ( ( 𝑖 + 1 ) ∈ V → ( [ ( 𝑖 + 1 ) / 𝑘 ] ( 𝑆 < 𝑘 → 𝐶 = 0 ) ↔ ( [ ( 𝑖 + 1 ) / 𝑘 ] 𝑆 < 𝑘 → [ ( 𝑖 + 1 ) / 𝑘 ] 𝐶 = 0 ) ) )
51 sbcbr2g ⊢ ( ( 𝑖 + 1 ) ∈ V → ( [ ( 𝑖 + 1 ) / 𝑘 ] 𝑆 < 𝑘 ↔ 𝑆 < ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝑘 ) )
52 csbvarg ⊢ ( ( 𝑖 + 1 ) ∈ V → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝑘 = ( 𝑖 + 1 ) )
53 52 breq2d ⊢ ( ( 𝑖 + 1 ) ∈ V → ( 𝑆 < ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝑘 ↔ 𝑆 < ( 𝑖 + 1 ) ) )
54 51 53 bitrd ⊢ ( ( 𝑖 + 1 ) ∈ V → ( [ ( 𝑖 + 1 ) / 𝑘 ] 𝑆 < 𝑘 ↔ 𝑆 < ( 𝑖 + 1 ) ) )
55 sbceq1g ⊢ ( ( 𝑖 + 1 ) ∈ V → ( [ ( 𝑖 + 1 ) / 𝑘 ] 𝐶 = 0 ↔ ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 = 0 ) )
56 54 55 imbi12d ⊢ ( ( 𝑖 + 1 ) ∈ V → ( ( [ ( 𝑖 + 1 ) / 𝑘 ] 𝑆 < 𝑘 → [ ( 𝑖 + 1 ) / 𝑘 ] 𝐶 = 0 ) ↔ ( 𝑆 < ( 𝑖 + 1 ) → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 = 0 ) ) )
57 50 56 bitrd ⊢ ( ( 𝑖 + 1 ) ∈ V → ( [ ( 𝑖 + 1 ) / 𝑘 ] ( 𝑆 < 𝑘 → 𝐶 = 0 ) ↔ ( 𝑆 < ( 𝑖 + 1 ) → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 = 0 ) ) )
58 49 57 ax-mp ⊢ ( [ ( 𝑖 + 1 ) / 𝑘 ] ( 𝑆 < 𝑘 → 𝐶 = 0 ) ↔ ( 𝑆 < ( 𝑖 + 1 ) → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 = 0 ) )
59 48 58 sylib ⊢ ( ( ( 𝑖 + 1 ) ∈ ℕ0 ∧ ∀ 𝑘 ∈ ℕ0 ( 𝑆 < 𝑘 → 𝐶 = 0 ) ) → ( 𝑆 < ( 𝑖 + 1 ) → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 = 0 ) )
60 17 7 59 syl2anr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑆 < ( 𝑖 + 1 ) → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 = 0 ) )
61 47 60 syld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑆 < 𝑖 → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 = 0 ) )
62 61 imp ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑆 < 𝑖 ) → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 = 0 )
63 36 62 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑆 < 𝑖 ) → ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) = ( 0 − 0 ) )
64 12 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑆 < 𝑖 ) → 𝐺 ∈ Grp )
65 1 4 grpidcl ⊢ ( 𝐺 ∈ Grp → 0 ∈ 𝐵 )
66 1 4 3 grpsubid ⊢ ( ( 𝐺 ∈ Grp ∧ 0 ∈ 𝐵 ) → ( 0 − 0 ) = 0 )
67 64 65 66 syl2anc2 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑆 < 𝑖 ) → ( 0 − 0 ) = 0 )
68 63 67 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑆 < 𝑖 ) → ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) = 0 )
69 68 ex ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑆 < 𝑖 → ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) = 0 ) )
70 69 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ℕ0 ( 𝑆 < 𝑖 → ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) = 0 ) )
71 1 4 9 22 6 70 gsummptnn0fz ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ℕ0 ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( 𝐺 Σg ( 𝑖 ∈ ( 0 ... 𝑆 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) )
72 fzssuz ⊢ ( 0 ... ( 𝑆 + 1 ) ) ⊆ ( ℤ≥ ‘ 0 )
73 72 a1i ⊢ ( 𝜑 → ( 0 ... ( 𝑆 + 1 ) ) ⊆ ( ℤ≥ ‘ 0 ) )
74 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
75 73 74 sseqtrrdi ⊢ ( 𝜑 → ( 0 ... ( 𝑆 + 1 ) ) ⊆ ℕ0 )
76 ssralv ⊢ ( ( 0 ... ( 𝑆 + 1 ) ) ⊆ ℕ0 → ( ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 → ∀ 𝑘 ∈ ( 0 ... ( 𝑆 + 1 ) ) 𝐶 ∈ 𝐵 ) )
77 75 5 76 sylc ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( 𝑆 + 1 ) ) 𝐶 ∈ 𝐵 )
78 1 2 3 6 77 telgsumfz0s ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ( 0 ... 𝑆 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 0 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑆 + 1 ) / 𝑘 ⦌ 𝐶 ) )
79 peano2nn0 ⊢ ( 𝑆 ∈ ℕ0 → ( 𝑆 + 1 ) ∈ ℕ0 )
80 6 79 syl ⊢ ( 𝜑 → ( 𝑆 + 1 ) ∈ ℕ0 )
81 37 ltp1d ⊢ ( 𝜑 → 𝑆 < ( 𝑆 + 1 ) )
82 rspsbca ⊢ ( ( ( 𝑆 + 1 ) ∈ ℕ0 ∧ ∀ 𝑘 ∈ ℕ0 ( 𝑆 < 𝑘 → 𝐶 = 0 ) ) → [ ( 𝑆 + 1 ) / 𝑘 ] ( 𝑆 < 𝑘 → 𝐶 = 0 ) )
83 ovex ⊢ ( 𝑆 + 1 ) ∈ V
84 sbcimg ⊢ ( ( 𝑆 + 1 ) ∈ V → ( [ ( 𝑆 + 1 ) / 𝑘 ] ( 𝑆 < 𝑘 → 𝐶 = 0 ) ↔ ( [ ( 𝑆 + 1 ) / 𝑘 ] 𝑆 < 𝑘 → [ ( 𝑆 + 1 ) / 𝑘 ] 𝐶 = 0 ) ) )
85 sbcbr2g ⊢ ( ( 𝑆 + 1 ) ∈ V → ( [ ( 𝑆 + 1 ) / 𝑘 ] 𝑆 < 𝑘 ↔ 𝑆 < ⦋ ( 𝑆 + 1 ) / 𝑘 ⦌ 𝑘 ) )
86 csbvarg ⊢ ( ( 𝑆 + 1 ) ∈ V → ⦋ ( 𝑆 + 1 ) / 𝑘 ⦌ 𝑘 = ( 𝑆 + 1 ) )
87 86 breq2d ⊢ ( ( 𝑆 + 1 ) ∈ V → ( 𝑆 < ⦋ ( 𝑆 + 1 ) / 𝑘 ⦌ 𝑘 ↔ 𝑆 < ( 𝑆 + 1 ) ) )
88 85 87 bitrd ⊢ ( ( 𝑆 + 1 ) ∈ V → ( [ ( 𝑆 + 1 ) / 𝑘 ] 𝑆 < 𝑘 ↔ 𝑆 < ( 𝑆 + 1 ) ) )
89 sbceq1g ⊢ ( ( 𝑆 + 1 ) ∈ V → ( [ ( 𝑆 + 1 ) / 𝑘 ] 𝐶 = 0 ↔ ⦋ ( 𝑆 + 1 ) / 𝑘 ⦌ 𝐶 = 0 ) )
90 88 89 imbi12d ⊢ ( ( 𝑆 + 1 ) ∈ V → ( ( [ ( 𝑆 + 1 ) / 𝑘 ] 𝑆 < 𝑘 → [ ( 𝑆 + 1 ) / 𝑘 ] 𝐶 = 0 ) ↔ ( 𝑆 < ( 𝑆 + 1 ) → ⦋ ( 𝑆 + 1 ) / 𝑘 ⦌ 𝐶 = 0 ) ) )
91 84 90 bitrd ⊢ ( ( 𝑆 + 1 ) ∈ V → ( [ ( 𝑆 + 1 ) / 𝑘 ] ( 𝑆 < 𝑘 → 𝐶 = 0 ) ↔ ( 𝑆 < ( 𝑆 + 1 ) → ⦋ ( 𝑆 + 1 ) / 𝑘 ⦌ 𝐶 = 0 ) ) )
92 83 91 ax-mp ⊢ ( [ ( 𝑆 + 1 ) / 𝑘 ] ( 𝑆 < 𝑘 → 𝐶 = 0 ) ↔ ( 𝑆 < ( 𝑆 + 1 ) → ⦋ ( 𝑆 + 1 ) / 𝑘 ⦌ 𝐶 = 0 ) )
93 82 92 sylib ⊢ ( ( ( 𝑆 + 1 ) ∈ ℕ0 ∧ ∀ 𝑘 ∈ ℕ0 ( 𝑆 < 𝑘 → 𝐶 = 0 ) ) → ( 𝑆 < ( 𝑆 + 1 ) → ⦋ ( 𝑆 + 1 ) / 𝑘 ⦌ 𝐶 = 0 ) )
94 93 ex ⊢ ( ( 𝑆 + 1 ) ∈ ℕ0 → ( ∀ 𝑘 ∈ ℕ0 ( 𝑆 < 𝑘 → 𝐶 = 0 ) → ( 𝑆 < ( 𝑆 + 1 ) → ⦋ ( 𝑆 + 1 ) / 𝑘 ⦌ 𝐶 = 0 ) ) )
95 80 7 81 94 syl3c ⊢ ( 𝜑 → ⦋ ( 𝑆 + 1 ) / 𝑘 ⦌ 𝐶 = 0 )
96 95 oveq2d ⊢ ( 𝜑 → ( ⦋ 0 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑆 + 1 ) / 𝑘 ⦌ 𝐶 ) = ( ⦋ 0 / 𝑘 ⦌ 𝐶 − 0 ) )
97 0nn0 ⊢ 0 ∈ ℕ0
98 97 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
99 rspcsbela ⊢ ( ( 0 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 ) → ⦋ 0 / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
100 98 5 99 syl2anc ⊢ ( 𝜑 → ⦋ 0 / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
101 1 4 3 grpsubid1 ⊢ ( ( 𝐺 ∈ Grp ∧ ⦋ 0 / 𝑘 ⦌ 𝐶 ∈ 𝐵 ) → ( ⦋ 0 / 𝑘 ⦌ 𝐶 − 0 ) = ⦋ 0 / 𝑘 ⦌ 𝐶 )
102 11 100 101 syl2anc ⊢ ( 𝜑 → ( ⦋ 0 / 𝑘 ⦌ 𝐶 − 0 ) = ⦋ 0 / 𝑘 ⦌ 𝐶 )
103 96 102 eqtrd ⊢ ( 𝜑 → ( ⦋ 0 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑆 + 1 ) / 𝑘 ⦌ 𝐶 ) = ⦋ 0 / 𝑘 ⦌ 𝐶 )
104 71 78 103 3eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ℕ0 ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ⦋ 0 / 𝑘 ⦌ 𝐶 )