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 ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℂ )
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) ) )