Theorem limsupvaluz3

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

Proof

Step	Hyp	Ref	Expression
1		limsupvaluz3.k	⊢ Ⅎ 𝑘 𝜑
2		limsupvaluz3.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		limsupvaluz3.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4		limsupvaluz3.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	limsupval4	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ) = -𝑒 ( lim inf ‘ ( 𝑘 ∈ 𝑍 ↦ -𝑒 𝐵 ) ) )