Metamath Proof Explorer

Theorem rlim0

Description: Express the predicate B ( z ) converges to 0 . (Contributed by Mario Carneiro, 16-Sep-2014) (Revised by Mario Carneiro, 28-Feb-2015)

Ref Expression
Hypotheses rlim0.1 
|- ( ph -> A. z e. A B e. CC )
rlim0.2 
|- ( ph -> A C_ RR )
Assertion rlim0 
|- ( ph -> ( ( z e. A |-> B ) ~~>r 0 <-> A. x e. RR+ E. y e. RR A. z e. A ( y <_ z -> ( abs ` B ) < x ) ) )

Proof

Step Hyp Ref Expression
1 rlim0.1 
 |-  ( ph -> A. z e. A B e. CC )
2 rlim0.2 
 |-  ( ph -> A C_ RR )
3 0cnd 
 |-  ( ph -> 0 e. CC )
4 1 2 3 rlim2 
 |-  ( ph -> ( ( z e. A |-> B ) ~~>r 0 <-> A. x e. RR+ E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - 0 ) ) < x ) ) )
5 subid1 
 |-  ( B e. CC -> ( B - 0 ) = B )
6 5 fveq2d 
 |-  ( B e. CC -> ( abs ` ( B - 0 ) ) = ( abs ` B ) )
7 6 breq1d 
 |-  ( B e. CC -> ( ( abs ` ( B - 0 ) ) < x <-> ( abs ` B ) < x ) )
8 7 imbi2d 
 |-  ( B e. CC -> ( ( y <_ z -> ( abs ` ( B - 0 ) ) < x ) <-> ( y <_ z -> ( abs ` B ) < x ) ) )
9 8 ralimi 
 |-  ( A. z e. A B e. CC -> A. z e. A ( ( y <_ z -> ( abs ` ( B - 0 ) ) < x ) <-> ( y <_ z -> ( abs ` B ) < x ) ) )
10 ralbi 
 |-  ( A. z e. A ( ( y <_ z -> ( abs ` ( B - 0 ) ) < x ) <-> ( y <_ z -> ( abs ` B ) < x ) ) -> ( A. z e. A ( y <_ z -> ( abs ` ( B - 0 ) ) < x ) <-> A. z e. A ( y <_ z -> ( abs ` B ) < x ) ) )
11 1 9 10 3syl 
 |-  ( ph -> ( A. z e. A ( y <_ z -> ( abs ` ( B - 0 ) ) < x ) <-> A. z e. A ( y <_ z -> ( abs ` B ) < x ) ) )
12 11 rexbidv 
 |-  ( ph -> ( E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - 0 ) ) < x ) <-> E. y e. RR A. z e. A ( y <_ z -> ( abs ` B ) < x ) ) )
13 12 ralbidv 
 |-  ( ph -> ( A. x e. RR+ E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - 0 ) ) < x ) <-> A. x e. RR+ E. y e. RR A. z e. A ( y <_ z -> ( abs ` B ) < x ) ) )
14 4 13 bitrd 
 |-  ( ph -> ( ( z e. A |-> B ) ~~>r 0 <-> A. x e. RR+ E. y e. RR A. z e. A ( y <_ z -> ( abs ` B ) < x ) ) )