Theorem liminfresuz

Description: If the real part of the domain of a function is a subset of the integers, the inferior limit doesn't change when the function is restricted to an upper set of integers. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	liminfresuz.m	$$⊢\phi \to M\in \mathbb{Z}$$
	liminfresuz.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	liminfresuz.f	$$⊢\phi \to F\in V$$
	liminfresuz.d	$$⊢\phi \to \mathrm{dom}\left({F\upharpoonright }_{ℝ}\right)\subseteq \mathbb{Z}$$
Assertion	liminfresuz	$$⊢\phi \to \mathrm{lim\; inf}\left({F\upharpoonright }_Z\right)=\mathrm{lim\; inf}\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		liminfresuz.m	$$⊢\phi \to M\in \mathbb{Z}$$
2		liminfresuz.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3		liminfresuz.f	$$⊢\phi \to F\in V$$
4		liminfresuz.d	$$⊢\phi \to \mathrm{dom}\left({F\upharpoonright }_{ℝ}\right)\subseteq \mathbb{Z}$$
5		rescom	$$⊢{\left({F\upharpoonright }_Z\right)\upharpoonright }_{ℝ}={\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_Z$$
6	5	fveq2i	$$⊢\mathrm{lim\; inf}\left({\left({F\upharpoonright }_Z\right)\upharpoonright }_{ℝ}\right)=\mathrm{lim\; inf}\left({\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_Z\right)$$
7	6	a1i	$$⊢\phi \to \mathrm{lim\; inf}\left({\left({F\upharpoonright }_Z\right)\upharpoonright }_{ℝ}\right)=\mathrm{lim\; inf}\left({\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_Z\right)$$
8		relres	$$⊢\mathrm{Rel}\left({F\upharpoonright }_{ℝ}\right)$$
9	8	a1i	$$⊢\phi \to \mathrm{Rel}\left({F\upharpoonright }_{ℝ}\right)$$
10		relssres	$$⊢\left(\mathrm{Rel}\left({F\upharpoonright }_{ℝ}\right)\wedge \mathrm{dom}\left({F\upharpoonright }_{ℝ}\right)\subseteq \mathbb{Z}\right)\to {\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_{\mathbb{Z}}={F\upharpoonright }_{ℝ}$$
11	9 4 10	syl2anc	$$⊢\phi \to {\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_{\mathbb{Z}}={F\upharpoonright }_{ℝ}$$
12	11	eqcomd	$$⊢\phi \to {F\upharpoonright }_{ℝ}={\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_{\mathbb{Z}}$$
13	12	reseq1d	$$⊢\phi \to {\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_{\left[M,\mathrm{+\infty }\right)}={\left({\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_{\mathbb{Z}}\right)\upharpoonright }_{\left[M,\mathrm{+\infty }\right)}$$
14		resres	$$⊢{\left({\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_{\mathbb{Z}}\right)\upharpoonright }_{\left[M,\mathrm{+\infty }\right)}={\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_{\left(\mathbb{Z}\cap \left[M,\mathrm{+\infty }\right)\right)}$$
15	14	a1i	$$⊢\phi \to {\left({\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_{\mathbb{Z}}\right)\upharpoonright }_{\left[M,\mathrm{+\infty }\right)}={\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_{\left(\mathbb{Z}\cap \left[M,\mathrm{+\infty }\right)\right)}$$
16	1 2	uzinico	$$⊢\phi \to Z=\mathbb{Z}\cap \left[M,\mathrm{+\infty }\right)$$
17	16	eqcomd	$$⊢\phi \to \mathbb{Z}\cap \left[M,\mathrm{+\infty }\right)=Z$$
18	17	reseq2d	$$⊢\phi \to {\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_{\left(\mathbb{Z}\cap \left[M,\mathrm{+\infty }\right)\right)}={\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_Z$$
19	13 15 18	3eqtrrd	$$⊢\phi \to {\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_Z={\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_{\left[M,\mathrm{+\infty }\right)}$$
20	19	fveq2d	$$⊢\phi \to \mathrm{lim\; inf}\left({\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_Z\right)=\mathrm{lim\; inf}\left({\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_{\left[M,\mathrm{+\infty }\right)}\right)$$
21	1	zred	$$⊢\phi \to M\in ℝ$$
22		eqid	$$⊢\left[M,\mathrm{+\infty }\right)=\left[M,\mathrm{+\infty }\right)$$
23	3	resexd	$$⊢\phi \to {F\upharpoonright }_{ℝ}\in \mathrm{V}$$
24	21 22 23	liminfresico	$$⊢\phi \to \mathrm{lim\; inf}\left({\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_{\left[M,\mathrm{+\infty }\right)}\right)=\mathrm{lim\; inf}\left({F\upharpoonright }_{ℝ}\right)$$
25	20 24	eqtrd	$$⊢\phi \to \mathrm{lim\; inf}\left({\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_Z\right)=\mathrm{lim\; inf}\left({F\upharpoonright }_{ℝ}\right)$$
26	7 25	eqtrd	$$⊢\phi \to \mathrm{lim\; inf}\left({\left({F\upharpoonright }_Z\right)\upharpoonright }_{ℝ}\right)=\mathrm{lim\; inf}\left({F\upharpoonright }_{ℝ}\right)$$
27	3	resexd	$$⊢\phi \to {F\upharpoonright }_Z\in \mathrm{V}$$
28	27	liminfresre	$$⊢\phi \to \mathrm{lim\; inf}\left({\left({F\upharpoonright }_Z\right)\upharpoonright }_{ℝ}\right)=\mathrm{lim\; inf}\left({F\upharpoonright }_Z\right)$$
29	3	liminfresre	$$⊢\phi \to \mathrm{lim\; inf}\left({F\upharpoonright }_{ℝ}\right)=\mathrm{lim\; inf}\left(F\right)$$
30	26 28 29	3eqtr3d	$$⊢\phi \to \mathrm{lim\; inf}\left({F\upharpoonright }_Z\right)=\mathrm{lim\; inf}\left(F\right)$$