Metamath Proof Explorer

Theorem isumshft

Description: Index shift of an infinite sum. (Contributed by Paul Chapman, 31-Oct-2007) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses isumshft.1 
|- Z = ( ZZ>= ` M )
isumshft.2 
|- W = ( ZZ>= ` ( M + K ) )
isumshft.3 
|- ( j = ( K + k ) -> A = B )
isumshft.4 
|- ( ph -> K e. ZZ )
isumshft.5 
|- ( ph -> M e. ZZ )
isumshft.6 
|- ( ( ph /\ j e. W ) -> A e. CC )
Assertion isumshft 
|- ( ph -> sum_ j e. W A = sum_ k e. Z B )

Proof

Step Hyp Ref Expression
1 isumshft.1 
 |-  Z = ( ZZ>= ` M )
2 isumshft.2 
 |-  W = ( ZZ>= ` ( M + K ) )
3 isumshft.3 
 |-  ( j = ( K + k ) -> A = B )
4 isumshft.4 
 |-  ( ph -> K e. ZZ )
5 isumshft.5 
 |-  ( ph -> M e. ZZ )
6 isumshft.6 
 |-  ( ( ph /\ j e. W ) -> A e. CC )
7 5 4 zaddcld 
 |-  ( ph -> ( M + K ) e. ZZ )
8 2 eleq2i 
 |-  ( m e. W <-> m e. ( ZZ>= ` ( M + K ) ) )
9 4 zcnd 
 |-  ( ph -> K e. CC )
10 eluzelcn 
 |-  ( m e. ( ZZ>= ` ( M + K ) ) -> m e. CC )
11 10 2 eleq2s 
 |-  ( m e. W -> m e. CC )
12 1 fvexi 
 |-  Z e. _V
13 12 mptex 
 |-  ( k e. Z |-> B ) e. _V
14 13 shftval 
 |-  ( ( K e. CC /\ m e. CC ) -> ( ( ( k e. Z |-> B ) shift K ) ` m ) = ( ( k e. Z |-> B ) ` ( m - K ) ) )
15 9 11 14 syl2an 
 |-  ( ( ph /\ m e. W ) -> ( ( ( k e. Z |-> B ) shift K ) ` m ) = ( ( k e. Z |-> B ) ` ( m - K ) ) )
16 simpr 
 |-  ( ( ph /\ k e. Z ) -> k e. Z )
17 eqid 
 |-  ( k e. Z |-> B ) = ( k e. Z |-> B )
18 17 fvmpt2i 
 |-  ( k e. Z -> ( ( k e. Z |-> B ) ` k ) = ( _I ` B ) )
19 16 18 syl 
 |-  ( ( ph /\ k e. Z ) -> ( ( k e. Z |-> B ) ` k ) = ( _I ` B ) )
20 eluzelcn 
 |-  ( k e. ( ZZ>= ` M ) -> k e. CC )
21 20 1 eleq2s 
 |-  ( k e. Z -> k e. CC )
22 addcom 
 |-  ( ( K e. CC /\ k e. CC ) -> ( K + k ) = ( k + K ) )
23 9 21 22 syl2an 
 |-  ( ( ph /\ k e. Z ) -> ( K + k ) = ( k + K ) )
24 id 
 |-  ( k e. Z -> k e. Z )
25 24 1 eleqtrdi 
 |-  ( k e. Z -> k e. ( ZZ>= ` M ) )
