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 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
seqshft2.2 ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
seqshft2.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝑘 + 𝐾 ) ) )
Assertion seqshft2 ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑁 + 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 seqshft2.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 seqshft2.2 ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
3 seqshft2.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝑘 + 𝐾 ) ) )
4 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
5 1 4 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
6 eleq1 ⊢ ( 𝑥 = 𝑀 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑀 ∈ ( 𝑀 ... 𝑁 ) ) )
7 fveq2 ⊢ ( 𝑥 = 𝑀 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) )
8 fvoveq1 ⊢ ( 𝑥 = 𝑀 → ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑥 + 𝐾 ) ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑀 + 𝐾 ) ) )
9 7 8 eqeq12d ⊢ ( 𝑥 = 𝑀 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑥 + 𝐾 ) ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑀 + 𝐾 ) ) ) )
10 6 9 imbi12d ⊢ ( 𝑥 = 𝑀 → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑥 + 𝐾 ) ) ) ↔ ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑀 + 𝐾 ) ) ) ) )
11 10 imbi2d ⊢ ( 𝑥 = 𝑀 → ( ( 𝜑 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑥 + 𝐾 ) ) ) ) ↔ ( 𝜑 → ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑀 + 𝐾 ) ) ) ) ) )
12 eleq1 ⊢ ( 𝑥 = 𝑛 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) )
13 fveq2 ⊢ ( 𝑥 = 𝑛 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) )
14 fvoveq1 ⊢ ( 𝑥 = 𝑛 → ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑥 + 𝐾 ) ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑛 + 𝐾 ) ) )
15 13 14 eqeq12d ⊢ ( 𝑥 = 𝑛 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑥 + 𝐾 ) ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑛 + 𝐾 ) ) ) )
16 12 15 imbi12d ⊢ ( 𝑥 = 𝑛 → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑥 + 𝐾 ) ) ) ↔ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑛 + 𝐾 ) ) ) ) )
17 16 imbi2d ⊢ ( 𝑥 = 𝑛 → ( ( 𝜑 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑥 + 𝐾 ) ) ) ) ↔ ( 𝜑 → ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑛 + 𝐾 ) ) ) ) ) )
18 eleq1 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) )
19 fveq2 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) )
20 fvoveq1 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑥 + 𝐾 ) ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( ( 𝑛 + 1 ) + 𝐾 ) ) )
21 19 20 eqeq12d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑥 + 𝐾 ) ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( ( 𝑛 + 1 ) + 𝐾 ) ) ) )
22 18 21 imbi12d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑥 + 𝐾 ) ) ) ↔ ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( ( 𝑛 + 1 ) + 𝐾 ) ) ) ) )
23 22 imbi2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑥 + 𝐾 ) ) ) ) ↔ ( 𝜑 → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( ( 𝑛 + 1 ) + 𝐾 ) ) ) ) ) )
24 eleq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑁 ∈ ( 𝑀 ... 𝑁 ) ) )
25 fveq2 ⊢ ( 𝑥 = 𝑁 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
26 fvoveq1 ⊢ ( 𝑥 = 𝑁 → ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑥 + 𝐾 ) ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑁 + 𝐾 ) ) )
27 25 26 eqeq12d ⊢ ( 𝑥 = 𝑁 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑥 + 𝐾 ) ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑁 + 𝐾 ) ) ) )
28 24 27 imbi12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑥 + 𝐾 ) ) ) ↔ ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑁 + 𝐾 ) ) ) ) )
29 28 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝜑 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑥 + 𝐾 ) ) ) ) ↔ ( 𝜑 → ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑁 + 𝐾 ) ) ) ) ) )
30 fveq2 ⊢ ( 𝑘 = 𝑀 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑀 ) )
31 fvoveq1 ⊢ ( 𝑘 = 𝑀 → ( 𝐺 ‘ ( 𝑘 + 𝐾 ) ) = ( 𝐺 ‘ ( 𝑀 + 𝐾 ) ) )
32 30 31 eqeq12d ⊢ ( 𝑘 = 𝑀 → ( ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝑘 + 𝐾 ) ) ↔ ( 𝐹 ‘ 𝑀 ) = ( 𝐺 ‘ ( 𝑀 + 𝐾 ) ) ) )
33 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝑘 + 𝐾 ) ) )
34 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
35 1 34 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
36 32 33 35 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) = ( 𝐺 ‘ ( 𝑀 + 𝐾 ) ) )
37 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
38 1 37 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
39 seq1 ⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )
40 38 39 syl ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )
41 38 2 zaddcld ⊢ ( 𝜑 → ( 𝑀 + 𝐾 ) ∈ ℤ )
42 seq1 ⊢ ( ( 𝑀 + 𝐾 ) ∈ ℤ → ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑀 + 𝐾 ) ) = ( 𝐺 ‘ ( 𝑀 + 𝐾 ) ) )
43 41 42 syl ⊢ ( 𝜑 → ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑀 + 𝐾 ) ) = ( 𝐺 ‘ ( 𝑀 + 𝐾 ) ) )
44 36 40 43 3eqtr4d ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑀 + 𝐾 ) ) )
45 44 a1i13 ⊢ ( 𝑀 ∈ ℤ → ( 𝜑 → ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑀 + 𝐾 ) ) ) ) )
46 peano2fzr ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝑛 ∈ ( 𝑀 ... 𝑁 ) )
47 46 adantl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → 𝑛 ∈ ( 𝑀 ... 𝑁 ) )
48 47 expr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) )
49 48 imim1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑛 + 𝐾 ) ) ) → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑛 + 𝐾 ) ) ) ) )
50 oveq1 ⊢ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑛 + 𝐾 ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑛 + 𝐾 ) ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
51 simprl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
52 seqp1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
53 51 52 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
54 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → 𝐾 ∈ ℤ )
55 eluzadd ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ℤ ) → ( 𝑛 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) )
56 51 54 55 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝑛 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) )
57 seqp1 ⊢ ( ( 𝑛 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) → ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( ( 𝑛 + 𝐾 ) + 1 ) ) = ( ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑛 + 𝐾 ) ) + ( 𝐺 ‘ ( ( 𝑛 + 𝐾 ) + 1 ) ) ) )
58 56 57 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( ( 𝑛 + 𝐾 ) + 1 ) ) = ( ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑛 + 𝐾 ) ) + ( 𝐺 ‘ ( ( 𝑛 + 𝐾 ) + 1 ) ) ) )
59 eluzelz ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑛 ∈ ℤ )
60 51 59 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → 𝑛 ∈ ℤ )
61 zcn ⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ )
62 zcn ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
63 ax-1cn ⊢ 1 ∈ ℂ
64 add32 ⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( ( 𝑛 + 1 ) + 𝐾 ) = ( ( 𝑛 + 𝐾 ) + 1 ) )
65 63 64 mp3an2 ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( ( 𝑛 + 1 ) + 𝐾 ) = ( ( 𝑛 + 𝐾 ) + 1 ) )
66 61 62 65 syl2an ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑛 + 1 ) + 𝐾 ) = ( ( 𝑛 + 𝐾 ) + 1 ) )
67 60 54 66 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( ( 𝑛 + 1 ) + 𝐾 ) = ( ( 𝑛 + 𝐾 ) + 1 ) )
68 67 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( ( 𝑛 + 1 ) + 𝐾 ) ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( ( 𝑛 + 𝐾 ) + 1 ) ) )
69 fveq2 ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
70 fvoveq1 ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝐺 ‘ ( 𝑘 + 𝐾 ) ) = ( 𝐺 ‘ ( ( 𝑛 + 1 ) + 𝐾 ) ) )
71 69 70 eqeq12d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝑘 + 𝐾 ) ) ↔ ( 𝐹 ‘ ( 𝑛 + 1 ) ) = ( 𝐺 ‘ ( ( 𝑛 + 1 ) + 𝐾 ) ) ) )
72 33 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝑘 + 𝐾 ) ) )
73 simprr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
74 71 72 73 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) = ( 𝐺 ‘ ( ( 𝑛 + 1 ) + 𝐾 ) ) )
75 67 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝐺 ‘ ( ( 𝑛 + 1 ) + 𝐾 ) ) = ( 𝐺 ‘ ( ( 𝑛 + 𝐾 ) + 1 ) ) )
76 74 75 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) = ( 𝐺 ‘ ( ( 𝑛 + 𝐾 ) + 1 ) ) )
77 76 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑛 + 𝐾 ) ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑛 + 𝐾 ) ) + ( 𝐺 ‘ ( ( 𝑛 + 𝐾 ) + 1 ) ) ) )
78 58 68 77 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( ( 𝑛 + 1 ) + 𝐾 ) ) = ( ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑛 + 𝐾 ) ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
79 53 78 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( ( 𝑛 + 1 ) + 𝐾 ) ) ↔ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑛 + 𝐾 ) ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
80 50 79 imbitrrid ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑛 + 𝐾 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( ( 𝑛 + 1 ) + 𝐾 ) ) ) )
81 49 80 animpimp2impd ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝜑 → ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑛 + 𝐾 ) ) ) ) → ( 𝜑 → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( ( 𝑛 + 1 ) + 𝐾 ) ) ) ) ) )
82 11 17 23 29 45 81 uzind4 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑁 + 𝐾 ) ) ) ) )
83 1 82 mpcom ⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑁 + 𝐾 ) ) ) )
84 5 83 mpd ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq ( 𝑀 + 𝐾 ) ( + , 𝐺 ) ‘ ( 𝑁 + 𝐾 ) ) )