This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ φ ∧ x ∈ A → B ∈ ℂ
Assertion lo1o12 ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ x ∈ A ⟼ B ∈ ≤𝑂⁡1

Proof

Step Hyp Ref Expression
1 lo1o12.1 ⊢ φ ∧ x ∈ A → B ∈ ℂ
2 1 fmpttd ⊢ φ → x ∈ A ⟼ B : A ⟶ ℂ
3 lo1o1 ⊢ x ∈ A ⟼ B : A ⟶ ℂ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ abs ∘ x ∈ A ⟼ B ∈ ≤𝑂⁡1
4 2 3 syl ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ abs ∘ x ∈ A ⟼ B ∈ ≤𝑂⁡1
5 absf ⊢ abs : ℂ ⟶ ℝ
6 5 a1i ⊢ φ → abs : ℂ ⟶ ℝ
7 6 1 cofmpt ⊢ φ → abs ∘ x ∈ A ⟼ B = x ∈ A ⟼ B
8 7 eleq1d ⊢ φ → abs ∘ x ∈ A ⟼ B ∈ ≤𝑂⁡1 ↔ x ∈ A ⟼ B ∈ ≤𝑂⁡1
9 4 8 bitrd ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ x ∈ A ⟼ B ∈ ≤𝑂⁡1