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 ) )