Metamath Proof Explorer

Theorem lo1o1

Description: A function is eventually bounded iff its absolute value is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Assertion lo1o1 ⊢ F : A ⟶ ℂ → F ∈ 𝑂⁡1 ↔ abs ∘ F ∈ ≤𝑂⁡1

Proof

Step Hyp Ref Expression
1 o1dm ⊢ F ∈ 𝑂⁡1 → dom ⁡ F ⊆ ℝ
2 fdm ⊢ F : A ⟶ ℂ → dom ⁡ F = A
3 2 sseq1d ⊢ F : A ⟶ ℂ → dom ⁡ F ⊆ ℝ ↔ A ⊆ ℝ
4 1 3 imbitrid ⊢ F : A ⟶ ℂ → F ∈ 𝑂⁡1 → A ⊆ ℝ
5 lo1dm ⊢ abs ∘ F ∈ ≤𝑂⁡1 → dom ⁡ abs ∘ F ⊆ ℝ
6 absf ⊢ abs : ℂ ⟶ ℝ
7 fco ⊢ abs : ℂ ⟶ ℝ ∧ F : A ⟶ ℂ → abs ∘ F : A ⟶ ℝ
8 6 7 mpan ⊢ F : A ⟶ ℂ → abs ∘ F : A ⟶ ℝ
9 8 fdmd ⊢ F : A ⟶ ℂ → dom ⁡ abs ∘ F = A
10 9 sseq1d ⊢ F : A ⟶ ℂ → dom ⁡ abs ∘ F ⊆ ℝ ↔ A ⊆ ℝ
11 5 10 imbitrid ⊢ F : A ⟶ ℂ → abs ∘ F ∈ ≤𝑂⁡1 → A ⊆ ℝ
12 fvco3 ⊢ F : A ⟶ ℂ ∧ y ∈ A → abs ∘ F ⁡ y = F ⁡ y
13 12 adantlr ⊢ F : A ⟶ ℂ ∧ A ⊆ ℝ ∧ y ∈ A → abs ∘ F ⁡ y = F ⁡ y
14 13 breq1d ⊢ F : A ⟶ ℂ ∧ A ⊆ ℝ ∧ y ∈ A → abs ∘ F ⁡ y ≤ m ↔ F ⁡ y ≤ m
15 14 imbi2d ⊢ F : A ⟶ ℂ ∧ A ⊆ ℝ ∧ y ∈ A → x ≤ y → abs ∘ F ⁡ y ≤ m ↔ x ≤ y → F ⁡ y ≤ m
16 15 ralbidva ⊢ F : A ⟶ ℂ ∧ A ⊆ ℝ → ∀ y ∈ A x ≤ y → abs ∘ F ⁡ y ≤ m ↔ ∀ y ∈ A x ≤ y → F ⁡ y ≤ m
17 16 2rexbidv ⊢ F : A ⟶ ℂ ∧ A ⊆ ℝ → ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ A x ≤ y → abs ∘ F ⁡ y ≤ m ↔ ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ A x ≤ y → F ⁡ y ≤ m
18 ello12 ⊢ abs ∘ F : A ⟶ ℝ ∧ A ⊆ ℝ → abs ∘ F ∈ ≤𝑂⁡1 ↔ ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ A x ≤ y → abs ∘ F ⁡ y ≤ m
19 8 18 sylan ⊢ F : A ⟶ ℂ ∧ A ⊆ ℝ → abs ∘ F ∈ ≤𝑂⁡1 ↔ ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ A x ≤ y → abs ∘ F ⁡ y ≤ m
20 elo12 ⊢ F : A ⟶ ℂ ∧ A ⊆ ℝ → F ∈ 𝑂⁡1 ↔ ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ A x ≤ y → F ⁡ y ≤ m
21 17 19 20 3bitr4rd ⊢ F : A ⟶ ℂ ∧ A ⊆ ℝ → F ∈ 𝑂⁡1 ↔ abs ∘ F ∈ ≤𝑂⁡1
22 21 ex ⊢ F : A ⟶ ℂ → A ⊆ ℝ → F ∈ 𝑂⁡1 ↔ abs ∘ F ∈ ≤𝑂⁡1
23 4 11 22 pm5.21ndd ⊢ F : A ⟶ ℂ → F ∈ 𝑂⁡1 ↔ abs ∘ F ∈ ≤𝑂⁡1