# Metamath Proof Explorer

## Theorem limsupubuzlem

Description: If the limsup is not +oo , then the function is bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupubuzlem.j ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}{\phi }$
limsupubuzlem.e ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{X}$
limsupubuzlem.m ${⊢}{\phi }\to {M}\in ℤ$
limsupubuzlem.z ${⊢}{Z}={ℤ}_{\ge {M}}$
limsupubuzlem.f ${⊢}{\phi }\to {F}:{Z}⟶ℝ$
limsupubuzlem.y ${⊢}{\phi }\to {Y}\in ℝ$
limsupubuzlem.k ${⊢}{\phi }\to {K}\in ℝ$
limsupubuzlem.b ${⊢}{\phi }\to \forall {j}\in {Z}\phantom{\rule{.4em}{0ex}}\left({K}\le {j}\to {F}\left({j}\right)\le {Y}\right)$
limsupubuzlem.n ${⊢}{N}=if\left(⌈{K}⌉\le {M},{M},⌈{K}⌉\right)$
limsupubuzlem.w ${⊢}{W}=sup\left(\mathrm{ran}\left({j}\in \left({M}\dots {N}\right)⟼{F}\left({j}\right)\right),ℝ,<\right)$
limsupubuzlem.x ${⊢}{X}=if\left({W}\le {Y},{Y},{W}\right)$
Assertion limsupubuzlem ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {x}$

### Proof

