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