Metamath Proof Explorer

Theorem seqshft2

Description: Shifting the index set of a sequence. (Contributed by Mario Carneiro, 27-Feb-2014) (Revised by Mario Carneiro, 27-May-2014)

Ref Expression
Hypotheses seqshft2.1 
|- ( ph -> N e. ( ZZ>= ` M ) )
seqshft2.2 
|- ( ph -> K e. ZZ )
seqshft2.3 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) = ( G ` ( k + K ) ) )
Assertion seqshft2 
|- ( ph -> ( seq M ( .+ , F ) ` N ) = ( seq ( M + K ) ( .+ , G ) ` ( N + K ) ) )

Proof

Step Hyp Ref Expression
1 seqshft2.1 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 seqshft2.2 
 |-  ( ph -> K e. ZZ )
3 seqshft2.3 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) = ( G ` ( k + K ) ) )
4 eluzfz2 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
5 1 4 syl 
 |-  ( ph -> N e. ( M ... N ) )
6 eleq1 
 |-  ( x = M -> ( x e. ( M ... N ) <-> M e. ( M ... N ) ) )
7 fveq2 
 |-  ( x = M -> ( seq M ( .+ , F ) ` x ) = ( seq M ( .+ , F ) ` M ) )
8 fvoveq1 
 |-  ( x = M -> ( seq ( M + K ) ( .+ , G ) ` ( x + K ) ) = ( seq ( M + K ) ( .+ , G ) ` ( M + K ) ) )
9 7 8 eqeq12d 
 |-  ( x = M -> ( ( seq M ( .+ , F ) ` x ) = ( seq ( M + K ) ( .+ , G ) ` ( x + K ) ) <-> ( seq M ( .+ , F ) ` M ) = ( seq ( M + K ) ( .+ , G ) ` ( M + K ) ) ) )
10 6 9 imbi12d 
 |-  ( x = M -> ( ( x e. ( M ... N ) -> ( seq M ( .+ , F ) ` x ) = ( seq ( M + K ) ( .+ , G ) ` ( x + K ) ) ) <-> ( M e. ( M ... N ) -> ( seq M ( .+ , F ) ` M ) = ( seq ( M + K ) ( .+ , G ) ` ( M + K ) ) ) ) )
11 10 imbi2d 
 |-  ( x = M -> ( ( ph -> ( x e. ( M ... N ) -> ( seq M ( .+ , F ) ` x ) = ( seq ( M + K ) ( .+ , G ) ` ( x + K ) ) ) ) <-> ( ph -> ( M e. ( M ... N ) -> ( seq M ( .+ , F ) ` M ) = ( seq ( M + K ) ( .+ , G ) ` ( M + K ) ) ) ) ) )
12 eleq1 
 |-  ( x = n -> ( x e. ( M ... N ) <-> n e. ( M ... N ) ) )
13 fveq2 
 |-  ( x = n -> ( seq M ( .+ , F ) ` x ) = ( seq M ( .+ , F ) ` n ) )
14 fvoveq1 
 |-  ( x = n -> ( seq ( M + K ) ( .+ , G ) ` ( x + K ) ) = ( seq ( M + K ) ( .+ , G ) ` ( n + K ) ) )
15 13 14 eqeq12d 
 |-  ( x = n -> ( ( seq M ( .+ , F ) ` x ) = ( seq ( M + K ) ( .+ , G ) ` ( x + K ) ) <-> ( seq M ( .+ , F ) ` n ) = ( seq ( M + K ) ( .+ , G ) ` ( n + K ) ) ) )
16 12 15 imbi12d 
 |-  ( x = n -> ( ( x e. ( M ... N ) -> ( seq M ( .+ , F ) ` x ) = ( seq ( M + K ) ( .+ , G ) ` ( x + K ) ) ) <-> ( n e. ( M ... N ) -> ( seq M ( .+ , F ) ` n ) = ( seq ( M + K ) ( .+ , G ) ` ( n + K ) ) ) ) )
17 16 imbi2d 
 |-  ( x = n -> ( ( ph -> ( x e. ( M ... N ) -> ( seq M ( .+ , F ) ` x ) = ( seq ( M + K ) ( .+ , G ) ` ( x + K ) ) ) ) <-> ( ph -> ( n e. ( M ... N ) -> ( seq M ( .+ , F ) ` n ) = ( seq ( M + K ) ( .+ , G ) ` ( n + K ) ) ) ) ) )
18 eleq1 
 |-  ( x = ( n + 1 ) -> ( x e. ( M ... N ) <-> ( n + 1 ) e. ( M ... N ) ) )
19 fveq2 
 |-  ( x = ( n + 1 ) -> ( seq M ( .+ , F ) ` x ) = ( seq M ( .+ , F ) ` ( n + 1 ) ) )
20 fvoveq1 
 |-  ( x = ( n + 1 ) -> ( seq ( M + K ) ( .+ , G ) ` ( x + K ) ) = ( seq ( M + K ) ( .+ , G ) ` ( ( n + 1 ) + K ) ) )
21 19 20 eqeq12d 
 |-  ( x = ( n + 1 ) -> ( ( seq M ( .+ , F ) ` x ) = ( seq ( M + K ) ( .+ , G ) ` ( x + K ) ) <-> ( seq M ( .+ , F ) ` ( n + 1 ) ) = ( seq ( M + K ) ( .+ , G ) ` ( ( n + 1 ) + K ) ) ) )
22 18 21 imbi12d 
 |-  ( x = ( n + 1 ) -> ( ( x e. ( M ... N ) -> ( seq M ( .+ , F ) ` x ) = ( seq ( M + K ) ( .+ , G ) ` ( x + K ) ) ) <-> ( ( n + 1 ) e. ( M ... N ) -> ( seq M ( .+ , F ) ` ( n + 1 ) ) = ( seq ( M + K ) ( .+ , G ) ` ( ( n + 1 ) + K ) ) ) ) )
23 22 imbi2d 
 |-  ( x = ( n + 1 ) -> ( ( ph -> ( x e. ( M ... N ) -> ( seq M ( .+ , F ) ` x ) = ( seq ( M + K ) ( .+ , G ) ` ( x + K ) ) ) ) <-> ( ph -> ( ( n + 1 ) e. ( M ... N ) -> ( seq M ( .+ , F ) ` ( n + 1 ) ) = ( seq ( M + K ) ( .+ , G ) ` ( ( n + 1 ) + K ) ) ) ) ) )
24 eleq1 
 |-  ( x = N -> ( x e. ( M ... N ) <-> N e. ( M ... N ) ) )
25 fveq2 
 |-  ( x = N -> ( seq M ( .+ , F ) ` x ) = ( seq M ( .+ , F ) ` N ) )
26 fvoveq1 
 |-  ( x = N -> ( seq ( M + K ) ( .+ , G ) ` ( x + K ) ) = ( seq ( M + K ) ( .+ , G ) ` ( N + K ) ) )
27 25 26 eqeq12d 
 |-  ( x = N -> ( ( seq M ( .+ , F ) ` x ) = ( seq ( M + K ) ( .+ , G ) ` ( x + K ) ) <-> ( seq M ( .+ , F ) ` N ) = ( seq ( M + K ) ( .+ , G ) ` ( N + K ) ) ) )
28 24 27 imbi12d 
 |-  ( x = N -> ( ( x e. ( M ... N ) -> ( seq M ( .+ , F ) ` x ) = ( seq ( M + K ) ( .+ , G ) ` ( x + K ) ) ) <-> ( N e. ( M ... N ) -> ( seq M ( .+ , F ) ` N ) = ( seq ( M + K ) ( .+ , G ) ` ( N + K ) ) ) ) )
29 28 imbi2d 
 |-  ( x = N -> ( ( ph -> ( x e. ( M ... N ) -> ( seq M ( .+ , F ) ` x ) = ( seq ( M + K ) ( .+ , G ) ` ( x + K ) ) ) ) <-> ( ph -> ( N e. ( M ... N ) -> ( seq M ( .+ , F ) ` N ) = ( seq ( M + K ) ( .+ , G ) ` ( N + K ) ) ) ) ) )
30 fveq2 
 |-  ( k = M -> ( F ` k ) = ( F ` M ) )
31 fvoveq1 
 |-  ( k = M -> ( G ` ( k + K ) ) = ( G ` ( M + K ) ) )
32 30 31 eqeq12d 
 |-  ( k = M -> ( ( F ` k ) = ( G ` ( k + K ) ) <-> ( F ` M ) = ( G ` ( M + K ) ) ) )
33 3 ralrimiva 
 |-  ( ph -> A. k e. ( M ... N ) ( F ` k ) = ( G ` ( k + K ) ) )
34 eluzfz1 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
35 1 34 syl 
 |-  ( ph -> M e. ( M ... N ) )
36 32 33 35 rspcdva 
 |-  ( ph -> ( F ` M ) = ( G ` ( M + K ) ) )
37 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
38 1 37 syl 
 |-  ( ph -> M e. ZZ )
39 seq1 
 |-  ( M e. ZZ -> ( seq M ( .+ , F ) ` M ) = ( F ` M ) )
40 38 39 syl 
 |-  ( ph -> ( seq M ( .+ , F ) ` M ) = ( F ` M ) )
41 38 2 zaddcld 
 |-  ( ph -> ( M + K ) e. ZZ )
42 seq1 
 |-  ( ( M + K ) e. ZZ -> ( seq ( M + K ) ( .+ , G ) ` ( M + K ) ) = ( G ` ( M + K ) ) )
43 41 42 syl 
 |-  ( ph -> ( seq ( M + K ) ( .+ , G ) ` ( M + K ) ) = ( G ` ( M + K ) ) )
44 36 40 43 3eqtr4d 
 |-  ( ph -> ( seq M ( .+ , F ) ` M ) = ( seq ( M + K ) ( .+ , G ) ` ( M + K ) ) )
45 44 a1i13 
 |-  ( M e. ZZ -> ( ph -> ( M e. ( M ... N ) -> ( seq M ( .+ , F ) ` M ) = ( seq ( M + K ) ( .+ , G ) ` ( M + K ) ) ) ) )
46 peano2fzr 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) -> n e. ( M ... N ) )
47 46 adantl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> n e. ( M ... N ) )
48 47 expr 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( ( n + 1 ) e. ( M ... N ) -> n e. ( M ... N ) ) )
49 48 imim1d 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( ( n e. ( M ... N ) -> ( seq M ( .+ , F ) ` n ) = ( seq ( M + K ) ( .+ , G ) ` ( n + K ) ) ) -> ( ( n + 1 ) e. ( M ... N ) -> ( seq M ( .+ , F ) ` n ) = ( seq ( M + K ) ( .+ , G ) ` ( n + K ) ) ) ) )
50 oveq1 
 |-  ( ( seq M ( .+ , F ) ` n ) = ( seq ( M + K ) ( .+ , G ) ` ( n + K ) ) -> ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) = ( ( seq ( M + K ) ( .+ , G ) ` ( n + K ) ) .+ ( F ` ( n + 1 ) ) ) )
51 simprl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> n e. ( ZZ>= ` M ) )
52 seqp1 
 |-  ( n e. ( ZZ>= ` M ) -> ( seq M ( .+ , F ) ` ( n + 1 ) ) = ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) )
