# 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}\in \mathrm{V}$
Assertion seqshft

### Proof

Step Hyp Ref Expression
1 seqshft.1 ${⊢}{F}\in \mathrm{V}$
2 seqfn
4 zsubcl ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {M}-{N}\in ℤ$
5 seqfn
6 4 5 syl
7 zcn ${⊢}{N}\in ℤ\to {N}\in ℂ$
8 7 adantl ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {N}\in ℂ$
9 seqex
10 9 shftfn
11 6 8 10 syl2anc
12 simpr ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {N}\in ℤ$
13 shftuz ${⊢}\left({N}\in ℤ\wedge {M}-{N}\in ℤ\right)\to \left\{{x}\in ℂ|{x}-{N}\in {ℤ}_{\ge \left({M}-{N}\right)}\right\}={ℤ}_{\ge \left({M}-{N}+{N}\right)}$
14 12 4 13 syl2anc ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left\{{x}\in ℂ|{x}-{N}\in {ℤ}_{\ge \left({M}-{N}\right)}\right\}={ℤ}_{\ge \left({M}-{N}+{N}\right)}$
15 zcn ${⊢}{M}\in ℤ\to {M}\in ℂ$
16 npcan ${⊢}\left({M}\in ℂ\wedge {N}\in ℂ\right)\to {M}-{N}+{N}={M}$
17 15 7 16 syl2an ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {M}-{N}+{N}={M}$
18 17 fveq2d ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {ℤ}_{\ge \left({M}-{N}+{N}\right)}={ℤ}_{\ge {M}}$
19 14 18 eqtrd ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left\{{x}\in ℂ|{x}-{N}\in {ℤ}_{\ge \left({M}-{N}\right)}\right\}={ℤ}_{\ge {M}}$
20 19 fneq2d
21 11 20 mpbid
22 negsub ${⊢}\left({M}\in ℂ\wedge {N}\in ℂ\right)\to {M}+-{N}={M}-{N}$
23 15 7 22 syl2an ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {M}+-{N}={M}-{N}$
24 23 adantr ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge {z}\in {ℤ}_{\ge {M}}\right)\to {M}+-{N}={M}-{N}$
25 24 seqeq1d
26 eluzelcn ${⊢}{z}\in {ℤ}_{\ge {M}}\to {z}\in ℂ$
27 negsub ${⊢}\left({z}\in ℂ\wedge {N}\in ℂ\right)\to {z}+-{N}={z}-{N}$
28 26 8 27 syl2anr ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge {z}\in {ℤ}_{\ge {M}}\right)\to {z}+-{N}={z}-{N}$
29 25 28 fveq12d
30 simpr ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge {z}\in {ℤ}_{\ge {M}}\right)\to {z}\in {ℤ}_{\ge {M}}$
31 znegcl ${⊢}{N}\in ℤ\to -{N}\in ℤ$
32 31 ad2antlr ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge {z}\in {ℤ}_{\ge {M}}\right)\to -{N}\in ℤ$
33 elfzelz ${⊢}{y}\in \left({M}\dots {z}\right)\to {y}\in ℤ$
34 33 zcnd ${⊢}{y}\in \left({M}\dots {z}\right)\to {y}\in ℂ$
35 1 shftval ${⊢}\left({N}\in ℂ\wedge {y}\in ℂ\right)\to \left({F}\mathrm{shift}{N}\right)\left({y}\right)={F}\left({y}-{N}\right)$
36 negsub ${⊢}\left({y}\in ℂ\wedge {N}\in ℂ\right)\to {y}+-{N}={y}-{N}$
37 36 ancoms ${⊢}\left({N}\in ℂ\wedge {y}\in ℂ\right)\to {y}+-{N}={y}-{N}$
38 37 fveq2d ${⊢}\left({N}\in ℂ\wedge {y}\in ℂ\right)\to {F}\left({y}+-{N}\right)={F}\left({y}-{N}\right)$
39 35 38 eqtr4d ${⊢}\left({N}\in ℂ\wedge {y}\in ℂ\right)\to \left({F}\mathrm{shift}{N}\right)\left({y}\right)={F}\left({y}+-{N}\right)$
40 7 34 39 syl2an ${⊢}\left({N}\in ℤ\wedge {y}\in \left({M}\dots {z}\right)\right)\to \left({F}\mathrm{shift}{N}\right)\left({y}\right)={F}\left({y}+-{N}\right)$
41 40 ad4ant24 ${⊢}\left(\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge {z}\in {ℤ}_{\ge {M}}\right)\wedge {y}\in \left({M}\dots {z}\right)\right)\to \left({F}\mathrm{shift}{N}\right)\left({y}\right)={F}\left({y}+-{N}\right)$
42 30 32 41 seqshft2
43 9 shftval
44 8 26 43 syl2an
45 29 42 44 3eqtr4d
46 3 21 45 eqfnfvd