Theorem limsupvaluz

Description: The superior limit, when the domain of the function is a set of upper integers (the first condition is needed, otherwise the l.h.s. would be -oo and the r.h.s. would be +oo ). (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupvaluz.m	$$⊢\phi \to M\in \mathbb{Z}$$
	limsupvaluz.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	limsupvaluz.f	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
Assertion	limsupvaluz	$$⊢\phi \to \mathrm{lim\; sup}\left(F\right)=inf\left(\mathrm{ran}\left(k\in Z⟼sup\left(\mathrm{ran}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge k}}\right),{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)$$

Proof

Step	Hyp	Ref	Expression
1		limsupvaluz.m	$$⊢\phi \to M\in \mathbb{Z}$$
2		limsupvaluz.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3		limsupvaluz.f	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
4		eqid	$$⊢\left(i\in ℝ⟼sup\left(F\left[\left[i,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)=\left(i\in ℝ⟼sup\left(F\left[\left[i,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)$$
5	2	fvexi	$$⊢Z\in \mathrm{V}$$
6	5	a1i	$$⊢\phi \to Z\in \mathrm{V}$$
7	3 6	fexd	$$⊢\phi \to F\in \mathrm{V}$$
8	2	uzssre2	$$⊢Z\subseteq ℝ$$
9	8	a1i	$$⊢\phi \to Z\subseteq ℝ$$
10	2	uzsup	$$⊢M\in \mathbb{Z}\to sup\left(Z,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
11	1 10	syl	$$⊢\phi \to sup\left(Z,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
12	4 7 9 11	limsupval2	$$⊢\phi \to \mathrm{lim\; sup}\left(F\right)=inf\left(\left(i\in ℝ⟼sup\left(F\left[\left[i,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)\left[Z\right],{ℝ}^{*},<\right)$$
13	9	mptimass	$$⊢\phi \to \left(i\in ℝ⟼sup\left(F\left[\left[i,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)\left[Z\right]=\mathrm{ran}\left(i\in Z⟼sup\left(F\left[\left[i,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)$$
14		oveq1	$$⊢i=n\to \left[i,\mathrm{+\infty }\right)=\left[n,\mathrm{+\infty }\right)$$
15	14	imaeq2d	$$⊢i=n\to F\left[\left[i,\mathrm{+\infty }\right)\right]=F\left[\left[n,\mathrm{+\infty }\right)\right]$$
16	15	ineq1d	$$⊢i=n\to F\left[\left[i,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}=F\left[\left[n,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}$$
17	16	supeq1d	$$⊢i=n\to sup\left(F\left[\left[i,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)=sup\left(F\left[\left[n,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)$$
18	17	cbvmptv	$$⊢\left(i\in Z⟼sup\left(F\left[\left[i,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)=\left(n\in Z⟼sup\left(F\left[\left[n,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)$$
19	3	fimassd	$$⊢\phi \to F\left[\left[n,\mathrm{+\infty }\right)\right]\subseteq {ℝ}^{*}$$
20		dfss2	$$⊢F\left[\left[n,\mathrm{+\infty }\right)\right]\subseteq {ℝ}^{*}\leftrightarrow F\left[\left[n,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}=F\left[\left[n,\mathrm{+\infty }\right)\right]$$
21	19 20	sylib	$$⊢\phi \to F\left[\left[n,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}=F\left[\left[n,\mathrm{+\infty }\right)\right]$$
22	21	adantr	$$⊢\left(\phi \wedge n\in Z\right)\to F\left[\left[n,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}=F\left[\left[n,\mathrm{+\infty }\right)\right]$$
23		df-ima	$$⊢F\left[\left[n,\mathrm{+\infty }\right)\right]=\mathrm{ran}\left({F\upharpoonright }_{\left[n,\mathrm{+\infty }\right)}\right)$$
24	23	a1i	$$⊢\left(\phi \wedge n\in Z\right)\to F\left[\left[n,\mathrm{+\infty }\right)\right]=\mathrm{ran}\left({F\upharpoonright }_{\left[n,\mathrm{+\infty }\right)}\right)$$
25		resindm	$$⊢{F\upharpoonright }_{\left(\left[n,\mathrm{+\infty }\right)\cap \mathrm{dom}F\right)}={F\upharpoonright }_{\left[n,\mathrm{+\infty }\right)}$$
26	2	ineq1i	$$⊢Z\cap \left[n,\mathrm{+\infty }\right)={\mathbb{Z}}_{\ge M}\cap \left[n,\mathrm{+\infty }\right)$$
27	26	ineqcomi	$$⊢\left[n,\mathrm{+\infty }\right)\cap Z={\mathbb{Z}}_{\ge M}\cap \left[n,\mathrm{+\infty }\right)$$
28	3	fdmd	$$⊢\phi \to \mathrm{dom}F=Z$$
29	28	ineq2d	$$⊢\phi \to \left[n,\mathrm{+\infty }\right)\cap \mathrm{dom}F=\left[n,\mathrm{+\infty }\right)\cap Z$$
30	29	adantr	$$⊢\left(\phi \wedge n\in Z\right)\to \left[n,\mathrm{+\infty }\right)\cap \mathrm{dom}F=\left[n,\mathrm{+\infty }\right)\cap Z$$
31	2	eleq2i	$$⊢n\in Z\leftrightarrow n\in {\mathbb{Z}}_{\ge M}$$
32	31	bilani	$$⊢\left(\phi \wedge n\in Z\right)\to n\in {\mathbb{Z}}_{\ge M}$$
33	32	uzinico2	$$⊢\left(\phi \wedge n\in Z\right)\to {\mathbb{Z}}_{\ge n}={\mathbb{Z}}_{\ge M}\cap \left[n,\mathrm{+\infty }\right)$$
34	27 30 33	3eqtr4a	$$⊢\left(\phi \wedge n\in Z\right)\to \left[n,\mathrm{+\infty }\right)\cap \mathrm{dom}F={\mathbb{Z}}_{\ge n}$$
35	34	reseq2d	$$⊢\left(\phi \wedge n\in Z\right)\to {F\upharpoonright }_{\left(\left[n,\mathrm{+\infty }\right)\cap \mathrm{dom}F\right)}={F\upharpoonright }_{{\mathbb{Z}}_{\ge n}}$$
36	25 35	eqtr3id	$$⊢\left(\phi \wedge n\in Z\right)\to {F\upharpoonright }_{\left[n,\mathrm{+\infty }\right)}={F\upharpoonright }_{{\mathbb{Z}}_{\ge n}}$$
37	36	rneqd	$$⊢\left(\phi \wedge n\in Z\right)\to \mathrm{ran}\left({F\upharpoonright }_{\left[n,\mathrm{+\infty }\right)}\right)=\mathrm{ran}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge n}}\right)$$
38	22 24 37	3eqtrd	$$⊢\left(\phi \wedge n\in Z\right)\to F\left[\left[n,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}=\mathrm{ran}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge n}}\right)$$
39	38	supeq1d	$$⊢\left(\phi \wedge n\in Z\right)\to sup\left(F\left[\left[n,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge n}}\right),{ℝ}^{*},<\right)$$
40	39	mpteq2dva	$$⊢\phi \to \left(n\in Z⟼sup\left(F\left[\left[n,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)=\left(n\in Z⟼sup\left(\mathrm{ran}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge n}}\right),{ℝ}^{*},<\right)\right)$$
41	18 40	eqtrid	$$⊢\phi \to \left(i\in Z⟼sup\left(F\left[\left[i,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)=\left(n\in Z⟼sup\left(\mathrm{ran}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge n}}\right),{ℝ}^{*},<\right)\right)$$
42	41	rneqd	$$⊢\phi \to \mathrm{ran}\left(i\in Z⟼sup\left(F\left[\left[i,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)=\mathrm{ran}\left(n\in Z⟼sup\left(\mathrm{ran}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge n}}\right),{ℝ}^{*},<\right)\right)$$
43	13 42	eqtrd	$$⊢\phi \to \left(i\in ℝ⟼sup\left(F\left[\left[i,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)\left[Z\right]=\mathrm{ran}\left(n\in Z⟼sup\left(\mathrm{ran}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge n}}\right),{ℝ}^{*},<\right)\right)$$
44	43	infeq1d	$$⊢\phi \to inf\left(\left(i\in ℝ⟼sup\left(F\left[\left[i,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)\left[Z\right],{ℝ}^{*},<\right)=inf\left(\mathrm{ran}\left(n\in Z⟼sup\left(\mathrm{ran}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge n}}\right),{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)$$
45		fveq2	$$⊢n=k\to {\mathbb{Z}}_{\ge n}={\mathbb{Z}}_{\ge k}$$
46	45	reseq2d	$$⊢n=k\to {F\upharpoonright }_{{\mathbb{Z}}_{\ge n}}={F\upharpoonright }_{{\mathbb{Z}}_{\ge k}}$$
47	46	rneqd	$$⊢n=k\to \mathrm{ran}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge n}}\right)=\mathrm{ran}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge k}}\right)$$
48	47	supeq1d	$$⊢n=k\to sup\left(\mathrm{ran}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge n}}\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge k}}\right),{ℝ}^{*},<\right)$$
49	48	cbvmptv	$$⊢\left(n\in Z⟼sup\left(\mathrm{ran}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge n}}\right),{ℝ}^{*},<\right)\right)=\left(k\in Z⟼sup\left(\mathrm{ran}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge k}}\right),{ℝ}^{*},<\right)\right)$$
50	49	rneqi	$$⊢\mathrm{ran}\left(n\in Z⟼sup\left(\mathrm{ran}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge n}}\right),{ℝ}^{*},<\right)\right)=\mathrm{ran}\left(k\in Z⟼sup\left(\mathrm{ran}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge k}}\right),{ℝ}^{*},<\right)\right)$$
51	50	infeq1i	$$⊢inf\left(\mathrm{ran}\left(n\in Z⟼sup\left(\mathrm{ran}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge n}}\right),{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)=inf\left(\mathrm{ran}\left(k\in Z⟼sup\left(\mathrm{ran}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge k}}\right),{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)$$
52	51	a1i	$$⊢\phi \to inf\left(\mathrm{ran}\left(n\in Z⟼sup\left(\mathrm{ran}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge n}}\right),{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)=inf\left(\mathrm{ran}\left(k\in Z⟼sup\left(\mathrm{ran}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge k}}\right),{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)$$
53	12 44 52	3eqtrd	$$⊢\phi \to \mathrm{lim\; sup}\left(F\right)=inf\left(\mathrm{ran}\left(k\in Z⟼sup\left(\mathrm{ran}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge k}}\right),{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)$$