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

Metamath Proof Explorer

Theorem telgsumfzs

Description: Telescoping group sum ranging over a finite set of sequential integers, using explicit substitution. (Contributed by AV, 23-Nov-2019)

Ref Expression
Hypotheses telgsumfzs.b 
|- B = ( Base ` G )
telgsumfzs.g 
|- ( ph -> G e. Abel )
telgsumfzs.m 
|- .- = ( -g ` G )
telgsumfzs.n 
|- ( ph -> N e. ( ZZ>= ` M ) )
telgsumfzs.f 
|- ( ph -> A. k e. ( M ... ( N + 1 ) ) C e. B )
Assertion telgsumfzs 
|- ( ph -> ( G gsum ( i e. ( M ... N ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( N + 1 ) / k ]_ C ) )

Proof

Step Hyp Ref Expression
1 telgsumfzs.b 
 |-  B = ( Base ` G )
2 telgsumfzs.g 
 |-  ( ph -> G e. Abel )
3 telgsumfzs.m 
 |-  .- = ( -g ` G )
4 telgsumfzs.n 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
5 telgsumfzs.f 
 |-  ( ph -> A. k e. ( M ... ( N + 1 ) ) C e. B )
6 oveq1 
 |-  ( x = M -> ( x + 1 ) = ( M + 1 ) )
7 6 oveq2d 
 |-  ( x = M -> ( M ... ( x + 1 ) ) = ( M ... ( M + 1 ) ) )
8 7 raleqdv 
 |-  ( x = M -> ( A. k e. ( M ... ( x + 1 ) ) C e. B <-> A. k e. ( M ... ( M + 1 ) ) C e. B ) )
9 8 anbi2d 
 |-  ( x = M -> ( ( ph /\ A. k e. ( M ... ( x + 1 ) ) C e. B ) <-> ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) ) )
10 oveq2 
 |-  ( x = M -> ( M ... x ) = ( M ... M ) )
11 10 mpteq1d 
 |-  ( x = M -> ( i e. ( M ... x ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) = ( i e. ( M ... M ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) )
12 11 oveq2d 
 |-  ( x = M -> ( G gsum ( i e. ( M ... x ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( G gsum ( i e. ( M ... M ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) )
13 6 csbeq1d 
 |-  ( x = M -> [_ ( x + 1 ) / k ]_ C = [_ ( M + 1 ) / k ]_ C )
14 13 oveq2d 
 |-  ( x = M -> ( [_ M / k ]_ C .- [_ ( x + 1 ) / k ]_ C ) = ( [_ M / k ]_ C .- [_ ( M + 1 ) / k ]_ C ) )
15 12 14 eqeq12d 
 |-  ( x = M -> ( ( G gsum ( i e. ( M ... x ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( x + 1 ) / k ]_ C ) <-> ( G gsum ( i e. ( M ... M ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( M + 1 ) / k ]_ C ) ) )
16 9 15 imbi12d 
 |-  ( x = M -> ( ( ( ph /\ A. k e. ( M ... ( x + 1 ) ) C e. B ) -> ( G gsum ( i e. ( M ... x ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( x + 1 ) / k ]_ C ) ) <-> ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> ( G gsum ( i e. ( M ... M ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( M + 1 ) / k ]_ C ) ) ) )
17 oveq1 
 |-  ( x = y -> ( x + 1 ) = ( y + 1 ) )
18 17 oveq2d 
 |-  ( x = y -> ( M ... ( x + 1 ) ) = ( M ... ( y + 1 ) ) )
19 18 raleqdv 
 |-  ( x = y -> ( A. k e. ( M ... ( x + 1 ) ) C e. B <-> A. k e. ( M ... ( y + 1 ) ) C e. B ) )
20 19 anbi2d 
 |-  ( x = y -> ( ( ph /\ A. k e. ( M ... ( x + 1 ) ) C e. B ) <-> ( ph /\ A. k e. ( M ... ( y + 1 ) ) C e. B ) ) )
21 oveq2 
 |-  ( x = y -> ( M ... x ) = ( M ... y ) )
22 21 mpteq1d 
 |-  ( x = y -> ( i e. ( M ... x ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) = ( i e. ( M ... y ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) )
23 22 oveq2d 
 |-  ( x = y -> ( G gsum ( i e. ( M ... x ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( G gsum ( i e. ( M ... y ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) )
24 17 csbeq1d 
 |-  ( x = y -> [_ ( x + 1 ) / k ]_ C = [_ ( y + 1 ) / k ]_ C )
25 24 oveq2d 
 |-  ( x = y -> ( [_ M / k ]_ C .- [_ ( x + 1 ) / k ]_ C ) = ( [_ M / k ]_ C .- [_ ( y + 1 ) / k ]_ C ) )
26 23 25 eqeq12d 
 |-  ( x = y -> ( ( G gsum ( i e. ( M ... x ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( x + 1 ) / k ]_ C ) <-> ( G gsum ( i e. ( M ... y ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( y + 1 ) / k ]_ C ) ) )
27 20 26 imbi12d 
 |-  ( x = y -> ( ( ( ph /\ A. k e. ( M ... ( x + 1 ) ) C e. B ) -> ( G gsum ( i e. ( M ... x ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( x + 1 ) / k ]_ C ) ) <-> ( ( ph /\ A. k e. ( M ... ( y + 1 ) ) C e. B ) -> ( G gsum ( i e. ( M ... y ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( y + 1 ) / k ]_ C ) ) ) )
28 oveq1 
 |-  ( x = ( y + 1 ) -> ( x + 1 ) = ( ( y + 1 ) + 1 ) )
29 28 oveq2d 
 |-  ( x = ( y + 1 ) -> ( M ... ( x + 1 ) ) = ( M ... ( ( y + 1 ) + 1 ) ) )
30 29 raleqdv 
 |-  ( x = ( y + 1 ) -> ( A. k e. ( M ... ( x + 1 ) ) C e. B <-> A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) )
31 30 anbi2d 
 |-  ( x = ( y + 1 ) -> ( ( ph /\ A. k e. ( M ... ( x + 1 ) ) C e. B ) <-> ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) )
32 oveq2 
 |-  ( x = ( y + 1 ) -> ( M ... x ) = ( M ... ( y + 1 ) ) )
33 32 mpteq1d 
 |-  ( x = ( y + 1 ) -> ( i e. ( M ... x ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) = ( i e. ( M ... ( y + 1 ) ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) )
34 33 oveq2d 
 |-  ( x = ( y + 1 ) -> ( G gsum ( i e. ( M ... x ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( G gsum ( i e. ( M ... ( y + 1 ) ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) )
35 28 csbeq1d 
 |-  ( x = ( y + 1 ) -> [_ ( x + 1 ) / k ]_ C = [_ ( ( y + 1 ) + 1 ) / k ]_ C )
36 35 oveq2d 
 |-  ( x = ( y + 1 ) -> ( [_ M / k ]_ C .- [_ ( x + 1 ) / k ]_ C ) = ( [_ M / k ]_ C .- [_ ( ( y + 1 ) + 1 ) / k ]_ C ) )
37 34 36 eqeq12d 
 |-  ( x = ( y + 1 ) -> ( ( G gsum ( i e. ( M ... x ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( x + 1 ) / k ]_ C ) <-> ( G gsum ( i e. ( M ... ( y + 1 ) ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( ( y + 1 ) + 1 ) / k ]_ C ) ) )
38 31 37 imbi12d 
 |-  ( x = ( y + 1 ) -> ( ( ( ph /\ A. k e. ( M ... ( x + 1 ) ) C e. B ) -> ( G gsum ( i e. ( M ... x ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( x + 1 ) / k ]_ C ) ) <-> ( ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) -> ( G gsum ( i e. ( M ... ( y + 1 ) ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( ( y + 1 ) + 1 ) / k ]_ C ) ) ) )
39 oveq1 
 |-  ( x = N -> ( x + 1 ) = ( N + 1 ) )
40 39 oveq2d 
 |-  ( x = N -> ( M ... ( x + 1 ) ) = ( M ... ( N + 1 ) ) )
41 40 raleqdv 
 |-  ( x = N -> ( A. k e. ( M ... ( x + 1 ) ) C e. B <-> A. k e. ( M ... ( N + 1 ) ) C e. B ) )
42 41 anbi2d 
 |-  ( x = N -> ( ( ph /\ A. k e. ( M ... ( x + 1 ) ) C e. B ) <-> ( ph /\ A. k e. ( M ... ( N + 1 ) ) C e. B ) ) )
43 oveq2 
 |-  ( x = N -> ( M ... x ) = ( M ... N ) )
44 43 mpteq1d 
 |-  ( x = N -> ( i e. ( M ... x ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) = ( i e. ( M ... N ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) )
45 44 oveq2d 
 |-  ( x = N -> ( G gsum ( i e. ( M ... x ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( G gsum ( i e. ( M ... N ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) )
46 39 csbeq1d 
 |-  ( x = N -> [_ ( x + 1 ) / k ]_ C = [_ ( N + 1 ) / k ]_ C )
47 46 oveq2d 
 |-  ( x = N -> ( [_ M / k ]_ C .- [_ ( x + 1 ) / k ]_ C ) = ( [_ M / k ]_ C .- [_ ( N + 1 ) / k ]_ C ) )
48 45 47 eqeq12d 
 |-  ( x = N -> ( ( G gsum ( i e. ( M ... x ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( x + 1 ) / k ]_ C ) <-> ( G gsum ( i e. ( M ... N ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( N + 1 ) / k ]_ C ) ) )
49 42 48 imbi12d 
 |-  ( x = N -> ( ( ( ph /\ A. k e. ( M ... ( x + 1 ) ) C e. B ) -> ( G gsum ( i e. ( M ... x ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( x + 1 ) / k ]_ C ) ) <-> ( ( ph /\ A. k e. ( M ... ( N + 1 ) ) C e. B ) -> ( G gsum ( i e. ( M ... N ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( N + 1 ) / k ]_ C ) ) ) )
50 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
51 4 50 syl 
 |-  ( ph -> M e. ZZ )
52 51 adantr 
 |-  ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> M e. ZZ )
53 fzsn 
 |-  ( M e. ZZ -> ( M ... M ) = { M } )
54 52 53 syl 
 |-  ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> ( M ... M ) = { M } )
55 54 mpteq1d 
 |-  ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> ( i e. ( M ... M ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) = ( i e. { M } |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) )
56 55 oveq2d 
 |-  ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> ( G gsum ( i e. ( M ... M ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( G gsum ( i e. { M } |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) )
57 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
58 2 57 syl 
 |-  ( ph -> G e. Grp )
59 58 grpmndd 
 |-  ( ph -> G e. Mnd )
60 59 adantr 
 |-  ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> G e. Mnd )
61 58 adantr 
 |-  ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> G e. Grp )
62 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
63 52 62 syl 
 |-  ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> M e. ( ZZ>= ` M ) )
