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 ⊢ Ⅎ x φ
liminfvalxrmpt.2 ⊢ φ → A ∈ V
liminfvalxrmpt.3 ⊢ φ ∧ x ∈ A → B ∈ ℝ *
Assertion liminfvalxrmpt ⊢ φ → lim inf ⁡ x ∈ A ⟼ B = − lim sup ⁡ x ∈ A ⟼ − B

Proof

Step Hyp Ref Expression
1 liminfvalxrmpt.1 ⊢ Ⅎ x φ
2 liminfvalxrmpt.2 ⊢ φ → A ∈ V
3 liminfvalxrmpt.3 ⊢ φ ∧ x ∈ A → B ∈ ℝ *
4 nfmpt1 ⊢ Ⅎ _ x x ∈ A ⟼ B
5 1 3 fmptd2f ⊢ φ → x ∈ A ⟼ B : A ⟶ ℝ *
6 4 2 5 liminfvalxr ⊢ φ → lim inf ⁡ x ∈ A ⟼ B = − lim sup ⁡ x ∈ A ⟼ − x ∈ A ⟼ B ⁡ x
7 eqidd ⊢ φ → x ∈ A ⟼ B = x ∈ A ⟼ B
8 7 3 fvmpt2d ⊢ φ ∧ x ∈ A → x ∈ A ⟼ B ⁡ x = B
9 8 xnegeqd ⊢ φ ∧ x ∈ A → − x ∈ A ⟼ B ⁡ x = − B
10 1 9 mpteq2da ⊢ φ → x ∈ A ⟼ − x ∈ A ⟼ B ⁡ x = x ∈ A ⟼ − B
11 10 fveq2d ⊢ φ → lim sup ⁡ x ∈ A ⟼ − x ∈ A ⟼ B ⁡ x = lim sup ⁡ x ∈ A ⟼ − B
12 11 xnegeqd ⊢ φ → − lim sup ⁡ x ∈ A ⟼ − x ∈ A ⟼ B ⁡ x = − lim sup ⁡ x ∈ A ⟼ − B
13 6 12 eqtrd ⊢ φ → lim inf ⁡ x ∈ A ⟼ B = − lim sup ⁡ x ∈ A ⟼ − B