# 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 ) )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ z e. ( ZZ>= ` M ) ) /\ y e. ( M ... z ) ) -> ( ( F shift N ) ` y ) = ( F ` ( y + -u N ) ) )`
` |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ z e. ( ZZ>= ` M ) ) -> ( seq M ( .+ , ( F shift N ) ) ` z ) = ( seq ( M + -u N ) ( .+ , F ) ` ( z + -u N ) ) )`
` |-  ( ( N e. CC /\ z e. CC ) -> ( ( seq ( M - N ) ( .+ , F ) shift N ) ` z ) = ( seq ( M - N ) ( .+ , F ) ` ( z - N ) ) )`
` |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ z e. ( ZZ>= ` M ) ) -> ( ( seq ( M - N ) ( .+ , F ) shift N ) ` z ) = ( seq ( M - N ) ( .+ , F ) ` ( z - N ) ) )`
` |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ z e. ( ZZ>= ` M ) ) -> ( seq M ( .+ , ( F shift N ) ) ` z ) = ( ( seq ( M - N ) ( .+ , F ) shift N ) ` z ) )`
` |-  ( ( M e. ZZ /\ N e. ZZ ) -> seq M ( .+ , ( F shift N ) ) = ( seq ( M - N ) ( .+ , F ) shift N ) )`