Theorem o1bddrp

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

	Ref	Expression
Hypotheses	o1bdd2.1	|- ( ph -> A C_ RR )
	o1bdd2.2	|- ( ph -> C e. RR )
	o1bdd2.3	|- ( ( ph /\ x e. A ) -> B e. CC )
	o1bdd2.4	|- ( ph -> ( x e. A |-> B ) e. O(1) )
	o1bdd2.5	|- ( ( ph /\ ( y e. RR /\ C <_ y ) ) -> M e. RR )
	o1bdd2.6	|- ( ( ( ph /\ x e. A ) /\ ( ( y e. RR /\ C <_ y ) /\ x < y ) ) -> ( abs ` B ) <_ M )
Assertion	o1bddrp	|- ( ph -> E. m e. RR+ A. x e. A ( abs ` B ) <_ m )

Proof

Step	Hyp	Ref	Expression
1		o1bdd2.1	|- ( ph -> A C_ RR )
2		o1bdd2.2	|- ( ph -> C e. RR )
3		o1bdd2.3	|- ( ( ph /\ x e. A ) -> B e. CC )
4		o1bdd2.4	|- ( ph -> ( x e. A |-> B ) e. O(1) )
5		o1bdd2.5	|- ( ( ph /\ ( y e. RR /\ C <_ y ) ) -> M e. RR )
6		o1bdd2.6	|- ( ( ( ph /\ x e. A ) /\ ( ( y e. RR /\ C <_ y ) /\ x < y ) ) -> ( abs ` B ) <_ M )
7	3	abscld	|- ( ( ph /\ x e. A ) -> ( abs ` B ) e. RR )
8	3	lo1o12	|- ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( x e. A |-> ( abs ` B ) ) e. <_O(1) ) )
9	4 8	mpbid	|- ( ph -> ( x e. A |-> ( abs ` B ) ) e. <_O(1) )
10	1 2 7 9 5 6	lo1bddrp	|- ( ph -> E. m e. RR+ A. x e. A ( abs ` B ) <_ m )