Theorem seqfveq

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

	Ref	Expression
Hypotheses	seqfveq.1	|- ( ph -> N e. ( ZZ>= ` M ) )
	seqfveq.2	|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) = ( G ` k ) )
Assertion	seqfveq	|- ( ph -> ( seq M ( .+ , F ) ` N ) = ( seq M ( .+ , G ) ` N ) )

Proof

Step	Hyp	Ref	Expression
1		seqfveq.1	|- ( ph -> N e. ( ZZ>= ` M ) )
2		seqfveq.2	|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) = ( G ` k ) )
3		eluzel2	|- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
4	1 3	syl	|- ( ph -> M e. ZZ )
5		uzid	|- ( M e. ZZ -> M e. ( ZZ>= ` M ) )
6	4 5	syl	|- ( ph -> M e. ( ZZ>= ` M ) )
7		seq1	|- ( M e. ZZ -> ( seq M ( .+ , F ) ` M ) = ( F ` M ) )
8	4 7	syl	|- ( ph -> ( seq M ( .+ , F ) ` M ) = ( F ` M ) )
9		fveq2	|- ( k = M -> ( F ` k ) = ( F ` M ) )
10		fveq2	|- ( k = M -> ( G ` k ) = ( G ` M ) )
11	9 10	eqeq12d	|- ( k = M -> ( ( F ` k ) = ( G ` k ) <-> ( F ` M ) = ( G ` M ) ) )
12	2	ralrimiva	|- ( ph -> A. k e. ( M ... N ) ( F ` k ) = ( G ` k ) )
13		eluzfz1	|- ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
14	1 13	syl	|- ( ph -> M e. ( M ... N ) )
15	11 12 14	rspcdva	|- ( ph -> ( F ` M ) = ( G ` M ) )
16	8 15	eqtrd	|- ( ph -> ( seq M ( .+ , F ) ` M ) = ( G ` M ) )
17		fzp1ss	|- ( M e. ZZ -> ( ( M + 1 ) ... N ) C_ ( M ... N ) )
18	4 17	syl	|- ( ph -> ( ( M + 1 ) ... N ) C_ ( M ... N ) )
19	18	sselda	|- ( ( ph /\ k e. ( ( M + 1 ) ... N ) ) -> k e. ( M ... N ) )
20	19 2	syldan	|- ( ( ph /\ k e. ( ( M + 1 ) ... N ) ) -> ( F ` k ) = ( G ` k ) )
21	6 16 1 20	seqfveq2	|- ( ph -> ( seq M ( .+ , F ) ` N ) = ( seq M ( .+ , G ) ` N ) )