Metamath Proof Explorer

Theorem seqfveq2

Description: Equality of sequences. (Contributed by NM, 17-Mar-2005) (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 ) )
seqfveq2.3 
|- ( ph -> N e. ( ZZ>= ` K ) )
seqfveq2.4 
|- ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( F ` k ) = ( G ` k ) )
Assertion seqfveq2 
|- ( ph -> ( seq M ( .+ , F ) ` N ) = ( seq K ( .+ , G ) ` N ) )

Proof

Step Hyp Ref Expression
1 seqfveq2.1 
 |-  ( ph -> K e. ( ZZ>= ` M ) )
2 seqfveq2.2 
 |-  ( ph -> ( seq M ( .+ , F ) ` K ) = ( G ` K ) )
3 seqfveq2.3 
 |-  ( ph -> N e. ( ZZ>= ` K ) )
4 seqfveq2.4 
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( F ` k ) = ( G ` k ) )
5 eluzfz2 
 |-  ( N e. ( ZZ>= ` K ) -> N e. ( K ... N ) )
6 3 5 syl 
 |-  ( ph -> N e. ( K ... N ) )
7 eleq1 
 |-  ( x = K -> ( x e. ( K ... N ) <-> K e. ( K ... N ) ) )
8 fveq2 
 |-  ( x = K -> ( seq M ( .+ , F ) ` x ) = ( seq M ( .+ , F ) ` K ) )
9 fveq2 
 |-  ( x = K -> ( seq K ( .+ , G ) ` x ) = ( seq K ( .+ , G ) ` K ) )
10 8 9 eqeq12d 
 |-  ( x = K -> ( ( seq M ( .+ , F ) ` x ) = ( seq K ( .+ , G ) ` x ) <-> ( seq M ( .+ , F ) ` K ) = ( seq K ( .+ , G ) ` K ) ) )
11 7 10 imbi12d 
 |-  ( x = K -> ( ( x e. ( K ... N ) -> ( seq M ( .+ , F ) ` x ) = ( seq K ( .+ , G ) ` x ) ) <-> ( K e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq K ( .+ , G ) ` K ) ) ) )
12 11 imbi2d 
 |-  ( x = K -> ( ( ph -> ( x e. ( K ... N ) -> ( seq M ( .+ , F ) ` x ) = ( seq K ( .+ , G ) ` x ) ) ) <-> ( ph -> ( K e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq K ( .+ , G ) ` K ) ) ) ) )
13 eleq1 
 |-  ( x = n -> ( x e. ( K ... N ) <-> n e. ( K ... N ) ) )
14 fveq2 
 |-  ( x = n -> ( seq M ( .+ , F ) ` x ) = ( seq M ( .+ , F ) ` n ) )
15 fveq2 
 |-  ( x = n -> ( seq K ( .+ , G ) ` x ) = ( seq K ( .+ , G ) ` n ) )
16 14 15 eqeq12d 
 |-  ( x = n -> ( ( seq M ( .+ , F ) ` x ) = ( seq K ( .+ , G ) ` x ) <-> ( seq M ( .+ , F ) ` n ) = ( seq K ( .+ , G ) ` n ) ) )
17 13 16 imbi12d 
 |-  ( x = n -> ( ( x e. ( K ... N ) -> ( seq M ( .+ , F ) ` x ) = ( seq K ( .+ , G ) ` x ) ) <-> ( n e. ( K ... N ) -> ( seq M ( .+ , F ) ` n ) = ( seq K ( .+ , G ) ` n ) ) ) )
18 17 imbi2d 
 |-  ( x = n -> ( ( ph -> ( x e. ( K ... N ) -> ( seq M ( .+ , F ) ` x ) = ( seq K ( .+ , G ) ` x ) ) ) <-> ( ph -> ( n e. ( K ... N ) -> ( seq M ( .+ , F ) ` n ) = ( seq K ( .+ , G ) ` n ) ) ) ) )
19 eleq1 
 |-  ( x = ( n + 1 ) -> ( x e. ( K ... N ) <-> ( n + 1 ) e. ( K ... N ) ) )
20 fveq2 
 |-  ( x = ( n + 1 ) -> ( seq M ( .+ , F ) ` x ) = ( seq M ( .+ , F ) ` ( n + 1 ) ) )
21 fveq2 
 |-  ( x = ( n + 1 ) -> ( seq K ( .+ , G ) ` x ) = ( seq K ( .+ , G ) ` ( n + 1 ) ) )
22 20 21 eqeq12d 
 |-  ( x = ( n + 1 ) -> ( ( seq M ( .+ , F ) ` x ) = ( seq K ( .+ , G ) ` x ) <-> ( seq M ( .+ , F ) ` ( n + 1 ) ) = ( seq K ( .+ , G ) ` ( n + 1 ) ) ) )
