This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem seqfeq

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

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

Proof

Step Hyp Ref Expression
1 seqfeq.1 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 seqfeq.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
3 seqfn ⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( + , 𝐹 ) Fn ( ℤ≥ ‘ 𝑀 ) )
4 1 3 syl ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) Fn ( ℤ≥ ‘ 𝑀 ) )
5 seqfn ⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( + , 𝐺 ) Fn ( ℤ≥ ‘ 𝑀 ) )
6 1 5 syl ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) Fn ( ℤ≥ ‘ 𝑀 ) )
7 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) )
8 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑥 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
9 8 2 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑥 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
10 9 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑥 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
11 7 10 seqfveq ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑥 ) )
12 4 6 11 eqfnfvd ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) = seq 𝑀 ( + , 𝐺 ) )