limsupval

Description: The superior limit of an infinite sequence F of extended real numbers, which is the infimum of the set of suprema of all upper infinite subsequences of F . Definition 12-4.1 of Gleason p. 175. (Contributed by NM, 26-Oct-2005) (Revised by AV, 12-Sep-2014)

		Ref	Expression
	Hypothesis	limsupval.1	$⊢ G = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
	Assertion	limsupval	$⊢ F \in V \to lim sup (F) = inf (ran G ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		limsupval.1	$⊢ G = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
2		elex	$⊢ F \in V \to F \in V$
3		imaeq1	$⊢ x = F \to x [[k, +∞)] = F [[k, +∞)]$
4	3	ineq1d	$⊢ x = F \to x [[k, +∞)] \cap ℝ^{} = F [[k, +∞)] \cap ℝ^{}$
5	4	supeq1d	$⊢ x = F \to sup (x [[k, +∞)] \cap ℝ^{} ℝ^{} <) = sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)$
6	5	mpteq2dv	$⊢ x = F \to (k \in ℝ ⟼ sup (x [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
7	6 1	eqtr4di	$⊢ x = F \to (k \in ℝ ⟼ sup (x [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = G$
8	7	rneqd	$⊢ x = F \to ran (k \in ℝ ⟼ sup (x [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = ran G$
9	8	infeq1d	$⊢ x = F \to inf (ran (k \in ℝ ⟼ sup (x [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) = inf (ran G ℝ^{} <)$
10		df-limsup	$⊢ lim sup = (x \in V ⟼ inf (ran (k \in ℝ ⟼ sup (x [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <))$
11		xrltso	$⊢ < Or ℝ^{*}$
12	11	infex	$⊢ inf (ran G ℝ^{*} <) \in V$
13	9 10 12	fvmpt	$⊢ F \in V \to lim sup (F) = inf (ran G ℝ^{*} <)$
14	2 13	syl	$⊢ F \in V \to lim sup (F) = inf (ran G ℝ^{*} <)$

Metamath Proof Explorer

Theorem limsupval

Proof