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

Metamath Proof Explorer

Theorem liminfvaluz

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 liminfvaluz.k ⊢ Ⅎ k φ
liminfvaluz.m ⊢ φ → M ∈ ℤ
liminfvaluz.z ⊢ Z = ℤ ≥ M
liminfvaluz.b ⊢ φ ∧ k ∈ Z → B ∈ ℝ *
Assertion liminfvaluz ⊢ φ → lim inf ⁡ k ∈ Z ⟼ B = − lim sup ⁡ k ∈ Z ⟼ − B

Proof

Step Hyp Ref Expression
1 liminfvaluz.k ⊢ Ⅎ k φ
2 liminfvaluz.m ⊢ φ → M ∈ ℤ
3 liminfvaluz.z ⊢ Z = ℤ ≥ M
4 liminfvaluz.b ⊢ φ ∧ k ∈ Z → B ∈ ℝ *
5 3 fvexi ⊢ Z ∈ V
6 5 a1i ⊢ φ → Z ∈ V
7 2 zred ⊢ φ → M ∈ ℝ
8 simpr ⊢ φ ∧ k ∈ Z ∩ M +∞ → k ∈ Z ∩ M +∞
9 2 3 uzinico3 ⊢ φ → Z = Z ∩ M +∞
10 9 eqcomd ⊢ φ → Z ∩ M +∞ = Z
11 10 adantr ⊢ φ ∧ k ∈ Z ∩ M +∞ → Z ∩ M +∞ = Z
12 8 11 eleqtrd ⊢ φ ∧ k ∈ Z ∩ M +∞ → k ∈ Z
13 12 4 syldan ⊢ φ ∧ k ∈ Z ∩ M +∞ → B ∈ ℝ *
14 1 6 7 13 liminfval3 ⊢ φ → lim inf ⁡ k ∈ Z ⟼ B = − lim sup ⁡ k ∈ Z ⟼ − B