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

Metamath Proof Explorer

Theorem limsupvaluz3

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

Proof

Step Hyp Ref Expression
1 limsupvaluz3.k ⊢ Ⅎ k φ
2 limsupvaluz3.m ⊢ φ → M ∈ ℤ
3 limsupvaluz3.z ⊢ Z = ℤ ≥ M
4 limsupvaluz3.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 limsupval4 ⊢ φ → lim sup ⁡ k ∈ Z ⟼ B = − lim inf ⁡ k ∈ Z ⟼ − B