Theorem liminfvaluz4

Description: Alternate definition of liminf for a real-valued function, defined on a set of upper integers. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	liminfvaluz4.1	$$⊢Ⅎk\phi$$
	liminfvaluz4.2	$$⊢\underset{\_}{Ⅎ}kF$$
	liminfvaluz4.3	$$⊢\phi \to M\in \mathbb{Z}$$
	liminfvaluz4.4	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	liminfvaluz4.5	$$⊢\phi \to F:Z⟶ℝ$$
Assertion	liminfvaluz4	$$⊢\phi \to \mathrm{lim\; inf}\left(F\right)=-\mathrm{lim\; sup}\left(\left(k\in Z⟼-F\left(k\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		liminfvaluz4.1	$$⊢Ⅎk\phi$$
2		liminfvaluz4.2	$$⊢\underset{\_}{Ⅎ}kF$$
3		liminfvaluz4.3	$$⊢\phi \to M\in \mathbb{Z}$$
4		liminfvaluz4.4	$$⊢Z={\mathbb{Z}}_{\ge M}$$
5		liminfvaluz4.5	$$⊢\phi \to F:Z⟶ℝ$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}kZ$$
7	6 2 5	feqmptdf	$$⊢\phi \to F=\left(k\in Z⟼F\left(k\right)\right)$$
8	7	fveq2d	$$⊢\phi \to \mathrm{lim\; inf}\left(F\right)=\mathrm{lim\; inf}\left(\left(k\in Z⟼F\left(k\right)\right)\right)$$
9	5	ffvelcdmda	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℝ$$
10	1 3 4 9	liminfvaluz2	$$⊢\phi \to \mathrm{lim\; inf}\left(\left(k\in Z⟼F\left(k\right)\right)\right)=-\mathrm{lim\; sup}\left(\left(k\in Z⟼-F\left(k\right)\right)\right)$$
11	8 10	eqtrd	$$⊢\phi \to \mathrm{lim\; inf}\left(F\right)=-\mathrm{lim\; sup}\left(\left(k\in Z⟼-F\left(k\right)\right)\right)$$