Theorem seqfveq

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

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

Proof

Step	Hyp	Ref	Expression
1		seqfveq.1	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2		seqfveq.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
3		eluzel2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
4	1 3	syl	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5		uzid	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
6	4 5	syl	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
7		seq1	⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )
8	4 7	syl	⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )
9		fveq2	⊢ ( 𝑘 = 𝑀 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑀 ) )
10		fveq2	⊢ ( 𝑘 = 𝑀 → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑀 ) )
11	9 10	eqeq12d	⊢ ( 𝑘 = 𝑀 → ( ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ↔ ( 𝐹 ‘ 𝑀 ) = ( 𝐺 ‘ 𝑀 ) ) )
12	2	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
13		eluzfz1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
14	1 13	syl	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
15	11 12 14	rspcdva	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) = ( 𝐺 ‘ 𝑀 ) )
16	8 15	eqtrd	⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( 𝐺 ‘ 𝑀 ) )
17		fzp1ss	⊢ ( 𝑀 ∈ ℤ → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
18	4 17	syl	⊢ ( 𝜑 → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
19	18	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
20	19 2	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
21	6 16 1 20	seqfveq2	⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) )