Metamath Proof Explorer

Theorem lo1bddrp

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

Ref Expression
Hypotheses lo1bdd2.1 
|- ( ph -> A C_ RR )
lo1bdd2.2 
|- ( ph -> C e. RR )
lo1bdd2.3 
|- ( ( ph /\ x e. A ) -> B e. RR )
lo1bdd2.4 
|- ( ph -> ( x e. A |-> B ) e. <_O(1) )
lo1bdd2.5 
|- ( ( ph /\ ( y e. RR /\ C <_ y ) ) -> M e. RR )
lo1bdd2.6 
|- ( ( ( ph /\ x e. A ) /\ ( ( y e. RR /\ C <_ y ) /\ x < y ) ) -> B <_ M )
Assertion lo1bddrp 
|- ( ph -> E. m e. RR+ A. x e. A B <_ m )

Proof

Step Hyp Ref Expression
1 lo1bdd2.1 
 |-  ( ph -> A C_ RR )
2 lo1bdd2.2 
 |-  ( ph -> C e. RR )
3 lo1bdd2.3 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
4 lo1bdd2.4 
 |-  ( ph -> ( x e. A |-> B ) e. <_O(1) )
5 lo1bdd2.5 
 |-  ( ( ph /\ ( y e. RR /\ C <_ y ) ) -> M e. RR )
6 lo1bdd2.6 
 |-  ( ( ( ph /\ x e. A ) /\ ( ( y e. RR /\ C <_ y ) /\ x < y ) ) -> B <_ M )
7 1 2 3 4 5 6 lo1bdd2 
 |-  ( ph -> E. n e. RR A. x e. A B <_ n )
8 simpr 
 |-  ( ( ph /\ n e. RR ) -> n e. RR )
9 8 recnd 
 |-  ( ( ph /\ n e. RR ) -> n e. CC )
10 9 abscld 
 |-  ( ( ph /\ n e. RR ) -> ( abs ` n ) e. RR )
11 9 absge0d 
 |-  ( ( ph /\ n e. RR ) -> 0 <_ ( abs ` n ) )
12 10 11 ge0p1rpd 
 |-  ( ( ph /\ n e. RR ) -> ( ( abs ` n ) + 1 ) e. RR+ )
13 simplr 
 |-  ( ( ( ph /\ n e. RR ) /\ x e. A ) -> n e. RR )
14 10 adantr 
 |-  ( ( ( ph /\ n e. RR ) /\ x e. A ) -> ( abs ` n ) e. RR )
15 peano2re 
 |-  ( ( abs ` n ) e. RR -> ( ( abs ` n ) + 1 ) e. RR )
16 14 15 syl 
 |-  ( ( ( ph /\ n e. RR ) /\ x e. A ) -> ( ( abs ` n ) + 1 ) e. RR )
17 13 leabsd 
 |-  ( ( ( ph /\ n e. RR ) /\ x e. A ) -> n <_ ( abs ` n ) )
18 14 lep1d 
 |-  ( ( ( ph /\ n e. RR ) /\ x e. A ) -> ( abs ` n ) <_ ( ( abs ` n ) + 1 ) )
19 13 14 16 17 18 letrd 
 |-  ( ( ( ph /\ n e. RR ) /\ x e. A ) -> n <_ ( ( abs ` n ) + 1 ) )
20 3 adantlr 
 |-  ( ( ( ph /\ n e. RR ) /\ x e. A ) -> B e. RR )
21 letr 
 |-  ( ( B e. RR /\ n e. RR /\ ( ( abs ` n ) + 1 ) e. RR ) -> ( ( B <_ n /\ n <_ ( ( abs ` n ) + 1 ) ) -> B <_ ( ( abs ` n ) + 1 ) ) )
22 20 13 16 21 syl3anc 
 |-  ( ( ( ph /\ n e. RR ) /\ x e. A ) -> ( ( B <_ n /\ n <_ ( ( abs ` n ) + 1 ) ) -> B <_ ( ( abs ` n ) + 1 ) ) )
23 19 22 mpan2d 
 |-  ( ( ( ph /\ n e. RR ) /\ x e. A ) -> ( B <_ n -> B <_ ( ( abs ` n ) + 1 ) ) )
24 23 ralimdva 
 |-  ( ( ph /\ n e. RR ) -> ( A. x e. A B <_ n -> A. x e. A B <_ ( ( abs ` n ) + 1 ) ) )
25 brralrspcev 
 |-  ( ( ( ( abs ` n ) + 1 ) e. RR+ /\ A. x e. A B <_ ( ( abs ` n ) + 1 ) ) -> E. m e. RR+ A. x e. A B <_ m )
26 12 24 25 syl6an 
 |-  ( ( ph /\ n e. RR ) -> ( A. x e. A B <_ n -> E. m e. RR+ A. x e. A B <_ m ) )
27 26 rexlimdva 
 |-  ( ph -> ( E. n e. RR A. x e. A B <_ n -> E. m e. RR+ A. x e. A B <_ m ) )
28 7 27 mpd 
 |-  ( ph -> E. m e. RR+ A. x e. A B <_ m )