Description: If an eventually bounded function is bounded on every interval A i^i ( -oo , y ) by a function M ( y ) , then the function is bounded on the whole domain. (Contributed by Mario Carneiro, 9-Apr-2016) (Proof shortened by Mario Carneiro, 26-May-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | o1bdd2.1 | ⊢ ( 𝜑 → 𝐴 ⊆ ℝ ) | |
| o1bdd2.2 | ⊢ ( 𝜑 → 𝐶 ∈ ℝ ) | ||
| o1bdd2.3 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) | ||
| o1bdd2.4 | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ) | ||
| o1bdd2.5 | ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦 ) ) → 𝑀 ∈ ℝ ) | ||
| o1bdd2.6 | ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( ( 𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( abs ‘ 𝐵 ) ≤ 𝑀 ) | ||
| Assertion | o1bdd2 | ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑚 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | o1bdd2.1 | ⊢ ( 𝜑 → 𝐴 ⊆ ℝ ) | |
| 2 | o1bdd2.2 | ⊢ ( 𝜑 → 𝐶 ∈ ℝ ) | |
| 3 | o1bdd2.3 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) | |
| 4 | o1bdd2.4 | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ) | |
| 5 | o1bdd2.5 | ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦 ) ) → 𝑀 ∈ ℝ ) | |
| 6 | o1bdd2.6 | ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( ( 𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( abs ‘ 𝐵 ) ≤ 𝑀 ) | |
| 7 | 3 | abscld | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ 𝐵 ) ∈ ℝ ) |
| 8 | 3 | lo1o12 | ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ ≤𝑂(1) ) ) |
| 9 | 4 8 | mpbid | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ ≤𝑂(1) ) |
| 10 | 1 2 7 9 5 6 | lo1bdd2 | ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑚 ) |