Metamath Proof Explorer

Theorem isumsplit

Description: Split off the first N terms of an infinite sum. (Contributed by Paul Chapman, 9-Feb-2008) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses isumsplit.1 
|- Z = ( ZZ>= ` M )
isumsplit.2 
|- W = ( ZZ>= ` N )
isumsplit.3 
|- ( ph -> N e. Z )
isumsplit.4 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
isumsplit.5 
|- ( ( ph /\ k e. Z ) -> A e. CC )
isumsplit.6 
|- ( ph -> seq M ( + , F ) e. dom ~~> )
Assertion isumsplit 
|- ( ph -> sum_ k e. Z A = ( sum_ k e. ( M ... ( N - 1 ) ) A + sum_ k e. W A ) )

Proof

Step Hyp Ref Expression
1 isumsplit.1 
 |-  Z = ( ZZ>= ` M )
2 isumsplit.2 
 |-  W = ( ZZ>= ` N )
3 isumsplit.3 
 |-  ( ph -> N e. Z )
4 isumsplit.4 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
5 isumsplit.5 
 |-  ( ( ph /\ k e. Z ) -> A e. CC )
6 isumsplit.6 
 |-  ( ph -> seq M ( + , F ) e. dom ~~> )
7 3 1 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
8 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
9 7 8 syl 
 |-  ( ph -> M e. ZZ )
10 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
11 7 10 syl 
 |-  ( ph -> N e. ZZ )
12 uzss 
 |-  ( N e. ( ZZ>= ` M ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
13 7 12 syl 
 |-  ( ph -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
14 13 2 1 3sstr4g 
 |-  ( ph -> W C_ Z )
15 14 sselda 
 |-  ( ( ph /\ k e. W ) -> k e. Z )
16 15 4 syldan 
 |-  ( ( ph /\ k e. W ) -> ( F ` k ) = A )
17 15 5 syldan 
 |-  ( ( ph /\ k e. W ) -> A e. CC )
18 4 5 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
19 1 3 18 iserex 
 |-  ( ph -> ( seq M ( + , F ) e. dom ~~> <-> seq N ( + , F ) e. dom ~~> ) )
20 6 19 mpbid 
 |-  ( ph -> seq N ( + , F ) e. dom ~~> )
21 2 11 16 17 20 isumclim2 
 |-  ( ph -> seq N ( + , F ) ~~> sum_ k e. W A )
22 fzfid 
 |-  ( ph -> ( M ... ( N - 1 ) ) e. Fin )
23 elfzuz 
 |-  ( k e. ( M ... ( N - 1 ) ) -> k e. ( ZZ>= ` M ) )
24 23 1 eleqtrrdi 
 |-  ( k e. ( M ... ( N - 1 ) ) -> k e. Z )
25 24 5 sylan2 
 |-  ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> A e. CC )
26 22 25 fsumcl 
 |-  ( ph -> sum_ k e. ( M ... ( N - 1 ) ) A e. CC )
27 15 18 syldan 
 |-  ( ( ph /\ k e. W ) -> ( F ` k ) e. CC )
28 2 11 27 serf 
 |-  ( ph -> seq N ( + , F ) : W --> CC )
29 28 ffvelrnda 
 |-  ( ( ph /\ j e. W ) -> ( seq N ( + , F ) ` j ) e. CC )
30 9 zred 
 |-  ( ph -> M e. RR )
31 30 ltm1d 
 |-  ( ph -> ( M - 1 ) < M )
32 peano2zm 
 |-  ( M e. ZZ -> ( M - 1 ) e. ZZ )
33 fzn 
 |-  ( ( M e. ZZ /\ ( M - 1 ) e. ZZ ) -> ( ( M - 1 ) < M <-> ( M ... ( M - 1 ) ) = (/) ) )
34 9 32 33 syl2anc2 
 |-  ( ph -> ( ( M - 1 ) < M <-> ( M ... ( M - 1 ) ) = (/) ) )
35 31 34 mpbid 
 |-  ( ph -> ( M ... ( M - 1 ) ) = (/) )
36 35 sumeq1d 
 |-  ( ph -> sum_ k e. ( M ... ( M - 1 ) ) A = sum_ k e. (/) A )
37 36 adantr 
 |-  ( ( ph /\ j e. W ) -> sum_ k e. ( M ... ( M - 1 ) ) A = sum_ k e. (/) A )
38 sum0 
 |-  sum_ k e. (/) A = 0
39 37 38 eqtrdi 
 |-  ( ( ph /\ j e. W ) -> sum_ k e. ( M ... ( M - 1 ) ) A = 0 )
40 39 oveq1d 
 |-  ( ( ph /\ j e. W ) -> ( sum_ k e. ( M ... ( M - 1 ) ) A + ( seq M ( + , F ) ` j ) ) = ( 0 + ( seq M ( + , F ) ` j ) ) )
41 14 sselda 
 |-  ( ( ph /\ j e. W ) -> j e. Z )
42 1 9 18 serf 
 |-  ( ph -> seq M ( + , F ) : Z --> CC )
43 42 ffvelrnda 
 |-  ( ( ph /\ j e. Z ) -> ( seq M ( + , F ) ` j ) e. CC )
