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

Proof

Step	Hyp	Ref	Expression
1		liminfgelimsup.1	$⊢ φ \to F \in V$
2		liminfgelimsup.2	$⊢ φ \to \forall k \in ℝ \exists j \in [k, +∞) F [[j, +∞)] \cap ℝ^{*} \neq \emptyset$
3	1	liminfcld	$⊢ φ \to lim inf (F) \in ℝ^{*}$
4	3	adantr	$⊢ (φ \land lim sup (F) \leq lim inf (F)) \to lim inf (F) \in ℝ^{*}$
5	1	limsupcld	$⊢ φ \to lim sup (F) \in ℝ^{*}$
6	5	adantr	$⊢ (φ \land lim sup (F) \leq lim inf (F)) \to lim sup (F) \in ℝ^{*}$
7	1 2	liminflelimsup	$⊢ φ \to lim inf (F) \leq lim sup (F)$
8	7	adantr	$⊢ (φ \land lim sup (F) \leq lim inf (F)) \to lim inf (F) \leq lim sup (F)$
9		simpr	$⊢ (φ \land lim sup (F) \leq lim inf (F)) \to lim sup (F) \leq lim inf (F)$
10	4 6 8 9	xrletrid	$⊢ (φ \land lim sup (F) \leq lim inf (F)) \to lim inf (F) = lim sup (F)$
11	5	adantr	$⊢ (φ \land lim inf (F) = lim sup (F)) \to lim sup (F) \in ℝ^{*}$
12		id	$⊢ lim inf (F) = lim sup (F) \to lim inf (F) = lim sup (F)$
13	12	eqcomd	$⊢ lim inf (F) = lim sup (F) \to lim sup (F) = lim inf (F)$
14	13	adantl	$⊢ (φ \land lim inf (F) = lim sup (F)) \to lim sup (F) = lim inf (F)$
15	11 14	xreqled	$⊢ (φ \land lim inf (F) = lim sup (F)) \to lim sup (F) \leq lim inf (F)$
16	10 15	impbida	$⊢ φ \to (lim sup (F) \leq lim inf (F) \leftrightarrow lim inf (F) = lim sup (F))$