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 φxSx+˙Z=x
seqid2.2 φKM
seqid2.3 φNK
seqid2.4 φseqM+˙FKS
seqid2.5 φxK+1NFx=Z
Assertion seqid2 φseqM+˙FK=seqM+˙FN

Proof

Step Hyp Ref Expression
1 seqid2.1 φxSx+˙Z=x
2 seqid2.2 φKM
3 seqid2.3 φNK
4 seqid2.4 φseqM+˙FKS
5 seqid2.5 φxK+1NFx=Z
6 eluzfz2 NKNKN
7 3 6 syl φNKN
8 eleq1 x=KxKNKKN
9 fveq2 x=KseqM+˙Fx=seqM+˙FK
10 9 eqeq2d x=KseqM+˙FK=seqM+˙FxseqM+˙FK=seqM+˙FK
11 8 10 imbi12d x=KxKNseqM+˙FK=seqM+˙FxKKNseqM+˙FK=seqM+˙FK
12 11 imbi2d x=KφxKNseqM+˙FK=seqM+˙FxφKKNseqM+˙FK=seqM+˙FK
13 eleq1 x=nxKNnKN
14 fveq2 x=nseqM+˙Fx=seqM+˙Fn
15 14 eqeq2d x=nseqM+˙FK=seqM+˙FxseqM+˙FK=seqM+˙Fn
16 13 15 imbi12d x=nxKNseqM+˙FK=seqM+˙FxnKNseqM+˙FK=seqM+˙Fn
17 16 imbi2d x=nφxKNseqM+˙FK=seqM+˙FxφnKNseqM+˙FK=seqM+˙Fn
18 eleq1 x=n+1xKNn+1KN
19 fveq2 x=n+1seqM+˙Fx=seqM+˙Fn+1
20 19 eqeq2d x=n+1seqM+˙FK=seqM+˙FxseqM+˙FK=seqM+˙Fn+1
21 18 20 imbi12d x=n+1xKNseqM+˙FK=seqM+˙Fxn+1KNseqM+˙FK=seqM+˙Fn+1
22 21 imbi2d x=n+1φxKNseqM+˙FK=seqM+˙Fxφn+1KNseqM+˙FK=seqM+˙Fn+1
23 eleq1 x=NxKNNKN
24 fveq2 x=NseqM+˙Fx=seqM+˙FN
25 24 eqeq2d x=NseqM+˙FK=seqM+˙FxseqM+˙FK=seqM+˙FN
26 23 25 imbi12d x=NxKNseqM+˙FK=seqM+˙FxNKNseqM+˙FK=seqM+˙FN
27 26 imbi2d x=NφxKNseqM+˙FK=seqM+˙FxφNKNseqM+˙FK=seqM+˙FN
28 eqidd KKNseqM+˙FK=seqM+˙FK
29 28 2a1i KφKKNseqM+˙FK=seqM+˙FK
30 peano2fzr nKn+1KNnKN
31 30 adantl φnKn+1KNnKN
32 31 expr φnKn+1KNnKN
33 32 imim1d φnKnKNseqM+˙FK=seqM+˙Fnn+1KNseqM+˙FK=seqM+˙Fn
34 oveq1 seqM+˙FK=seqM+˙FnseqM+˙FK+˙Fn+1=seqM+˙Fn+˙Fn+1
35 fveqeq2 x=n+1Fx=ZFn+1=Z
36 5 ralrimiva φxK+1NFx=Z
37 36 adantr φnKn+1KNxK+1NFx=Z
38 eluzp1p1 nKn+1K+1
39 38 ad2antrl φnKn+1KNn+1K+1
40 elfzuz3 n+1KNNn+1
41 40 ad2antll φnKn+1KNNn+1
42 elfzuzb n+1K+1Nn+1K+1Nn+1
43 39 41 42 sylanbrc φnKn+1KNn+1K+1N
44 35 37 43 rspcdva φnKn+1KNFn+1=Z
45 44 oveq2d φnKn+1KNseqM+˙FK+˙Fn+1=seqM+˙FK+˙Z
46 oveq1 x=seqM+˙FKx+˙Z=seqM+˙FK+˙Z
47 id x=seqM+˙FKx=seqM+˙FK
48 46 47 eqeq12d x=seqM+˙FKx+˙Z=xseqM+˙FK+˙Z=seqM+˙FK
49 1 ralrimiva φxSx+˙Z=x
50 48 49 4 rspcdva φseqM+˙FK+˙Z=seqM+˙FK
51 50 adantr φnKn+1KNseqM+˙FK+˙Z=seqM+˙FK
52 45 51 eqtr2d φnKn+1KNseqM+˙FK=seqM+˙FK+˙Fn+1
53 simprl φnKn+1KNnK
54 2 adantr φnKn+1KNKM
55 uztrn nKKMnM
56 53 54 55 syl2anc φnKn+1KNnM
57 seqp1 nMseqM+˙Fn+1=seqM+˙Fn+˙Fn+1
58 56 57 syl φnKn+1KNseqM+˙Fn+1=seqM+˙Fn+˙Fn+1
59 52 58 eqeq12d φnKn+1KNseqM+˙FK=seqM+˙Fn+1seqM+˙FK+˙Fn+1=seqM+˙Fn+˙Fn+1
60 34 59 imbitrrid φnKn+1KNseqM+˙FK=seqM+˙FnseqM+˙FK=seqM+˙Fn+1
61 33 60 animpimp2impd nKφnKNseqM+˙FK=seqM+˙Fnφn+1KNseqM+˙FK=seqM+˙Fn+1
62 12 17 22 27 29 61 uzind4 NKφNKNseqM+˙FK=seqM+˙FN
63 3 62 mpcom φNKNseqM+˙FK=seqM+˙FN
64 7 63 mpd φseqM+˙FK=seqM+˙FN