Description: If an eventually bounded function is bounded on every interval A i^i ( -oo , y ) by a function M ( y ) , then the function is bounded on the whole domain. (Contributed by Mario Carneiro, 9-Apr-2016) (Proof shortened by Mario Carneiro, 26-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 | o1bdd2 | |- ( ph -> E. m e. RR A. x e. A ( abs ` B ) <_ m ) |
| 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 | lo1bdd2 | |- ( ph -> E. m e. RR A. x e. A ( abs ` B ) <_ m ) |