Metamath Proof Explorer


Theorem liminfvaluz

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 liminfvaluz.k 𝑘 𝜑
liminfvaluz.m ( 𝜑𝑀 ∈ ℤ )
liminfvaluz.z 𝑍 = ( ℤ𝑀 )
liminfvaluz.b ( ( 𝜑𝑘𝑍 ) → 𝐵 ∈ ℝ* )
Assertion liminfvaluz ( 𝜑 → ( lim inf ‘ ( 𝑘𝑍𝐵 ) ) = -𝑒 ( lim sup ‘ ( 𝑘𝑍 ↦ -𝑒 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 liminfvaluz.k 𝑘 𝜑
2 liminfvaluz.m ( 𝜑𝑀 ∈ ℤ )
3 liminfvaluz.z 𝑍 = ( ℤ𝑀 )
4 liminfvaluz.b ( ( 𝜑𝑘𝑍 ) → 𝐵 ∈ ℝ* )
5 3 fvexi 𝑍 ∈ V
6 5 a1i ( 𝜑𝑍 ∈ V )
7 2 zred ( 𝜑𝑀 ∈ ℝ )
8 simpr ( ( 𝜑𝑘 ∈ ( 𝑍 ∩ ( 𝑀 [,) +∞ ) ) ) → 𝑘 ∈ ( 𝑍 ∩ ( 𝑀 [,) +∞ ) ) )
9 2 3 uzinico3 ( 𝜑𝑍 = ( 𝑍 ∩ ( 𝑀 [,) +∞ ) ) )
10 9 eqcomd ( 𝜑 → ( 𝑍 ∩ ( 𝑀 [,) +∞ ) ) = 𝑍 )
11 10 adantr ( ( 𝜑𝑘 ∈ ( 𝑍 ∩ ( 𝑀 [,) +∞ ) ) ) → ( 𝑍 ∩ ( 𝑀 [,) +∞ ) ) = 𝑍 )
12 8 11 eleqtrd ( ( 𝜑𝑘 ∈ ( 𝑍 ∩ ( 𝑀 [,) +∞ ) ) ) → 𝑘𝑍 )
13 12 4 syldan ( ( 𝜑𝑘 ∈ ( 𝑍 ∩ ( 𝑀 [,) +∞ ) ) ) → 𝐵 ∈ ℝ* )
14 1 6 7 13 liminfval3 ( 𝜑 → ( lim inf ‘ ( 𝑘𝑍𝐵 ) ) = -𝑒 ( lim sup ‘ ( 𝑘𝑍 ↦ -𝑒 𝐵 ) ) )