# Metamath Proof Explorer

## Theorem liminflelimsupuz

Description: The superior limit is greater than or equal to the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses liminflelimsupuz.1 ${⊢}{\phi }\to {M}\in ℤ$
liminflelimsupuz.2 ${⊢}{Z}={ℤ}_{\ge {M}}$
liminflelimsupuz.3 ${⊢}{\phi }\to {F}:{Z}⟶{ℝ}^{*}$
Assertion liminflelimsupuz ${⊢}{\phi }\to \mathrm{lim inf}\left({F}\right)\le \mathrm{lim sup}\left({F}\right)$

### Proof

Step Hyp Ref Expression
1 liminflelimsupuz.1 ${⊢}{\phi }\to {M}\in ℤ$
2 liminflelimsupuz.2 ${⊢}{Z}={ℤ}_{\ge {M}}$
3 liminflelimsupuz.3 ${⊢}{\phi }\to {F}:{Z}⟶{ℝ}^{*}$
4 2 fvexi ${⊢}{Z}\in \mathrm{V}$
5 4 a1i ${⊢}{\phi }\to {Z}\in \mathrm{V}$
6 3 5 fexd ${⊢}{\phi }\to {F}\in \mathrm{V}$
7 1 2 uzubico2 ${⊢}{\phi }\to \forall {k}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {j}\in \left[{k},\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}{j}\in {Z}$
8 3 ffnd ${⊢}{\phi }\to {F}Fn{Z}$
9 8 adantr ${⊢}\left({\phi }\wedge {j}\in {Z}\right)\to {F}Fn{Z}$
10 simpr ${⊢}\left({\phi }\wedge {j}\in {Z}\right)\to {j}\in {Z}$
11 id ${⊢}{j}\in {Z}\to {j}\in {Z}$
12 2 11 uzxrd ${⊢}{j}\in {Z}\to {j}\in {ℝ}^{*}$
13 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
14 13 a1i ${⊢}{j}\in {Z}\to \mathrm{+\infty }\in {ℝ}^{*}$
15 12 xrleidd ${⊢}{j}\in {Z}\to {j}\le {j}$
16 2 11 uzred ${⊢}{j}\in {Z}\to {j}\in ℝ$
17 ltpnf ${⊢}{j}\in ℝ\to {j}<\mathrm{+\infty }$
18 16 17 syl ${⊢}{j}\in {Z}\to {j}<\mathrm{+\infty }$
19 12 14 12 15 18 elicod ${⊢}{j}\in {Z}\to {j}\in \left[{j},\mathrm{+\infty }\right)$
20 19 adantl ${⊢}\left({\phi }\wedge {j}\in {Z}\right)\to {j}\in \left[{j},\mathrm{+\infty }\right)$
21 9 10 20 fnfvimad ${⊢}\left({\phi }\wedge {j}\in {Z}\right)\to {F}\left({j}\right)\in {F}\left[\left[{j},\mathrm{+\infty }\right)\right]$
22 3 ffvelrnda ${⊢}\left({\phi }\wedge {j}\in {Z}\right)\to {F}\left({j}\right)\in {ℝ}^{*}$
23 21 22 elind ${⊢}\left({\phi }\wedge {j}\in {Z}\right)\to {F}\left({j}\right)\in \left({F}\left[\left[{j},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\right)$
24 23 ne0d ${⊢}\left({\phi }\wedge {j}\in {Z}\right)\to {F}\left[\left[{j},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\ne \varnothing$
25 24 ex ${⊢}{\phi }\to \left({j}\in {Z}\to {F}\left[\left[{j},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\ne \varnothing \right)$
26 25 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in ℝ\right)\wedge {j}\in \left[{k},\mathrm{+\infty }\right)\right)\to \left({j}\in {Z}\to {F}\left[\left[{j},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\ne \varnothing \right)$
27 26 reximdva ${⊢}\left({\phi }\wedge {k}\in ℝ\right)\to \left(\exists {j}\in \left[{k},\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}{j}\in {Z}\to \exists {j}\in \left[{k},\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}{F}\left[\left[{j},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\ne \varnothing \right)$
28 27 ralimdva ${⊢}{\phi }\to \left(\forall {k}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {j}\in \left[{k},\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}{j}\in {Z}\to \forall {k}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {j}\in \left[{k},\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}{F}\left[\left[{j},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\ne \varnothing \right)$
29 7 28 mpd ${⊢}{\phi }\to \forall {k}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {j}\in \left[{k},\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}{F}\left[\left[{j},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\ne \varnothing$
30 6 29 liminflelimsup ${⊢}{\phi }\to \mathrm{lim inf}\left({F}\right)\le \mathrm{lim sup}\left({F}\right)$