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 
|- B = ( Base ` G )
telgsums.g 
|- ( ph -> G e. Abel )
telgsums.m 
|- .- = ( -g ` G )
telgsums.0 
|- .0. = ( 0g ` G )
telgsums.f 
|- ( ph -> A. k e. NN0 C e. B )
telgsums.s 
|- ( ph -> S e. NN0 )
telgsums.u 
|- ( ph -> A. k e. NN0 ( S < k -> C = .0. ) )
Assertion telgsums 
|- ( ph -> ( G gsum ( i e. NN0 |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = [_ 0 / k ]_ C )

Proof

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