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 ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ )
lo1o1.1 ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) )
Assertion o1lo1d ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ ≤𝑂(1) )

Proof

Step Hyp Ref Expression
1 o1lo1.1 ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ )
2 lo1o1.1 ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) )
3 1 o1lo1 ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) ↔ ( ( 𝑥𝐴𝐵 ) ∈ ≤𝑂(1) ∧ ( 𝑥𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ) ) )
4 2 3 mpbid ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∈ ≤𝑂(1) ∧ ( 𝑥𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ) )
5 4 simpld ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ ≤𝑂(1) )