Metamath Proof Explorer

Theorem serf0

Description: If an infinite series converges, its underlying sequence converges to zero. (Contributed by NM, 2-Sep-2005) (Revised by Mario Carneiro, 16-Feb-2014)

Ref Expression
Hypotheses caucvgb.1 
|- Z = ( ZZ>= ` M )
serf0.2 
|- ( ph -> M e. ZZ )
serf0.3 
|- ( ph -> F e. V )
serf0.4 
|- ( ph -> seq M ( + , F ) e. dom ~~> )
serf0.5 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
Assertion serf0 
|- ( ph -> F ~~> 0 )

Proof

Step Hyp Ref Expression
1 caucvgb.1 
 |-  Z = ( ZZ>= ` M )
2 serf0.2 
 |-  ( ph -> M e. ZZ )
3 serf0.3 
 |-  ( ph -> F e. V )
4 serf0.4 
 |-  ( ph -> seq M ( + , F ) e. dom ~~> )
5 serf0.5 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
6 1 caucvgb 
 |-  ( ( M e. ZZ /\ seq M ( + , F ) e. dom ~~> ) -> ( seq M ( + , F ) e. dom ~~> <-> A. x e. RR+ E. j e. Z A. m e. ( ZZ>= ` j ) ( ( seq M ( + , F ) ` m ) e. CC /\ ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` j ) ) ) < x ) ) )
7 2 4 6 syl2anc 
 |-  ( ph -> ( seq M ( + , F ) e. dom ~~> <-> A. x e. RR+ E. j e. Z A. m e. ( ZZ>= ` j ) ( ( seq M ( + , F ) ` m ) e. CC /\ ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` j ) ) ) < x ) ) )
8 4 7 mpbid 
 |-  ( ph -> A. x e. RR+ E. j e. Z A. m e. ( ZZ>= ` j ) ( ( seq M ( + , F ) ` m ) e. CC /\ ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` j ) ) ) < x ) )
9 1 cau3 
 |-  ( A. x e. RR+ E. j e. Z A. m e. ( ZZ>= ` j ) ( ( seq M ( + , F ) ` m ) e. CC /\ ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` j ) ) ) < x ) <-> A. x e. RR+ E. j e. Z A. m e. ( ZZ>= ` j ) ( ( seq M ( + , F ) ` m ) e. CC /\ A. k e. ( ZZ>= ` m ) ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` k ) ) ) < x ) )
10 8 9 sylib 
 |-  ( ph -> A. x e. RR+ E. j e. Z A. m e. ( ZZ>= ` j ) ( ( seq M ( + , F ) ` m ) e. CC /\ A. k e. ( ZZ>= ` m ) ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` k ) ) ) < x ) )
11 1 peano2uzs 
 |-  ( j e. Z -> ( j + 1 ) e. Z )
12 11 adantl 
 |-  ( ( ph /\ j e. Z ) -> ( j + 1 ) e. Z )
13 eluzelz 
 |-  ( m e. ( ZZ>= ` j ) -> m e. ZZ )
14 uzid 
 |-  ( m e. ZZ -> m e. ( ZZ>= ` m ) )
15 peano2uz 
 |-  ( m e. ( ZZ>= ` m ) -> ( m + 1 ) e. ( ZZ>= ` m ) )
16 fveq2 
 |-  ( k = ( m + 1 ) -> ( seq M ( + , F ) ` k ) = ( seq M ( + , F ) ` ( m + 1 ) ) )
17 16 oveq2d 
 |-  ( k = ( m + 1 ) -> ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` k ) ) = ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` ( m + 1 ) ) ) )
18 17 fveq2d 
 |-  ( k = ( m + 1 ) -> ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` k ) ) ) = ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` ( m + 1 ) ) ) ) )
19 18 breq1d 
 |-  ( k = ( m + 1 ) -> ( ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` k ) ) ) < x <-> ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` ( m + 1 ) ) ) ) < x ) )
20 19 rspcv 
 |-  ( ( m + 1 ) e. ( ZZ>= ` m ) -> ( A. k e. ( ZZ>= ` m ) ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` k ) ) ) < x -> ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` ( m + 1 ) ) ) ) < x ) )