44 41 43 syldan 
 |-  ( ( ph /\ j e. W ) -> ( seq M ( + , F ) ` j ) e. CC )
45 44 addid2d 
 |-  ( ( ph /\ j e. W ) -> ( 0 + ( seq M ( + , F ) ` j ) ) = ( seq M ( + , F ) ` j ) )
46 40 45 eqtr2d 
 |-  ( ( ph /\ j e. W ) -> ( seq M ( + , F ) ` j ) = ( sum_ k e. ( M ... ( M - 1 ) ) A + ( seq M ( + , F ) ` j ) ) )
47 oveq1 
 |-  ( N = M -> ( N - 1 ) = ( M - 1 ) )
48 47 oveq2d 
 |-  ( N = M -> ( M ... ( N - 1 ) ) = ( M ... ( M - 1 ) ) )
49 48 sumeq1d 
 |-  ( N = M -> sum_ k e. ( M ... ( N - 1 ) ) A = sum_ k e. ( M ... ( M - 1 ) ) A )
50 seqeq1 
 |-  ( N = M -> seq N ( + , F ) = seq M ( + , F ) )
51 50 fveq1d 
 |-  ( N = M -> ( seq N ( + , F ) ` j ) = ( seq M ( + , F ) ` j ) )
52 49 51 oveq12d 
 |-  ( N = M -> ( sum_ k e. ( M ... ( N - 1 ) ) A + ( seq N ( + , F ) ` j ) ) = ( sum_ k e. ( M ... ( M - 1 ) ) A + ( seq M ( + , F ) ` j ) ) )
53 52 eqeq2d 
 |-  ( N = M -> ( ( seq M ( + , F ) ` j ) = ( sum_ k e. ( M ... ( N - 1 ) ) A + ( seq N ( + , F ) ` j ) ) <-> ( seq M ( + , F ) ` j ) = ( sum_ k e. ( M ... ( M - 1 ) ) A + ( seq M ( + , F ) ` j ) ) ) )
54 46 53 syl5ibrcom 
 |-  ( ( ph /\ j e. W ) -> ( N = M -> ( seq M ( + , F ) ` j ) = ( sum_ k e. ( M ... ( N - 1 ) ) A + ( seq N ( + , F ) ` j ) ) ) )
55 addcl 
 |-  ( ( k e. CC /\ m e. CC ) -> ( k + m ) e. CC )
56 55 adantl 
 |-  ( ( ( ( ph /\ j e. W ) /\ N e. ( ZZ>= ` ( M + 1 ) ) ) /\ ( k e. CC /\ m e. CC ) ) -> ( k + m ) e. CC )
57 addass 
 |-  ( ( k e. CC /\ m e. CC /\ x e. CC ) -> ( ( k + m ) + x ) = ( k + ( m + x ) ) )
58 57 adantl 
 |-  ( ( ( ( ph /\ j e. W ) /\ N e. ( ZZ>= ` ( M + 1 ) ) ) /\ ( k e. CC /\ m e. CC /\ x e. CC ) ) -> ( ( k + m ) + x ) = ( k + ( m + x ) ) )
59 simplr 
 |-  ( ( ( ph /\ j e. W ) /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> j e. W )
60 simpll 
 |-  ( ( ( ph /\ j e. W ) /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ph )
61 11 zcnd 
 |-  ( ph -> N e. CC )
62 ax-1cn 
 |-  1 e. CC
63 npcan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
64 61 62 63 sylancl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
65 64 eqcomd 
 |-  ( ph -> N = ( ( N - 1 ) + 1 ) )
66 60 65 syl 
 |-  ( ( ( ph /\ j e. W ) /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> N = ( ( N - 1 ) + 1 ) )
67 66 fveq2d 
 |-  ( ( ( ph /\ j e. W ) /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ZZ>= ` N ) = ( ZZ>= ` ( ( N - 1 ) + 1 ) ) )
68 2 67 eqtrid 
 |-  ( ( ( ph /\ j e. W ) /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> W = ( ZZ>= ` ( ( N - 1 ) + 1 ) ) )
69 59 68 eleqtrd 
 |-  ( ( ( ph /\ j e. W ) /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> j e. ( ZZ>= ` ( ( N - 1 ) + 1 ) ) )
70 9 adantr 
 |-  ( ( ph /\ j e. W ) -> M e. ZZ )
71 eluzp1m1 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( N - 1 ) e. ( ZZ>= ` M ) )
72 70 71 sylan 
 |-  ( ( ( ph /\ j e. W ) /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( N - 1 ) e. ( ZZ>= ` M ) )
73 elfzuz 
 |-  ( k e. ( M ... j ) -> k e. ( ZZ>= ` M ) )
74 73 1 eleqtrrdi 
 |-  ( k e. ( M ... j ) -> k e. Z )
75 60 74 18 syl2an 
 |-  ( ( ( ( ph /\ j e. W ) /\ N e. ( ZZ>= ` ( M + 1 ) ) ) /\ k e. ( M ... j ) ) -> ( F ` k ) e. CC )
76 56 58 69 72 75 seqsplit 
 |-  ( ( ( ph /\ j e. W ) /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( seq M ( + , F ) ` j ) = ( ( seq M ( + , F ) ` ( N - 1 ) ) + ( seq ( ( N - 1 ) + 1 ) ( + , F ) ` j ) ) )
77 60 24 4 syl2an 
 |-  ( ( ( ( ph /\ j e. W ) /\ N e. ( ZZ>= ` ( M + 1 ) ) ) /\ k e. ( M ... ( N - 1 ) ) ) -> ( F ` k ) = A )
78 60 24 5 syl2an 
 |-  ( ( ( ( ph /\ j e. W ) /\ N e. ( ZZ>= ` ( M + 1 ) ) ) /\ k e. ( M ... ( N - 1 ) ) ) -> A e. CC )
79 77 72 78 fsumser 
 |-  ( ( ( ph /\ j e. W ) /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> sum_ k e. ( M ... ( N - 1 ) ) A = ( seq M ( + , F ) ` ( N - 1 ) ) )
80 66 seqeq1d 
 |-  ( ( ( ph /\ j e. W ) /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> seq N ( + , F ) = seq ( ( N - 1 ) + 1 ) ( + , F ) )
81 80 fveq1d 
 |-  ( ( ( ph /\ j e. W ) /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( seq N ( + , F ) ` j ) = ( seq ( ( N - 1 ) + 1 ) ( + , F ) ` j ) )
82 79 81 oveq12d 
 |-  ( ( ( ph /\ j e. W ) /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( sum_ k e. ( M ... ( N - 1 ) ) A + ( seq N ( + , F ) ` j ) ) = ( ( seq M ( + , F ) ` ( N - 1 ) ) + ( seq ( ( N - 1 ) + 1 ) ( + , F ) ` j ) ) )
83 76 82 eqtr4d 
 |-  ( ( ( ph /\ j e. W ) /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( seq M ( + , F ) ` j ) = ( sum_ k e. ( M ... ( N - 1 ) ) A + ( seq N ( + , F ) ` j ) ) )
84 83 ex 
 |-  ( ( ph /\ j e. W ) -> ( N e. ( ZZ>= ` ( M + 1 ) ) -> ( seq M ( + , F ) ` j ) = ( sum_ k e. ( M ... ( N - 1 ) ) A + ( seq N ( + , F ) ` j ) ) ) )
85 uzp1 
 |-  ( N e. ( ZZ>= ` M ) -> ( N = M \/ N e. ( ZZ>= ` ( M + 1 ) ) ) )
86 7 85 syl 
 |-  ( ph -> ( N = M \/ N e. ( ZZ>= ` ( M + 1 ) ) ) )
87 86 adantr 
 |-  ( ( ph /\ j e. W ) -> ( N = M \/ N e. ( ZZ>= ` ( M + 1 ) ) ) )
88 54 84 87 mpjaod 
 |-  ( ( ph /\ j e. W ) -> ( seq M ( + , F ) ` j ) = ( sum_ k e. ( M ... ( N - 1 ) ) A + ( seq N ( + , F ) ` j ) ) )
89 2 11 21 26 6 29 88 climaddc2 
 |-  ( ph -> seq M ( + , F ) ~~> ( sum_ k e. ( M ... ( N - 1 ) ) A + sum_ k e. W A ) )
90 1 9 4 5 89 isumclim 
 |-  ( ph -> sum_ k e. Z A = ( sum_ k e. ( M ... ( N - 1 ) ) A + sum_ k e. W A ) )