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 ‘ 𝐹 ) ) ) )