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

Metamath Proof Explorer

Theorem liminfvalxrmpt

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

Ref Expression
Hypotheses liminfvalxrmpt.1 ⊢ Ⅎ 𝑥 𝜑
liminfvalxrmpt.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
liminfvalxrmpt.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
Assertion liminfvalxrmpt ( 𝜑 → ( lim inf ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 liminfvalxrmpt.1 ⊢ Ⅎ 𝑥 𝜑
2 liminfvalxrmpt.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 liminfvalxrmpt.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
4 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5 1 3 fmptd2f ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℝ* )
6 4 2 5 liminfvalxr ⊢ ( 𝜑 → ( lim inf ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ) )
7 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
8 7 3 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
9 8 xnegeqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → -𝑒 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = -𝑒 𝐵 )
10 1 9 mpteq2da ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ -𝑒 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) )
11 10 fveq2d ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) )
12 11 xnegeqd ⊢ ( 𝜑 → -𝑒 ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) )
13 6 12 eqtrd ⊢ ( 𝜑 → ( lim inf ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) )