Metamath Proof Explorer

Theorem seqfeq2

Description: Equality of sequences. (Contributed by Mario Carneiro, 13-Jul-2013) (Revised by Mario Carneiro, 27-May-2014)

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

Proof

Step Hyp Ref Expression
1 seqfveq2.1 ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 seqfveq2.2 ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( 𝐺 ‘ 𝐾 ) )
3 seqfeq2.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
4 eluzel2 ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
5 seqfn ⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( + , 𝐹 ) Fn ( ℤ≥ ‘ 𝑀 ) )
6 1 4 5 3syl ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) Fn ( ℤ≥ ‘ 𝑀 ) )
7 uzss ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝐾 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
8 1 7 syl ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝐾 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
9 fnssres ⊢ ( ( seq 𝑀 ( + , 𝐹 ) Fn ( ℤ≥ ‘ 𝑀 ) ∧ ( ℤ≥ ‘ 𝐾 ) ⊆ ( ℤ≥ ‘ 𝑀 ) ) → ( seq 𝑀 ( + , 𝐹 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) Fn ( ℤ≥ ‘ 𝐾 ) )
10 6 8 9 syl2anc ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) Fn ( ℤ≥ ‘ 𝐾 ) )
11 eluzelz ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝐾 ∈ ℤ )
12 seqfn ⊢ ( 𝐾 ∈ ℤ → seq 𝐾 ( + , 𝐺 ) Fn ( ℤ≥ ‘ 𝐾 ) )
13 1 11 12 3syl ⊢ ( 𝜑 → seq 𝐾 ( + , 𝐺 ) Fn ( ℤ≥ ‘ 𝐾 ) )
14 fvres ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) → ( ( seq 𝑀 ( + , 𝐹 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) )
16 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
17 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( 𝐺 ‘ 𝐾 ) )
18 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) )
19 elfzuz ⊢ ( 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) )
20 19 3 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
21 20 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
22 16 17 18 21 seqfveq2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑥 ) )
23 15 22 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) ‘ 𝑥 ) = ( seq 𝐾 ( + , 𝐺 ) ‘ 𝑥 ) )
24 10 13 23 eqfnfvd ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) = seq 𝐾 ( + , 𝐺 ) )