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 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climliminflimsup3.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climliminflimsup3.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
Assertion climliminflimsup3 ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ ( ( lim inf ‘ 𝐹 ) ∈ ℝ ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ) )

Proof

Step Hyp Ref Expression
1 climliminflimsup3.1 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 climliminflimsup3.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 climliminflimsup3.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
4 1 2 3 climliminflimsup ⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ ( ( lim inf ‘ 𝐹 ) ∈ ℝ ∧ ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) ) ) )
5 3 frexr ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
6 1 2 5 liminfgelimsupuz ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) ↔ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) )
7 6 anbi2d ⊢ ( 𝜑 → ( ( ( lim inf ‘ 𝐹 ) ∈ ℝ ∧ ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) ) ↔ ( ( lim inf ‘ 𝐹 ) ∈ ℝ ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ) )
8 4 7 bitrd ⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ ( ( lim inf ‘ 𝐹 ) ∈ ℝ ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ) )