Metamath Proof Explorer

Theorem clim0c

Description: Express the predicate F converges to 0 . (Contributed by NM, 24-Feb-2008) (Revised by Mario Carneiro, 31-Jan-2014)

Ref Expression
Hypotheses clim0.1 
|- Z = ( ZZ>= ` M )
clim0.2 
|- ( ph -> M e. ZZ )
clim0.3 
|- ( ph -> F e. V )
clim0.4 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
clim0c.6 
|- ( ( ph /\ k e. Z ) -> B e. CC )
Assertion clim0c 
|- ( ph -> ( F ~~> 0 <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` B ) < x ) )

Proof

Step Hyp Ref Expression
1 clim0.1 
 |-  Z = ( ZZ>= ` M )
2 clim0.2 
 |-  ( ph -> M e. ZZ )
3 clim0.3 
 |-  ( ph -> F e. V )
4 clim0.4 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
5 clim0c.6 
 |-  ( ( ph /\ k e. Z ) -> B e. CC )
6 0cnd 
 |-  ( ph -> 0 e. CC )
7 1 2 3 4 6 5 clim2c 
 |-  ( ph -> ( F ~~> 0 <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( B - 0 ) ) < x ) )
8 1 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
9 5 subid1d 
 |-  ( ( ph /\ k e. Z ) -> ( B - 0 ) = B )
10 9 fveq2d 
 |-  ( ( ph /\ k e. Z ) -> ( abs ` ( B - 0 ) ) = ( abs ` B ) )
11 10 breq1d 
 |-  ( ( ph /\ k e. Z ) -> ( ( abs ` ( B - 0 ) ) < x <-> ( abs ` B ) < x ) )
12 8 11 sylan2 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( abs ` ( B - 0 ) ) < x <-> ( abs ` B ) < x ) )
13 12 anassrs 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( abs ` ( B - 0 ) ) < x <-> ( abs ` B ) < x ) )
14 13 ralbidva 
 |-  ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( B - 0 ) ) < x <-> A. k e. ( ZZ>= ` j ) ( abs ` B ) < x ) )
15 14 rexbidva 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( B - 0 ) ) < x <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` B ) < x ) )
16 15 ralbidv 
 |-  ( ph -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( B - 0 ) ) < x <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` B ) < x ) )
17 7 16 bitrd 
 |-  ( ph -> ( F ~~> 0 <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` B ) < x ) )