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 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
60 58 59 syl 
 |-  ( ph -> G e. Mnd )
61 60 adantr 
 |-  ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> G e. Mnd )
62 58 adantr 
 |-  ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> G e. Grp )
63 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
64 52 63 syl 
 |-  ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> M e. ( ZZ>= ` M ) )
65 peano2uz 
 |-  ( M e. ( ZZ>= ` M ) -> ( M + 1 ) e. ( ZZ>= ` M ) )
66 64 65 syl 
 |-  ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> ( M + 1 ) e. ( ZZ>= ` M ) )
67 eluzfz1 
 |-  ( ( M + 1 ) e. ( ZZ>= ` M ) -> M e. ( M ... ( M + 1 ) ) )
68 66 67 syl 
 |-  ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> M e. ( M ... ( M + 1 ) ) )
69 rspcsbela 
 |-  ( ( M e. ( M ... ( M + 1 ) ) /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> [_ M / k ]_ C e. B )
70 68 69 sylancom 
 |-  ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> [_ M / k ]_ C e. B )
71 eluzfz2 
 |-  ( ( M + 1 ) e. ( ZZ>= ` M ) -> ( M + 1 ) e. ( M ... ( M + 1 ) ) )
72 66 71 syl 
 |-  ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> ( M + 1 ) e. ( M ... ( M + 1 ) ) )
73 rspcsbela 
 |-  ( ( ( M + 1 ) e. ( M ... ( M + 1 ) ) /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> [_ ( M + 1 ) / k ]_ C e. B )
74 72 73 sylancom 
 |-  ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> [_ ( M + 1 ) / k ]_ C e. B )
75 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 )
76 62 70 74 75 syl3anc 
 |-  ( ( ph /\ A. k e. ( M ... ( M + 1 ) ) C e. B ) -> ( [_ M / k ]_ C .- [_ ( M + 1 ) / k ]_ C ) e. B )
77 csbeq1 
 |-  ( i = M -> [_ i / k ]_ C = [_ M / k ]_ C )
78 oveq1 
 |-  ( i = M -> ( i + 1 ) = ( M + 1 ) )
79 78 csbeq1d 
 |-  ( i = M -> [_ ( i + 1 ) / k ]_ C = [_ ( M + 1 ) / k ]_ C )
80 77 79 oveq12d 
 |-  ( i = M -> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) = ( [_ M / k ]_ C .- [_ ( M + 1 ) / k ]_ C ) )
81 80 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 ) )
82 1 61 52 76 81 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 ) )
83 56 82 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 ) )
84 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 ) ) )
85 84 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 ) ) ) )
86 eluzelz 
 |-  ( y e. ( ZZ>= ` M ) -> y e. ZZ )
87 86 peano2zd 
 |-  ( y e. ( ZZ>= ` M ) -> ( y + 1 ) e. ZZ )
88 87 peano2zd 
 |-  ( y e. ( ZZ>= ` M ) -> ( ( y + 1 ) + 1 ) e. ZZ )
89 peano2z 
 |-  ( y e. ZZ -> ( y + 1 ) e. ZZ )
90 89 zred 
 |-  ( y e. ZZ -> ( y + 1 ) e. RR )
91 86 90 syl 
 |-  ( y e. ( ZZ>= ` M ) -> ( y + 1 ) e. RR )
92 91 lep1d 
 |-  ( y e. ( ZZ>= ` M ) -> ( y + 1 ) <_ ( ( y + 1 ) + 1 ) )
93 eluz2 
 |-  ( ( ( y + 1 ) + 1 ) e. ( ZZ>= ` ( y + 1 ) ) <-> ( ( y + 1 ) e. ZZ /\ ( ( y + 1 ) + 1 ) e. ZZ /\ ( y + 1 ) <_ ( ( y + 1 ) + 1 ) ) )
94 87 88 92 93 syl3anbrc 
 |-  ( y e. ( ZZ>= ` M ) -> ( ( y + 1 ) + 1 ) e. ( ZZ>= ` ( y + 1 ) ) )
95 fzss2 
 |-  ( ( ( y + 1 ) + 1 ) e. ( ZZ>= ` ( y + 1 ) ) -> ( M ... ( y + 1 ) ) C_ ( M ... ( ( y + 1 ) + 1 ) ) )
96 94 95 syl 
 |-  ( y e. ( ZZ>= ` M ) -> ( M ... ( y + 1 ) ) C_ ( M ... ( ( y + 1 ) + 1 ) ) )
97 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 ) )
98 96 97 syl 
 |-  ( y e. ( ZZ>= ` M ) -> ( A. k e. ( M ... ( ( y + 1 ) + 1 ) ) C e. B -> A. k e. ( M ... ( y + 1 ) ) C e. B ) )
99 98 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 ) )
100 85 99 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 ) ) ) )
101 16 27 38 49 83 100 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 ) ) )
102 101 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 ) ) ) )
103 4 102 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 ) ) )
104 5 103 mpd 
 |-  ( ph -> ( G gsum ( i e. ( M ... N ) |-> ( [_ i / k ]_ C .- [_ ( i + 1 ) / k ]_ C ) ) ) = ( [_ M / k ]_ C .- [_ ( N + 1 ) / k ]_ C ) )