Theorem liminflelimsup

Description: The superior limit is greater than or equal to the inferior limit. The second hypothesis is needed (see liminflelimsupcex for a counterexample). The inequality can be strict, see liminfltlimsupex . (Contributed by Glauco Siliprandi, 2-Jan-2022)

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

Proof

Step	Hyp	Ref	Expression
1		liminflelimsup.1	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2		liminflelimsup.2	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ ( 𝑘 [,) +∞ ) ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ )
3		oveq1	⊢ ( 𝑘 = 𝑖 → ( 𝑘 [,) +∞ ) = ( 𝑖 [,) +∞ ) )
4	3	rexeqdv	⊢ ( 𝑘 = 𝑖 → ( ∃ 𝑗 ∈ ( 𝑘 [,) +∞ ) ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ↔ ∃ 𝑗 ∈ ( 𝑖 [,) +∞ ) ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ) )
5		oveq1	⊢ ( 𝑗 = 𝑙 → ( 𝑗 [,) +∞ ) = ( 𝑙 [,) +∞ ) )
6	5	imaeq2d	⊢ ( 𝑗 = 𝑙 → ( 𝐹 “ ( 𝑗 [,) +∞ ) ) = ( 𝐹 “ ( 𝑙 [,) +∞ ) ) )
7	6	ineq1d	⊢ ( 𝑗 = 𝑙 → ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) = ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) )
8	7	neeq1d	⊢ ( 𝑗 = 𝑙 → ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ↔ ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ) )
9	8	cbvrexvw	⊢ ( ∃ 𝑗 ∈ ( 𝑖 [,) +∞ ) ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ↔ ∃ 𝑙 ∈ ( 𝑖 [,) +∞ ) ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ )
10	9	a1i	⊢ ( 𝑘 = 𝑖 → ( ∃ 𝑗 ∈ ( 𝑖 [,) +∞ ) ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ↔ ∃ 𝑙 ∈ ( 𝑖 [,) +∞ ) ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ) )
11	4 10	bitrd	⊢ ( 𝑘 = 𝑖 → ( ∃ 𝑗 ∈ ( 𝑘 [,) +∞ ) ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ↔ ∃ 𝑙 ∈ ( 𝑖 [,) +∞ ) ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ) )
12	11	cbvralvw	⊢ ( ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ ( 𝑘 [,) +∞ ) ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ↔ ∀ 𝑖 ∈ ℝ ∃ 𝑙 ∈ ( 𝑖 [,) +∞ ) ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ )
13	2 12	sylib	⊢ ( 𝜑 → ∀ 𝑖 ∈ ℝ ∃ 𝑙 ∈ ( 𝑖 [,) +∞ ) ( ( 𝐹 “ ( 𝑙 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ )
14	1 13	liminflelimsuplem	⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ≤ ( lim sup ‘ 𝐹 ) )