Theorem liminfval4

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

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

Proof

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