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