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 φ G Abel
telgsums.m - ˙ = - G
telgsums.0 0 ˙ = 0 G
telgsums.f φ k 0 C B
telgsums.s φ S 0
telgsums.u φ k 0 S < k C = 0 ˙
Assertion telgsums φ G i 0 i / k C - ˙ i + 1 / k C = 0 / k C

Proof

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