This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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