23 19 22 imbi12d 
 |-  ( x = ( n + 1 ) -> ( ( x e. ( K ... N ) -> ( seq M ( .+ , F ) ` x ) = ( seq K ( .+ , G ) ` x ) ) <-> ( ( n + 1 ) e. ( K ... N ) -> ( seq M ( .+ , F ) ` ( n + 1 ) ) = ( seq K ( .+ , G ) ` ( n + 1 ) ) ) ) )
24 23 imbi2d 
 |-  ( x = ( n + 1 ) -> ( ( ph -> ( x e. ( K ... N ) -> ( seq M ( .+ , F ) ` x ) = ( seq K ( .+ , G ) ` x ) ) ) <-> ( ph -> ( ( n + 1 ) e. ( K ... N ) -> ( seq M ( .+ , F ) ` ( n + 1 ) ) = ( seq K ( .+ , G ) ` ( n + 1 ) ) ) ) ) )
25 eleq1 
 |-  ( x = N -> ( x e. ( K ... N ) <-> N e. ( K ... N ) ) )
26 fveq2 
 |-  ( x = N -> ( seq M ( .+ , F ) ` x ) = ( seq M ( .+ , F ) ` N ) )
27 fveq2 
 |-  ( x = N -> ( seq K ( .+ , G ) ` x ) = ( seq K ( .+ , G ) ` N ) )
28 26 27 eqeq12d 
 |-  ( x = N -> ( ( seq M ( .+ , F ) ` x ) = ( seq K ( .+ , G ) ` x ) <-> ( seq M ( .+ , F ) ` N ) = ( seq K ( .+ , G ) ` N ) ) )
29 25 28 imbi12d 
 |-  ( x = N -> ( ( x e. ( K ... N ) -> ( seq M ( .+ , F ) ` x ) = ( seq K ( .+ , G ) ` x ) ) <-> ( N e. ( K ... N ) -> ( seq M ( .+ , F ) ` N ) = ( seq K ( .+ , G ) ` N ) ) ) )
30 29 imbi2d 
 |-  ( x = N -> ( ( ph -> ( x e. ( K ... N ) -> ( seq M ( .+ , F ) ` x ) = ( seq K ( .+ , G ) ` x ) ) ) <-> ( ph -> ( N e. ( K ... N ) -> ( seq M ( .+ , F ) ` N ) = ( seq K ( .+ , G ) ` N ) ) ) ) )
31 eluzelz 
 |-  ( K e. ( ZZ>= ` M ) -> K e. ZZ )
32 seq1 
 |-  ( K e. ZZ -> ( seq K ( .+ , G ) ` K ) = ( G ` K ) )
33 1 31 32 3syl 
 |-  ( ph -> ( seq K ( .+ , G ) ` K ) = ( G ` K ) )
34 2 33 eqtr4d 
 |-  ( ph -> ( seq M ( .+ , F ) ` K ) = ( seq K ( .+ , G ) ` K ) )
35 34 a1d 
 |-  ( ph -> ( K e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq K ( .+ , G ) ` K ) ) )
36 peano2fzr 
 |-  ( ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) -> n e. ( K ... N ) )
37 36 adantl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> n e. ( K ... N ) )
38 37 expr 
 |-  ( ( ph /\ n e. ( ZZ>= ` K ) ) -> ( ( n + 1 ) e. ( K ... N ) -> n e. ( K ... N ) ) )
39 38 imim1d 
 |-  ( ( ph /\ n e. ( ZZ>= ` K ) ) -> ( ( n e. ( K ... N ) -> ( seq M ( .+ , F ) ` n ) = ( seq K ( .+ , G ) ` n ) ) -> ( ( n + 1 ) e. ( K ... N ) -> ( seq M ( .+ , F ) ` n ) = ( seq K ( .+ , G ) ` n ) ) ) )
40 oveq1 
 |-  ( ( seq M ( .+ , F ) ` n ) = ( seq K ( .+ , G ) ` n ) -> ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) = ( ( seq K ( .+ , G ) ` n ) .+ ( F ` ( n + 1 ) ) ) )
41 simpl 
 |-  ( ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) -> n e. ( ZZ>= ` K ) )
42 uztrn 
 |-  ( ( n e. ( ZZ>= ` K ) /\ K e. ( ZZ>= ` M ) ) -> n e. ( ZZ>= ` M ) )
43 41 1 42 syl2anr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> n e. ( ZZ>= ` M ) )
44 seqp1 
 |-  ( n e. ( ZZ>= ` M ) -> ( seq M ( .+ , F ) ` ( n + 1 ) ) = ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) )
45 43 44 syl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> ( seq M ( .+ , F ) ` ( n + 1 ) ) = ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) )
46 seqp1 
 |-  ( n e. ( ZZ>= ` K ) -> ( seq K ( .+ , G ) ` ( n + 1 ) ) = ( ( seq K ( .+ , G ) ` n ) .+ ( G ` ( n + 1 ) ) ) )
47 46 ad2antrl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> ( seq K ( .+ , G ) ` ( n + 1 ) ) = ( ( seq K ( .+ , G ) ` n ) .+ ( G ` ( n + 1 ) ) ) )
48 fveq2 
 |-  ( k = ( n + 1 ) -> ( F ` k ) = ( F ` ( n + 1 ) ) )
49 fveq2 
 |-  ( k = ( n + 1 ) -> ( G ` k ) = ( G ` ( n + 1 ) ) )
50 48 49 eqeq12d 
 |-  ( k = ( n + 1 ) -> ( ( F ` k ) = ( G ` k ) <-> ( F ` ( n + 1 ) ) = ( G ` ( n + 1 ) ) ) )
51 4 ralrimiva 
 |-  ( ph -> A. k e. ( ( K + 1 ) ... N ) ( F ` k ) = ( G ` k ) )
52 51 adantr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> A. k e. ( ( K + 1 ) ... N ) ( F ` k ) = ( G ` k ) )
53 eluzp1p1 
 |-  ( n e. ( ZZ>= ` K ) -> ( n + 1 ) e. ( ZZ>= ` ( K + 1 ) ) )
54 53 ad2antrl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> ( n + 1 ) e. ( ZZ>= ` ( K + 1 ) ) )
55 elfzuz3 
 |-  ( ( n + 1 ) e. ( K ... N ) -> N e. ( ZZ>= ` ( n + 1 ) ) )
56 55 ad2antll 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> N e. ( ZZ>= ` ( n + 1 ) ) )
57 elfzuzb 
 |-  ( ( n + 1 ) e. ( ( K + 1 ) ... N ) <-> ( ( n + 1 ) e. ( ZZ>= ` ( K + 1 ) ) /\ N e. ( ZZ>= ` ( n + 1 ) ) ) )
58 54 56 57 sylanbrc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> ( n + 1 ) e. ( ( K + 1 ) ... N ) )
59 50 52 58 rspcdva 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> ( F ` ( n + 1 ) ) = ( G ` ( n + 1 ) ) )
60 59 oveq2d 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> ( ( seq K ( .+ , G ) ` n ) .+ ( F ` ( n + 1 ) ) ) = ( ( seq K ( .+ , G ) ` n ) .+ ( G ` ( n + 1 ) ) ) )
61 47 60 eqtr4d 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> ( seq K ( .+ , G ) ` ( n + 1 ) ) = ( ( seq K ( .+ , G ) ` n ) .+ ( F ` ( n + 1 ) ) ) )
62 45 61 eqeq12d 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> ( ( seq M ( .+ , F ) ` ( n + 1 ) ) = ( seq K ( .+ , G ) ` ( n + 1 ) ) <-> ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) = ( ( seq K ( .+ , G ) ` n ) .+ ( F ` ( n + 1 ) ) ) ) )
63 40 62 imbitrrid 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> ( ( seq M ( .+ , F ) ` n ) = ( seq K ( .+ , G ) ` n ) -> ( seq M ( .+ , F ) ` ( n + 1 ) ) = ( seq K ( .+ , G ) ` ( n + 1 ) ) ) )
64 39 63 animpimp2impd 
 |-  ( n e. ( ZZ>= ` K ) -> ( ( ph -> ( n e. ( K ... N ) -> ( seq M ( .+ , F ) ` n ) = ( seq K ( .+ , G ) ` n ) ) ) -> ( ph -> ( ( n + 1 ) e. ( K ... N ) -> ( seq M ( .+ , F ) ` ( n + 1 ) ) = ( seq K ( .+ , G ) ` ( n + 1 ) ) ) ) ) )
65 12 18 24 30 35 64 uzind4i 
 |-  ( N e. ( ZZ>= ` K ) -> ( ph -> ( N e. ( K ... N ) -> ( seq M ( .+ , F ) ` N ) = ( seq K ( .+ , G ) ` N ) ) ) )
66 3 65 mpcom 
 |-  ( ph -> ( N e. ( K ... N ) -> ( seq M ( .+ , F ) ` N ) = ( seq K ( .+ , G ) ` N ) ) )
67 6 66 mpd 
 |-  ( ph -> ( seq M ( .+ , F ) ` N ) = ( seq K ( .+ , G ) ` N ) )