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	⊢ Ⅎ 𝑘 𝜑
	liminfvaluz3.2	⊢ Ⅎ 𝑘 𝐹
	liminfvaluz3.3	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	liminfvaluz3.4	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	liminfvaluz3.5	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
Assertion	liminfvaluz3	⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = -𝑒 ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑘 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		liminfvaluz3.1	⊢ Ⅎ 𝑘 𝜑
2		liminfvaluz3.2	⊢ Ⅎ 𝑘 𝐹
3		liminfvaluz3.3	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4		liminfvaluz3.4	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5		liminfvaluz3.5	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
6		nfcv	⊢ Ⅎ 𝑘 𝑍
7	6 2 5	feqmptdf	⊢ ( 𝜑 → 𝐹 = ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) )
8	7	fveq2d	⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = ( lim inf ‘ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
9	5	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
10	1 3 4 9	liminfvaluz	⊢ ( 𝜑 → ( lim inf ‘ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = -𝑒 ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑘 ) ) ) )
11	8 10	eqtrd	⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = -𝑒 ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑘 ) ) ) )