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 \mathbb{Z}$$
	liminflelimsupuz.2	$$⊢Z={\mathbb{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 \mathbb{Z}$$
2		liminflelimsupuz.2	$$⊢Z={\mathbb{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 ℝ\exists j\in \left[k,\mathrm{+\infty }\right)j\in Z$$
8	3	ffnd	$$⊢\phi \to FFnZ$$
9	8	adantr	$$⊢\left(\phi \wedge j\in Z\right)\to FFnZ$$
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	ffvelcdmda	$$⊢\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)j\in Z\to \exists j\in \left[k,\mathrm{+\infty }\right)F\left[\left[j,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\ne \varnothing \right)$$
28	27	ralimdva	$$⊢\phi \to \left(\forall k\in ℝ\exists j\in \left[k,\mathrm{+\infty }\right)j\in Z\to \forall k\in ℝ\exists j\in \left[k,\mathrm{+\infty }\right)F\left[\left[j,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\ne \varnothing \right)$$
29	7 28	mpd	$$⊢\phi \to \forall k\in ℝ\exists j\in \left[k,\mathrm{+\infty }\right)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)$$