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	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
Assertion	lo1o12	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ ≤𝑂(1) ) )

Proof

Step	Hyp	Ref	Expression
1		lo1o12.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
2	1	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
3		lo1o1	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( abs ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ≤𝑂(1) ) )
4	2 3	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( abs ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ≤𝑂(1) ) )
5		absf	⊢ abs : ℂ ⟶ ℝ
6	5	a1i	⊢ ( 𝜑 → abs : ℂ ⟶ ℝ )
7	6 1	cofmpt	⊢ ( 𝜑 → ( abs ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) )
8	7	eleq1d	⊢ ( 𝜑 → ( ( abs ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ≤𝑂(1) ↔ ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ ≤𝑂(1) ) )
9	4 8	bitrd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ ≤𝑂(1) ) )