This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) )