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	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℂ$$
Assertion	lo1o12	$$⊢\phi \to \left(\left(x\in A⟼B\right)\in 𝑂\left(1\right)\leftrightarrow \left(x\in A⟼\left|B\right|\right)\in \le 𝑂\left(1\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lo1o12.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℂ$$
2	1	fmpttd	$$⊢\phi \to \left(x\in A⟼B\right):A⟶ℂ$$
3		lo1o1	$$⊢\left(x\in A⟼B\right):A⟶ℂ\to \left(\left(x\in A⟼B\right)\in 𝑂\left(1\right)\leftrightarrow \mathrm{abs}\circ \left(x\in A⟼B\right)\in \le 𝑂\left(1\right)\right)$$
4	2 3	syl	$$⊢\phi \to \left(\left(x\in A⟼B\right)\in 𝑂\left(1\right)\leftrightarrow \mathrm{abs}\circ \left(x\in A⟼B\right)\in \le 𝑂\left(1\right)\right)$$
5		absf	$$⊢\mathrm{abs}:ℂ⟶ℝ$$
6	5	a1i	$$⊢\phi \to \mathrm{abs}:ℂ⟶ℝ$$
7	6 1	cofmpt	$$⊢\phi \to \mathrm{abs}\circ \left(x\in A⟼B\right)=\left(x\in A⟼\left|B\right|\right)$$
8	7	eleq1d	$$⊢\phi \to \left(\mathrm{abs}\circ \left(x\in A⟼B\right)\in \le 𝑂\left(1\right)\leftrightarrow \left(x\in A⟼\left|B\right|\right)\in \le 𝑂\left(1\right)\right)$$
9	4 8	bitrd	$$⊢\phi \to \left(\left(x\in A⟼B\right)\in 𝑂\left(1\right)\leftrightarrow \left(x\in A⟼\left|B\right|\right)\in \le 𝑂\left(1\right)\right)$$