limsupresre

Description: The supremum limit of a function only depends on the real part of its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021)

		Ref	Expression
	Hypothesis	limsupresre.1	$⊢ φ \to F \in V$
	Assertion	limsupresre	$⊢ φ \to lim sup ({F ↾}_{ℝ}) = lim sup (F)$

Proof

Step	Hyp	Ref	Expression
1		limsupresre.1	$⊢ φ \to F \in V$
2		id	$⊢ k \in ℝ \to k \in ℝ$
3		pnfxr	$⊢ +∞ \in ℝ^{*}$
4	3	a1i	$⊢ k \in ℝ \to +∞ \in ℝ^{*}$
5		icossre	$⊢ (k \in ℝ \land +∞ \in ℝ^{*}) \to [k, +∞) \subseteq ℝ$
6	2 4 5	syl2anc	$⊢ k \in ℝ \to [k, +∞) \subseteq ℝ$
7		resima2	$⊢ [k, +∞) \subseteq ℝ \to ({F ↾}_{ℝ}) [[k, +∞)] = F [[k, +∞)]$
8	6 7	syl	$⊢ k \in ℝ \to ({F ↾}_{ℝ}) [[k, +∞)] = F [[k, +∞)]$
9	8	ineq1d	$⊢ k \in ℝ \to ({F ↾}_{ℝ}) [[k, +∞)] \cap ℝ^{} = F [[k, +∞)] \cap ℝ^{}$
10	9	supeq1d	$⊢ k \in ℝ \to sup (({F ↾}_{ℝ}) [[k, +∞)] \cap ℝ^{} ℝ^{} <) = sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)$
11	10	mpteq2ia	$⊢ (k \in ℝ ⟼ sup (({F ↾}_{ℝ}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
12	11	a1i	$⊢ φ \to (k \in ℝ ⟼ sup (({F ↾}_{ℝ}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
13	12	rneqd	$⊢ φ \to ran (k \in ℝ ⟼ sup (({F ↾}_{ℝ}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = ran (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
14	13	infeq1d	$⊢ φ \to sup (ran (k \in ℝ ⟼ sup (({F ↾}_{ℝ}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) = sup (ran (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <)$
15	1	resexd	$⊢ φ \to {F ↾}_{ℝ} \in V$
16		eqid	$⊢ (k \in ℝ ⟼ sup (({F ↾}_{ℝ}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ sup (({F ↾}_{ℝ}) [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
17	16	limsupval	$⊢ {F ↾}_{ℝ} \in V \to lim sup ({F ↾}_{ℝ}) = sup (ran (k \in ℝ ⟼ sup (({F ↾}_{ℝ}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
18	15 17	syl	$⊢ φ \to lim sup ({F ↾}_{ℝ}) = sup (ran (k \in ℝ ⟼ sup (({F ↾}_{ℝ}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
19		eqid	$⊢ (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
20	19	limsupval	$⊢ F \in V \to lim sup (F) = sup (ran (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
21	1 20	syl	$⊢ φ \to lim sup (F) = sup (ran (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
22	14 18 21	3eqtr4d	$⊢ φ \to lim sup ({F ↾}_{ℝ}) = lim sup (F)$

Metamath Proof Explorer

Theorem limsupresre

Proof