Metamath Proof Explorer

Theorem rlimo1

Description: Any function with a finite limit is eventually bounded. (Contributed by Mario Carneiro, 18-Sep-2014)

Ref Expression
Assertion rlimo1 
|- ( F ~~>r A -> F e. O(1) )

Proof

Step Hyp Ref Expression
1 rlimf 
 |-  ( F ~~>r A -> F : dom F --> CC )
2 1 ffvelrnda 
 |-  ( ( F ~~>r A /\ z e. dom F ) -> ( F ` z ) e. CC )
3 2 ralrimiva 
 |-  ( F ~~>r A -> A. z e. dom F ( F ` z ) e. CC )
4 1rp 
 |-  1 e. RR+
5 4 a1i 
 |-  ( F ~~>r A -> 1 e. RR+ )
6 1 feqmptd 
 |-  ( F ~~>r A -> F = ( z e. dom F |-> ( F ` z ) ) )
7 id 
 |-  ( F ~~>r A -> F ~~>r A )
8 6 7 eqbrtrrd 
 |-  ( F ~~>r A -> ( z e. dom F |-> ( F ` z ) ) ~~>r A )
9 3 5 8 rlimi 
 |-  ( F ~~>r A -> E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - A ) ) < 1 ) )
10 rlimcl 
 |-  ( F ~~>r A -> A e. CC )
11 10 adantr 
 |-  ( ( F ~~>r A /\ y e. RR ) -> A e. CC )
12 11 abscld 
 |-  ( ( F ~~>r A /\ y e. RR ) -> ( abs ` A ) e. RR )
13 peano2re 
 |-  ( ( abs ` A ) e. RR -> ( ( abs ` A ) + 1 ) e. RR )
14 12 13 syl 
 |-  ( ( F ~~>r A /\ y e. RR ) -> ( ( abs ` A ) + 1 ) e. RR )
15 2 adantlr 
 |-  ( ( ( F ~~>r A /\ y e. RR ) /\ z e. dom F ) -> ( F ` z ) e. CC )
16 11 adantr 
 |-  ( ( ( F ~~>r A /\ y e. RR ) /\ z e. dom F ) -> A e. CC )
17 15 16 abs2difd 
 |-  ( ( ( F ~~>r A /\ y e. RR ) /\ z e. dom F ) -> ( ( abs ` ( F ` z ) ) - ( abs ` A ) ) <_ ( abs ` ( ( F ` z ) - A ) ) )
18 15 abscld 
 |-  ( ( ( F ~~>r A /\ y e. RR ) /\ z e. dom F ) -> ( abs ` ( F ` z ) ) e. RR )
19 12 adantr 
 |-  ( ( ( F ~~>r A /\ y e. RR ) /\ z e. dom F ) -> ( abs ` A ) e. RR )
20 18 19 resubcld 
 |-  ( ( ( F ~~>r A /\ y e. RR ) /\ z e. dom F ) -> ( ( abs ` ( F ` z ) ) - ( abs ` A ) ) e. RR )
