Metamath Proof Explorer

Theorem lo1o1

Description: A function is eventually bounded iff its absolute value is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Assertion lo1o1 
|- ( F : A --> CC -> ( F e. O(1) <-> ( abs o. F ) e. <_O(1) ) )

Proof

Step Hyp Ref Expression
1 o1dm 
 |-  ( F e. O(1) -> dom F C_ RR )
2 fdm 
 |-  ( F : A --> CC -> dom F = A )
3 2 sseq1d 
 |-  ( F : A --> CC -> ( dom F C_ RR <-> A C_ RR ) )
4 1 3 imbitrid 
 |-  ( F : A --> CC -> ( F e. O(1) -> A C_ RR ) )
5 lo1dm 
 |-  ( ( abs o. F ) e. <_O(1) -> dom ( abs o. F ) C_ RR )
6 absf 
 |-  abs : CC --> RR
7 fco 
 |-  ( ( abs : CC --> RR /\ F : A --> CC ) -> ( abs o. F ) : A --> RR )
8 6 7 mpan 
 |-  ( F : A --> CC -> ( abs o. F ) : A --> RR )
9 8 fdmd 
 |-  ( F : A --> CC -> dom ( abs o. F ) = A )
10 9 sseq1d 
 |-  ( F : A --> CC -> ( dom ( abs o. F ) C_ RR <-> A C_ RR ) )
11 5 10 imbitrid 
 |-  ( F : A --> CC -> ( ( abs o. F ) e. <_O(1) -> A C_ RR ) )
12 fvco3 
 |-  ( ( F : A --> CC /\ y e. A ) -> ( ( abs o. F ) ` y ) = ( abs ` ( F ` y ) ) )
13 12 adantlr 
 |-  ( ( ( F : A --> CC /\ A C_ RR ) /\ y e. A ) -> ( ( abs o. F ) ` y ) = ( abs ` ( F ` y ) ) )
14 13 breq1d 
 |-  ( ( ( F : A --> CC /\ A C_ RR ) /\ y e. A ) -> ( ( ( abs o. F ) ` y ) <_ m <-> ( abs ` ( F ` y ) ) <_ m ) )
15 14 imbi2d 
 |-  ( ( ( F : A --> CC /\ A C_ RR ) /\ y e. A ) -> ( ( x <_ y -> ( ( abs o. F ) ` y ) <_ m ) <-> ( x <_ y -> ( abs ` ( F ` y ) ) <_ m ) ) )
16 15 ralbidva 
 |-  ( ( F : A --> CC /\ A C_ RR ) -> ( A. y e. A ( x <_ y -> ( ( abs o. F ) ` y ) <_ m ) <-> A. y e. A ( x <_ y -> ( abs ` ( F ` y ) ) <_ m ) ) )
17 16 2rexbidv 
 |-  ( ( F : A --> CC /\ A C_ RR ) -> ( E. x e. RR E. m e. RR A. y e. A ( x <_ y -> ( ( abs o. F ) ` y ) <_ m ) <-> E. x e. RR E. m e. RR A. y e. A ( x <_ y -> ( abs ` ( F ` y ) ) <_ m ) ) )
18 ello12 
 |-  ( ( ( abs o. F ) : A --> RR /\ A C_ RR ) -> ( ( abs o. F ) e. <_O(1) <-> E. x e. RR E. m e. RR A. y e. A ( x <_ y -> ( ( abs o. F ) ` y ) <_ m ) ) )
19 8 18 sylan 
 |-  ( ( F : A --> CC /\ A C_ RR ) -> ( ( abs o. F ) e. <_O(1) <-> E. x e. RR E. m e. RR A. y e. A ( x <_ y -> ( ( abs o. F ) ` y ) <_ m ) ) )
20 elo12 
 |-  ( ( F : A --> CC /\ A C_ RR ) -> ( F e. O(1) <-> E. x e. RR E. m e. RR A. y e. A ( x <_ y -> ( abs ` ( F ` y ) ) <_ m ) ) )
21 17 19 20 3bitr4rd 
 |-  ( ( F : A --> CC /\ A C_ RR ) -> ( F e. O(1) <-> ( abs o. F ) e. <_O(1) ) )
22 21 ex 
 |-  ( F : A --> CC -> ( A C_ RR -> ( F e. O(1) <-> ( abs o. F ) e. <_O(1) ) ) )
23 4 11 22 pm5.21ndd 
 |-  ( F : A --> CC -> ( F e. O(1) <-> ( abs o. F ) e. <_O(1) ) )