21 13 14 15 20 4syl 
 |-  ( m e. ( ZZ>= ` j ) -> ( A. k e. ( ZZ>= ` m ) ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` k ) ) ) < x -> ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` ( m + 1 ) ) ) ) < x ) )
22 21 adantld 
 |-  ( m e. ( ZZ>= ` j ) -> ( ( ( seq M ( + , F ) ` m ) e. CC /\ A. k e. ( ZZ>= ` m ) ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` k ) ) ) < x ) -> ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` ( m + 1 ) ) ) ) < x ) )
23 22 ralimia 
 |-  ( A. m e. ( ZZ>= ` j ) ( ( seq M ( + , F ) ` m ) e. CC /\ A. k e. ( ZZ>= ` m ) ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` k ) ) ) < x ) -> A. m e. ( ZZ>= ` j ) ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` ( m + 1 ) ) ) ) < x )
24 simpr 
 |-  ( ( ph /\ j e. Z ) -> j e. Z )
25 24 1 eleqtrdi 
 |-  ( ( ph /\ j e. Z ) -> j e. ( ZZ>= ` M ) )
26 eluzelz 
 |-  ( j e. ( ZZ>= ` M ) -> j e. ZZ )
27 25 26 syl 
 |-  ( ( ph /\ j e. Z ) -> j e. ZZ )
28 eluzp1m1 
 |-  ( ( j e. ZZ /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> ( k - 1 ) e. ( ZZ>= ` j ) )
29 27 28 sylan 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> ( k - 1 ) e. ( ZZ>= ` j ) )
30 fveq2 
 |-  ( m = ( k - 1 ) -> ( seq M ( + , F ) ` m ) = ( seq M ( + , F ) ` ( k - 1 ) ) )
31 fvoveq1 
 |-  ( m = ( k - 1 ) -> ( seq M ( + , F ) ` ( m + 1 ) ) = ( seq M ( + , F ) ` ( ( k - 1 ) + 1 ) ) )
32 30 31 oveq12d 
 |-  ( m = ( k - 1 ) -> ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` ( m + 1 ) ) ) = ( ( seq M ( + , F ) ` ( k - 1 ) ) - ( seq M ( + , F ) ` ( ( k - 1 ) + 1 ) ) ) )
33 32 fveq2d 
 |-  ( m = ( k - 1 ) -> ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` ( m + 1 ) ) ) ) = ( abs ` ( ( seq M ( + , F ) ` ( k - 1 ) ) - ( seq M ( + , F ) ` ( ( k - 1 ) + 1 ) ) ) ) )
34 33 breq1d 
 |-  ( m = ( k - 1 ) -> ( ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` ( m + 1 ) ) ) ) < x <-> ( abs ` ( ( seq M ( + , F ) ` ( k - 1 ) ) - ( seq M ( + , F ) ` ( ( k - 1 ) + 1 ) ) ) ) < x ) )
35 34 rspcv 
 |-  ( ( k - 1 ) e. ( ZZ>= ` j ) -> ( A. m e. ( ZZ>= ` j ) ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` ( m + 1 ) ) ) ) < x -> ( abs ` ( ( seq M ( + , F ) ` ( k - 1 ) ) - ( seq M ( + , F ) ` ( ( k - 1 ) + 1 ) ) ) ) < x ) )
36 29 35 syl 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> ( A. m e. ( ZZ>= ` j ) ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` ( m + 1 ) ) ) ) < x -> ( abs ` ( ( seq M ( + , F ) ` ( k - 1 ) ) - ( seq M ( + , F ) ` ( ( k - 1 ) + 1 ) ) ) ) < x ) )
37 1 2 5 serf 
 |-  ( ph -> seq M ( + , F ) : Z --> CC )
38 37 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> seq M ( + , F ) : Z --> CC )
39 1 uztrn2 
 |-  ( ( j e. Z /\ ( k - 1 ) e. ( ZZ>= ` j ) ) -> ( k - 1 ) e. Z )
