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

Metamath Proof Explorer

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