This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem climabs0

Description: Convergence to zero of the absolute value is equivalent to convergence to zero. (Contributed by NM, 8-Jul-2008) (Revised by Mario Carneiro, 31-Jan-2014)

Ref Expression
Hypotheses climabs0.1 
|- Z = ( ZZ>= ` M )
climabs0.2 
|- ( ph -> M e. ZZ )
climabs0.3 
|- ( ph -> F e. V )
climabs0.4 
|- ( ph -> G e. W )
climabs0.5 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
climabs0.6 
|- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( abs ` ( F ` k ) ) )
Assertion climabs0 
|- ( ph -> ( F ~~> 0 <-> G ~~> 0 ) )

Proof

Step Hyp Ref Expression
1 climabs0.1 
 |-  Z = ( ZZ>= ` M )
2 climabs0.2 
 |-  ( ph -> M e. ZZ )
3 climabs0.3 
 |-  ( ph -> F e. V )
4 climabs0.4 
 |-  ( ph -> G e. W )
5 climabs0.5 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
6 climabs0.6 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) = ( abs ` ( F ` k ) ) )
7 1 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
8 absidm 
 |-  ( ( F ` k ) e. CC -> ( abs ` ( abs ` ( F ` k ) ) ) = ( abs ` ( F ` k ) ) )
9 5 8 syl 
 |-  ( ( ph /\ k e. Z ) -> ( abs ` ( abs ` ( F ` k ) ) ) = ( abs ` ( F ` k ) ) )
10 9 breq1d 
 |-  ( ( ph /\ k e. Z ) -> ( ( abs ` ( abs ` ( F ` k ) ) ) < x <-> ( abs ` ( F ` k ) ) < x ) )
11 7 10 sylan2 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( abs ` ( abs ` ( F ` k ) ) ) < x <-> ( abs ` ( F ` k ) ) < x ) )
12 11 anassrs 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( abs ` ( abs ` ( F ` k ) ) ) < x <-> ( abs ` ( F ` k ) ) < x ) )
13 12 ralbidva 
 |-  ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( abs ` ( F ` k ) ) ) < x <-> A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < x ) )
14 13 rexbidva 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( abs ` ( F ` k ) ) ) < x <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < x ) )
15 14 ralbidv 
 |-  ( ph -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( abs ` ( F ` k ) ) ) < x <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < x ) )
16 5 abscld 
 |-  ( ( ph /\ k e. Z ) -> ( abs ` ( F ` k ) ) e. RR )
17 16 recnd 
 |-  ( ( ph /\ k e. Z ) -> ( abs ` ( F ` k ) ) e. CC )
18 1 2 4 6 17 clim0c 
 |-  ( ph -> ( G ~~> 0 <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( abs ` ( F ` k ) ) ) < x ) )
19 eqidd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = ( F ` k ) )
20 1 2 3 19 5 clim0c 
 |-  ( ph -> ( F ~~> 0 <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < x ) )
21 15 18 20 3bitr4rd 
 |-  ( ph -> ( F ~~> 0 <-> G ~~> 0 ) )