53 51 52 syl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( seq M ( .+ , F ) ` ( n + 1 ) ) = ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) )
54 2 adantr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> K e. ZZ )
55 eluzadd 
 |-  ( ( n e. ( ZZ>= ` M ) /\ K e. ZZ ) -> ( n + K ) e. ( ZZ>= ` ( M + K ) ) )
56 51 54 55 syl2anc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( n + K ) e. ( ZZ>= ` ( M + K ) ) )
57 seqp1 
 |-  ( ( n + K ) e. ( ZZ>= ` ( M + K ) ) -> ( seq ( M + K ) ( .+ , G ) ` ( ( n + K ) + 1 ) ) = ( ( seq ( M + K ) ( .+ , G ) ` ( n + K ) ) .+ ( G ` ( ( n + K ) + 1 ) ) ) )
58 56 57 syl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( seq ( M + K ) ( .+ , G ) ` ( ( n + K ) + 1 ) ) = ( ( seq ( M + K ) ( .+ , G ) ` ( n + K ) ) .+ ( G ` ( ( n + K ) + 1 ) ) ) )
59 eluzelz 
 |-  ( n e. ( ZZ>= ` M ) -> n e. ZZ )
60 51 59 syl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> n e. ZZ )
61 zcn 
 |-  ( n e. ZZ -> n e. CC )
