Metamath Proof Explorer

Theorem explecnv

Description: A sequence of terms converges to zero when it is less than powers of a number A whose absolute value is smaller than 1. (Contributed by NM, 19-Jul-2008) (Revised by Mario Carneiro, 26-Apr-2014)

Ref Expression
Hypotheses explecnv.1 
|- Z = ( ZZ>= ` M )
explecnv.2 
|- ( ph -> F e. V )
explecnv.3 
|- ( ph -> M e. ZZ )
explecnv.5 
|- ( ph -> A e. RR )
explecnv.4 
|- ( ph -> ( abs ` A ) < 1 )
explecnv.6 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
explecnv.7 
|- ( ( ph /\ k e. Z ) -> ( abs ` ( F ` k ) ) <_ ( A ^ k ) )
Assertion explecnv 
|- ( ph -> F ~~> 0 )

Proof

Step Hyp Ref Expression
1 explecnv.1 
 |-  Z = ( ZZ>= ` M )
2 explecnv.2 
 |-  ( ph -> F e. V )
3 explecnv.3 
 |-  ( ph -> M e. ZZ )
4 explecnv.5 
 |-  ( ph -> A e. RR )
5 explecnv.4 
 |-  ( ph -> ( abs ` A ) < 1 )
6 explecnv.6 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
7 explecnv.7 
 |-  ( ( ph /\ k e. Z ) -> ( abs ` ( F ` k ) ) <_ ( A ^ k ) )
8 eqid 
 |-  ( ZZ>= ` if ( M <_ 0 , 0 , M ) ) = ( ZZ>= ` if ( M <_ 0 , 0 , M ) )
9 0z 
 |-  0 e. ZZ
10 ifcl 
 |-  ( ( 0 e. ZZ /\ M e. ZZ ) -> if ( M <_ 0 , 0 , M ) e. ZZ )
11 9 3 10 sylancr 
 |-  ( ph -> if ( M <_ 0 , 0 , M ) e. ZZ )
12 4 recnd 
 |-  ( ph -> A e. CC )
13 12 5 expcnv 
 |-  ( ph -> ( n e. NN0 |-> ( A ^ n ) ) ~~> 0 )
14 1 fvexi 
 |-  Z e. _V
15 14 mptex 
 |-  ( n e. Z |-> ( abs ` ( F ` n ) ) ) e. _V
16 15 a1i 
 |-  ( ph -> ( n e. Z |-> ( abs ` ( F ` n ) ) ) e. _V )
17 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
18 1 17 ineq12i 
 |-  ( Z i^i NN0 ) = ( ( ZZ>= ` M ) i^i ( ZZ>= ` 0 ) )
19 uzin 
 |-  ( ( M e. ZZ /\ 0 e. ZZ ) -> ( ( ZZ>= ` M ) i^i ( ZZ>= ` 0 ) ) = ( ZZ>= ` if ( M <_ 0 , 0 , M ) ) )
20 3 9 19 sylancl 
 |-  ( ph -> ( ( ZZ>= ` M ) i^i ( ZZ>= ` 0 ) ) = ( ZZ>= ` if ( M <_ 0 , 0 , M ) ) )
21 18 20 syl5req 
 |-  ( ph -> ( ZZ>= ` if ( M <_ 0 , 0 , M ) ) = ( Z i^i NN0 ) )
22 21 eleq2d 
 |-  ( ph -> ( k e. ( ZZ>= ` if ( M <_ 0 , 0 , M ) ) <-> k e. ( Z i^i NN0 ) ) )
23 22 biimpa 
 |-  ( ( ph /\ k e. ( ZZ>= ` if ( M <_ 0 , 0 , M ) ) ) -> k e. ( Z i^i NN0 ) )
24 23 elin2d 
 |-  ( ( ph /\ k e. ( ZZ>= ` if ( M <_ 0 , 0 , M ) ) ) -> k e. NN0 )
25 oveq2 
 |-  ( n = k -> ( A ^ n ) = ( A ^ k ) )
26 eqid 
 |-  ( n e. NN0 |-> ( A ^ n ) ) = ( n e. NN0 |-> ( A ^ n ) )
27 ovex 
 |-  ( A ^ k ) e. _V
