# Metamath Proof Explorer

## Theorem lo1bdd2

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)

Ref Expression
Hypotheses lo1bdd2.1 ${⊢}{\phi }\to {A}\subseteq ℝ$
lo1bdd2.2 ${⊢}{\phi }\to {C}\in ℝ$
lo1bdd2.3 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℝ$
lo1bdd2.4 ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)$
lo1bdd2.5 ${⊢}\left({\phi }\wedge \left({y}\in ℝ\wedge {C}\le {y}\right)\right)\to {M}\in ℝ$
lo1bdd2.6 ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge \left(\left({y}\in ℝ\wedge {C}\le {y}\right)\wedge {x}<{y}\right)\right)\to {B}\le {M}$
Assertion lo1bdd2 ${⊢}{\phi }\to \exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {m}$

### Proof

Step Hyp Ref Expression
1 lo1bdd2.1 ${⊢}{\phi }\to {A}\subseteq ℝ$
2 lo1bdd2.2 ${⊢}{\phi }\to {C}\in ℝ$
3 lo1bdd2.3 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℝ$
4 lo1bdd2.4 ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)$
5 lo1bdd2.5 ${⊢}\left({\phi }\wedge \left({y}\in ℝ\wedge {C}\le {y}\right)\right)\to {M}\in ℝ$
6 lo1bdd2.6 ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge \left(\left({y}\in ℝ\wedge {C}\le {y}\right)\wedge {x}<{y}\right)\right)\to {B}\le {M}$
7 1 3 2 ello1mpt2 ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)↔\exists {y}\in \left[{C},\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\exists {n}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {n}\right)\right)$
8 4 7 mpbid ${⊢}{\phi }\to \exists {y}\in \left[{C},\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\exists {n}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {n}\right)$
9 elicopnf ${⊢}{C}\in ℝ\to \left({y}\in \left[{C},\mathrm{+\infty }\right)↔\left({y}\in ℝ\wedge {C}\le {y}\right)\right)$
10 2 9 syl ${⊢}{\phi }\to \left({y}\in \left[{C},\mathrm{+\infty }\right)↔\left({y}\in ℝ\wedge {C}\le {y}\right)\right)$
11 10 biimpa ${⊢}\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\to \left({y}\in ℝ\wedge {C}\le {y}\right)$
12 11 5 syldan ${⊢}\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\to {M}\in ℝ$
13 12 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge \left({n}\in ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {n}\right)\right)\right)\wedge {n}\le {M}\right)\to {M}\in ℝ$
14 simplrl ${⊢}\left(\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge \left({n}\in ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {n}\right)\right)\right)\wedge ¬{n}\le {M}\right)\to {n}\in ℝ$
15 13 14 ifclda ${⊢}\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge \left({n}\in ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {n}\right)\right)\right)\to if\left({n}\le {M},{M},{n}\right)\in ℝ$
16 1 ad2antrr ${⊢}\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge {n}\in ℝ\right)\to {A}\subseteq ℝ$
17 16 sselda ${⊢}\left(\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge {n}\in ℝ\right)\wedge {x}\in {A}\right)\to {x}\in ℝ$
18 11 simpld ${⊢}\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\to {y}\in ℝ$
19 18 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge {n}\in ℝ\right)\wedge {x}\in {A}\right)\to {y}\in ℝ$
20 17 19 ltnled ${⊢}\left(\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge {n}\in ℝ\right)\wedge {x}\in {A}\right)\to \left({x}<{y}↔¬{y}\le {x}\right)$
21 6 expr ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge \left({y}\in ℝ\wedge {C}\le {y}\right)\right)\to \left({x}<{y}\to {B}\le {M}\right)$
22 21 an32s ${⊢}\left(\left({\phi }\wedge \left({y}\in ℝ\wedge {C}\le {y}\right)\right)\wedge {x}\in {A}\right)\to \left({x}<{y}\to {B}\le {M}\right)$
23 11 22 syldanl ${⊢}\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge {x}\in {A}\right)\to \left({x}<{y}\to {B}\le {M}\right)$
24 23 adantlr ${⊢}\left(\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge {n}\in ℝ\right)\wedge {x}\in {A}\right)\to \left({x}<{y}\to {B}\le {M}\right)$
25 simplr ${⊢}\left(\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge {n}\in ℝ\right)\wedge {x}\in {A}\right)\to {n}\in ℝ$
26 12 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge {n}\in ℝ\right)\wedge {x}\in {A}\right)\to {M}\in ℝ$
27 max2 ${⊢}\left({n}\in ℝ\wedge {M}\in ℝ\right)\to {M}\le if\left({n}\le {M},{M},{n}\right)$
28 25 26 27 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge {n}\in ℝ\right)\wedge {x}\in {A}\right)\to {M}\le if\left({n}\le {M},{M},{n}\right)$
29 3 ad4ant14 ${⊢}\left(\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge {n}\in ℝ\right)\wedge {x}\in {A}\right)\to {B}\in ℝ$
30 12 ad5ant12 ${⊢}\left(\left(\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge {n}\in ℝ\right)\wedge {x}\in {A}\right)\wedge {n}\le {M}\right)\to {M}\in ℝ$
31 simpllr ${⊢}\left(\left(\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge {n}\in ℝ\right)\wedge {x}\in {A}\right)\wedge ¬{n}\le {M}\right)\to {n}\in ℝ$
32 30 31 ifclda ${⊢}\left(\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge {n}\in ℝ\right)\wedge {x}\in {A}\right)\to if\left({n}\le {M},{M},{n}\right)\in ℝ$
33 letr ${⊢}\left({B}\in ℝ\wedge {M}\in ℝ\wedge if\left({n}\le {M},{M},{n}\right)\in ℝ\right)\to \left(\left({B}\le {M}\wedge {M}\le if\left({n}\le {M},{M},{n}\right)\right)\to {B}\le if\left({n}\le {M},{M},{n}\right)\right)$
34 29 26 32 33 syl3anc ${⊢}\left(\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge {n}\in ℝ\right)\wedge {x}\in {A}\right)\to \left(\left({B}\le {M}\wedge {M}\le if\left({n}\le {M},{M},{n}\right)\right)\to {B}\le if\left({n}\le {M},{M},{n}\right)\right)$
35 28 34 mpan2d ${⊢}\left(\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge {n}\in ℝ\right)\wedge {x}\in {A}\right)\to \left({B}\le {M}\to {B}\le if\left({n}\le {M},{M},{n}\right)\right)$
36 24 35 syld ${⊢}\left(\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge {n}\in ℝ\right)\wedge {x}\in {A}\right)\to \left({x}<{y}\to {B}\le if\left({n}\le {M},{M},{n}\right)\right)$
37 20 36 sylbird ${⊢}\left(\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge {n}\in ℝ\right)\wedge {x}\in {A}\right)\to \left(¬{y}\le {x}\to {B}\le if\left({n}\le {M},{M},{n}\right)\right)$
38 max1 ${⊢}\left({n}\in ℝ\wedge {M}\in ℝ\right)\to {n}\le if\left({n}\le {M},{M},{n}\right)$
39 25 26 38 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge {n}\in ℝ\right)\wedge {x}\in {A}\right)\to {n}\le if\left({n}\le {M},{M},{n}\right)$
40 letr ${⊢}\left({B}\in ℝ\wedge {n}\in ℝ\wedge if\left({n}\le {M},{M},{n}\right)\in ℝ\right)\to \left(\left({B}\le {n}\wedge {n}\le if\left({n}\le {M},{M},{n}\right)\right)\to {B}\le if\left({n}\le {M},{M},{n}\right)\right)$
41 29 25 32 40 syl3anc ${⊢}\left(\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge {n}\in ℝ\right)\wedge {x}\in {A}\right)\to \left(\left({B}\le {n}\wedge {n}\le if\left({n}\le {M},{M},{n}\right)\right)\to {B}\le if\left({n}\le {M},{M},{n}\right)\right)$
42 39 41 mpan2d ${⊢}\left(\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge {n}\in ℝ\right)\wedge {x}\in {A}\right)\to \left({B}\le {n}\to {B}\le if\left({n}\le {M},{M},{n}\right)\right)$
43 37 42 jad ${⊢}\left(\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge {n}\in ℝ\right)\wedge {x}\in {A}\right)\to \left(\left({y}\le {x}\to {B}\le {n}\right)\to {B}\le if\left({n}\le {M},{M},{n}\right)\right)$
44 43 ralimdva ${⊢}\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge {n}\in ℝ\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {n}\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le if\left({n}\le {M},{M},{n}\right)\right)$
45 44 impr ${⊢}\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge \left({n}\in ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {n}\right)\right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le if\left({n}\le {M},{M},{n}\right)$
46 brralrspcev ${⊢}\left(if\left({n}\le {M},{M},{n}\right)\in ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le if\left({n}\le {M},{M},{n}\right)\right)\to \exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {m}$
47 15 45 46 syl2anc ${⊢}\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge \left({n}\in ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {n}\right)\right)\right)\to \exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {m}$
48 47 expr ${⊢}\left(\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\wedge {n}\in ℝ\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {n}\right)\to \exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {m}\right)$
49 48 rexlimdva ${⊢}\left({\phi }\wedge {y}\in \left[{C},\mathrm{+\infty }\right)\right)\to \left(\exists {n}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {n}\right)\to \exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {m}\right)$
50 49 rexlimdva ${⊢}{\phi }\to \left(\exists {y}\in \left[{C},\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\exists {n}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {n}\right)\to \exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {m}\right)$
51 8 50 mpd ${⊢}{\phi }\to \exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {m}$