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 FV
Assertion seqshft MNseqM+˙FshiftN=seqMN+˙FshiftN

Proof

Step Hyp Ref Expression
1 seqshft.1 FV
2 seqfn MseqM+˙FshiftNFnM
3 2 adantr MNseqM+˙FshiftNFnM
4 zsubcl MNMN
5 seqfn MNseqMN+˙FFnMN
6 4 5 syl MNseqMN+˙FFnMN
7 zcn NN
8 7 adantl MNN
9 seqex seqMN+˙FV
10 9 shftfn seqMN+˙FFnMNNseqMN+˙FshiftNFnx|xNMN
11 6 8 10 syl2anc MNseqMN+˙FshiftNFnx|xNMN
12 simpr MNN
13 shftuz NMNx|xNMN=M-N+N
14 12 4 13 syl2anc MNx|xNMN=M-N+N
15 zcn MM
16 npcan MNM-N+N=M
17 15 7 16 syl2an MNM-N+N=M
18 17 fveq2d MNM-N+N=M
19 14 18 eqtrd MNx|xNMN=M
20 19 fneq2d MNseqMN+˙FshiftNFnx|xNMNseqMN+˙FshiftNFnM
21 11 20 mpbid MNseqMN+˙FshiftNFnM
22 negsub MNM+- N=MN
23 15 7 22 syl2an MNM+- N=MN
24 23 adantr MNzMM+- N=MN
25 24 seqeq1d MNzMseqM+- N+˙F=seqMN+˙F
26 eluzelcn zMz
27 negsub zNz+- N=zN
28 26 8 27 syl2anr MNzMz+- N=zN
29 25 28 fveq12d MNzMseqM+- N+˙Fz+- N=seqMN+˙FzN
30 simpr MNzMzM
31 znegcl NN
32 31 ad2antlr MNzMN
33 elfzelz yMzy
34 33 zcnd yMzy
35 1 shftval NyFshiftNy=FyN
36 negsub yNy+- N=yN
37 36 ancoms Nyy+- N=yN
38 37 fveq2d NyFy+- N=FyN
39 35 38 eqtr4d NyFshiftNy=Fy+- N
40 7 34 39 syl2an NyMzFshiftNy=Fy+- N
41 40 ad4ant24 MNzMyMzFshiftNy=Fy+- N
42 30 32 41 seqshft2 MNzMseqM+˙FshiftNz=seqM+- N+˙Fz+- N
43 9 shftval NzseqMN+˙FshiftNz=seqMN+˙FzN
44 8 26 43 syl2an MNzMseqMN+˙FshiftNz=seqMN+˙FzN
45 29 42 44 3eqtr4d MNzMseqM+˙FshiftNz=seqMN+˙FshiftNz
46 3 21 45 eqfnfvd MNseqM+˙FshiftN=seqMN+˙FshiftN