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

Proof

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