Metamath Proof Explorer

Theorem limsupvaluz4

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

Ref Expression
Hypotheses limsupvaluz4.k ⊢ Ⅎ k φ
limsupvaluz4.m ⊢ φ → M ∈ ℤ
limsupvaluz4.z ⊢ Z = ℤ ≥ M
limsupvaluz4.b ⊢ φ ∧ k ∈ Z → B ∈ ℝ
Assertion limsupvaluz4 ⊢ φ → lim sup ⁡ k ∈ Z ⟼ B = − lim inf ⁡ k ∈ Z ⟼ − B

Proof

Step Hyp Ref Expression
1 limsupvaluz4.k ⊢ Ⅎ k φ
2 limsupvaluz4.m ⊢ φ → M ∈ ℤ
3 limsupvaluz4.z ⊢ Z = ℤ ≥ M
4 limsupvaluz4.b ⊢ φ ∧ k ∈ Z → B ∈ ℝ
5 4 rexrd ⊢ φ ∧ k ∈ Z → B ∈ ℝ *
6 1 2 3 5 limsupvaluz3 ⊢ φ → lim sup ⁡ k ∈ Z ⟼ B = − lim inf ⁡ k ∈ Z ⟼ − B
7 4 rexnegd ⊢ φ ∧ k ∈ Z → − B = − B
8 1 7 mpteq2da ⊢ φ → k ∈ Z ⟼ − B = k ∈ Z ⟼ − B
9 8 fveq2d ⊢ φ → lim inf ⁡ k ∈ Z ⟼ − B = lim inf ⁡ k ∈ Z ⟼ − B
10 9 xnegeqd ⊢ φ → − lim inf ⁡ k ∈ Z ⟼ − B = − lim inf ⁡ k ∈ Z ⟼ − B
11 6 10 eqtrd ⊢ φ → lim sup ⁡ k ∈ Z ⟼ B = − lim inf ⁡ k ∈ Z ⟼ − B