28 25 26 27 fvmpt 
 |-  ( k e. NN0 -> ( ( n e. NN0 |-> ( A ^ n ) ) ` k ) = ( A ^ k ) )
29 24 28 syl 
 |-  ( ( ph /\ k e. ( ZZ>= ` if ( M <_ 0 , 0 , M ) ) ) -> ( ( n e. NN0 |-> ( A ^ n ) ) ` k ) = ( A ^ k ) )
30 4 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` if ( M <_ 0 , 0 , M ) ) ) -> A e. RR )
31 30 24 reexpcld 
 |-  ( ( ph /\ k e. ( ZZ>= ` if ( M <_ 0 , 0 , M ) ) ) -> ( A ^ k ) e. RR )
32 29 31 eqeltrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` if ( M <_ 0 , 0 , M ) ) ) -> ( ( n e. NN0 |-> ( A ^ n ) ) ` k ) e. RR )
33 23 elin1d 
 |-  ( ( ph /\ k e. ( ZZ>= ` if ( M <_ 0 , 0 , M ) ) ) -> k e. Z )
34 2fveq3 
 |-  ( n = k -> ( abs ` ( F ` n ) ) = ( abs ` ( F ` k ) ) )
35 eqid 
 |-  ( n e. Z |-> ( abs ` ( F ` n ) ) ) = ( n e. Z |-> ( abs ` ( F ` n ) ) )
36 fvex 
 |-  ( abs ` ( F ` k ) ) e. _V
37 34 35 36 fvmpt 
 |-  ( k e. Z -> ( ( n e. Z |-> ( abs ` ( F ` n ) ) ) ` k ) = ( abs ` ( F ` k ) ) )
38 33 37 syl 
 |-  ( ( ph /\ k e. ( ZZ>= ` if ( M <_ 0 , 0 , M ) ) ) -> ( ( n e. Z |-> ( abs ` ( F ` n ) ) ) ` k ) = ( abs ` ( F ` k ) ) )
39 33 6 syldan 
 |-  ( ( ph /\ k e. ( ZZ>= ` if ( M <_ 0 , 0 , M ) ) ) -> ( F ` k ) e. CC )
40 39 abscld 
 |-  ( ( ph /\ k e. ( ZZ>= ` if ( M <_ 0 , 0 , M ) ) ) -> ( abs ` ( F ` k ) ) e. RR )
41 38 40 eqeltrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` if ( M <_ 0 , 0 , M ) ) ) -> ( ( n e. Z |-> ( abs ` ( F ` n ) ) ) ` k ) e. RR )
42 33 7 syldan 
 |-  ( ( ph /\ k e. ( ZZ>= ` if ( M <_ 0 , 0 , M ) ) ) -> ( abs ` ( F ` k ) ) <_ ( A ^ k ) )
43 42 38 29 3brtr4d 
 |-  ( ( ph /\ k e. ( ZZ>= ` if ( M <_ 0 , 0 , M ) ) ) -> ( ( n e. Z |-> ( abs ` ( F ` n ) ) ) ` k ) <_ ( ( n e. NN0 |-> ( A ^ n ) ) ` k ) )
44 39 absge0d 
 |-  ( ( ph /\ k e. ( ZZ>= ` if ( M <_ 0 , 0 , M ) ) ) -> 0 <_ ( abs ` ( F ` k ) ) )
45 44 38 breqtrrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` if ( M <_ 0 , 0 , M ) ) ) -> 0 <_ ( ( n e. Z |-> ( abs ` ( F ` n ) ) ) ` k ) )
46 8 11 13 16 32 41 43 45 climsqz2 
 |-  ( ph -> ( n e. Z |-> ( abs ` ( F ` n ) ) ) ~~> 0 )
47 37 adantl 
 |-  ( ( ph /\ k e. Z ) -> ( ( n e. Z |-> ( abs ` ( F ` n ) ) ) ` k ) = ( abs ` ( F ` k ) ) )
48 1 3 2 16 6 47 climabs0 
 |-  ( ph -> ( F ~~> 0 <-> ( n e. Z |-> ( abs ` ( F ` n ) ) ) ~~> 0 ) )
49 46 48 mpbird 
 |-  ( ph -> F ~~> 0 )