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

Metamath Proof Explorer

Theorem climliminflimsup3

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

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

Proof

Step Hyp Ref Expression
1 climliminflimsup3.1 ⊢ φ → M ∈ ℤ
2 climliminflimsup3.2 ⊢ Z = ℤ ≥ M
3 climliminflimsup3.3 ⊢ φ → F : Z ⟶ ℝ
4 1 2 3 climliminflimsup ⊢ φ → F ∈ dom ⁡ ⇝ ↔ lim inf ⁡ 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 inf ⁡ F ∈ ℝ ∧ lim sup ⁡ F ≤ lim inf ⁡ F ↔ lim inf ⁡ F ∈ ℝ ∧ lim inf ⁡ F = lim sup ⁡ F
8 4 7 bitrd ⊢ φ → F ∈ dom ⁡ ⇝ ↔ lim inf ⁡ F ∈ ℝ ∧ lim inf ⁡ F = lim sup ⁡ F