# Metamath Proof Explorer

## Theorem limsupre

Description: If a sequence is bounded, then the limsup is real. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 13-Sep-2020)

Ref Expression
Hypotheses limsupre.1 ${⊢}{\phi }\to {B}\subseteq ℝ$
limsupre.2 ${⊢}{\phi }\to sup\left({B},{ℝ}^{*},<\right)=\mathrm{+\infty }$
limsupre.f ${⊢}{\phi }\to {F}:{B}⟶ℝ$
limsupre.bnd ${⊢}{\phi }\to \exists {b}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)$
Assertion limsupre ${⊢}{\phi }\to \mathrm{lim sup}\left({F}\right)\in ℝ$

### Proof

Step Hyp Ref Expression
1 limsupre.1 ${⊢}{\phi }\to {B}\subseteq ℝ$
2 limsupre.2 ${⊢}{\phi }\to sup\left({B},{ℝ}^{*},<\right)=\mathrm{+\infty }$
3 limsupre.f ${⊢}{\phi }\to {F}:{B}⟶ℝ$
4 limsupre.bnd ${⊢}{\phi }\to \exists {b}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)$
5 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
6 5 a1i ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to \mathrm{-\infty }\in {ℝ}^{*}$
7 renegcl ${⊢}{b}\in ℝ\to -{b}\in ℝ$
8 7 rexrd ${⊢}{b}\in ℝ\to -{b}\in {ℝ}^{*}$
9 8 ad2antlr ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to -{b}\in {ℝ}^{*}$
10 reex ${⊢}ℝ\in \mathrm{V}$
11 10 a1i ${⊢}{\phi }\to ℝ\in \mathrm{V}$
12 11 1 ssexd ${⊢}{\phi }\to {B}\in \mathrm{V}$
13 fex ${⊢}\left({F}:{B}⟶ℝ\wedge {B}\in \mathrm{V}\right)\to {F}\in \mathrm{V}$
14 3 12 13 syl2anc ${⊢}{\phi }\to {F}\in \mathrm{V}$
15 limsupcl ${⊢}{F}\in \mathrm{V}\to \mathrm{lim sup}\left({F}\right)\in {ℝ}^{*}$
16 14 15 syl ${⊢}{\phi }\to \mathrm{lim sup}\left({F}\right)\in {ℝ}^{*}$
17 16 ad2antrr ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to \mathrm{lim sup}\left({F}\right)\in {ℝ}^{*}$
18 7 mnfltd ${⊢}{b}\in ℝ\to \mathrm{-\infty }<-{b}$
19 18 ad2antlr ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to \mathrm{-\infty }<-{b}$
20 1 ad2antrr ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to {B}\subseteq ℝ$
21 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
22 21 a1i ${⊢}{\phi }\to ℝ\subseteq {ℝ}^{*}$
23 3 22 fssd ${⊢}{\phi }\to {F}:{B}⟶{ℝ}^{*}$
24 23 ad2antrr ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to {F}:{B}⟶{ℝ}^{*}$
25 2 ad2antrr ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to sup\left({B},{ℝ}^{*},<\right)=\mathrm{+\infty }$
26 simpr ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)$
27 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {b}\in ℝ\right)$
28 nfre1 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)$
29 27 28 nfan ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)$
30 nfv ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {b}\in ℝ\right)$
31 nfv ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}{k}\in ℝ$
32 nfra1 ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)$
33 30 31 32 nf3an ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge {k}\in ℝ\wedge \forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)$
34 simp13 ${⊢}\left(\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge {k}\in ℝ\wedge \forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\wedge {j}\in {B}\wedge {k}\le {j}\right)\to \forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)$
35 simp2 ${⊢}\left(\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge {k}\in ℝ\wedge \forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\wedge {j}\in {B}\wedge {k}\le {j}\right)\to {j}\in {B}$
36 simp3 ${⊢}\left(\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge {k}\in ℝ\wedge \forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\wedge {j}\in {B}\wedge {k}\le {j}\right)\to {k}\le {j}$
37 rspa ${⊢}\left(\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\wedge {j}\in {B}\right)\to \left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)$
38 37 imp ${⊢}\left(\left(\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\wedge {j}\in {B}\right)\wedge {k}\le {j}\right)\to \left|{F}\left({j}\right)\right|\le {b}$
39 34 35 36 38 syl21anc ${⊢}\left(\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge {k}\in ℝ\wedge \forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\wedge {j}\in {B}\wedge {k}\le {j}\right)\to \left|{F}\left({j}\right)\right|\le {b}$
40 simp11l ${⊢}\left(\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge {k}\in ℝ\wedge \forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\wedge {j}\in {B}\wedge {k}\le {j}\right)\to {\phi }$
41 3 ffvelrnda ${⊢}\left({\phi }\wedge {j}\in {B}\right)\to {F}\left({j}\right)\in ℝ$
42 40 35 41 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge {k}\in ℝ\wedge \forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\wedge {j}\in {B}\wedge {k}\le {j}\right)\to {F}\left({j}\right)\in ℝ$
43 simp11r ${⊢}\left(\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge {k}\in ℝ\wedge \forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\wedge {j}\in {B}\wedge {k}\le {j}\right)\to {b}\in ℝ$
44 42 43 absled ${⊢}\left(\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge {k}\in ℝ\wedge \forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\wedge {j}\in {B}\wedge {k}\le {j}\right)\to \left(\left|{F}\left({j}\right)\right|\le {b}↔\left(-{b}\le {F}\left({j}\right)\wedge {F}\left({j}\right)\le {b}\right)\right)$
45 39 44 mpbid ${⊢}\left(\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge {k}\in ℝ\wedge \forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\wedge {j}\in {B}\wedge {k}\le {j}\right)\to \left(-{b}\le {F}\left({j}\right)\wedge {F}\left({j}\right)\le {b}\right)$
46 45 simpld ${⊢}\left(\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge {k}\in ℝ\wedge \forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\wedge {j}\in {B}\wedge {k}\le {j}\right)\to -{b}\le {F}\left({j}\right)$
47 46 3exp ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge {k}\in ℝ\wedge \forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to \left({j}\in {B}\to \left({k}\le {j}\to -{b}\le {F}\left({j}\right)\right)\right)$
48 33 47 ralrimi ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge {k}\in ℝ\wedge \forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to \forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to -{b}\le {F}\left({j}\right)\right)$
49 48 3exp ${⊢}\left({\phi }\wedge {b}\in ℝ\right)\to \left({k}\in ℝ\to \left(\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\to \forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to -{b}\le {F}\left({j}\right)\right)\right)\right)$
50 49 adantr ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to \left({k}\in ℝ\to \left(\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\to \forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to -{b}\le {F}\left({j}\right)\right)\right)\right)$
51 29 50 reximdai ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to \left(\exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\to \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to -{b}\le {F}\left({j}\right)\right)\right)$
52 26 51 mpd ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to -{b}\le {F}\left({j}\right)\right)$
53 breq2 ${⊢}{i}={j}\to \left({h}\le {i}↔{h}\le {j}\right)$
54 fveq2 ${⊢}{i}={j}\to {F}\left({i}\right)={F}\left({j}\right)$
55 54 breq2d ${⊢}{i}={j}\to \left(-{b}\le {F}\left({i}\right)↔-{b}\le {F}\left({j}\right)\right)$
56 53 55 imbi12d ${⊢}{i}={j}\to \left(\left({h}\le {i}\to -{b}\le {F}\left({i}\right)\right)↔\left({h}\le {j}\to -{b}\le {F}\left({j}\right)\right)\right)$
57 56 cbvralv ${⊢}\forall {i}\in {B}\phantom{\rule{.4em}{0ex}}\left({h}\le {i}\to -{b}\le {F}\left({i}\right)\right)↔\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({h}\le {j}\to -{b}\le {F}\left({j}\right)\right)$
58 breq1 ${⊢}{h}={k}\to \left({h}\le {j}↔{k}\le {j}\right)$
59 58 imbi1d ${⊢}{h}={k}\to \left(\left({h}\le {j}\to -{b}\le {F}\left({j}\right)\right)↔\left({k}\le {j}\to -{b}\le {F}\left({j}\right)\right)\right)$
60 59 ralbidv ${⊢}{h}={k}\to \left(\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({h}\le {j}\to -{b}\le {F}\left({j}\right)\right)↔\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to -{b}\le {F}\left({j}\right)\right)\right)$
61 57 60 syl5bb ${⊢}{h}={k}\to \left(\forall {i}\in {B}\phantom{\rule{.4em}{0ex}}\left({h}\le {i}\to -{b}\le {F}\left({i}\right)\right)↔\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to -{b}\le {F}\left({j}\right)\right)\right)$
62 61 cbvrexv ${⊢}\exists {h}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {i}\in {B}\phantom{\rule{.4em}{0ex}}\left({h}\le {i}\to -{b}\le {F}\left({i}\right)\right)↔\exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to -{b}\le {F}\left({j}\right)\right)$
63 52 62 sylibr ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to \exists {h}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {i}\in {B}\phantom{\rule{.4em}{0ex}}\left({h}\le {i}\to -{b}\le {F}\left({i}\right)\right)$
64 20 24 9 25 63 limsupbnd2 ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to -{b}\le \mathrm{lim sup}\left({F}\right)$
65 6 9 17 19 64 xrltletrd ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to \mathrm{-\infty }<\mathrm{lim sup}\left({F}\right)$
66 65 4 r19.29a ${⊢}{\phi }\to \mathrm{-\infty }<\mathrm{lim sup}\left({F}\right)$
67 rexr ${⊢}{b}\in ℝ\to {b}\in {ℝ}^{*}$
68 67 ad2antlr ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to {b}\in {ℝ}^{*}$
69 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
70 69 a1i ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to \mathrm{+\infty }\in {ℝ}^{*}$
71 45 simprd ${⊢}\left(\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge {k}\in ℝ\wedge \forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\wedge {j}\in {B}\wedge {k}\le {j}\right)\to {F}\left({j}\right)\le {b}$
72 71 3exp ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge {k}\in ℝ\wedge \forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to \left({j}\in {B}\to \left({k}\le {j}\to {F}\left({j}\right)\le {b}\right)\right)$
73 33 72 ralrimi ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge {k}\in ℝ\wedge \forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to \forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to {F}\left({j}\right)\le {b}\right)$
74 73 3exp ${⊢}\left({\phi }\wedge {b}\in ℝ\right)\to \left({k}\in ℝ\to \left(\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\to \forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to {F}\left({j}\right)\le {b}\right)\right)\right)$
75 74 adantr ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to \left({k}\in ℝ\to \left(\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\to \forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to {F}\left({j}\right)\le {b}\right)\right)\right)$
76 29 75 reximdai ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to \left(\exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\to \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to {F}\left({j}\right)\le {b}\right)\right)$
77 26 76 mpd ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to {F}\left({j}\right)\le {b}\right)$
78 54 breq1d ${⊢}{i}={j}\to \left({F}\left({i}\right)\le {b}↔{F}\left({j}\right)\le {b}\right)$
79 53 78 imbi12d ${⊢}{i}={j}\to \left(\left({h}\le {i}\to {F}\left({i}\right)\le {b}\right)↔\left({h}\le {j}\to {F}\left({j}\right)\le {b}\right)\right)$
80 79 cbvralv ${⊢}\forall {i}\in {B}\phantom{\rule{.4em}{0ex}}\left({h}\le {i}\to {F}\left({i}\right)\le {b}\right)↔\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({h}\le {j}\to {F}\left({j}\right)\le {b}\right)$
81 58 imbi1d ${⊢}{h}={k}\to \left(\left({h}\le {j}\to {F}\left({j}\right)\le {b}\right)↔\left({k}\le {j}\to {F}\left({j}\right)\le {b}\right)\right)$
82 81 ralbidv ${⊢}{h}={k}\to \left(\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({h}\le {j}\to {F}\left({j}\right)\le {b}\right)↔\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to {F}\left({j}\right)\le {b}\right)\right)$
83 80 82 syl5bb ${⊢}{h}={k}\to \left(\forall {i}\in {B}\phantom{\rule{.4em}{0ex}}\left({h}\le {i}\to {F}\left({i}\right)\le {b}\right)↔\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to {F}\left({j}\right)\le {b}\right)\right)$
84 83 cbvrexv ${⊢}\exists {h}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {i}\in {B}\phantom{\rule{.4em}{0ex}}\left({h}\le {i}\to {F}\left({i}\right)\le {b}\right)↔\exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to {F}\left({j}\right)\le {b}\right)$
85 77 84 sylibr ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to \exists {h}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {i}\in {B}\phantom{\rule{.4em}{0ex}}\left({h}\le {i}\to {F}\left({i}\right)\le {b}\right)$
86 20 24 68 85 limsupbnd1 ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to \mathrm{lim sup}\left({F}\right)\le {b}$
87 ltpnf ${⊢}{b}\in ℝ\to {b}<\mathrm{+\infty }$
88 87 ad2antlr ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to {b}<\mathrm{+\infty }$
89 17 68 70 86 88 xrlelttrd ${⊢}\left(\left({\phi }\wedge {b}\in ℝ\right)\wedge \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {B}\phantom{\rule{.4em}{0ex}}\left({k}\le {j}\to \left|{F}\left({j}\right)\right|\le {b}\right)\right)\to \mathrm{lim sup}\left({F}\right)<\mathrm{+\infty }$
90 89 4 r19.29a ${⊢}{\phi }\to \mathrm{lim sup}\left({F}\right)<\mathrm{+\infty }$
91 xrrebnd ${⊢}\mathrm{lim sup}\left({F}\right)\in {ℝ}^{*}\to \left(\mathrm{lim sup}\left({F}\right)\in ℝ↔\left(\mathrm{-\infty }<\mathrm{lim sup}\left({F}\right)\wedge \mathrm{lim sup}\left({F}\right)<\mathrm{+\infty }\right)\right)$
92 16 91 syl ${⊢}{\phi }\to \left(\mathrm{lim sup}\left({F}\right)\in ℝ↔\left(\mathrm{-\infty }<\mathrm{lim sup}\left({F}\right)\wedge \mathrm{lim sup}\left({F}\right)<\mathrm{+\infty }\right)\right)$
93 66 90 92 mpbir2and ${⊢}{\phi }\to \mathrm{lim sup}\left({F}\right)\in ℝ$