Metamath Proof Explorer


Theorem o1lo1d

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) )

Proof

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) )