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 φ N M
seqshft2.2 φ K
seqshft2.3 φ k M N F k = G k + K
Assertion seqshft2 φ seq M + ˙ F N = seq M + K + ˙ G N + K

Proof

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