This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
10 1 3 4 9 liminfvaluz ⊢ ( 𝜑 → ( lim inf ‘ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = -𝑒 ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑘 ) ) ) )
11 8 10 eqtrd ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = -𝑒 ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑘 ) ) ) )