Metamath Proof Explorer

Theorem seqfeq2

Description: Equality of sequences. (Contributed by Mario Carneiro, 13-Jul-2013) (Revised by Mario Carneiro, 27-May-2014)

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

Proof

Step Hyp Ref Expression
1 seqfveq2.1 
 |-  ( ph -> K e. ( ZZ>= ` M ) )
2 seqfveq2.2 
 |-  ( ph -> ( seq M ( .+ , F ) ` K ) = ( G ` K ) )
3 seqfeq2.4 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( K + 1 ) ) ) -> ( F ` k ) = ( G ` k ) )
4 eluzel2 
 |-  ( K e. ( ZZ>= ` M ) -> M e. ZZ )
5 seqfn 
 |-  ( M e. ZZ -> seq M ( .+ , F ) Fn ( ZZ>= ` M ) )
6 1 4 5 3syl 
 |-  ( ph -> seq M ( .+ , F ) Fn ( ZZ>= ` M ) )
7 uzss 
 |-  ( K e. ( ZZ>= ` M ) -> ( ZZ>= ` K ) C_ ( ZZ>= ` M ) )
8 1 7 syl 
 |-  ( ph -> ( ZZ>= ` K ) C_ ( ZZ>= ` M ) )
9 fnssres 
 |-  ( ( seq M ( .+ , F ) Fn ( ZZ>= ` M ) /\ ( ZZ>= ` K ) C_ ( ZZ>= ` M ) ) -> ( seq M ( .+ , F ) |` ( ZZ>= ` K ) ) Fn ( ZZ>= ` K ) )
10 6 8 9 syl2anc 
 |-  ( ph -> ( seq M ( .+ , F ) |` ( ZZ>= ` K ) ) Fn ( ZZ>= ` K ) )
11 eluzelz 
 |-  ( K e. ( ZZ>= ` M ) -> K e. ZZ )
12 seqfn 
 |-  ( K e. ZZ -> seq K ( .+ , G ) Fn ( ZZ>= ` K ) )
13 1 11 12 3syl 
 |-  ( ph -> seq K ( .+ , G ) Fn ( ZZ>= ` K ) )
14 fvres 
 |-  ( x e. ( ZZ>= ` K ) -> ( ( seq M ( .+ , F ) |` ( ZZ>= ` K ) ) ` x ) = ( seq M ( .+ , F ) ` x ) )
15 14 adantl 
 |-  ( ( ph /\ x e. ( ZZ>= ` K ) ) -> ( ( seq M ( .+ , F ) |` ( ZZ>= ` K ) ) ` x ) = ( seq M ( .+ , F ) ` x ) )
16 1 adantr 
 |-  ( ( ph /\ x e. ( ZZ>= ` K ) ) -> K e. ( ZZ>= ` M ) )
17 2 adantr 
 |-  ( ( ph /\ x e. ( ZZ>= ` K ) ) -> ( seq M ( .+ , F ) ` K ) = ( G ` K ) )
18 simpr 
 |-  ( ( ph /\ x e. ( ZZ>= ` K ) ) -> x e. ( ZZ>= ` K ) )
19 elfzuz 
 |-  ( k e. ( ( K + 1 ) ... x ) -> k e. ( ZZ>= ` ( K + 1 ) ) )
20 19 3 sylan2 
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... x ) ) -> ( F ` k ) = ( G ` k ) )
21 20 adantlr 
 |-  ( ( ( ph /\ x e. ( ZZ>= ` K ) ) /\ k e. ( ( K + 1 ) ... x ) ) -> ( F ` k ) = ( G ` k ) )
22 16 17 18 21 seqfveq2 
 |-  ( ( ph /\ x e. ( ZZ>= ` K ) ) -> ( seq M ( .+ , F ) ` x ) = ( seq K ( .+ , G ) ` x ) )
23 15 22 eqtrd 
 |-  ( ( ph /\ x e. ( ZZ>= ` K ) ) -> ( ( seq M ( .+ , F ) |` ( ZZ>= ` K ) ) ` x ) = ( seq K ( .+ , G ) ` x ) )
24 10 13 23 eqfnfvd 
 |-  ( ph -> ( seq M ( .+ , F ) |` ( ZZ>= ` K ) ) = seq K ( .+ , G ) )