# Metamath Proof Explorer

## Theorem o1lo12

Description: A lower bounded real function is eventually bounded iff it is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses o1lo1.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℝ$
o1lo12.2 ${⊢}{\phi }\to {M}\in ℝ$
o1lo12.3 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {M}\le {B}$
Assertion o1lo12 ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in 𝑂\left(1\right)↔\left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)\right)$

### Proof

Step Hyp Ref Expression
1 o1lo1.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℝ$
2 o1lo12.2 ${⊢}{\phi }\to {M}\in ℝ$
3 o1lo12.3 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {M}\le {B}$
4 o1dm ${⊢}\left({x}\in {A}⟼{B}\right)\in 𝑂\left(1\right)\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)\subseteq ℝ$
5 4 a1i ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in 𝑂\left(1\right)\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)\subseteq ℝ\right)$
6 lo1dm ${⊢}\left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)\subseteq ℝ$
7 6 a1i ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)\subseteq ℝ\right)$
8 1 ralrimiva ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in ℝ$
9 dmmptg ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in ℝ\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)={A}$
10 8 9 syl ${⊢}{\phi }\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)={A}$
11 10 sseq1d ${⊢}{\phi }\to \left(\mathrm{dom}\left({x}\in {A}⟼{B}\right)\subseteq ℝ↔{A}\subseteq ℝ\right)$
12 simpr ${⊢}\left({\phi }\wedge {A}\subseteq ℝ\right)\to {A}\subseteq ℝ$
13 1 renegcld ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to -{B}\in ℝ$
14 13 adantlr ${⊢}\left(\left({\phi }\wedge {A}\subseteq ℝ\right)\wedge {x}\in {A}\right)\to -{B}\in ℝ$
15 2 adantr ${⊢}\left({\phi }\wedge {A}\subseteq ℝ\right)\to {M}\in ℝ$
16 15 renegcld ${⊢}\left({\phi }\wedge {A}\subseteq ℝ\right)\to -{M}\in ℝ$
17 2 adantr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {M}\in ℝ$
18 17 1 lenegd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({M}\le {B}↔-{B}\le -{M}\right)$
19 3 18 mpbid ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to -{B}\le -{M}$
20 19 ad2ant2r ${⊢}\left(\left({\phi }\wedge {A}\subseteq ℝ\right)\wedge \left({x}\in {A}\wedge {M}\le {x}\right)\right)\to -{B}\le -{M}$
21 12 14 15 16 20 ello1d ${⊢}\left({\phi }\wedge {A}\subseteq ℝ\right)\to \left({x}\in {A}⟼-{B}\right)\in \le 𝑂\left(1\right)$
22 1 o1lo1 ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in 𝑂\left(1\right)↔\left(\left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)\wedge \left({x}\in {A}⟼-{B}\right)\in \le 𝑂\left(1\right)\right)\right)$
23 22 rbaibd ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼-{B}\right)\in \le 𝑂\left(1\right)\right)\to \left(\left({x}\in {A}⟼{B}\right)\in 𝑂\left(1\right)↔\left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)\right)$
24 21 23 syldan ${⊢}\left({\phi }\wedge {A}\subseteq ℝ\right)\to \left(\left({x}\in {A}⟼{B}\right)\in 𝑂\left(1\right)↔\left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)\right)$
25 24 ex ${⊢}{\phi }\to \left({A}\subseteq ℝ\to \left(\left({x}\in {A}⟼{B}\right)\in 𝑂\left(1\right)↔\left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)\right)\right)$
26 11 25 sylbid ${⊢}{\phi }\to \left(\mathrm{dom}\left({x}\in {A}⟼{B}\right)\subseteq ℝ\to \left(\left({x}\in {A}⟼{B}\right)\in 𝑂\left(1\right)↔\left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)\right)\right)$
27 5 7 26 pm5.21ndd ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in 𝑂\left(1\right)↔\left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)\right)$