Metamath Proof Explorer


Theorem rlim0lt

Description: Use strictly less-than in place of less equal in the real limit predicate. (Contributed by Mario Carneiro, 18-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 rlim0lt
|- ( 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 rlim2lt
 |-  ( 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 ) ) )