Theorem limsupvaluz4

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

Proof

Step	Hyp	Ref	Expression
1		limsupvaluz4.k	⊢ Ⅎ 𝑘 𝜑
2		limsupvaluz4.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		limsupvaluz4.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4		limsupvaluz4.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
5	4	rexrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℝ* )
6	1 2 3 5	limsupvaluz3	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ) = -𝑒 ( lim inf ‘ ( 𝑘 ∈ 𝑍 ↦ -𝑒 𝐵 ) ) )
7	4	rexnegd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → -𝑒 𝐵 = - 𝐵 )
8	1 7	mpteq2da	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ -𝑒 𝐵 ) = ( 𝑘 ∈ 𝑍 ↦ - 𝐵 ) )
9	8	fveq2d	⊢ ( 𝜑 → ( lim inf ‘ ( 𝑘 ∈ 𝑍 ↦ -𝑒 𝐵 ) ) = ( lim inf ‘ ( 𝑘 ∈ 𝑍 ↦ - 𝐵 ) ) )
10	9	xnegeqd	⊢ ( 𝜑 → -𝑒 ( lim inf ‘ ( 𝑘 ∈ 𝑍 ↦ -𝑒 𝐵 ) ) = -𝑒 ( lim inf ‘ ( 𝑘 ∈ 𝑍 ↦ - 𝐵 ) ) )
11	6 10	eqtrd	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ) = -𝑒 ( lim inf ‘ ( 𝑘 ∈ 𝑍 ↦ - 𝐵 ) ) )