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 ‘ 𝐵 ) ≤ 𝑚 )