21 15 16 subcld 
 |-  ( ( ( F ~~>r A /\ y e. RR ) /\ z e. dom F ) -> ( ( F ` z ) - A ) e. CC )
22 21 abscld 
 |-  ( ( ( F ~~>r A /\ y e. RR ) /\ z e. dom F ) -> ( abs ` ( ( F ` z ) - A ) ) e. RR )
23 1red 
 |-  ( ( ( F ~~>r A /\ y e. RR ) /\ z e. dom F ) -> 1 e. RR )
24 lelttr 
 |-  ( ( ( ( abs ` ( F ` z ) ) - ( abs ` A ) ) e. RR /\ ( abs ` ( ( F ` z ) - A ) ) e. RR /\ 1 e. RR ) -> ( ( ( ( abs ` ( F ` z ) ) - ( abs ` A ) ) <_ ( abs ` ( ( F ` z ) - A ) ) /\ ( abs ` ( ( F ` z ) - A ) ) < 1 ) -> ( ( abs ` ( F ` z ) ) - ( abs ` A ) ) < 1 ) )
25 20 22 23 24 syl3anc 
 |-  ( ( ( F ~~>r A /\ y e. RR ) /\ z e. dom F ) -> ( ( ( ( abs ` ( F ` z ) ) - ( abs ` A ) ) <_ ( abs ` ( ( F ` z ) - A ) ) /\ ( abs ` ( ( F ` z ) - A ) ) < 1 ) -> ( ( abs ` ( F ` z ) ) - ( abs ` A ) ) < 1 ) )
26 17 25 mpand 
 |-  ( ( ( F ~~>r A /\ y e. RR ) /\ z e. dom F ) -> ( ( abs ` ( ( F ` z ) - A ) ) < 1 -> ( ( abs ` ( F ` z ) ) - ( abs ` A ) ) < 1 ) )
27 18 19 23 ltsubadd2d 
 |-  ( ( ( F ~~>r A /\ y e. RR ) /\ z e. dom F ) -> ( ( ( abs ` ( F ` z ) ) - ( abs ` A ) ) < 1 <-> ( abs ` ( F ` z ) ) < ( ( abs ` A ) + 1 ) ) )
28 26 27 sylibd 
 |-  ( ( ( F ~~>r A /\ y e. RR ) /\ z e. dom F ) -> ( ( abs ` ( ( F ` z ) - A ) ) < 1 -> ( abs ` ( F ` z ) ) < ( ( abs ` A ) + 1 ) ) )
29 14 adantr 
 |-  ( ( ( F ~~>r A /\ y e. RR ) /\ z e. dom F ) -> ( ( abs ` A ) + 1 ) e. RR )
30 ltle 
 |-  ( ( ( abs ` ( F ` z ) ) e. RR /\ ( ( abs ` A ) + 1 ) e. RR ) -> ( ( abs ` ( F ` z ) ) < ( ( abs ` A ) + 1 ) -> ( abs ` ( F ` z ) ) <_ ( ( abs ` A ) + 1 ) ) )
31 18 29 30 syl2anc 
 |-  ( ( ( F ~~>r A /\ y e. RR ) /\ z e. dom F ) -> ( ( abs ` ( F ` z ) ) < ( ( abs ` A ) + 1 ) -> ( abs ` ( F ` z ) ) <_ ( ( abs ` A ) + 1 ) ) )
32 28 31 syld 
 |-  ( ( ( F ~~>r A /\ y e. RR ) /\ z e. dom F ) -> ( ( abs ` ( ( F ` z ) - A ) ) < 1 -> ( abs ` ( F ` z ) ) <_ ( ( abs ` A ) + 1 ) ) )
33 32 imim2d 
 |-  ( ( ( F ~~>r A /\ y e. RR ) /\ z e. dom F ) -> ( ( y <_ z -> ( abs ` ( ( F ` z ) - A ) ) < 1 ) -> ( y <_ z -> ( abs ` ( F ` z ) ) <_ ( ( abs ` A ) + 1 ) ) ) )
34 33 ralimdva 
 |-  ( ( F ~~>r A /\ y e. RR ) -> ( A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - A ) ) < 1 ) -> A. z e. dom F ( y <_ z -> ( abs ` ( F ` z ) ) <_ ( ( abs ` A ) + 1 ) ) ) )
35 breq2 
 |-  ( w = ( ( abs ` A ) + 1 ) -> ( ( abs ` ( F ` z ) ) <_ w <-> ( abs ` ( F ` z ) ) <_ ( ( abs ` A ) + 1 ) ) )
36 35 imbi2d 
 |-  ( w = ( ( abs ` A ) + 1 ) -> ( ( y <_ z -> ( abs ` ( F ` z ) ) <_ w ) <-> ( y <_ z -> ( abs ` ( F ` z ) ) <_ ( ( abs ` A ) + 1 ) ) ) )
37 36 ralbidv 
 |-  ( w = ( ( abs ` A ) + 1 ) -> ( A. z e. dom F ( y <_ z -> ( abs ` ( F ` z ) ) <_ w ) <-> A. z e. dom F ( y <_ z -> ( abs ` ( F ` z ) ) <_ ( ( abs ` A ) + 1 ) ) ) )
38 37 rspcev 
 |-  ( ( ( ( abs ` A ) + 1 ) e. RR /\ A. z e. dom F ( y <_ z -> ( abs ` ( F ` z ) ) <_ ( ( abs ` A ) + 1 ) ) ) -> E. w e. RR A. z e. dom F ( y <_ z -> ( abs ` ( F ` z ) ) <_ w ) )
39 14 34 38 syl6an 
 |-  ( ( F ~~>r A /\ y e. RR ) -> ( A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - A ) ) < 1 ) -> E. w e. RR A. z e. dom F ( y <_ z -> ( abs ` ( F ` z ) ) <_ w ) ) )
40 39 reximdva 
 |-  ( F ~~>r A -> ( E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - A ) ) < 1 ) -> E. y e. RR E. w e. RR A. z e. dom F ( y <_ z -> ( abs ` ( F ` z ) ) <_ w ) ) )
41 9 40 mpd 
 |-  ( F ~~>r A -> E. y e. RR E. w e. RR A. z e. dom F ( y <_ z -> ( abs ` ( F ` z ) ) <_ w ) )
42 rlimss 
 |-  ( F ~~>r A -> dom F C_ RR )
43 elo12 
 |-  ( ( F : dom F --> CC /\ dom F C_ RR ) -> ( F e. O(1) <-> E. y e. RR E. w e. RR A. z e. dom F ( y <_ z -> ( abs ` ( F ` z ) ) <_ w ) ) )
44 1 42 43 syl2anc 
 |-  ( F ~~>r A -> ( F e. O(1) <-> E. y e. RR E. w e. RR A. z e. dom F ( y <_ z -> ( abs ` ( F ` z ) ) <_ w ) ) )
45 41 44 mpbird 
 |-  ( F ~~>r A -> F e. O(1) )