Metamath Proof Explorer


Theorem o1bddrp

Description: Refine o1bdd2 to give a strictly positive upper bound. (Contributed by Mario Carneiro, 25-May-2016)

Ref Expression
Hypotheses o1bdd2.1 ( 𝜑𝐴 ⊆ ℝ )
o1bdd2.2 ( 𝜑𝐶 ∈ ℝ )
o1bdd2.3 ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℂ )
o1bdd2.4 ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) )
o1bdd2.5 ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝐶𝑦 ) ) → 𝑀 ∈ ℝ )
o1bdd2.6 ( ( ( 𝜑𝑥𝐴 ) ∧ ( ( 𝑦 ∈ ℝ ∧ 𝐶𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( abs ‘ 𝐵 ) ≤ 𝑀 )
Assertion o1bddrp ( 𝜑 → ∃ 𝑚 ∈ ℝ+𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑚 )

Proof

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 lo1bddrp ( 𝜑 → ∃ 𝑚 ∈ ℝ+𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑚 )