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