Theorem limsupval4

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

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

Proof

Step	Hyp	Ref	Expression
1		limsupval4.x	⊢ Ⅎ 𝑥 𝜑
2		limsupval4.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		limsupval4.m	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
4		limsupval4.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ) → 𝐵 ∈ ℝ* )
5		ovex	⊢ ( 𝑀 [,) +∞ ) ∈ V
6	5	inex2	⊢ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ∈ V
7	6	mptex	⊢ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ 𝐵 ) ∈ V
8		limsupcl	⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ 𝐵 ) ∈ V → ( lim sup ‘ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ 𝐵 ) ) ∈ ℝ* )
9	7 8	ax-mp	⊢ ( lim sup ‘ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ 𝐵 ) ) ∈ ℝ*
10	9	a1i	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ 𝐵 ) ) ∈ ℝ* )
11	10	xnegnegd	⊢ ( 𝜑 → -𝑒 -𝑒 ( lim sup ‘ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ 𝐵 ) ) = ( lim sup ‘ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ 𝐵 ) ) )
12	11	eqcomd	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ 𝐵 ) ) = -𝑒 -𝑒 ( lim sup ‘ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ 𝐵 ) ) )
13		eqid	⊢ ( 𝑀 [,) +∞ ) = ( 𝑀 [,) +∞ )
14	2 3 13	limsupresicompt	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = ( lim sup ‘ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ 𝐵 ) ) )
15	4	xnegcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ) → -𝑒 𝐵 ∈ ℝ* )
16	1 2 3 15	liminfval3	⊢ ( 𝜑 → ( lim inf ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 -𝑒 𝐵 ) ) )
17	2 3 13	limsupresicompt	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 -𝑒 𝐵 ) ) = ( lim sup ‘ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ -𝑒 -𝑒 𝐵 ) ) )
18	4	xnegnegd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ) → -𝑒 -𝑒 𝐵 = 𝐵 )
19	1 18	mpteq2da	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ -𝑒 -𝑒 𝐵 ) = ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ 𝐵 ) )
20	19	fveq2d	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ -𝑒 -𝑒 𝐵 ) ) = ( lim sup ‘ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ 𝐵 ) ) )
21	17 20	eqtrd	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 -𝑒 𝐵 ) ) = ( lim sup ‘ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ 𝐵 ) ) )
22	21	xnegeqd	⊢ ( 𝜑 → -𝑒 ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 -𝑒 𝐵 ) ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ 𝐵 ) ) )
23	16 22	eqtrd	⊢ ( 𝜑 → ( lim inf ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ 𝐵 ) ) )
24	23	xnegeqd	⊢ ( 𝜑 → -𝑒 ( lim inf ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) = -𝑒 -𝑒 ( lim sup ‘ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝑀 [,) +∞ ) ) ↦ 𝐵 ) ) )
25	12 14 24	3eqtr4d	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = -𝑒 ( lim inf ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) )