Step Hyp Ref Expression
1 limsupubuzlem.j ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}{\phi }$
2 limsupubuzlem.e ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{X}$
3 limsupubuzlem.m ${⊢}{\phi }\to {M}\in ℤ$
4 limsupubuzlem.z ${⊢}{Z}={ℤ}_{\ge {M}}$
5 limsupubuzlem.f ${⊢}{\phi }\to {F}:{Z}⟶ℝ$
6 limsupubuzlem.y ${⊢}{\phi }\to {Y}\in ℝ$
7 limsupubuzlem.k ${⊢}{\phi }\to {K}\in ℝ$
8 limsupubuzlem.b ${⊢}{\phi }\to \forall {j}\in {Z}\phantom{\rule{.4em}{0ex}}\left({K}\le {j}\to {F}\left({j}\right)\le {Y}\right)$
9 limsupubuzlem.n ${⊢}{N}=if\left(⌈{K}⌉\le {M},{M},⌈{K}⌉\right)$
10 limsupubuzlem.w ${⊢}{W}=sup\left(\mathrm{ran}\left({j}\in \left({M}\dots {N}\right)⟼{F}\left({j}\right)\right),ℝ,<\right)$
11 limsupubuzlem.x ${⊢}{X}=if\left({W}\le {Y},{Y},{W}\right)$
12 10 a1i ${⊢}{\phi }\to {W}=sup\left(\mathrm{ran}\left({j}\in \left({M}\dots {N}\right)⟼{F}\left({j}\right)\right),ℝ,<\right)$
13 ltso ${⊢}<\mathrm{Or}ℝ$
14 13 a1i ${⊢}{\phi }\to <\mathrm{Or}ℝ$
15 fzfid ${⊢}{\phi }\to \left({M}\dots {N}\right)\in \mathrm{Fin}$
16 eqid ${⊢}{ℤ}_{\ge {M}}={ℤ}_{\ge {M}}$
17 9 a1i ${⊢}{\phi }\to {N}=if\left(⌈{K}⌉\le {M},{M},⌈{K}⌉\right)$
18 ceilcl ${⊢}{K}\in ℝ\to ⌈{K}⌉\in ℤ$
19 7 18 syl ${⊢}{\phi }\to ⌈{K}⌉\in ℤ$
20 3 19 ifcld ${⊢}{\phi }\to if\left(⌈{K}⌉\le {M},{M},⌈{K}⌉\right)\in ℤ$
21 17 20 eqeltrd ${⊢}{\phi }\to {N}\in ℤ$
22 19 zred ${⊢}{\phi }\to ⌈{K}⌉\in ℝ$
23 3 zred ${⊢}{\phi }\to {M}\in ℝ$
24 max2 ${⊢}\left(⌈{K}⌉\in ℝ\wedge {M}\in ℝ\right)\to {M}\le if\left(⌈{K}⌉\le {M},{M},⌈{K}⌉\right)$
25 22 23 24 syl2anc ${⊢}{\phi }\to {M}\le if\left(⌈{K}⌉\le {M},{M},⌈{K}⌉\right)$
26 17 eqcomd ${⊢}{\phi }\to if\left(⌈{K}⌉\le {M},{M},⌈{K}⌉\right)={N}$
27 25 26 breqtrd ${⊢}{\phi }\to {M}\le {N}$
28 16 3 21 27 eluzd ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
29 eluzfz2 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}\in \left({M}\dots {N}\right)$
30 28 29 syl ${⊢}{\phi }\to {N}\in \left({M}\dots {N}\right)$
31 30 ne0d ${⊢}{\phi }\to \left({M}\dots {N}\right)\ne \varnothing$
32 5 adantr ${⊢}\left({\phi }\wedge {j}\in \left({M}\dots {N}\right)\right)\to {F}:{Z}⟶ℝ$
33 3 adantr ${⊢}\left({\phi }\wedge {j}\in \left({M}\dots {N}\right)\right)\to {M}\in ℤ$
34 elfzelz ${⊢}{j}\in \left({M}\dots {N}\right)\to {j}\in ℤ$
35 34 adantl ${⊢}\left({\phi }\wedge {j}\in \left({M}\dots {N}\right)\right)\to {j}\in ℤ$
36 elfzle1 ${⊢}{j}\in \left({M}\dots {N}\right)\to {M}\le {j}$
37 36 adantl ${⊢}\left({\phi }\wedge {j}\in \left({M}\dots {N}\right)\right)\to {M}\le {j}$
38 16 33 35 37 eluzd ${⊢}\left({\phi }\wedge {j}\in \left({M}\dots {N}\right)\right)\to {j}\in {ℤ}_{\ge {M}}$
39 38 4 eleqtrrdi ${⊢}\left({\phi }\wedge {j}\in \left({M}\dots {N}\right)\right)\to {j}\in {Z}$
40 32 39 ffvelrnd ${⊢}\left({\phi }\wedge {j}\in \left({M}\dots {N}\right)\right)\to {F}\left({j}\right)\in ℝ$
41 1 14 15 31 40 fisupclrnmpt ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({j}\in \left({M}\dots {N}\right)⟼{F}\left({j}\right)\right),ℝ,<\right)\in ℝ$
42 12 41 eqeltrd ${⊢}{\phi }\to {W}\in ℝ$
43 6 42 ifcld ${⊢}{\phi }\to if\left({W}\le {Y},{Y},{W}\right)\in ℝ$
44 11 43 eqeltrid ${⊢}{\phi }\to {X}\in ℝ$
45 5 ffvelrnda ${⊢}\left({\phi }\wedge {j}\in {Z}\right)\to {F}\left({j}\right)\in ℝ$
46 45 adantr ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {j}\le {N}\right)\to {F}\left({j}\right)\in ℝ$
47 42 ad2antrr ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {j}\le {N}\right)\to {W}\in ℝ$
48 44 ad2antrr ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {j}\le {N}\right)\to {X}\in ℝ$
49 simpll ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {j}\le {N}\right)\to {\phi }$
50 3 ad2antrr ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {j}\le {N}\right)\to {M}\in ℤ$
51 21 ad2antrr ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {j}\le {N}\right)\to {N}\in ℤ$
52 4 eluzelz2 ${⊢}{j}\in {Z}\to {j}\in ℤ$
53 52 ad2antlr ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {j}\le {N}\right)\to {j}\in ℤ$
54 4 eleq2i ${⊢}{j}\in {Z}↔{j}\in {ℤ}_{\ge {M}}$
55 54 biimpi ${⊢}{j}\in {Z}\to {j}\in {ℤ}_{\ge {M}}$
56 eluzle ${⊢}{j}\in {ℤ}_{\ge {M}}\to {M}\le {j}$
57 55 56 syl ${⊢}{j}\in {Z}\to {M}\le {j}$
58 57 ad2antlr ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {j}\le {N}\right)\to {M}\le {j}$
59 simpr ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {j}\le {N}\right)\to {j}\le {N}$
60 50 51 53 58 59 elfzd ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {j}\le {N}\right)\to {j}\in \left({M}\dots {N}\right)$
61 1 15 40 fimaxre4 ${⊢}{\phi }\to \exists {b}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in \left({M}\dots {N}\right)\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {b}$
62 1 40 61 suprubrnmpt ${⊢}\left({\phi }\wedge {j}\in \left({M}\dots {N}\right)\right)\to {F}\left({j}\right)\le sup\left(\mathrm{ran}\left({j}\in \left({M}\dots {N}\right)⟼{F}\left({j}\right)\right),ℝ,<\right)$
63 62 10 breqtrrdi ${⊢}\left({\phi }\wedge {j}\in \left({M}\dots {N}\right)\right)\to {F}\left({j}\right)\le {W}$
64 49 60 63 syl2anc ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {j}\le {N}\right)\to {F}\left({j}\right)\le {W}$
65 max1 ${⊢}\left({W}\in ℝ\wedge {Y}\in ℝ\right)\to {W}\le if\left({W}\le {Y},{Y},{W}\right)$
66 42 6 65 syl2anc ${⊢}{\phi }\to {W}\le if\left({W}\le {Y},{Y},{W}\right)$
67 66 11 breqtrrdi ${⊢}{\phi }\to {W}\le {X}$
68 67 ad2antrr ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {j}\le {N}\right)\to {W}\le {X}$
69 46 47 48 64 68 letrd ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {j}\le {N}\right)\to {F}\left({j}\right)\le {X}$
70 7 ad2antrr ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge ¬{j}\le {N}\right)\to {K}\in ℝ$
71 uzssre ${⊢}{ℤ}_{\ge {M}}\subseteq ℝ$
72 4 71 eqsstri ${⊢}{Z}\subseteq ℝ$
73 72 sseli ${⊢}{j}\in {Z}\to {j}\in ℝ$
74 73 ad2antlr ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge ¬{j}\le {N}\right)\to {j}\in ℝ$
75 71 28 sseldi ${⊢}{\phi }\to {N}\in ℝ$
76 75 ad2antrr ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge ¬{j}\le {N}\right)\to {N}\in ℝ$
77 ceilge ${⊢}{K}\in ℝ\to {K}\le ⌈{K}⌉$
78 7 77 syl ${⊢}{\phi }\to {K}\le ⌈{K}⌉$
79 max1 ${⊢}\left(⌈{K}⌉\in ℝ\wedge {M}\in ℝ\right)\to ⌈{K}⌉\le if\left(⌈{K}⌉\le {M},{M},⌈{K}⌉\right)$
80 22 23 79 syl2anc ${⊢}{\phi }\to ⌈{K}⌉\le if\left(⌈{K}⌉\le {M},{M},⌈{K}⌉\right)$
81 80 26 breqtrd ${⊢}{\phi }\to ⌈{K}⌉\le {N}$
82 7 22 75 78 81 letrd ${⊢}{\phi }\to {K}\le {N}$
83 82 ad2antrr ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge ¬{j}\le {N}\right)\to {K}\le {N}$
84 simpr ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge ¬{j}\le {N}\right)\to ¬{j}\le {N}$
85 76 74 ltnled ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge ¬{j}\le {N}\right)\to \left({N}<{j}↔¬{j}\le {N}\right)$
86 84 85 mpbird ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge ¬{j}\le {N}\right)\to {N}<{j}$
87 70 76 74 83 86 lelttrd ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge ¬{j}\le {N}\right)\to {K}<{j}$
88 70 74 87 ltled ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge ¬{j}\le {N}\right)\to {K}\le {j}$
89 45 adantr ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {K}\le {j}\right)\to {F}\left({j}\right)\in ℝ$
90 6 ad2antrr ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {K}\le {j}\right)\to {Y}\in ℝ$
91 44 ad2antrr ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {K}\le {j}\right)\to {X}\in ℝ$
92 simpr ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {K}\le {j}\right)\to {K}\le {j}$
93 8 r19.21bi ${⊢}\left({\phi }\wedge {j}\in {Z}\right)\to \left({K}\le {j}\to {F}\left({j}\right)\le {Y}\right)$
94 93 adantr ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {K}\le {j}\right)\to \left({K}\le {j}\to {F}\left({j}\right)\le {Y}\right)$
95 92 94 mpd ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {K}\le {j}\right)\to {F}\left({j}\right)\le {Y}$
96 max2 ${⊢}\left({W}\in ℝ\wedge {Y}\in ℝ\right)\to {Y}\le if\left({W}\le {Y},{Y},{W}\right)$
97 42 6 96 syl2anc ${⊢}{\phi }\to {Y}\le if\left({W}\le {Y},{Y},{W}\right)$
98 97 11 breqtrrdi ${⊢}{\phi }\to {Y}\le {X}$
99 98 ad2antrr ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {K}\le {j}\right)\to {Y}\le {X}$
100 89 90 91 95 99 letrd ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {K}\le {j}\right)\to {F}\left({j}\right)\le {X}$
101 88 100 syldan ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge ¬{j}\le {N}\right)\to {F}\left({j}\right)\le {X}$
102 69 101 pm2.61dan ${⊢}\left({\phi }\wedge {j}\in {Z}\right)\to {F}\left({j}\right)\le {X}$
103 102 ex ${⊢}{\phi }\to \left({j}\in {Z}\to {F}\left({j}\right)\le {X}\right)$
104 1 103 ralrimi ${⊢}{\phi }\to \forall {j}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {X}$
105 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {j}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {X}$
106 nfcv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{x}$
107 106 2 nfeq ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}{x}={X}$
108 breq2 ${⊢}{x}={X}\to \left({F}\left({j}\right)\le {x}↔{F}\left({j}\right)\le {X}\right)$
109 107 108 ralbid ${⊢}{x}={X}\to \left(\forall {j}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {x}↔\forall {j}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {X}\right)$
110 105 109 rspce ${⊢}\left({X}\in ℝ\wedge \forall {j}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {X}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {x}$
111 44 104 110 syl2anc ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {x}$