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 
|- ( ph -> M e. ZZ )
seqfeq.2 
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = ( G ` k ) )
Assertion seqfeq 
|- ( ph -> seq M ( .+ , F ) = seq M ( .+ , G ) )

Proof

Step Hyp Ref Expression
1 seqfeq.1 
 |-  ( ph -> M e. ZZ )
2 seqfeq.2 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = ( G ` k ) )
3 seqfn 
 |-  ( M e. ZZ -> seq M ( .+ , F ) Fn ( ZZ>= ` M ) )
4 1 3 syl 
 |-  ( ph -> seq M ( .+ , F ) Fn ( ZZ>= ` M ) )
5 seqfn 
 |-  ( M e. ZZ -> seq M ( .+ , G ) Fn ( ZZ>= ` M ) )
6 1 5 syl 
 |-  ( ph -> seq M ( .+ , G ) Fn ( ZZ>= ` M ) )
7 simpr 
 |-  ( ( ph /\ x e. ( ZZ>= ` M ) ) -> x e. ( ZZ>= ` M ) )
8 elfzuz 
 |-  ( k e. ( M ... x ) -> k e. ( ZZ>= ` M ) )
9 8 2 sylan2 
 |-  ( ( ph /\ k e. ( M ... x ) ) -> ( F ` k ) = ( G ` k ) )
10 9 adantlr 
 |-  ( ( ( ph /\ x e. ( ZZ>= ` M ) ) /\ k e. ( M ... x ) ) -> ( F ` k ) = ( G ` k ) )
11 7 10 seqfveq 
 |-  ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( seq M ( .+ , F ) ` x ) = ( seq M ( .+ , G ) ` x ) )
12 4 6 11 eqfnfvd 
 |-  ( ph -> seq M ( .+ , F ) = seq M ( .+ , G ) )