64 peano2uz 
 |-  ( M e. ( ZZ>= ` M ) -> ( M + 1 ) e. ( ZZ>= ` M ) )
65 63 64 syl 
 |-  ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> ( M + 1 ) e. ( ZZ>= ` M ) )
66 eluzfz1 
 |-  ( ( M + 1 ) e. ( ZZ>= ` M ) -> M e. ( M ... ( M + 1 ) ) )
67 65 66 syl 
 |-  ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> M e. ( M ... ( M + 1 ) ) )
68 rspcsbela 
 |-  ( ( M e. ( M ... ( M + 1 ) ) /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> [_ M / k ]_ C e. B )
69 67 68 sylancom 
 |-  ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> [_ M / k ]_ C e. B )
70 eluzfz2 
 |-  ( ( M + 1 ) e. ( ZZ>= ` M ) -> ( M + 1 ) e. ( M ... ( M + 1 ) ) )
71 65 70 syl 
 |-  ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> ( M + 1 ) e. ( M ... ( M + 1 ) ) )
72 rspcsbela 
 |-  ( ( ( M + 1 ) e. ( M ... ( M + 1 ) ) /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> [_ ( M + 1 ) / k ]_ C e. B )
73 71 72 sylancom 
 |-  ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> [_ ( M + 1 ) / k ]_ C e. B )
74 1 3 grpsubcl 
 |-  ( ( G e. Grp /\ [_ M / k ]_ C e. B /\ [_ ( M + 1 ) / k ]_ C e. B ) -> ( [_ M / k ]_ C .- [_ ( M + 1 ) / k ]_ C ) e. B )
75 61 69 73 74 syl3anc 
 |-  ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> ( [_ M / k ]_ C .- [_ ( M + 1 ) / k ]_ C ) e. B )
76 csbeq1 
 |-  ( i = M -> [_ i / k ]_ C = [_ M / k ]_ C )
77 oveq1 
 |-  ( i = M -> ( i + 1 ) = ( M + 1 ) )
78 77 csbeq1d 
 |-  ( i = M -> [_ ( i + 1 ) / k ]_ C = [_ ( M + 1 ) / k ]_ C )
79 76 78 oveq12d 
 |-  ( i = M -> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) = ( [_ M / k ]_ C .- [_ ( M + 1 ) / k ]_ C ) )
80 79 adantl 
 |-  ( ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) /\ i = M ) -> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) = ( [_ M / k ]_ C .- [_ ( M + 1 ) / k ]_ C ) )
81 1 60 52 75 80 gsumsnd 
 |-  ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> ( G gsum ( i e. { M } |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( M + 1 ) / k ]_ C ) )
82 56 81 eqtrd 
 |-  ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> ( G gsum ( i e. ( M ... M ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( M + 1 ) / k ]_ C ) )
83 1 2 3 telgsumfzslem 
 |-  ( ( y e. ( ZZ>= ` M ) /\ ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) ) -> ( ( G gsum ( i e. ( M ... y ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( y + 1 ) / k ]_ C ) -> ( G gsum ( i e. ( M ... ( y + 1 ) ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( ( y + 1 ) + 1 ) / k ]_ C ) ) )
84 83 ex 
 |-  ( y e. ( ZZ>= ` M ) -> ( ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) -> ( ( G gsum ( i e. ( M ... y ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( y + 1 ) / k ]_ C ) -> ( G gsum ( i e. ( M ... ( y + 1 ) ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( ( y + 1 ) + 1 ) / k ]_ C ) ) ) )
85 eluzelz 
 |-  ( y e. ( ZZ>= ` M ) -> y e. ZZ )
86 85 peano2zd 
 |-  ( y e. ( ZZ>= ` M ) -> ( y + 1 ) e. ZZ )
87 86 peano2zd 
 |-  ( y e. ( ZZ>= ` M ) -> ( ( y + 1 ) + 1 ) e. ZZ )
88 peano2z 
 |-  ( y e. ZZ -> ( y + 1 ) e. ZZ )
89 88 zred 
 |-  ( y e. ZZ -> ( y + 1 ) e. RR )
90 85 89 syl 
 |-  ( y e. ( ZZ>= ` M ) -> ( y + 1 ) e. RR )
91 90 lep1d 
 |-  ( y e. ( ZZ>= ` M ) -> ( y + 1 ) <_ ( ( y + 1 ) + 1 ) )
92 eluz2 
 |-  ( ( ( y + 1 ) + 1 ) e. ( ZZ>= ` ( y + 1 ) ) <-> ( ( y + 1 ) e. ZZ /\ ( ( y + 1 ) + 1 ) e. ZZ /\ ( y + 1 ) <_ ( ( y + 1 ) + 1 ) ) )
93 86 87 91 92 syl3anbrc 
 |-  ( y e. ( ZZ>= ` M ) -> ( ( y + 1 ) + 1 ) e. ( ZZ>= ` ( y + 1 ) ) )
94 fzss2 
 |-  ( ( ( y + 1 ) + 1 ) e. ( ZZ>= ` ( y + 1 ) ) -> ( M ... ( y + 1 ) ) C_ ( M ... ( ( y + 1 ) + 1 ) ) )
95 93 94 syl 
 |-  ( y e. ( ZZ>= ` M ) -> ( M ... ( y + 1 ) ) C_ ( M ... ( ( y + 1 ) + 1 ) ) )
96 ssralv 
 |-  ( ( M ... ( y + 1 ) ) C_ ( M ... ( ( y + 1 ) + 1 ) ) -> ( A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B -> A. k e. ( M ... ( y + 1 ) ) C e. B ) )
97 95 96 syl 
 |-  ( y e. ( ZZ>= ` M ) -> ( A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B -> A. k e. ( M ... ( y + 1 ) ) C e. B ) )
98 97 adantld 
 |-  ( y e. ( ZZ>= ` M ) -> ( ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) -> A. k e. ( M ... ( y + 1 ) ) C e. B ) )
99 84 98 a2and 
 |-  ( y e. ( ZZ>= ` M ) -> ( ( ( ph /\ A. k e. ( M ... ( y + 1 ) ) C e. B ) -> ( G gsum ( i e. ( M ... y ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( y + 1 ) / k ]_ C ) ) -> ( ( ph /\ A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B ) -> ( G gsum ( i e. ( M ... ( y + 1 ) ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( ( y + 1 ) + 1 ) / k ]_ C ) ) ) )
100 16 27 38 49 82 99 uzind4i 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( ph /\ A. k e. ( M ... ( N + 1 ) ) C e. B ) -> ( G gsum ( i e. ( M ... N ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( N + 1 ) / k ]_ C ) ) )
101 100 expd 
 |-  ( N e. ( ZZ>= ` M ) -> ( ph -> ( A. k e. ( M ... ( N + 1 ) ) C e. B -> ( G gsum ( i e. ( M ... N ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( N + 1 ) / k ]_ C ) ) ) )
102 4 101 mpcom 
 |-  ( ph -> ( A. k e. ( M ... ( N + 1 ) ) C e. B -> ( G gsum ( i e. ( M ... N ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( N + 1 ) / k ]_ C ) ) )
103 5 102 mpd 
 |-  ( ph -> ( G gsum ( i e. ( M ... N ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( N + 1 ) / k ]_ C ) )