40 24 29 39 syl2an2r 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> ( k - 1 ) e. Z )
41 38 40 ffvelcdmd 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> ( seq M ( + , F ) ` ( k - 1 ) ) e. CC )
42 1 uztrn2 
 |-  ( ( ( j + 1 ) e. Z /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> k e. Z )
43 12 42 sylan 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> k e. Z )
44 38 43 ffvelcdmd 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> ( seq M ( + , F ) ` k ) e. CC )
45 41 44 abssubd 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> ( abs ` ( ( seq M ( + , F ) ` ( k - 1 ) ) - ( seq M ( + , F ) ` k ) ) ) = ( abs ` ( ( seq M ( + , F ) ` k ) - ( seq M ( + , F ) ` ( k - 1 ) ) ) ) )
46 eluzelz 
 |-  ( k e. ( ZZ>= ` ( j + 1 ) ) -> k e. ZZ )
47 46 adantl 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> k e. ZZ )
48 47 zcnd 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> k e. CC )
49 ax-1cn 
 |-  1 e. CC
50 npcan 
 |-  ( ( k e. CC /\ 1 e. CC ) -> ( ( k - 1 ) + 1 ) = k )
51 48 49 50 sylancl 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> ( ( k - 1 ) + 1 ) = k )
52 51 fveq2d 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> ( seq M ( + , F ) ` ( ( k - 1 ) + 1 ) ) = ( seq M ( + , F ) ` k ) )
53 52 oveq2d 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> ( ( seq M ( + , F ) ` ( k - 1 ) ) - ( seq M ( + , F ) ` ( ( k - 1 ) + 1 ) ) ) = ( ( seq M ( + , F ) ` ( k - 1 ) ) - ( seq M ( + , F ) ` k ) ) )
54 53 fveq2d 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> ( abs ` ( ( seq M ( + , F ) ` ( k - 1 ) ) - ( seq M ( + , F ) ` ( ( k - 1 ) + 1 ) ) ) ) = ( abs ` ( ( seq M ( + , F ) ` ( k - 1 ) ) - ( seq M ( + , F ) ` k ) ) ) )
55 2 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> M e. ZZ )
56 eluzp1p1 
 |-  ( j e. ( ZZ>= ` M ) -> ( j + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
57 25 56 syl 
 |-  ( ( ph /\ j e. Z ) -> ( j + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
58 eqid 
 |-  ( ZZ>= ` ( M + 1 ) ) = ( ZZ>= ` ( M + 1 ) )
59 58 uztrn2 
 |-  ( ( ( j + 1 ) e. ( ZZ>= ` ( M + 1 ) ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> k e. ( ZZ>= ` ( M + 1 ) ) )
60 57 59 sylan 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> k e. ( ZZ>= ` ( M + 1 ) ) )
61 seqm1 
 |-  ( ( M e. ZZ /\ k e. ( ZZ>= ` ( M + 1 ) ) ) -> ( seq M ( + , F ) ` k ) = ( ( seq M ( + , F ) ` ( k - 1 ) ) + ( F ` k ) ) )
62 55 60 61 syl2anc 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> ( seq M ( + , F ) ` k ) = ( ( seq M ( + , F ) ` ( k - 1 ) ) + ( F ` k ) ) )
63 62 oveq1d 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> ( ( seq M ( + , F ) ` k ) - ( seq M ( + , F ) ` ( k - 1 ) ) ) = ( ( ( seq M ( + , F ) ` ( k - 1 ) ) + ( F ` k ) ) - ( seq M ( + , F ) ` ( k - 1 ) ) ) )
64 5 adantlr 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. Z ) -> ( F ` k ) e. CC )
65 43 64 syldan 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> ( F ` k ) e. CC )
66 41 65 pncan2d 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> ( ( ( seq M ( + , F ) ` ( k - 1 ) ) + ( F ` k ) ) - ( seq M ( + , F ) ` ( k - 1 ) ) ) = ( F ` k ) )
67 63 66 eqtr2d 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> ( F ` k ) = ( ( seq M ( + , F ) ` k ) - ( seq M ( + , F ) ` ( k - 1 ) ) ) )
68 67 fveq2d 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> ( abs ` ( F ` k ) ) = ( abs ` ( ( seq M ( + , F ) ` k ) - ( seq M ( + , F ) ` ( k - 1 ) ) ) ) )
69 45 54 68 3eqtr4d 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> ( abs ` ( ( seq M ( + , F ) ` ( k - 1 ) ) - ( seq M ( + , F ) ` ( ( k - 1 ) + 1 ) ) ) ) = ( abs ` ( F ` k ) ) )
70 69 breq1d 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> ( ( abs ` ( ( seq M ( + , F ) ` ( k - 1 ) ) - ( seq M ( + , F ) ` ( ( k - 1 ) + 1 ) ) ) ) < x <-> ( abs ` ( F ` k ) ) < x ) )
71 36 70 sylibd 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> ( A. m e. ( ZZ>= ` j ) ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` ( m + 1 ) ) ) ) < x -> ( abs ` ( F ` k ) ) < x ) )
72 71 ralrimdva 
 |-  ( ( ph /\ j e. Z ) -> ( A. m e. ( ZZ>= ` j ) ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` ( m + 1 ) ) ) ) < x -> A. k e. ( ZZ>= ` ( j + 1 ) ) ( abs ` ( F ` k ) ) < x ) )
