Metamath Proof Explorer

Theorem liminfgelimsupuz

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 liminfgelimsupuz.1 ⊢ φ → M ∈ ℤ
liminfgelimsupuz.2 ⊢ Z = ℤ ≥ M
liminfgelimsupuz.3 ⊢ φ → F : Z ⟶ ℝ *
Assertion liminfgelimsupuz ⊢ φ → lim sup ⁡ F ≤ lim inf ⁡ F ↔ lim inf ⁡ F = lim sup ⁡ F

Proof

Step Hyp Ref Expression
1 liminfgelimsupuz.1 ⊢ φ → M ∈ ℤ
2 liminfgelimsupuz.2 ⊢ Z = ℤ ≥ M
3 liminfgelimsupuz.3 ⊢ φ → F : Z ⟶ ℝ *
4 2 fvexi ⊢ Z ∈ V
5 4 a1i ⊢ φ → Z ∈ V
6 3 5 fexd ⊢ φ → F ∈ V
7 6 liminfcld ⊢ φ → lim inf ⁡ F ∈ ℝ *
8 7 adantr ⊢ φ ∧ lim sup ⁡ F ≤ lim inf ⁡ F → lim inf ⁡ F ∈ ℝ *
9 6 limsupcld ⊢ φ → lim sup ⁡ F ∈ ℝ *
10 9 adantr ⊢ φ ∧ lim sup ⁡ F ≤ lim inf ⁡ F → lim sup ⁡ F ∈ ℝ *
11 1 2 3 liminflelimsupuz ⊢ φ → lim inf ⁡ F ≤ lim sup ⁡ F
12 11 adantr ⊢ φ ∧ lim sup ⁡ F ≤ lim inf ⁡ F → lim inf ⁡ F ≤ lim sup ⁡ F
13 simpr ⊢ φ ∧ lim sup ⁡ F ≤ lim inf ⁡ F → lim sup ⁡ F ≤ lim inf ⁡ F
14 8 10 12 13 xrletrid ⊢ φ ∧ lim sup ⁡ F ≤ lim inf ⁡ F → lim inf ⁡ F = lim sup ⁡ F
15 9 adantr ⊢ φ ∧ lim inf ⁡ F = lim sup ⁡ F → lim sup ⁡ F ∈ ℝ *
16 id ⊢ lim inf ⁡ F = lim sup ⁡ F → lim inf ⁡ F = lim sup ⁡ F
17 16 eqcomd ⊢ lim inf ⁡ F = lim sup ⁡ F → lim sup ⁡ F = lim inf ⁡ F
18 17 adantl ⊢ φ ∧ lim inf ⁡ F = lim sup ⁡ F → lim sup ⁡ F = lim inf ⁡ F
19 15 18 xreqled ⊢ φ ∧ lim inf ⁡ F = lim sup ⁡ F → lim sup ⁡ F ≤ lim inf ⁡ F
20 14 19 impbida ⊢ φ → lim sup ⁡ F ≤ lim inf ⁡ F ↔ lim inf ⁡ F = lim sup ⁡ F