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

Metamath Proof Explorer

Theorem liminfvaluz3

Description: Alternate definition of liminf for an extended real-valued function, defined on a set of upper integers. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses liminfvaluz3.1 ⊢ Ⅎ k φ
liminfvaluz3.2 ⊢ Ⅎ _ k F
liminfvaluz3.3 ⊢ φ → M ∈ ℤ
liminfvaluz3.4 ⊢ Z = ℤ ≥ M
liminfvaluz3.5 ⊢ φ → F : Z ⟶ ℝ *
Assertion liminfvaluz3 ⊢ φ → lim inf ⁡ F = − lim sup ⁡ k ∈ Z ⟼ − F ⁡ k

Proof

Step Hyp Ref Expression
1 liminfvaluz3.1 ⊢ Ⅎ k φ
2 liminfvaluz3.2 ⊢ Ⅎ _ k F
3 liminfvaluz3.3 ⊢ φ → M ∈ ℤ
4 liminfvaluz3.4 ⊢ Z = ℤ ≥ M
5 liminfvaluz3.5 ⊢ φ → F : Z ⟶ ℝ *
6 nfcv ⊢ Ⅎ _ k Z
7 6 2 5 feqmptdf ⊢ φ → F = k ∈ Z ⟼ F ⁡ k
8 7 fveq2d ⊢ φ → lim inf ⁡ F = lim inf ⁡ k ∈ Z ⟼ F ⁡ k
9 5 ffvelcdmda ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℝ *
10 1 3 4 9 liminfvaluz ⊢ φ → lim inf ⁡ k ∈ Z ⟼ F ⁡ k = − lim sup ⁡ k ∈ Z ⟼ − F ⁡ k
11 8 10 eqtrd ⊢ φ → lim inf ⁡ F = − lim sup ⁡ k ∈ Z ⟼ − F ⁡ k