# Metamath Proof Explorer

## Theorem seqshft2

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

Ref Expression
Hypotheses seqshft2.1 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
seqshft2.2 ${⊢}{\phi }\to {K}\in ℤ$
seqshft2.3 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {N}\right)\right)\to {F}\left({k}\right)={G}\left({k}+{K}\right)$
Assertion seqshft2

### Proof

Step Hyp Ref Expression
1 seqshft2.1 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
2 seqshft2.2 ${⊢}{\phi }\to {K}\in ℤ$
3 seqshft2.3 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {N}\right)\right)\to {F}\left({k}\right)={G}\left({k}+{K}\right)$
4 eluzfz2 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}\in \left({M}\dots {N}\right)$
5 1 4 syl ${⊢}{\phi }\to {N}\in \left({M}\dots {N}\right)$
6 eleq1 ${⊢}{x}={M}\to \left({x}\in \left({M}\dots {N}\right)↔{M}\in \left({M}\dots {N}\right)\right)$
7 fveq2
8 fvoveq1
9 7 8 eqeq12d
10 6 9 imbi12d
11 10 imbi2d
12 eleq1 ${⊢}{x}={n}\to \left({x}\in \left({M}\dots {N}\right)↔{n}\in \left({M}\dots {N}\right)\right)$
13 fveq2
14 fvoveq1
15 13 14 eqeq12d
16 12 15 imbi12d
17 16 imbi2d
18 eleq1 ${⊢}{x}={n}+1\to \left({x}\in \left({M}\dots {N}\right)↔{n}+1\in \left({M}\dots {N}\right)\right)$
19 fveq2
20 fvoveq1
21 19 20 eqeq12d
22 18 21 imbi12d
23 22 imbi2d
24 eleq1 ${⊢}{x}={N}\to \left({x}\in \left({M}\dots {N}\right)↔{N}\in \left({M}\dots {N}\right)\right)$
25 fveq2
26 fvoveq1
27 25 26 eqeq12d
28 24 27 imbi12d
29 28 imbi2d
30 fveq2 ${⊢}{k}={M}\to {F}\left({k}\right)={F}\left({M}\right)$
31 fvoveq1 ${⊢}{k}={M}\to {G}\left({k}+{K}\right)={G}\left({M}+{K}\right)$
32 30 31 eqeq12d ${⊢}{k}={M}\to \left({F}\left({k}\right)={G}\left({k}+{K}\right)↔{F}\left({M}\right)={G}\left({M}+{K}\right)\right)$
33 3 ralrimiva ${⊢}{\phi }\to \forall {k}\in \left({M}\dots {N}\right)\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)={G}\left({k}+{K}\right)$
34 eluzfz1 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\in \left({M}\dots {N}\right)$
35 1 34 syl ${⊢}{\phi }\to {M}\in \left({M}\dots {N}\right)$
36 32 33 35 rspcdva ${⊢}{\phi }\to {F}\left({M}\right)={G}\left({M}+{K}\right)$
37 eluzel2 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\in ℤ$
38 1 37 syl ${⊢}{\phi }\to {M}\in ℤ$
39 seq1
40 38 39 syl
41 38 2 zaddcld ${⊢}{\phi }\to {M}+{K}\in ℤ$
42 seq1
43 41 42 syl
44 36 40 43 3eqtr4d
45 44 a1i13
46 peano2fzr ${⊢}\left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\to {n}\in \left({M}\dots {N}\right)$
47 46 adantl ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to {n}\in \left({M}\dots {N}\right)$
48 47 expr ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {M}}\right)\to \left({n}+1\in \left({M}\dots {N}\right)\to {n}\in \left({M}\dots {N}\right)\right)$
49 48 imim1d
50 oveq1
51 simprl ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to {n}\in {ℤ}_{\ge {M}}$
52 seqp1
53 51 52 syl
54 2 adantr ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to {K}\in ℤ$
55 eluzadd ${⊢}\left({n}\in {ℤ}_{\ge {M}}\wedge {K}\in ℤ\right)\to {n}+{K}\in {ℤ}_{\ge \left({M}+{K}\right)}$
56 51 54 55 syl2anc ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to {n}+{K}\in {ℤ}_{\ge \left({M}+{K}\right)}$
57 seqp1
58 56 57 syl
59 eluzelz ${⊢}{n}\in {ℤ}_{\ge {M}}\to {n}\in ℤ$
60 51 59 syl ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to {n}\in ℤ$
61 zcn ${⊢}{n}\in ℤ\to {n}\in ℂ$
62 zcn ${⊢}{K}\in ℤ\to {K}\in ℂ$
63 ax-1cn ${⊢}1\in ℂ$
64 add32 ${⊢}\left({n}\in ℂ\wedge 1\in ℂ\wedge {K}\in ℂ\right)\to {n}+1+{K}={n}+{K}+1$
65 63 64 mp3an2 ${⊢}\left({n}\in ℂ\wedge {K}\in ℂ\right)\to {n}+1+{K}={n}+{K}+1$
66 61 62 65 syl2an ${⊢}\left({n}\in ℤ\wedge {K}\in ℤ\right)\to {n}+1+{K}={n}+{K}+1$
67 60 54 66 syl2anc ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to {n}+1+{K}={n}+{K}+1$
68 67 fveq2d
69 fveq2 ${⊢}{k}={n}+1\to {F}\left({k}\right)={F}\left({n}+1\right)$
70 fvoveq1 ${⊢}{k}={n}+1\to {G}\left({k}+{K}\right)={G}\left({n}+1+{K}\right)$
71 69 70 eqeq12d ${⊢}{k}={n}+1\to \left({F}\left({k}\right)={G}\left({k}+{K}\right)↔{F}\left({n}+1\right)={G}\left({n}+1+{K}\right)\right)$
72 33 adantr ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to \forall {k}\in \left({M}\dots {N}\right)\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)={G}\left({k}+{K}\right)$
73 simprr ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to {n}+1\in \left({M}\dots {N}\right)$
74 71 72 73 rspcdva ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to {F}\left({n}+1\right)={G}\left({n}+1+{K}\right)$
75 67 fveq2d ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to {G}\left({n}+1+{K}\right)={G}\left({n}+{K}+1\right)$
76 74 75 eqtrd ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to {F}\left({n}+1\right)={G}\left({n}+{K}+1\right)$
77 76 oveq2d
78 58 68 77 3eqtr4d
79 53 78 eqeq12d
80 50 79 syl5ibr
81 49 80 animpimp2impd
82 11 17 23 29 45 81 uzind4
83 1 82 mpcom
84 5 83 mpd