limsupresico

Description: The superior limit doesn't change when a function is restricted to the upper part of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupresico.1	$⊢ φ \to M \in ℝ$
	limsupresico.2	$⊢ Z = [M, +∞)$
	limsupresico.3	$⊢ φ \to F \in V$
Assertion	limsupresico	$⊢ φ \to lim sup ({F ↾}_{Z}) = lim sup (F)$

Proof

Step	Hyp	Ref	Expression
1		limsupresico.1	$⊢ φ \to M \in ℝ$
2		limsupresico.2	$⊢ Z = [M, +∞)$
3		limsupresico.3	$⊢ φ \to F \in V$
4	1	rexrd	$⊢ φ \to M \in ℝ^{*}$
5	4	ad2antrr	$⊢ ((φ \land k \in Z) \land y \in [k, +∞)) \to M \in ℝ^{*}$
6		pnfxr	$⊢ +∞ \in ℝ^{*}$
7	6	a1i	$⊢ ((φ \land k \in Z) \land y \in [k, +∞)) \to +∞ \in ℝ^{*}$
8		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
9	6	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
10		icossre	$⊢ (M \in ℝ \land +∞ \in ℝ^{*}) \to [M, +∞) \subseteq ℝ$
11	1 9 10	syl2anc	$⊢ φ \to [M, +∞) \subseteq ℝ$
12	11	adantr	$⊢ (φ \land k \in Z) \to [M, +∞) \subseteq ℝ$
13	2	eleq2i	$⊢ k \in Z \leftrightarrow k \in [M, +∞)$
14	13	bilani	$⊢ (φ \land k \in Z) \to k \in [M, +∞)$
15	12 14	sseldd	$⊢ (φ \land k \in Z) \to k \in ℝ$
16	15	adantr	$⊢ ((φ \land k \in Z) \land y \in [k, +∞)) \to k \in ℝ$
17		simpr	$⊢ ((φ \land k \in Z) \land y \in [k, +∞)) \to y \in [k, +∞)$
18		elicore	$⊢ (k \in ℝ \land y \in [k, +∞)) \to y \in ℝ$
19	16 17 18	syl2anc	$⊢ ((φ \land k \in Z) \land y \in [k, +∞)) \to y \in ℝ$
20	8 19	sselid	$⊢ ((φ \land k \in Z) \land y \in [k, +∞)) \to y \in ℝ^{*}$
21	1	ad2antrr	$⊢ ((φ \land k \in Z) \land y \in [k, +∞)) \to M \in ℝ$
22	4	adantr	$⊢ (φ \land k \in Z) \to M \in ℝ^{*}$
23	6	a1i	$⊢ (φ \land k \in Z) \to +∞ \in ℝ^{*}$
24	22 23 14	icogelbd	$⊢ (φ \land k \in Z) \to M \leq k$
25	24	adantr	$⊢ ((φ \land k \in Z) \land y \in [k, +∞)) \to M \leq k$
26	8 16	sselid	$⊢ ((φ \land k \in Z) \land y \in [k, +∞)) \to k \in ℝ^{*}$
27	26 7 17	icogelbd	$⊢ ((φ \land k \in Z) \land y \in [k, +∞)) \to k \leq y$
28	21 16 19 25 27	letrd	$⊢ ((φ \land k \in Z) \land y \in [k, +∞)) \to M \leq y$
29	19	ltpnfd	$⊢ ((φ \land k \in Z) \land y \in [k, +∞)) \to y < +∞$
30	5 7 20 28 29	elicod	$⊢ ((φ \land k \in Z) \land y \in [k, +∞)) \to y \in [M, +∞)$
31	30 2	eleqtrrdi	$⊢ ((φ \land k \in Z) \land y \in [k, +∞)) \to y \in Z$
32	31	ssd	$⊢ (φ \land k \in Z) \to [k, +∞) \subseteq Z$
33		resima2	$⊢ [k, +∞) \subseteq Z \to ({F ↾}_{Z}) [[k, +∞)] = F [[k, +∞)]$
34	32 33	syl	$⊢ (φ \land k \in Z) \to ({F ↾}_{Z}) [[k, +∞)] = F [[k, +∞)]$
35	34	ineq1d	$⊢ (φ \land k \in Z) \to ({F ↾}_{Z}) [[k, +∞)] \cap ℝ^{} = F [[k, +∞)] \cap ℝ^{}$
36	35	supeq1d	$⊢ (φ \land k \in Z) \to sup (({F ↾}_{Z}) [[k, +∞)] \cap ℝ^{} ℝ^{} <) = sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)$
37	36	mpteq2dva	$⊢ φ \to (k \in Z ⟼ sup (({F ↾}_{Z}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in Z ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
38	37	rneqd	$⊢ φ \to ran (k \in Z ⟼ sup (({F ↾}_{Z}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = ran (k \in Z ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
39	2 11	eqsstrid	$⊢ φ \to Z \subseteq ℝ$
40	39	mptimass	$⊢ φ \to (k \in ℝ ⟼ sup (({F ↾}_{Z}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) [Z] = ran (k \in Z ⟼ sup (({F ↾}_{Z}) [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
41	39	mptimass	$⊢ φ \to (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) [Z] = ran (k \in Z ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
42	38 40 41	3eqtr4d	$⊢ φ \to (k \in ℝ ⟼ sup (({F ↾}_{Z}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) [Z] = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) [Z]$
43	42	infeq1d	$⊢ φ \to inf ((k \in ℝ ⟼ sup (({F ↾}_{Z}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) [Z] ℝ^{} <) = inf ((k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) [Z] ℝ^{} <)$
44		eqid	$⊢ (k \in ℝ ⟼ sup (({F ↾}_{Z}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ sup (({F ↾}_{Z}) [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
45	3	resexd	$⊢ φ \to {F ↾}_{Z} \in V$
46	2	supeq1i	$⊢ sup (Z ℝ^{} <) = sup ([M, +∞) ℝ^{} <)$
47	46	a1i	$⊢ φ \to sup (Z ℝ^{} <) = sup ([M, +∞) ℝ^{} <)$
48	1	renepnfd	$⊢ φ \to M \neq +∞$
49		icopnfsup	$⊢ (M \in ℝ^{} \land M \neq +∞) \to sup ([M, +∞) ℝ^{} <) = +∞$
50	4 48 49	syl2anc	$⊢ φ \to sup ([M, +∞) ℝ^{*} <) = +∞$
51	47 50	eqtrd	$⊢ φ \to sup (Z ℝ^{*} <) = +∞$
52	44 45 39 51	limsupval2	$⊢ φ \to lim sup ({F ↾}_{Z}) = inf ((k \in ℝ ⟼ sup (({F ↾}_{Z}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) [Z] ℝ^{*} <)$
53		eqid	$⊢ (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
54	53 3 39 51	limsupval2	$⊢ φ \to lim sup (F) = inf ((k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) [Z] ℝ^{*} <)$
55	43 52 54	3eqtr4d	$⊢ φ \to lim sup ({F ↾}_{Z}) = lim sup (F)$

Metamath Proof Explorer

Theorem limsupresico

Proof