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

Metamath Proof Explorer

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 ) )