liminfvalxr

Description: Alternate definition of liminf when F is an extended real-valued function. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	liminfvalxr.1	$⊢ \underline{Ⅎ} x F$
	liminfvalxr.2	$⊢ φ \to A \in V$
	liminfvalxr.3	$⊢ φ \to F : A ⟶ ℝ^{*}$
Assertion	liminfvalxr	$⊢ φ \to lim inf (F) = - lim sup ((x \in A ⟼ - F (x)))$

Proof

Step	Hyp	Ref	Expression
1		liminfvalxr.1	$⊢ \underline{Ⅎ} x F$
2		liminfvalxr.2	$⊢ φ \to A \in V$
3		liminfvalxr.3	$⊢ φ \to F : A ⟶ ℝ^{*}$
4		nftru	$⊢ Ⅎ k ⊤$
5		inss2	$⊢ F [[k, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
6		infxrcl	$⊢ F [[k, +∞)] \cap ℝ^{} \subseteq ℝ^{} \to sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
7	5 6	ax-mp	$⊢ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
8	7	a1i	$⊢ (⊤ \land k \in ℝ) \to sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
9	4 8	supminfxrrnmpt	$⊢ ⊤ \to sup (ran (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) = - sup (ran (k \in ℝ ⟼ - sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <)$
10	9	mptru	$⊢ sup (ran (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) = - sup (ran (k \in ℝ ⟼ - sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <)$
11	10	a1i	$⊢ φ \to sup (ran (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) = - sup (ran (k \in ℝ ⟼ - sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <)$
12		tru	$⊢ ⊤$
13		inss2	$⊢ (y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
14	13	a1i	$⊢ ⊤ \to (y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
15	14	supminfxr2	$⊢ ⊤ \to sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <) = - sup (\{z \in ℝ^{} \| - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})\} ℝ^{*} <)$
16	12 15	ax-mp	$⊢ sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <) = - sup (\{z \in ℝ^{} \| - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})\} ℝ^{*} <)$
17	16	a1i	$⊢ φ \to sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <) = - sup (\{z \in ℝ^{} \| - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})\} ℝ^{*} <)$
18		elinel1	$⊢ - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{*}) \to - z \in (y \in A ⟼ - F (y)) [[k, +∞)]$
19		nfmpt1	$⊢ \underline{Ⅎ} y (y \in A ⟼ - F (y))$
20		xnegex	$⊢ - F (y) \in V$
21		eqid	$⊢ (y \in A ⟼ - F (y)) = (y \in A ⟼ - F (y))$
22	20 21	fnmpti	$⊢ (y \in A ⟼ - F (y)) Fn A$
23	22	a1i	$⊢ φ \to (y \in A ⟼ - F (y)) Fn A$
24	23	adantr	$⊢ (φ \land - z \in (y \in A ⟼ - F (y)) [[k, +∞)]) \to (y \in A ⟼ - F (y)) Fn A$
25		simpr	$⊢ (φ \land - z \in (y \in A ⟼ - F (y)) [[k, +∞)]) \to - z \in (y \in A ⟼ - F (y)) [[k, +∞)]$
26	19 24 25	fvelimad	$⊢ (φ \land - z \in (y \in A ⟼ - F (y)) [[k, +∞)]) \to \exists y \in (A \cap [k, +∞)) (y \in A ⟼ - F (y)) (y) = - z$
27	26	3adant2	$⊢ (φ \land z \in ℝ^{*} \land - z \in (y \in A ⟼ - F (y)) [[k, +∞)]) \to \exists y \in (A \cap [k, +∞)) (y \in A ⟼ - F (y)) (y) = - z$
28	18 27	syl3an3	$⊢ (φ \land z \in ℝ^{} \land - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})) \to \exists y \in (A \cap [k, +∞)) (y \in A ⟼ - F (y)) (y) = - z$
29		elinel2	$⊢ - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{}) \to - z \in ℝ^{}$
30		elinel1	$⊢ y \in (A \cap [k, +∞)) \to y \in A$
31	20	a1i	$⊢ y \in (A \cap [k, +∞)) \to - F (y) \in V$
32	21	fvmpt2	$⊢ (y \in A \land - F (y) \in V) \to (y \in A ⟼ - F (y)) (y) = - F (y)$
33	30 31 32	syl2anc	$⊢ y \in (A \cap [k, +∞)) \to (y \in A ⟼ - F (y)) (y) = - F (y)$
34	33	eqcomd	$⊢ y \in (A \cap [k, +∞)) \to - F (y) = (y \in A ⟼ - F (y)) (y)$
35	34	adantr	$⊢ (y \in (A \cap [k, +∞)) \land (y \in A ⟼ - F (y)) (y) = - z) \to - F (y) = (y \in A ⟼ - F (y)) (y)$
36		simpr	$⊢ (y \in (A \cap [k, +∞)) \land (y \in A ⟼ - F (y)) (y) = - z) \to (y \in A ⟼ - F (y)) (y) = - z$
37	35 36	eqtrd	$⊢ (y \in (A \cap [k, +∞)) \land (y \in A ⟼ - F (y)) (y) = - z) \to - F (y) = - z$
38	37	adantll	$⊢ (((φ \land z \in ℝ^{*}) \land y \in (A \cap [k, +∞))) \land (y \in A ⟼ - F (y)) (y) = - z) \to - F (y) = - z$
39		eqcom	$⊢ - F (y) = - z \leftrightarrow - z = - F (y)$
40	39	biimpi	$⊢ - F (y) = - z \to - z = - F (y)$
41	40	adantl	$⊢ (((φ \land z \in ℝ^{*}) \land y \in (A \cap [k, +∞))) \land - F (y) = - z) \to - z = - F (y)$
42		simplr	$⊢ ((φ \land z \in ℝ^{}) \land y \in (A \cap [k, +∞))) \to z \in ℝ^{}$
43	3	adantr	$⊢ (φ \land y \in (A \cap [k, +∞))) \to F : A ⟶ ℝ^{*}$
44	30	adantl	$⊢ (φ \land y \in (A \cap [k, +∞))) \to y \in A$
45	43 44	ffvelrnd	$⊢ (φ \land y \in (A \cap [k, +∞))) \to F (y) \in ℝ^{*}$
46	45	adantlr	$⊢ ((φ \land z \in ℝ^{}) \land y \in (A \cap [k, +∞))) \to F (y) \in ℝ^{}$
47		xneg11	$⊢ (z \in ℝ^{} \land F (y) \in ℝ^{}) \to (- z = - F (y) \leftrightarrow z = F (y))$
48	42 46 47	syl2anc	$⊢ ((φ \land z \in ℝ^{*}) \land y \in (A \cap [k, +∞))) \to (- z = - F (y) \leftrightarrow z = F (y))$
49	48	adantr	$⊢ (((φ \land z \in ℝ^{*}) \land y \in (A \cap [k, +∞))) \land - F (y) = - z) \to (- z = - F (y) \leftrightarrow z = F (y))$
50	41 49	mpbid	$⊢ (((φ \land z \in ℝ^{*}) \land y \in (A \cap [k, +∞))) \land - F (y) = - z) \to z = F (y)$
51	3	ffund	$⊢ φ \to Fun F$
52	51 30	anim12i	$⊢ (φ \land y \in (A \cap [k, +∞))) \to (Fun F \land y \in A)$
53	52	simpld	$⊢ (φ \land y \in (A \cap [k, +∞))) \to Fun F$
54	3	fdmd	$⊢ φ \to dom F = A$
55	54	eqcomd	$⊢ φ \to A = dom F$
56	55	adantr	$⊢ (φ \land y \in (A \cap [k, +∞))) \to A = dom F$
57	44 56	eleqtrd	$⊢ (φ \land y \in (A \cap [k, +∞))) \to y \in dom F$
58	53 57	jca	$⊢ (φ \land y \in (A \cap [k, +∞))) \to (Fun F \land y \in dom F)$
59		elinel2	$⊢ y \in (A \cap [k, +∞)) \to y \in [k, +∞)$
60	59	adantl	$⊢ (φ \land y \in (A \cap [k, +∞))) \to y \in [k, +∞)$
61		funfvima	$⊢ (Fun F \land y \in dom F) \to (y \in [k, +∞) \to F (y) \in F [[k, +∞)])$
62	58 60 61	sylc	$⊢ (φ \land y \in (A \cap [k, +∞))) \to F (y) \in F [[k, +∞)]$
63	62	ad4ant13	$⊢ (((φ \land z \in ℝ^{*}) \land y \in (A \cap [k, +∞))) \land - F (y) = - z) \to F (y) \in F [[k, +∞)]$
64	50 63	eqeltrd	$⊢ (((φ \land z \in ℝ^{*}) \land y \in (A \cap [k, +∞))) \land - F (y) = - z) \to z \in F [[k, +∞)]$
65	38 64	syldan	$⊢ (((φ \land z \in ℝ^{*}) \land y \in (A \cap [k, +∞))) \land (y \in A ⟼ - F (y)) (y) = - z) \to z \in F [[k, +∞)]$
66	65	rexlimdva2	$⊢ (φ \land z \in ℝ^{*}) \to (\exists y \in (A \cap [k, +∞)) (y \in A ⟼ - F (y)) (y) = - z \to z \in F [[k, +∞)])$
67	66	3adant3	$⊢ (φ \land z \in ℝ^{} \land - z \in ℝ^{}) \to (\exists y \in (A \cap [k, +∞)) (y \in A ⟼ - F (y)) (y) = - z \to z \in F [[k, +∞)])$
68	29 67	syl3an3	$⊢ (φ \land z \in ℝ^{} \land - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})) \to (\exists y \in (A \cap [k, +∞)) (y \in A ⟼ - F (y)) (y) = - z \to z \in F [[k, +∞)])$
69	28 68	mpd	$⊢ (φ \land z \in ℝ^{} \land - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})) \to z \in F [[k, +∞)]$
70	69	rabssdv	$⊢ φ \to \{z \in ℝ^{} \| - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})\} \subseteq F [[k, +∞)]$
71		ssrab2	$⊢ \{z \in ℝ^{} \| - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})\} \subseteq ℝ^{*}$
72	71	a1i	$⊢ φ \to \{z \in ℝ^{} \| - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})\} \subseteq ℝ^{*}$
73	70 72	ssind	$⊢ φ \to \{z \in ℝ^{} \| - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})\} \subseteq F [[k, +∞)] \cap ℝ^{*}$
74	5	a1i	$⊢ φ \to F [[k, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
75	3	ffnd	$⊢ φ \to F Fn A$
76	75	adantr	$⊢ (φ \land z \in (F [[k, +∞)] \cap ℝ^{*})) \to F Fn A$
77		elinel1	$⊢ z \in (F [[k, +∞)] \cap ℝ^{*}) \to z \in F [[k, +∞)]$
78	77	adantl	$⊢ (φ \land z \in (F [[k, +∞)] \cap ℝ^{*})) \to z \in F [[k, +∞)]$
79		fvelima2	$⊢ (F Fn A \land z \in F [[k, +∞)]) \to \exists y \in (A \cap [k, +∞)) F (y) = z$
80	76 78 79	syl2anc	$⊢ (φ \land z \in (F [[k, +∞)] \cap ℝ^{*})) \to \exists y \in (A \cap [k, +∞)) F (y) = z$
81		elinel2	$⊢ z \in (F [[k, +∞)] \cap ℝ^{}) \to z \in ℝ^{}$
82		eqcom	$⊢ F (y) = z \leftrightarrow z = F (y)$
83	82	biimpi	$⊢ F (y) = z \to z = F (y)$
84	83	adantl	$⊢ (z \in ℝ^{*} \land F (y) = z) \to z = F (y)$
85	84	xnegeqd	$⊢ (z \in ℝ^{*} \land F (y) = z) \to - z = - F (y)$
86		simpl	$⊢ (z \in ℝ^{} \land F (y) = z) \to z \in ℝ^{}$
87	84 86	eqeltrrd	$⊢ (z \in ℝ^{} \land F (y) = z) \to F (y) \in ℝ^{}$
88	86 87 47	syl2anc	$⊢ (z \in ℝ^{*} \land F (y) = z) \to (- z = - F (y) \leftrightarrow z = F (y))$
89	85 88	mpbid	$⊢ (z \in ℝ^{*} \land F (y) = z) \to z = F (y)$
90	89	xnegeqd	$⊢ (z \in ℝ^{*} \land F (y) = z) \to - z = - F (y)$
91	90	ex	$⊢ z \in ℝ^{*} \to (F (y) = z \to - z = - F (y))$
92	91	reximdv	$⊢ z \in ℝ^{*} \to (\exists y \in (A \cap [k, +∞)) F (y) = z \to \exists y \in (A \cap [k, +∞)) - z = - F (y))$
93	81 92	syl	$⊢ z \in (F [[k, +∞)] \cap ℝ^{*}) \to (\exists y \in (A \cap [k, +∞)) F (y) = z \to \exists y \in (A \cap [k, +∞)) - z = - F (y))$
94	93	adantl	$⊢ (φ \land z \in (F [[k, +∞)] \cap ℝ^{*})) \to (\exists y \in (A \cap [k, +∞)) F (y) = z \to \exists y \in (A \cap [k, +∞)) - z = - F (y))$
95	80 94	mpd	$⊢ (φ \land z \in (F [[k, +∞)] \cap ℝ^{*})) \to \exists y \in (A \cap [k, +∞)) - z = - F (y)$
96		xnegex	$⊢ - z \in V$
97		elmptima	$⊢ - z \in V \to (- z \in (y \in A ⟼ - F (y)) [[k, +∞)] \leftrightarrow \exists y \in (A \cap [k, +∞)) - z = - F (y))$
98	96 97	ax-mp	$⊢ - z \in (y \in A ⟼ - F (y)) [[k, +∞)] \leftrightarrow \exists y \in (A \cap [k, +∞)) - z = - F (y)$
99	95 98	sylibr	$⊢ (φ \land z \in (F [[k, +∞)] \cap ℝ^{*})) \to - z \in (y \in A ⟼ - F (y)) [[k, +∞)]$
100	74	sselda	$⊢ (φ \land z \in (F [[k, +∞)] \cap ℝ^{})) \to z \in ℝ^{}$
101	100	xnegcld	$⊢ (φ \land z \in (F [[k, +∞)] \cap ℝ^{})) \to - z \in ℝ^{}$
102	99 101	elind	$⊢ (φ \land z \in (F [[k, +∞)] \cap ℝ^{})) \to - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})$
103	74 102	ssrabdv	$⊢ φ \to F [[k, +∞)] \cap ℝ^{} \subseteq \{z \in ℝ^{} \| - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{*})\}$
104	73 103	eqssd	$⊢ φ \to \{z \in ℝ^{} \| - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})\} = F [[k, +∞)] \cap ℝ^{*}$
105	104	infeq1d	$⊢ φ \to sup (\{z \in ℝ^{} \| - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})\} ℝ^{} <) = sup (F [[k, +∞)] \cap ℝ^{} ℝ^{*} <)$
106	105	xnegeqd	$⊢ φ \to - sup (\{z \in ℝ^{} \| - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})\} ℝ^{} <) = - sup (F [[k, +∞)] \cap ℝ^{} ℝ^{*} <)$
107	17 106	eqtr2d	$⊢ φ \to - sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) = sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <)$
108	107	mpteq2dv	$⊢ φ \to (k \in ℝ ⟼ - sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
109	108	rneqd	$⊢ φ \to ran (k \in ℝ ⟼ - sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = ran (k \in ℝ ⟼ sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
110	109	infeq1d	$⊢ φ \to sup (ran (k \in ℝ ⟼ - sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) = sup (ran (k \in ℝ ⟼ sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <)$
111	110	xnegeqd	$⊢ φ \to - sup (ran (k \in ℝ ⟼ - sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) = - sup (ran (k \in ℝ ⟼ sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <)$
112	11 111	eqtrd	$⊢ φ \to sup (ran (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) = - sup (ran (k \in ℝ ⟼ sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <)$
113	3 2	fexd	$⊢ φ \to F \in V$
114		eqid	$⊢ (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
115	114	liminfval	$⊢ F \in V \to lim inf (F) = sup (ran (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
116	113 115	syl	$⊢ φ \to lim inf (F) = sup (ran (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
117	2	mptexd	$⊢ φ \to (y \in A ⟼ - F (y)) \in V$
118		eqid	$⊢ (k \in ℝ ⟼ sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
119	118	limsupval	$⊢ (y \in A ⟼ - F (y)) \in V \to lim sup ((y \in A ⟼ - F (y))) = sup (ran (k \in ℝ ⟼ sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
120	117 119	syl	$⊢ φ \to lim sup ((y \in A ⟼ - F (y))) = sup (ran (k \in ℝ ⟼ sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
121	120	xnegeqd	$⊢ φ \to - lim sup ((y \in A ⟼ - F (y))) = - sup (ran (k \in ℝ ⟼ sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
122	112 116 121	3eqtr4d	$⊢ φ \to lim inf (F) = - lim sup ((y \in A ⟼ - F (y)))$
123		nfcv	$⊢ \underline{Ⅎ} x y$
124	1 123	nffv	$⊢ \underline{Ⅎ} x F (y)$
125	124	nfxneg	$⊢ \underline{Ⅎ} x (- F (y))$
126		nfcv	$⊢ \underline{Ⅎ} y (- F (x))$
127		fveq2	$⊢ y = x \to F (y) = F (x)$
128	127	xnegeqd	$⊢ y = x \to - F (y) = - F (x)$
129	125 126 128	cbvmpt	$⊢ (y \in A ⟼ - F (y)) = (x \in A ⟼ - F (x))$
130	129	fveq2i	$⊢ lim sup ((y \in A ⟼ - F (y))) = lim sup ((x \in A ⟼ - F (x)))$
131	130	xnegeqi	$⊢ - lim sup ((y \in A ⟼ - F (y))) = - lim sup ((x \in A ⟼ - F (x)))$
132	131	a1i	$⊢ φ \to - lim sup ((y \in A ⟼ - F (y))) = - lim sup ((x \in A ⟼ - F (x)))$
133	122 132	eqtrd	$⊢ φ \to lim inf (F) = - lim sup ((x \in A ⟼ - F (x)))$

Metamath Proof Explorer

Theorem liminfvalxr

Proof