Metamath Proof Explorer

Theorem seqid2

Description: The last few partial sums of a sequence that ends with all zeroes (or any element which is a right-identity for .+ ) are all the same. (Contributed by Mario Carneiro, 13-Jul-2013) (Revised by Mario Carneiro, 27-May-2014)

Ref Expression
Hypotheses seqid2.1 
|- ( ( ph /\ x e. S ) -> ( x .+ Z ) = x )
seqid2.2 
|- ( ph -> K e. ( ZZ>= ` M ) )
seqid2.3 
|- ( ph -> N e. ( ZZ>= ` K ) )
seqid2.4 
|- ( ph -> ( seq M ( .+ , F ) ` K ) e. S )
seqid2.5 
|- ( ( ph /\ x e. ( ( K + 1 ) ... N ) ) -> ( F ` x ) = Z )
Assertion seqid2 
|- ( ph -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` N ) )

Proof

Step Hyp Ref Expression
1 seqid2.1 
 |-  ( ( ph /\ x e. S ) -> ( x .+ Z ) = x )
2 seqid2.2 
 |-  ( ph -> K e. ( ZZ>= ` M ) )
3 seqid2.3 
 |-  ( ph -> N e. ( ZZ>= ` K ) )
4 seqid2.4 
 |-  ( ph -> ( seq M ( .+ , F ) ` K ) e. S )
5 seqid2.5 
 |-  ( ( ph /\ x e. ( ( K + 1 ) ... N ) ) -> ( F ` x ) = Z )
6 eluzfz2 
 |-  ( N e. ( ZZ>= ` K ) -> N e. ( K ... N ) )
7 3 6 syl 
 |-  ( ph -> N e. ( K ... N ) )
8 eleq1 
 |-  ( x = K -> ( x e. ( K ... N ) <-> K e. ( K ... N ) ) )
9 fveq2 
 |-  ( x = K -> ( seq M ( .+ , F ) ` x ) = ( seq M ( .+ , F ) ` K ) )
10 9 eqeq2d 
 |-  ( x = K -> ( ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` x ) <-> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` K ) ) )
11 8 10 imbi12d 
 |-  ( x = K -> ( ( x e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` x ) ) <-> ( K e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` K ) ) ) )
12 11 imbi2d 
 |-  ( x = K -> ( ( ph -> ( x e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` x ) ) ) <-> ( ph -> ( K e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` 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 14 eqeq2d 
 |-  ( x = n -> ( ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` x ) <-> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` n ) ) )
16 13 15 imbi12d 
 |-  ( x = n -> ( ( x e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` x ) ) <-> ( n e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` n ) ) ) )
17 16 imbi2d 
 |-  ( x = n -> ( ( ph -> ( x e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` x ) ) ) <-> ( ph -> ( n e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` n ) ) ) ) )
18 eleq1 
 |-  ( x = ( n + 1 ) -> ( x e. ( K ... N ) <-> ( n + 1 ) e. ( K ... N ) ) )
19 fveq2 
 |-  ( x = ( n + 1 ) -> ( seq M ( .+ , F ) ` x ) = ( seq M ( .+ , F ) ` ( n + 1 ) ) )
20 19 eqeq2d 
 |-  ( x = ( n + 1 ) -> ( ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` x ) <-> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` ( n + 1 ) ) ) )
21 18 20 imbi12d 
 |-  ( x = ( n + 1 ) -> ( ( x e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` x ) ) <-> ( ( n + 1 ) e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` ( n + 1 ) ) ) ) )
22 21 imbi2d 
 |-  ( x = ( n + 1 ) -> ( ( ph -> ( x e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` x ) ) ) <-> ( ph -> ( ( n + 1 ) e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` ( n + 1 ) ) ) ) ) )
23 eleq1 
 |-  ( x = N -> ( x e. ( K ... N ) <-> N e. ( K ... N ) ) )
24 fveq2 
 |-  ( x = N -> ( seq M ( .+ , F ) ` x ) = ( seq M ( .+ , F ) ` N ) )
25 24 eqeq2d 
 |-  ( x = N -> ( ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` x ) <-> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` N ) ) )
26 23 25 imbi12d 
 |-  ( x = N -> ( ( x e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` x ) ) <-> ( N e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` N ) ) ) )
27 26 imbi2d 
 |-  ( x = N -> ( ( ph -> ( x e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` x ) ) ) <-> ( ph -> ( N e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` N ) ) ) ) )
28 eqidd 
 |-  ( K e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` K ) )
29 28 2a1i 
 |-  ( K e. ZZ -> ( ph -> ( K e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` K ) ) ) )
30 peano2fzr 
 |-  ( ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) -> n e. ( K ... N ) )
31 30 adantl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> n e. ( K ... N ) )
32 31 expr 
 |-  ( ( ph /\ n e. ( ZZ>= ` K ) ) -> ( ( n + 1 ) e. ( K ... N ) -> n e. ( K ... N ) ) )
33 32 imim1d 
 |-  ( ( ph /\ n e. ( ZZ>= ` K ) ) -> ( ( n e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` n ) ) -> ( ( n + 1 ) e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` n ) ) ) )
