Theorem liminfval3

Description: Alternate definition of liminf when the given function is eventually extended real-valued. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	liminfval3.x	⊢ Ⅎ 𝑥 𝜑
	liminfval3.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	liminfval3.m	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
	liminfval3.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ) → 𝐵 ∈ ℝ* )
Assertion	liminfval3	⊢ ( 𝜑 → ( lim inf ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		liminfval3.x	⊢ Ⅎ 𝑥 𝜑
2		liminfval3.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		liminfval3.m	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
4		liminfval3.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ) → 𝐵 ∈ ℝ* )
5		inss1	⊢ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ⊆ 𝐴
6	5	a1i	⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ⊆ 𝐴 )
7	2 6	ssexd	⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ∈ V )
8	1 7 4	liminfvalxrmpt	⊢ ( 𝜑 → ( lim inf ‘ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ 𝐵 ) ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ -𝑒 𝐵 ) ) )
9		eqid	⊢ ( 𝑀 [,) +∞ ) = ( 𝑀 [,) +∞ )
10	3 9 2	liminfresicompt	⊢ ( 𝜑 → ( lim inf ‘ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ 𝐵 ) ) = ( lim inf ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )
11	10	eqcomd	⊢ ( 𝜑 → ( lim inf ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = ( lim inf ‘ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ 𝐵 ) ) )
12	2 3 9	limsupresicompt	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) = ( lim sup ‘ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ -𝑒 𝐵 ) ) )
13	12	xnegeqd	⊢ ( 𝜑 → -𝑒 ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ -𝑒 𝐵 ) ) )
14	8 11 13	3eqtr4d	⊢ ( 𝜑 → ( lim inf ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) )