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