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	$⊢ φ \to F \in V$
	liminflelimsup.2	$⊢ φ \to \forall k \in ℝ \exists j \in [k, +∞) F [[j, +∞)] \cap ℝ^{*} \neq \emptyset$
Assertion	liminflelimsup	$⊢ φ \to lim inf (F) \leq lim sup (F)$

Proof

Step	Hyp	Ref	Expression
1		liminflelimsup.1	$⊢ φ \to F \in V$
2		liminflelimsup.2	$⊢ φ \to \forall k \in ℝ \exists j \in [k, +∞) F [[j, +∞)] \cap ℝ^{*} \neq \emptyset$
3		oveq1	$⊢ k = i \to [k, +∞) = [i, +∞)$
4	3	rexeqdv	$⊢ k = i \to (\exists j \in [k, +∞) F [[j, +∞)] \cap ℝ^{} \neq \emptyset \leftrightarrow \exists j \in [i, +∞) F [[j, +∞)] \cap ℝ^{} \neq \emptyset)$
5		oveq1	$⊢ j = l \to [j, +∞) = [l, +∞)$
6	5	imaeq2d	$⊢ j = l \to F [[j, +∞)] = F [[l, +∞)]$
7	6	ineq1d	$⊢ j = l \to F [[j, +∞)] \cap ℝ^{} = F [[l, +∞)] \cap ℝ^{}$
8	7	neeq1d	$⊢ j = l \to (F [[j, +∞)] \cap ℝ^{} \neq \emptyset \leftrightarrow F [[l, +∞)] \cap ℝ^{} \neq \emptyset)$
9	8	cbvrexvw	$⊢ \exists j \in [i, +∞) F [[j, +∞)] \cap ℝ^{} \neq \emptyset \leftrightarrow \exists l \in [i, +∞) F [[l, +∞)] \cap ℝ^{} \neq \emptyset$
10	9	a1i	$⊢ k = i \to (\exists j \in [i, +∞) F [[j, +∞)] \cap ℝ^{} \neq \emptyset \leftrightarrow \exists l \in [i, +∞) F [[l, +∞)] \cap ℝ^{} \neq \emptyset)$
11	4 10	bitrd	$⊢ k = i \to (\exists j \in [k, +∞) F [[j, +∞)] \cap ℝ^{} \neq \emptyset \leftrightarrow \exists l \in [i, +∞) F [[l, +∞)] \cap ℝ^{} \neq \emptyset)$
12	11	cbvralvw	$⊢ \forall k \in ℝ \exists j \in [k, +∞) F [[j, +∞)] \cap ℝ^{} \neq \emptyset \leftrightarrow \forall i \in ℝ \exists l \in [i, +∞) F [[l, +∞)] \cap ℝ^{} \neq \emptyset$
13	2 12	sylib	$⊢ φ \to \forall i \in ℝ \exists l \in [i, +∞) F [[l, +∞)] \cap ℝ^{*} \neq \emptyset$
14	1 13	liminflelimsuplem	$⊢ φ \to lim inf (F) \leq lim sup (F)$

Metamath Proof Explorer

Theorem liminflelimsup

Proof