Description: A real eventually bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | o1lo1.1 | |- ( ( ph /\ x e. A ) -> B e. RR ) |
|
lo1o1.1 | |- ( ph -> ( x e. A |-> B ) e. O(1) ) |
||
Assertion | o1lo1d | |- ( ph -> ( x e. A |-> B ) e. <_O(1) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | o1lo1.1 | |- ( ( ph /\ x e. A ) -> B e. RR ) |
|
2 | lo1o1.1 | |- ( ph -> ( x e. A |-> B ) e. O(1) ) |
|
3 | 1 | o1lo1 | |- ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> -u B ) e. <_O(1) ) ) ) |
4 | 2 3 | mpbid | |- ( ph -> ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> -u B ) e. <_O(1) ) ) |
5 | 4 | simpld | |- ( ph -> ( x e. A |-> B ) e. <_O(1) ) |