Metamath Proof Explorer

Theorem seqfveq2

Description: Equality of sequences. (Contributed by NM, 17-Mar-2005) (Revised by Mario Carneiro, 27-May-2014)

Ref Expression
Hypotheses seqfveq2.1 ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
seqfveq2.2 ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( 𝐺 ‘ 𝐾 ) )
seqfveq2.3 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
seqfveq2.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
Assertion seqfveq2 ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 seqfveq2.1 ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 seqfveq2.2 ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( 𝐺 ‘ 𝐾 ) )
3 seqfveq2.3 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
4 seqfveq2.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
5 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝑁 ∈ ( 𝐾 ... 𝑁 ) )
6 3 5 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐾 ... 𝑁 ) )
7 eleq1 ⊢ ( 𝑥 = 𝐾 → ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) ↔ 𝐾 ∈ ( 𝐾 ... 𝑁 ) ) )
8 fveq2 ⊢ ( 𝑥 = 𝐾 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) )
9 fveq2 ⊢ ( 𝑥 = 𝐾 → ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑥 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝐾 ) )
10 8 9 eqeq12d ⊢ ( 𝑥 = 𝐾 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑥 ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝐾 ) ) )
11 7 10 imbi12d ⊢ ( 𝑥 = 𝐾 → ( ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑥 ) ) ↔ ( 𝐾 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝐾 ) ) ) )
12 11 imbi2d ⊢ ( 𝑥 = 𝐾 → ( ( 𝜑 → ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( 𝐾 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝐾 ) ) ) ) )
13 eleq1 ⊢ ( 𝑥 = 𝑛 → ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) ↔ 𝑛 ∈ ( 𝐾 ... 𝑁 ) ) )
14 fveq2 ⊢ ( 𝑥 = 𝑛 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) )
15 fveq2 ⊢ ( 𝑥 = 𝑛 → ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑥 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑛 ) )
16 14 15 eqeq12d ⊢ ( 𝑥 = 𝑛 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑥 ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑛 ) ) )
17 13 16 imbi12d ⊢ ( 𝑥 = 𝑛 → ( ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑥 ) ) ↔ ( 𝑛 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑛 ) ) ) )
18 17 imbi2d ⊢ ( 𝑥 = 𝑛 → ( ( 𝜑 → ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( 𝑛 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑛 ) ) ) ) )
19 eleq1 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) ↔ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) )
20 fveq2 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) )
21 fveq2 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑥 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) )
22 20 21 eqeq12d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑥 ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( seq 𝐾 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) )
23 19 22 imbi12d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑥 ) ) ↔ ( ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( seq 𝐾 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) ) )
24 23 imbi2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( seq 𝐾 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) ) ) )
25 eleq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) ↔ 𝑁 ∈ ( 𝐾 ... 𝑁 ) ) )
26 fveq2 ⊢ ( 𝑥 = 𝑁 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
27 fveq2 ⊢ ( 𝑥 = 𝑁 → ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑥 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑁 ) )
28 26 27 eqeq12d ⊢ ( 𝑥 = 𝑁 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑥 ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑁 ) ) )
29 25 28 imbi12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑥 ) ) ↔ ( 𝑁 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑁 ) ) ) )
30 29 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝜑 → ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( 𝑁 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑁 ) ) ) ) )
31 eluzelz ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝐾 ∈ ℤ )
32 seq1 ⊢ ( 𝐾 ∈ ℤ → ( seq 𝐾 ( + , 𝐺 ) ‘ 𝐾 ) = ( 𝐺 ‘ 𝐾 ) )
33 1 31 32 3syl ⊢ ( 𝜑 → ( seq 𝐾 ( + , 𝐺 ) ‘ 𝐾 ) = ( 𝐺 ‘ 𝐾 ) )
34 2 33 eqtr4d ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝐾 ) )
35 34 a1d ⊢ ( 𝜑 → ( 𝐾 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝐾 ) ) )
36 peano2fzr ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) → 𝑛 ∈ ( 𝐾 ... 𝑁 ) )
37 36 adantl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → 𝑛 ∈ ( 𝐾 ... 𝑁 ) )
38 37 expr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) → 𝑛 ∈ ( 𝐾 ... 𝑁 ) ) )
39 38 imim1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 𝑛 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑛 ) ) → ( ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑛 ) ) ) )
40 oveq1 ⊢ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑛 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
41 simpl ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) )
42 uztrn ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
43 41 1 42 syl2anr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
44 seqp1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
45 43 44 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
46 seqp1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) → ( seq 𝐾 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
47 46 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → ( seq 𝐾 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
48 fveq2 ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
49 fveq2 ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝑛 + 1 ) ) )
50 48 49 eqeq12d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ↔ ( 𝐹 ‘ ( 𝑛 + 1 ) ) = ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
51 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
52 51 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → ∀ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
53 eluzp1p1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) )
54 53 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) )
55 elfzuz3 ⊢ ( ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) )
56 55 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) )
57 elfzuzb ⊢ ( ( 𝑛 + 1 ) ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ↔ ( ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) )
58 54 56 57 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → ( 𝑛 + 1 ) ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) )
59 50 52 58 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) = ( 𝐺 ‘ ( 𝑛 + 1 ) ) )
60 59 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → ( ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
61 47 60 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → ( seq 𝐾 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
62 45 61 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( seq 𝐾 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ↔ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
63 40 62 imbitrrid ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑛 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( seq 𝐾 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) )
64 39 63 animpimp2impd ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) → ( ( 𝜑 → ( 𝑛 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑛 ) ) ) → ( 𝜑 → ( ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( seq 𝐾 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) ) ) )
65 12 18 24 30 35 64 uzind4i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝜑 → ( 𝑁 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑁 ) ) ) )
66 3 65 mpcom ⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑁 ) ) )
67 6 66 mpd ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑁 ) )