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

Metamath Proof Explorer

Theorem climliminflimsup4

Description: A sequence of real numbers converges if and only if its superior limit is real and equal to its inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses climliminflimsup4.1 ⊢ φ → M ∈ ℤ
climliminflimsup4.2 ⊢ Z = ℤ ≥ M
climliminflimsup4.3 ⊢ φ → F : Z ⟶ ℝ
Assertion climliminflimsup4 ⊢ φ → F ∈ dom ⁡ ⇝ ↔ lim sup ⁡ F ∈ ℝ ∧ lim inf ⁡ F = lim sup ⁡ F

Proof

Step Hyp Ref Expression
1 climliminflimsup4.1 ⊢ φ → M ∈ ℤ
2 climliminflimsup4.2 ⊢ Z = ℤ ≥ M
3 climliminflimsup4.3 ⊢ φ → F : Z ⟶ ℝ
4 1 2 3 climliminflimsup2 ⊢ φ → F ∈ dom ⁡ ⇝ ↔ lim sup ⁡ F ∈ ℝ ∧ lim sup ⁡ F ≤ lim inf ⁡ F
5 3 frexr ⊢ φ → F : Z ⟶ ℝ *
6 1 2 5 liminfgelimsupuz ⊢ φ → lim sup ⁡ F ≤ lim inf ⁡ F ↔ lim inf ⁡ F = lim sup ⁡ F
7 6 anbi2d ⊢ φ → lim sup ⁡ F ∈ ℝ ∧ lim sup ⁡ F ≤ lim inf ⁡ F ↔ lim sup ⁡ F ∈ ℝ ∧ lim inf ⁡ F = lim sup ⁡ F
8 4 7 bitrd ⊢ φ → F ∈ dom ⁡ ⇝ ↔ lim sup ⁡ F ∈ ℝ ∧ lim inf ⁡ F = lim sup ⁡ F