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 | |
|
Assertion | seqshft | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | seqshft.1 | |
|
2 | seqfn | |
|
3 | 2 | adantr | |
4 | zsubcl | |
|
5 | seqfn | |
|
6 | 4 5 | syl | |
7 | zcn | |
|
8 | 7 | adantl | |
9 | seqex | |
|
10 | 9 | shftfn | |
11 | 6 8 10 | syl2anc | |
12 | simpr | |
|
13 | shftuz | |
|
14 | 12 4 13 | syl2anc | |
15 | zcn | |
|
16 | npcan | |
|
17 | 15 7 16 | syl2an | |
18 | 17 | fveq2d | |
19 | 14 18 | eqtrd | |
20 | 19 | fneq2d | |
21 | 11 20 | mpbid | |
22 | negsub | |
|
23 | 15 7 22 | syl2an | |
24 | 23 | adantr | |
25 | 24 | seqeq1d | |
26 | eluzelcn | |
|
27 | negsub | |
|
28 | 26 8 27 | syl2anr | |
29 | 25 28 | fveq12d | |
30 | simpr | |
|
31 | znegcl | |
|
32 | 31 | ad2antlr | |
33 | elfzelz | |
|
34 | 33 | zcnd | |
35 | 1 | shftval | |
36 | negsub | |
|
37 | 36 | ancoms | |
38 | 37 | fveq2d | |
39 | 35 38 | eqtr4d | |
40 | 7 34 39 | syl2an | |
41 | 40 | ad4ant24 | |
42 | 30 32 41 | seqshft2 | |
43 | 9 | shftval | |
44 | 8 26 43 | syl2an | |
45 | 29 42 44 | 3eqtr4d | |
46 | 3 21 45 | eqfnfvd | |