Theorem liminfvaluz3

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

	Ref	Expression
Hypotheses	liminfvaluz3.1	$$⊢Ⅎk\phi$$
	liminfvaluz3.2	$$⊢\underset{\_}{Ⅎ}kF$$
	liminfvaluz3.3	$$⊢\phi \to M\in \mathbb{Z}$$
	liminfvaluz3.4	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	liminfvaluz3.5	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
Assertion	liminfvaluz3	$$⊢\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		liminfvaluz3.1	$$⊢Ⅎk\phi$$
2		liminfvaluz3.2	$$⊢\underset{\_}{Ⅎ}kF$$
3		liminfvaluz3.3	$$⊢\phi \to M\in \mathbb{Z}$$
4		liminfvaluz3.4	$$⊢Z={\mathbb{Z}}_{\ge M}$$
5		liminfvaluz3.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	ffvelrnda	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in {ℝ}^{*}$$
10	1 3 4 9	liminfvaluz	$$⊢\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)$$