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 𝑀 ( + , 𝐺 ) )