73 23 72 syl5 
 |-  ( ( ph /\ j e. Z ) -> ( A. m e. ( ZZ>= ` j ) ( ( seq M ( + , F ) ` m ) e. CC /\ A. k e. ( ZZ>= ` m ) ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` k ) ) ) < x ) -> A. k e. ( ZZ>= ` ( j + 1 ) ) ( abs ` ( F ` k ) ) < x ) )
74 fveq2 
 |-  ( n = ( j + 1 ) -> ( ZZ>= ` n ) = ( ZZ>= ` ( j + 1 ) ) )
75 74 raleqdv 
 |-  ( n = ( j + 1 ) -> ( A. k e. ( ZZ>= ` n ) ( abs ` ( F ` k ) ) < x <-> A. k e. ( ZZ>= ` ( j + 1 ) ) ( abs ` ( F ` k ) ) < x ) )
76 75 rspcev 
 |-  ( ( ( j + 1 ) e. Z /\ A. k e. ( ZZ>= ` ( j + 1 ) ) ( abs ` ( F ` k ) ) < x ) -> E. n e. Z A. k e. ( ZZ>= ` n ) ( abs ` ( F ` k ) ) < x )
77 12 73 76 syl6an 
 |-  ( ( ph /\ j e. Z ) -> ( A. m e. ( ZZ>= ` j ) ( ( seq M ( + , F ) ` m ) e. CC /\ A. k e. ( ZZ>= ` m ) ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` k ) ) ) < x ) -> E. n e. Z A. k e. ( ZZ>= ` n ) ( abs ` ( F ` k ) ) < x ) )
78 77 rexlimdva 
 |-  ( ph -> ( E. j e. Z A. m e. ( ZZ>= ` j ) ( ( seq M ( + , F ) ` m ) e. CC /\ A. k e. ( ZZ>= ` m ) ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` k ) ) ) < x ) -> E. n e. Z A. k e. ( ZZ>= ` n ) ( abs ` ( F ` k ) ) < x ) )
79 78 ralimdv 
 |-  ( ph -> ( A. x e. RR+ E. j e. Z A. m e. ( ZZ>= ` j ) ( ( seq M ( + , F ) ` m ) e. CC /\ A. k e. ( ZZ>= ` m ) ( abs ` ( ( seq M ( + , F ) ` m ) - ( seq M ( + , F ) ` k ) ) ) < x ) -> A. x e. RR+ E. n e. Z A. k e. ( ZZ>= ` n ) ( abs ` ( F ` k ) ) < x ) )
80 10 79 mpd 
 |-  ( ph -> A. x e. RR+ E. n e. Z A. k e. ( ZZ>= ` n ) ( abs ` ( F ` k ) ) < x )
81 eqidd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = ( F ` k ) )
82 1 2 3 81 5 clim0c 
 |-  ( ph -> ( F ~~> 0 <-> A. x e. RR+ E. n e. Z A. k e. ( ZZ>= ` n ) ( abs ` ( F ` k ) ) < x ) )
83 80 82 mpbird 
 |-  ( ph -> F ~~> 0 )