Metamath Proof Explorer

Theorem rlimi

Description: Convergence at infinity of a function on the reals. (Contributed by Mario Carneiro, 28-Feb-2015)

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 )
Assertion rlimi 
|- ( ph -> E. y e. RR 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 breq2 
 |-  ( x = R -> ( ( abs ` ( B - C ) ) < x <-> ( abs ` ( B - C ) ) < R ) )
5 4 imbi2d 
 |-  ( x = R -> ( ( y <_ z -> ( abs ` ( B - C ) ) < x ) <-> ( y <_ z -> ( abs ` ( B - C ) ) < R ) ) )
6 5 rexralbidv 
 |-  ( x = R -> ( E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) <-> E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < R ) ) )
7 rlimf 
 |-  ( ( z e. A |-> B ) ~~>r C -> ( z e. A |-> B ) : dom ( z e. A |-> B ) --> CC )
8 3 7 syl 
 |-  ( ph -> ( z e. A |-> B ) : dom ( z e. A |-> B ) --> CC )
9 eqid 
 |-  ( z e. A |-> B ) = ( z e. A |-> B )
10 9 fmpt 
 |-  ( A. z e. A B e. V <-> ( z e. A |-> B ) : A --> V )
11 1 10 sylib 
 |-  ( ph -> ( z e. A |-> B ) : A --> V )
12 11 fdmd 
 |-  ( ph -> dom ( z e. A |-> B ) = A )
13 12 feq2d 
 |-  ( ph -> ( ( z e. A |-> B ) : dom ( z e. A |-> B ) --> CC <-> ( z e. A |-> B ) : A --> CC ) )
14 8 13 mpbid 
 |-  ( ph -> ( z e. A |-> B ) : A --> CC )
15 9 fmpt 
 |-  ( A. z e. A B e. CC <-> ( z e. A |-> B ) : A --> CC )
16 14 15 sylibr 
 |-  ( ph -> A. z e. A B e. CC )
17 rlimss 
 |-  ( ( z e. A |-> B ) ~~>r C -> dom ( z e. A |-> B ) C_ RR )
18 3 17 syl 
 |-  ( ph -> dom ( z e. A |-> B ) C_ RR )
19 12 18 eqsstrrd 
 |-  ( ph -> A C_ RR )
20 rlimcl 
 |-  ( ( z e. A |-> B ) ~~>r C -> C e. CC )
21 3 20 syl 
 |-  ( ph -> C e. CC )
22 16 19 21 rlim2 
 |-  ( ph -> ( ( z e. A |-> B ) ~~>r C <-> A. x e. RR+ E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )
23 3 22 mpbid 
 |-  ( ph -> A. x e. RR+ E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) )
24 6 23 2 rspcdva 
 |-  ( ph -> E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < R ) )