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

Metamath Proof Explorer

Theorem lo1o12

Description: A function is eventually bounded iff its absolute value is eventually upper bounded. (This function is useful for converting theorems about <_O(1) to O(1) .) (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Hypothesis lo1o12.1 
|- ( ( ph /\ x e. A ) -> B e. CC )
Assertion lo1o12 
|- ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( x e. A |-> ( abs ` B ) ) e. <_O(1) ) )

Proof

Step Hyp Ref Expression
1 lo1o12.1 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
2 1 fmpttd 
 |-  ( ph -> ( x e. A |-> B ) : A --> CC )
3 lo1o1 
 |-  ( ( x e. A |-> B ) : A --> CC -> ( ( x e. A |-> B ) e. O(1) <-> ( abs o. ( x e. A |-> B ) ) e. <_O(1) ) )
4 2 3 syl 
 |-  ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( abs o. ( x e. A |-> B ) ) e. <_O(1) ) )
5 absf 
 |-  abs : CC --> RR
6 5 a1i 
 |-  ( ph -> abs : CC --> RR )
7 6 1 cofmpt 
 |-  ( ph -> ( abs o. ( x e. A |-> B ) ) = ( x e. A |-> ( abs ` B ) ) )
8 7 eleq1d 
 |-  ( ph -> ( ( abs o. ( x e. A |-> B ) ) e. <_O(1) <-> ( x e. A |-> ( abs ` B ) ) e. <_O(1) ) )
9 4 8 bitrd 
 |-  ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( x e. A |-> ( abs ` B ) ) e. <_O(1) ) )