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 ( 𝐹 : 𝐴 ⟶ ℂ → ( 𝐹 ∈ 𝑂(1) ↔ ( abs ∘ 𝐹 ) ∈ ≤𝑂(1) ) )

Proof

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