liminfresico

Description: The inferior limit doesn't change when a function is restricted to an upperset of reals. (Contributed by Glauco Siliprandi, 2-Jan-2022)

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

Proof

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

Metamath Proof Explorer

Theorem liminfresico

Proof