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

Proof

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