34 oveq1 
 |-  ( ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` n ) -> ( ( seq M ( .+ , F ) ` K ) .+ ( F ` ( n + 1 ) ) ) = ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) )
35 fveqeq2 
 |-  ( x = ( n + 1 ) -> ( ( F ` x ) = Z <-> ( F ` ( n + 1 ) ) = Z ) )
36 5 ralrimiva 
 |-  ( ph -> A. x e. ( ( K + 1 ) ... N ) ( F ` x ) = Z )
37 36 adantr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> A. x e. ( ( K + 1 ) ... N ) ( F ` x ) = Z )
38 eluzp1p1 
 |-  ( n e. ( ZZ>= ` K ) -> ( n + 1 ) e. ( ZZ>= ` ( K + 1 ) ) )
39 38 ad2antrl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> ( n + 1 ) e. ( ZZ>= ` ( K + 1 ) ) )
40 elfzuz3 
 |-  ( ( n + 1 ) e. ( K ... N ) -> N e. ( ZZ>= ` ( n + 1 ) ) )
41 40 ad2antll 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> N e. ( ZZ>= ` ( n + 1 ) ) )
42 elfzuzb 
 |-  ( ( n + 1 ) e. ( ( K + 1 ) ... N ) <-> ( ( n + 1 ) e. ( ZZ>= ` ( K + 1 ) ) /\ N e. ( ZZ>= ` ( n + 1 ) ) ) )
43 39 41 42 sylanbrc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> ( n + 1 ) e. ( ( K + 1 ) ... N ) )
44 35 37 43 rspcdva 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> ( F ` ( n + 1 ) ) = Z )
45 44 oveq2d 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> ( ( seq M ( .+ , F ) ` K ) .+ ( F ` ( n + 1 ) ) ) = ( ( seq M ( .+ , F ) ` K ) .+ Z ) )
46 oveq1 
 |-  ( x = ( seq M ( .+ , F ) ` K ) -> ( x .+ Z ) = ( ( seq M ( .+ , F ) ` K ) .+ Z ) )
47 id 
 |-  ( x = ( seq M ( .+ , F ) ` K ) -> x = ( seq M ( .+ , F ) ` K ) )
48 46 47 eqeq12d 
 |-  ( x = ( seq M ( .+ , F ) ` K ) -> ( ( x .+ Z ) = x <-> ( ( seq M ( .+ , F ) ` K ) .+ Z ) = ( seq M ( .+ , F ) ` K ) ) )
49 1 ralrimiva 
 |-  ( ph -> A. x e. S ( x .+ Z ) = x )
50 48 49 4 rspcdva 
 |-  ( ph -> ( ( seq M ( .+ , F ) ` K ) .+ Z ) = ( seq M ( .+ , F ) ` K ) )
51 50 adantr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> ( ( seq M ( .+ , F ) ` K ) .+ Z ) = ( seq M ( .+ , F ) ` K ) )
52 45 51 eqtr2d 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> ( seq M ( .+ , F ) ` K ) = ( ( seq M ( .+ , F ) ` K ) .+ ( F ` ( n + 1 ) ) ) )
53 simprl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> n e. ( ZZ>= ` K ) )
54 2 adantr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> K e. ( ZZ>= ` M ) )
55 uztrn 
 |-  ( ( n e. ( ZZ>= ` K ) /\ K e. ( ZZ>= ` M ) ) -> n e. ( ZZ>= ` M ) )
56 53 54 55 syl2anc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> n e. ( ZZ>= ` M ) )
57 seqp1 
 |-  ( n e. ( ZZ>= ` M ) -> ( seq M ( .+ , F ) ` ( n + 1 ) ) = ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) )
58 56 57 syl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> ( seq M ( .+ , F ) ` ( n + 1 ) ) = ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) )
59 52 58 eqeq12d 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> ( ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` ( n + 1 ) ) <-> ( ( seq M ( .+ , F ) ` K ) .+ ( F ` ( n + 1 ) ) ) = ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) ) )
60 34 59 syl5ibr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` K ) /\ ( n + 1 ) e. ( K ... N ) ) ) -> ( ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` n ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` ( n + 1 ) ) ) )
61 33 60 animpimp2impd 
 |-  ( n e. ( ZZ>= ` K ) -> ( ( ph -> ( n e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` n ) ) ) -> ( ph -> ( ( n + 1 ) e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` ( n + 1 ) ) ) ) ) )
62 12 17 22 27 29 61 uzind4 
 |-  ( N e. ( ZZ>= ` K ) -> ( ph -> ( N e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` N ) ) ) )
63 3 62 mpcom 
 |-  ( ph -> ( N e. ( K ... N ) -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` N ) ) )
64 7 63 mpd 
 |-  ( ph -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` N ) )