26 eluzadd 
 |-  ( ( k e. ( ZZ>= ` M ) /\ K e. ZZ ) -> ( k + K ) e. ( ZZ>= ` ( M + K ) ) )
27 25 4 26 syl2anr 
 |-  ( ( ph /\ k e. Z ) -> ( k + K ) e. ( ZZ>= ` ( M + K ) ) )
28 23 27 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( K + k ) e. ( ZZ>= ` ( M + K ) ) )
29 28 2 eleqtrrdi 
 |-  ( ( ph /\ k e. Z ) -> ( K + k ) e. W )
30 eqid 
 |-  ( j e. W |-> A ) = ( j e. W |-> A )
31 3 30 fvmpti 
 |-  ( ( K + k ) e. W -> ( ( j e. W |-> A ) ` ( K + k ) ) = ( _I ` B ) )
32 29 31 syl 
 |-  ( ( ph /\ k e. Z ) -> ( ( j e. W |-> A ) ` ( K + k ) ) = ( _I ` B ) )
33 19 32 eqtr4d 
 |-  ( ( ph /\ k e. Z ) -> ( ( k e. Z |-> B ) ` k ) = ( ( j e. W |-> A ) ` ( K + k ) ) )
34 33 ralrimiva 
 |-  ( ph -> A. k e. Z ( ( k e. Z |-> B ) ` k ) = ( ( j e. W |-> A ) ` ( K + k ) ) )
35 nffvmpt1 
 |-  F/_ k ( ( k e. Z |-> B ) ` n )
36 35 nfeq1 
 |-  F/ k ( ( k e. Z |-> B ) ` n ) = ( ( j e. W |-> A ) ` ( K + n ) )
37 fveq2 
 |-  ( k = n -> ( ( k e. Z |-> B ) ` k ) = ( ( k e. Z |-> B ) ` n ) )
38 oveq2 
 |-  ( k = n -> ( K + k ) = ( K + n ) )
39 38 fveq2d 
 |-  ( k = n -> ( ( j e. W |-> A ) ` ( K + k ) ) = ( ( j e. W |-> A ) ` ( K + n ) ) )
40 37 39 eqeq12d 
 |-  ( k = n -> ( ( ( k e. Z |-> B ) ` k ) = ( ( j e. W |-> A ) ` ( K + k ) ) <-> ( ( k e. Z |-> B ) ` n ) = ( ( j e. W |-> A ) ` ( K + n ) ) ) )
41 36 40 rspc 
 |-  ( n e. Z -> ( A. k e. Z ( ( k e. Z |-> B ) ` k ) = ( ( j e. W |-> A ) ` ( K + k ) ) -> ( ( k e. Z |-> B ) ` n ) = ( ( j e. W |-> A ) ` ( K + n ) ) ) )
42 34 41 mpan9 
 |-  ( ( ph /\ n e. Z ) -> ( ( k e. Z |-> B ) ` n ) = ( ( j e. W |-> A ) ` ( K + n ) ) )
43 42 ralrimiva 
 |-  ( ph -> A. n e. Z ( ( k e. Z |-> B ) ` n ) = ( ( j e. W |-> A ) ` ( K + n ) ) )
44 5 adantr 
 |-  ( ( ph /\ m e. W ) -> M e. ZZ )
45 4 adantr 
 |-  ( ( ph /\ m e. W ) -> K e. ZZ )
46 simpr 
 |-  ( ( ph /\ m e. W ) -> m e. W )
47 46 2 eleqtrdi 
 |-  ( ( ph /\ m e. W ) -> m e. ( ZZ>= ` ( M + K ) ) )
