Theorem liminfgelimsup

Description: The inferior limit is greater than or equal to the superior limit if and only if they are equal. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	liminfgelimsup.1	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	liminfgelimsup.2	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ ( 𝑘 [,) +∞ ) ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ )
Assertion	liminfgelimsup	⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) ↔ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		liminfgelimsup.1	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2		liminfgelimsup.2	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ ( 𝑘 [,) +∞ ) ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ )
3	1	liminfcld	⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ∈ ℝ* )
4	3	adantr	⊢ ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) ) → ( lim inf ‘ 𝐹 ) ∈ ℝ* )
5	1	limsupcld	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
6	5	adantr	⊢ ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) ) → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
7	1 2	liminflelimsup	⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ≤ ( lim sup ‘ 𝐹 ) )
8	7	adantr	⊢ ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) ) → ( lim inf ‘ 𝐹 ) ≤ ( lim sup ‘ 𝐹 ) )
9		simpr	⊢ ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) ) → ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) )
10	4 6 8 9	xrletrid	⊢ ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) ) → ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) )
11	5	adantr	⊢ ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
12		id	⊢ ( ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) → ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) )
13	12	eqcomd	⊢ ( ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) → ( lim sup ‘ 𝐹 ) = ( lim inf ‘ 𝐹 ) )
14	13	adantl	⊢ ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) → ( lim sup ‘ 𝐹 ) = ( lim inf ‘ 𝐹 ) )
15	11 14	xreqled	⊢ ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) → ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) )
16	10 15	impbida	⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) ↔ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) )