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

Metamath Proof Explorer

Theorem liminfgelimsup

Description: The inferior limit is greater than or equal to the superior limit if and only if they are equal. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses liminfgelimsup.1 ⊢ φ → F ∈ V
liminfgelimsup.2 ⊢ φ → ∀ k ∈ ℝ ∃ j ∈ k +∞ F j +∞ ∩ ℝ * ≠ ∅
Assertion liminfgelimsup ⊢ φ → lim sup ⁡ F ≤ lim inf ⁡ F ↔ lim inf ⁡ F = lim sup ⁡ F

Proof

Step Hyp Ref Expression
1 liminfgelimsup.1 ⊢ φ → F ∈ V
2 liminfgelimsup.2 ⊢ φ → ∀ k ∈ ℝ ∃ j ∈ k +∞ F j +∞ ∩ ℝ * ≠ ∅
3 1 liminfcld ⊢ φ → lim inf ⁡ F ∈ ℝ *
4 3 adantr ⊢ φ ∧ lim sup ⁡ F ≤ lim inf ⁡ F → lim inf ⁡ F ∈ ℝ *
5 1 limsupcld ⊢ φ → lim sup ⁡ F ∈ ℝ *
6 5 adantr ⊢ φ ∧ lim sup ⁡ F ≤ lim inf ⁡ F → lim sup ⁡ F ∈ ℝ *
7 1 2 liminflelimsup ⊢ φ → lim inf ⁡ F ≤ lim sup ⁡ F
8 7 adantr ⊢ φ ∧ lim sup ⁡ F ≤ lim inf ⁡ F → lim inf ⁡ F ≤ lim sup ⁡ F
9 simpr ⊢ φ ∧ lim sup ⁡ F ≤ lim inf ⁡ F → lim sup ⁡ F ≤ lim inf ⁡ F
10 4 6 8 9 xrletrid ⊢ φ ∧ lim sup ⁡ F ≤ lim inf ⁡ F → lim inf ⁡ F = lim sup ⁡ F
11 5 adantr ⊢ φ ∧ lim inf ⁡ F = lim sup ⁡ F → lim sup ⁡ F ∈ ℝ *
12 id ⊢ lim inf ⁡ F = lim sup ⁡ F → lim inf ⁡ F = lim sup ⁡ F
13 12 eqcomd ⊢ lim inf ⁡ F = lim sup ⁡ F → lim sup ⁡ F = lim inf ⁡ F
14 13 adantl ⊢ φ ∧ lim inf ⁡ F = lim sup ⁡ F → lim sup ⁡ F = lim inf ⁡ F
15 11 14 xreqled ⊢ φ ∧ lim inf ⁡ F = lim sup ⁡ F → lim sup ⁡ F ≤ lim inf ⁡ F
16 10 15 impbida ⊢ φ → lim sup ⁡ F ≤ lim inf ⁡ F ↔ lim inf ⁡ F = lim sup ⁡ F