48 eluzsub 
 |-  ( ( M e. ZZ /\ K e. ZZ /\ m e. ( ZZ>= ` ( M + K ) ) ) -> ( m - K ) e. ( ZZ>= ` M ) )
49 44 45 47 48 syl3anc 
 |-  ( ( ph /\ m e. W ) -> ( m - K ) e. ( ZZ>= ` M ) )
50 49 1 eleqtrrdi 
 |-  ( ( ph /\ m e. W ) -> ( m - K ) e. Z )
51 fveq2 
 |-  ( n = ( m - K ) -> ( ( k e. Z |-> B ) ` n ) = ( ( k e. Z |-> B ) ` ( m - K ) ) )
52 oveq2 
 |-  ( n = ( m - K ) -> ( K + n ) = ( K + ( m - K ) ) )
53 52 fveq2d 
 |-  ( n = ( m - K ) -> ( ( j e. W |-> A ) ` ( K + n ) ) = ( ( j e. W |-> A ) ` ( K + ( m - K ) ) ) )
54 51 53 eqeq12d 
 |-  ( n = ( m - K ) -> ( ( ( k e. Z |-> B ) ` n ) = ( ( j e. W |-> A ) ` ( K + n ) ) <-> ( ( k e. Z |-> B ) ` ( m - K ) ) = ( ( j e. W |-> A ) ` ( K + ( m - K ) ) ) ) )
55 54 rspccva 
 |-  ( ( A. n e. Z ( ( k e. Z |-> B ) ` n ) = ( ( j e. W |-> A ) ` ( K + n ) ) /\ ( m - K ) e. Z ) -> ( ( k e. Z |-> B ) ` ( m - K ) ) = ( ( j e. W |-> A ) ` ( K + ( m - K ) ) ) )
56 43 50 55 syl2an2r 
 |-  ( ( ph /\ m e. W ) -> ( ( k e. Z |-> B ) ` ( m - K ) ) = ( ( j e. W |-> A ) ` ( K + ( m - K ) ) ) )
57 pncan3 
 |-  ( ( K e. CC /\ m e. CC ) -> ( K + ( m - K ) ) = m )
58 9 11 57 syl2an 
 |-  ( ( ph /\ m e. W ) -> ( K + ( m - K ) ) = m )
59 58 fveq2d 
 |-  ( ( ph /\ m e. W ) -> ( ( j e. W |-> A ) ` ( K + ( m - K ) ) ) = ( ( j e. W |-> A ) ` m ) )
60 15 56 59 3eqtrrd 
 |-  ( ( ph /\ m e. W ) -> ( ( j e. W |-> A ) ` m ) = ( ( ( k e. Z |-> B ) shift K ) ` m ) )
61 8 60 sylan2br 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( M + K ) ) ) -> ( ( j e. W |-> A ) ` m ) = ( ( ( k e. Z |-> B ) shift K ) ` m ) )
62 7 61 seqfeq 
 |-  ( ph -> seq ( M + K ) ( + , ( j e. W |-> A ) ) = seq ( M + K ) ( + , ( ( k e. Z |-> B ) shift K ) ) )
63 62 breq1d 
 |-  ( ph -> ( seq ( M + K ) ( + , ( j e. W |-> A ) ) ~~> x <-> seq ( M + K ) ( + , ( ( k e. Z |-> B ) shift K ) ) ~~> x ) )
64 13 isershft 
 |-  ( ( M e. ZZ /\ K e. ZZ ) -> ( seq M ( + , ( k e. Z |-> B ) ) ~~> x <-> seq ( M + K ) ( + , ( ( k e. Z |-> B ) shift K ) ) ~~> x ) )
65 5 4 64 syl2anc 
 |-  ( ph -> ( seq M ( + , ( k e. Z |-> B ) ) ~~> x <-> seq ( M + K ) ( + , ( ( k e. Z |-> B ) shift K ) ) ~~> x ) )
66 63 65 bitr4d 
 |-  ( ph -> ( seq ( M + K ) ( + , ( j e. W |-> A ) ) ~~> x <-> seq M ( + , ( k e. Z |-> B ) ) ~~> x ) )
67 66 iotabidv 
 |-  ( ph -> ( iota x seq ( M + K ) ( + , ( j e. W |-> A ) ) ~~> x ) = ( iota x seq M ( + , ( k e. Z |-> B ) ) ~~> x ) )
68 df-fv 
 |-  ( ~~> ` seq ( M + K ) ( + , ( j e. W |-> A ) ) ) = ( iota x seq ( M + K ) ( + , ( j e. W |-> A ) ) ~~> x )
69 df-fv 
 |-  ( ~~> ` seq M ( + , ( k e. Z |-> B ) ) ) = ( iota x seq M ( + , ( k e. Z |-> B ) ) ~~> x )
70 67 68 69 3eqtr4g 
 |-  ( ph -> ( ~~> ` seq ( M + K ) ( + , ( j e. W |-> A ) ) ) = ( ~~> ` seq M ( + , ( k e. Z |-> B ) ) ) )
71 eqidd 
 |-  ( ( ph /\ m e. W ) -> ( ( j e. W |-> A ) ` m ) = ( ( j e. W |-> A ) ` m ) )
72 6 fmpttd 
 |-  ( ph -> ( j e. W |-> A ) : W --> CC )
73 72 ffvelrnda 
 |-  ( ( ph /\ m e. W ) -> ( ( j e. W |-> A ) ` m ) e. CC )
74 2 7 71 73 isum 
 |-  ( ph -> sum_ m e. W ( ( j e. W |-> A ) ` m ) = ( ~~> ` seq ( M + K ) ( + , ( j e. W |-> A ) ) ) )
75 eqidd 
 |-  ( ( ph /\ n e. Z ) -> ( ( k e. Z |-> B ) ` n ) = ( ( k e. Z |-> B ) ` n ) )
76 29 ralrimiva 
 |-  ( ph -> A. k e. Z ( K + k ) e. W )
77 38 eleq1d 
 |-  ( k = n -> ( ( K + k ) e. W <-> ( K + n ) e. W ) )
78 77 rspccva 
 |-  ( ( A. k e. Z ( K + k ) e. W /\ n e. Z ) -> ( K + n ) e. W )
79 76 78 sylan 
 |-  ( ( ph /\ n e. Z ) -> ( K + n ) e. W )
80 ffvelrn 
 |-  ( ( ( j e. W |-> A ) : W --> CC /\ ( K + n ) e. W ) -> ( ( j e. W |-> A ) ` ( K + n ) ) e. CC )
81 72 79 80 syl2an2r 
 |-  ( ( ph /\ n e. Z ) -> ( ( j e. W |-> A ) ` ( K + n ) ) e. CC )
82 42 81 eqeltrd 
 |-  ( ( ph /\ n e. Z ) -> ( ( k e. Z |-> B ) ` n ) e. CC )
83 1 5 75 82 isum 
 |-  ( ph -> sum_ n e. Z ( ( k e. Z |-> B ) ` n ) = ( ~~> ` seq M ( + , ( k e. Z |-> B ) ) ) )
84 70 74 83 3eqtr4d 
 |-  ( ph -> sum_ m e. W ( ( j e. W |-> A ) ` m ) = sum_ n e. Z ( ( k e. Z |-> B ) ` n ) )
85 sumfc 
 |-  sum_ m e. W ( ( j e. W |-> A ) ` m ) = sum_ j e. W A
86 sumfc 
 |-  sum_ n e. Z ( ( k e. Z |-> B ) ` n ) = sum_ k e. Z B
87 84 85 86 3eqtr3g 
 |-  ( ph -> sum_ j e. W A = sum_ k e. Z B )