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

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 ‘ ( 𝑘 ∈ 𝑍 ↦ -_𝑒 𝐵 ) ) )