This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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