Metamath Proof Explorer

Theorem seqshft

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

Ref Expression
Hypothesis seqshft.1 
|- F e. _V
Assertion seqshft 
|- ( ( M e. ZZ /\ N e. ZZ ) -> seq M ( .+ , ( F shift N ) ) = ( seq ( M - N ) ( .+ , F ) shift N ) )

Proof

Step Hyp Ref Expression
1 seqshft.1 
 |-  F e. _V
2 seqfn 
 |-  ( M e. ZZ -> seq M ( .+ , ( F shift N ) ) Fn ( ZZ>= ` M ) )
3 2 adantr 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> seq M ( .+ , ( F shift N ) ) Fn ( ZZ>= ` M ) )
4 zsubcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M - N ) e. ZZ )
5 seqfn 
 |-  ( ( M - N ) e. ZZ -> seq ( M - N ) ( .+ , F ) Fn ( ZZ>= ` ( M - N ) ) )
6 4 5 syl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> seq ( M - N ) ( .+ , F ) Fn ( ZZ>= ` ( M - N ) ) )
7 zcn 
 |-  ( N e. ZZ -> N e. CC )
8 7 adantl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> N e. CC )
9 seqex 
 |-  seq ( M - N ) ( .+ , F ) e. _V
10 9 shftfn 
 |-  ( ( seq ( M - N ) ( .+ , F ) Fn ( ZZ>= ` ( M - N ) ) /\ N e. CC ) -> ( seq ( M - N ) ( .+ , F ) shift N ) Fn { x e. CC | ( x - N ) e. ( ZZ>= ` ( M - N ) ) } )
11 6 8 10 syl2anc 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( seq ( M - N ) ( .+ , F ) shift N ) Fn { x e. CC | ( x - N ) e. ( ZZ>= ` ( M - N ) ) } )
12 simpr 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> N e. ZZ )
13 shftuz 
 |-  ( ( N e. ZZ /\ ( M - N ) e. ZZ ) -> { x e. CC | ( x - N ) e. ( ZZ>= ` ( M - N ) ) } = ( ZZ>= ` ( ( M - N ) + N ) ) )
14 12 4 13 syl2anc 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> { x e. CC | ( x - N ) e. ( ZZ>= ` ( M - N ) ) } = ( ZZ>= ` ( ( M - N ) + N ) ) )
15 zcn 
 |-  ( M e. ZZ -> M e. CC )
16 npcan 
 |-  ( ( M e. CC /\ N e. CC ) -> ( ( M - N ) + N ) = M )
17 15 7 16 syl2an 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M - N ) + N ) = M )
18 17 fveq2d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ZZ>= ` ( ( M - N ) + N ) ) = ( ZZ>= ` M ) )
19 14 18 eqtrd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> { x e. CC | ( x - N ) e. ( ZZ>= ` ( M - N ) ) } = ( ZZ>= ` M ) )
20 19 fneq2d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( seq ( M - N ) ( .+ , F ) shift N ) Fn { x e. CC | ( x - N ) e. ( ZZ>= ` ( M - N ) ) } <-> ( seq ( M - N ) ( .+ , F ) shift N ) Fn ( ZZ>= ` M ) ) )
21 11 20 mpbid 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( seq ( M - N ) ( .+ , F ) shift N ) Fn ( ZZ>= ` M ) )
22 negsub 
 |-  ( ( M e. CC /\ N e. CC ) -> ( M + -u N ) = ( M - N ) )
23 15 7 22 syl2an 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M + -u N ) = ( M - N ) )
24 23 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ z e. ( ZZ>= ` M ) ) -> ( M + -u N ) = ( M - N ) )
25 24 seqeq1d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ z e. ( ZZ>= ` M ) ) -> seq ( M + -u N ) ( .+ , F ) = seq ( M - N ) ( .+ , F ) )
26 eluzelcn 
 |-  ( z e. ( ZZ>= ` M ) -> z e. CC )
27 negsub 
 |-  ( ( z e. CC /\ N e. CC ) -> ( z + -u N ) = ( z - N ) )
28 26 8 27 syl2anr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ z e. ( ZZ>= ` M ) ) -> ( z + -u N ) = ( z - N ) )
29 25 28 fveq12d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ z e. ( ZZ>= ` M ) ) -> ( seq ( M + -u N ) ( .+ , F ) ` ( z + -u N ) ) = ( seq ( M - N ) ( .+ , F ) ` ( z - N ) ) )
30 simpr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ z e. ( ZZ>= ` M ) ) -> z e. ( ZZ>= ` M ) )
31 znegcl 
 |-  ( N e. ZZ -> -u N e. ZZ )
32 31 ad2antlr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ z e. ( ZZ>= ` M ) ) -> -u N e. ZZ )
33 elfzelz 
 |-  ( y e. ( M ... z ) -> y e. ZZ )
34 33 zcnd 
 |-  ( y e. ( M ... z ) -> y e. CC )
35 1 shftval 
 |-  ( ( N e. CC /\ y e. CC ) -> ( ( F shift N ) ` y ) = ( F ` ( y - N ) ) )
36 negsub 
 |-  ( ( y e. CC /\ N e. CC ) -> ( y + -u N ) = ( y - N ) )
37 36 ancoms 
 |-  ( ( N e. CC /\ y e. CC ) -> ( y + -u N ) = ( y - N ) )
38 37 fveq2d 
 |-  ( ( N e. CC /\ y e. CC ) -> ( F ` ( y + -u N ) ) = ( F ` ( y - N ) ) )
39 35 38 eqtr4d 
 |-  ( ( N e. CC /\ y e. CC ) -> ( ( F shift N ) ` y ) = ( F ` ( y + -u N ) ) )
40 7 34 39 syl2an 
 |-  ( ( N e. ZZ /\ y e. ( M ... z ) ) -> ( ( F shift N ) ` y ) = ( F ` ( y + -u N ) ) )
41 40 ad4ant24 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ z e. ( ZZ>= ` M ) ) /\ y e. ( M ... z ) ) -> ( ( F shift N ) ` y ) = ( F ` ( y + -u N ) ) )
42 30 32 41 seqshft2 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ z e. ( ZZ>= ` M ) ) -> ( seq M ( .+ , ( F shift N ) ) ` z ) = ( seq ( M + -u N ) ( .+ , F ) ` ( z + -u N ) ) )
43 9 shftval 
 |-  ( ( N e. CC /\ z e. CC ) -> ( ( seq ( M - N ) ( .+ , F ) shift N ) ` z ) = ( seq ( M - N ) ( .+ , F ) ` ( z - N ) ) )
44 8 26 43 syl2an 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ z e. ( ZZ>= ` M ) ) -> ( ( seq ( M - N ) ( .+ , F ) shift N ) ` z ) = ( seq ( M - N ) ( .+ , F ) ` ( z - N ) ) )
45 29 42 44 3eqtr4d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ z e. ( ZZ>= ` M ) ) -> ( seq M ( .+ , ( F shift N ) ) ` z ) = ( ( seq ( M - N ) ( .+ , F ) shift N ) ` z ) )
46 3 21 45 eqfnfvd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> seq M ( .+ , ( F shift N ) ) = ( seq ( M - N ) ( .+ , F ) shift N ) )