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

Metamath Proof Explorer

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