62 zcn 
 |-  ( K e. ZZ -> K e. CC )
63 ax-1cn 
 |-  1 e. CC
64 add32 
 |-  ( ( n e. CC /\ 1 e. CC /\ K e. CC ) -> ( ( n + 1 ) + K ) = ( ( n + K ) + 1 ) )
65 63 64 mp3an2 
 |-  ( ( n e. CC /\ K e. CC ) -> ( ( n + 1 ) + K ) = ( ( n + K ) + 1 ) )
66 61 62 65 syl2an 
 |-  ( ( n e. ZZ /\ K e. ZZ ) -> ( ( n + 1 ) + K ) = ( ( n + K ) + 1 ) )
67 60 54 66 syl2anc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( ( n + 1 ) + K ) = ( ( n + K ) + 1 ) )
68 67 fveq2d 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( seq ( M + K ) ( .+ , G ) ` ( ( n + 1 ) + K ) ) = ( seq ( M + K ) ( .+ , G ) ` ( ( n + K ) + 1 ) ) )
69 fveq2 
 |-  ( k = ( n + 1 ) -> ( F ` k ) = ( F ` ( n + 1 ) ) )
70 fvoveq1 
 |-  ( k = ( n + 1 ) -> ( G ` ( k + K ) ) = ( G ` ( ( n + 1 ) + K ) ) )
71 69 70 eqeq12d 
 |-  ( k = ( n + 1 ) -> ( ( F ` k ) = ( G ` ( k + K ) ) <-> ( F ` ( n + 1 ) ) = ( G ` ( ( n + 1 ) + K ) ) ) )
72 33 adantr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> A. k e. ( M ... N ) ( F ` k ) = ( G ` ( k + K ) ) )
73 simprr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( n + 1 ) e. ( M ... N ) )
74 71 72 73 rspcdva 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( F ` ( n + 1 ) ) = ( G ` ( ( n + 1 ) + K ) ) )
75 67 fveq2d 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( G ` ( ( n + 1 ) + K ) ) = ( G ` ( ( n + K ) + 1 ) ) )
76 74 75 eqtrd 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( F ` ( n + 1 ) ) = ( G ` ( ( n + K ) + 1 ) ) )
77 76 oveq2d 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( ( seq ( M + K ) ( .+ , G ) ` ( n + K ) ) .+ ( F ` ( n + 1 ) ) ) = ( ( seq ( M + K ) ( .+ , G ) ` ( n + K ) ) .+ ( G ` ( ( n + K ) + 1 ) ) ) )
78 58 68 77 3eqtr4d 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( seq ( M + K ) ( .+ , G ) ` ( ( n + 1 ) + K ) ) = ( ( seq ( M + K ) ( .+ , G ) ` ( n + K ) ) .+ ( F ` ( n + 1 ) ) ) )
79 53 78 eqeq12d 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( ( seq M ( .+ , F ) ` ( n + 1 ) ) = ( seq ( M + K ) ( .+ , G ) ` ( ( n + 1 ) + K ) ) <-> ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) = ( ( seq ( M + K ) ( .+ , G ) ` ( n + K ) ) .+ ( F ` ( n + 1 ) ) ) ) )
80 50 79 syl5ibr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( ( seq M ( .+ , F ) ` n ) = ( seq ( M + K ) ( .+ , G ) ` ( n + K ) ) -> ( seq M ( .+ , F ) ` ( n + 1 ) ) = ( seq ( M + K ) ( .+ , G ) ` ( ( n + 1 ) + K ) ) ) )
81 49 80 animpimp2impd 
 |-  ( n e. ( ZZ>= ` M ) -> ( ( ph -> ( n e. ( M ... N ) -> ( seq M ( .+ , F ) ` n ) = ( seq ( M + K ) ( .+ , G ) ` ( n + K ) ) ) ) -> ( ph -> ( ( n + 1 ) e. ( M ... N ) -> ( seq M ( .+ , F ) ` ( n + 1 ) ) = ( seq ( M + K ) ( .+ , G ) ` ( ( n + 1 ) + K ) ) ) ) ) )
82 11 17 23 29 45 81 uzind4 
 |-  ( N e. ( ZZ>= ` M ) -> ( ph -> ( N e. ( M ... N ) -> ( seq M ( .+ , F ) ` N ) = ( seq ( M + K ) ( .+ , G ) ` ( N + K ) ) ) ) )
83 1 82 mpcom 
 |-  ( ph -> ( N e. ( M ... N ) -> ( seq M ( .+ , F ) ` N ) = ( seq ( M + K ) ( .+ , G ) ` ( N + K ) ) ) )
84 5 83 mpd 
 |-  ( ph -> ( seq M ( .+ , F ) ` N ) = ( seq ( M + K ) ( .+ , G ) ` ( N + K ) ) )