o1bddrp

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

	Ref	Expression
Hypotheses	o1bdd2.1	$⊢ φ \to A \subseteq ℝ$
	o1bdd2.2	$⊢ φ \to C \in ℝ$
	o1bdd2.3	$⊢ (φ \land x \in A) \to B \in ℂ$
	o1bdd2.4	$⊢ φ \to (x \in A ⟼ B) \in 𝑂 (1)$
	o1bdd2.5	$⊢ (φ \land (y \in ℝ \land C \leq y)) \to M \in ℝ$
	o1bdd2.6	$⊢ ((φ \land x \in A) \land ((y \in ℝ \land C \leq y) \land x < y)) \to \|B\| \leq M$
Assertion	o1bddrp	$⊢ φ \to \exists m \in ℝ^{+} \forall x \in A \|B\| \leq m$

Step	Hyp	Ref	Expression
1		o1bdd2.1	$⊢ φ \to A \subseteq ℝ$
2		o1bdd2.2	$⊢ φ \to C \in ℝ$
3		o1bdd2.3	$⊢ (φ \land x \in A) \to B \in ℂ$
4		o1bdd2.4	$⊢ φ \to (x \in A ⟼ B) \in 𝑂 (1)$
5		o1bdd2.5	$⊢ (φ \land (y \in ℝ \land C \leq y)) \to M \in ℝ$
6		o1bdd2.6	$⊢ ((φ \land x \in A) \land ((y \in ℝ \land C \leq y) \land x < y)) \to \|B\| \leq M$
7	3	abscld	$⊢ (φ \land x \in A) \to \|B\| \in ℝ$
8	3	lo1o12	$⊢ φ \to ((x \in A ⟼ B) \in 𝑂 (1) \leftrightarrow (x \in A ⟼ \|B\|) \in \leq 𝑂 (1))$
9	4 8	mpbid	$⊢ φ \to (x \in A ⟼ \|B\|) \in \leq 𝑂 (1)$
10	1 2 7 9 5 6	lo1bddrp	$⊢ φ \to \exists m \in ℝ^{+} \forall x \in A \|B\| \leq m$

Metamath Proof Explorer