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