Metamath Proof Explorer


Theorem clim0

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 )
Assertion clim0
|- ( ph -> ( F ~~> 0 <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( 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 1 2 3 4 clim2
 |-  ( ph -> ( F ~~> 0 <-> ( 0 e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - 0 ) ) < x ) ) ) )
6 0cn
 |-  0 e. CC
7 6 biantrur
 |-  ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - 0 ) ) < x ) <-> ( 0 e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - 0 ) ) < x ) ) )
8 subid1
 |-  ( B e. CC -> ( B - 0 ) = B )
9 8 fveq2d
 |-  ( B e. CC -> ( abs ` ( B - 0 ) ) = ( abs ` B ) )
10 9 breq1d
 |-  ( B e. CC -> ( ( abs ` ( B - 0 ) ) < x <-> ( abs ` B ) < x ) )
11 10 pm5.32i
 |-  ( ( B e. CC /\ ( abs ` ( B - 0 ) ) < x ) <-> ( B e. CC /\ ( abs ` B ) < x ) )
12 11 ralbii
 |-  ( A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - 0 ) ) < x ) <-> A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` B ) < x ) )
13 12 rexbii
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - 0 ) ) < x ) <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` B ) < x ) )
14 13 ralbii
 |-  ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - 0 ) ) < x ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` B ) < x ) )
15 7 14 bitr3i
 |-  ( ( 0 e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - 0 ) ) < x ) ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` B ) < x ) )
16 5 15 bitrdi
 |-  ( ph -> ( F ~~> 0 <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` B ) < x ) ) )