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