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