Theorem rlimi2

Description: Convergence at infinity of a function on the reals. (Contributed by Mario Carneiro, 12-May-2016)

	Ref	Expression
Hypotheses	rlimi.1	|- ( ph -> A. z e. A B e. V )
	rlimi.2	|- ( ph -> R e. RR+ )
	rlimi.3	|- ( ph -> ( z e. A |-> B ) ~~>r C )
	rlimi.4	|- ( ph -> D e. RR )
Assertion	rlimi2	|- ( ph -> E. y e. ( D [,) +oo ) A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < R ) )

Proof

Step	Hyp	Ref	Expression
1		rlimi.1	|- ( ph -> A. z e. A B e. V )
2		rlimi.2	|- ( ph -> R e. RR+ )
3		rlimi.3	|- ( ph -> ( z e. A |-> B ) ~~>r C )
4		rlimi.4	|- ( ph -> D e. RR )
5	1 2 3	rlimi	|- ( ph -> E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < R ) )
6		eqid	|- ( z e. A |-> B ) = ( z e. A |-> B )
7	6	fnmpt	|- ( A. z e. A B e. V -> ( z e. A |-> B ) Fn A )
8		fndm	|- ( ( z e. A |-> B ) Fn A -> dom ( z e. A |-> B ) = A )
9	1 7 8	3syl	|- ( ph -> dom ( z e. A |-> B ) = A )
10		rlimss	|- ( ( z e. A |-> B ) ~~>r C -> dom ( z e. A |-> B ) C_ RR )
11	3 10	syl	|- ( ph -> dom ( z e. A |-> B ) C_ RR )
12	9 11	eqsstrrd	|- ( ph -> A C_ RR )
13		rexico	|- ( ( A C_ RR /\ D e. RR ) -> ( E. y e. ( D [,) +oo ) A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < R ) <-> E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < R ) ) )
14	12 4 13	syl2anc	|- ( ph -> ( E. y e. ( D [,) +oo ) A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < R ) <-> E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < R ) ) )
15	5 14	mpbird	|- ( ph -> E. y e. ( D [,) +oo ) A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < R ) )