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 inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
7	5 6	ax-mp	$⊢ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
8	7	a1i	$⊢ (⊤ \land k \in ℝ) \to inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
9	4 8	supminfxrrnmpt	$⊢ ⊤ \to sup (ran (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) = - inf (ran (k \in ℝ ⟼ - inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <)$
10	9	mptru	$⊢ sup (ran (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) = - inf (ran (k \in ℝ ⟼ - inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <)$
11	10	a1i	$⊢ φ \to sup (ran (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) = - inf (ran (k \in ℝ ⟼ - inf (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 ℝ^{} ℝ^{} <) = - inf (\{z \in ℝ^{} \| - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})\} ℝ^{*} <)$
16	12 15	ax-mp	$⊢ sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <) = - inf (\{z \in ℝ^{} \| - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})\} ℝ^{*} <)$
17	16	a1i	$⊢ φ \to sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <) = - inf (\{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	bilani	$⊢ (((φ \land z \in ℝ^{*}) \land y \in (A \cap [k, +∞))) \land - F (y) = - z) \to - z = - F (y)$
41		simplr	$⊢ ((φ \land z \in ℝ^{}) \land y \in (A \cap [k, +∞))) \to z \in ℝ^{}$
42	3	adantr	$⊢ (φ \land y \in (A \cap [k, +∞))) \to F : A ⟶ ℝ^{*}$
43	30	adantl	$⊢ (φ \land y \in (A \cap [k, +∞))) \to y \in A$
44	42 43	ffvelcdmd	$⊢ (φ \land y \in (A \cap [k, +∞))) \to F (y) \in ℝ^{*}$
45	44	adantlr	$⊢ ((φ \land z \in ℝ^{}) \land y \in (A \cap [k, +∞))) \to F (y) \in ℝ^{}$
46		xneg11	$⊢ (z \in ℝ^{} \land F (y) \in ℝ^{}) \to (- z = - F (y) \leftrightarrow z = F (y))$
47	41 45 46	syl2anc	$⊢ ((φ \land z \in ℝ^{*}) \land y \in (A \cap [k, +∞))) \to (- z = - F (y) \leftrightarrow z = F (y))$
48	47	adantr	$⊢ (((φ \land z \in ℝ^{*}) \land y \in (A \cap [k, +∞))) \land - F (y) = - z) \to (- z = - F (y) \leftrightarrow z = F (y))$
49	40 48	mpbid	$⊢ (((φ \land z \in ℝ^{*}) \land y \in (A \cap [k, +∞))) \land - F (y) = - z) \to z = F (y)$
50	3	ffund	$⊢ φ \to Fun F$
51	50 30	anim12i	$⊢ (φ \land y \in (A \cap [k, +∞))) \to (Fun F \land y \in A)$
52	51	simpld	$⊢ (φ \land y \in (A \cap [k, +∞))) \to Fun F$
53	3	fdmd	$⊢ φ \to dom F = A$
54	53	eqcomd	$⊢ φ \to A = dom F$
55	54	adantr	$⊢ (φ \land y \in (A \cap [k, +∞))) \to A = dom F$
56	43 55	eleqtrd	$⊢ (φ \land y \in (A \cap [k, +∞))) \to y \in dom F$
57	52 56	jca	$⊢ (φ \land y \in (A \cap [k, +∞))) \to (Fun F \land y \in dom F)$
58		elinel2	$⊢ y \in (A \cap [k, +∞)) \to y \in [k, +∞)$
59	58	adantl	$⊢ (φ \land y \in (A \cap [k, +∞))) \to y \in [k, +∞)$
60		funfvima	$⊢ (Fun F \land y \in dom F) \to (y \in [k, +∞) \to F (y) \in F [[k, +∞)])$
61	57 59 60	sylc	$⊢ (φ \land y \in (A \cap [k, +∞))) \to F (y) \in F [[k, +∞)]$
62	61	ad4ant13	$⊢ (((φ \land z \in ℝ^{*}) \land y \in (A \cap [k, +∞))) \land - F (y) = - z) \to F (y) \in F [[k, +∞)]$
63	49 62	eqeltrd	$⊢ (((φ \land z \in ℝ^{*}) \land y \in (A \cap [k, +∞))) \land - F (y) = - z) \to z \in F [[k, +∞)]$
64	38 63	syldan	$⊢ (((φ \land z \in ℝ^{*}) \land y \in (A \cap [k, +∞))) \land (y \in A ⟼ - F (y)) (y) = - z) \to z \in F [[k, +∞)]$
65	64	rexlimdva2	$⊢ (φ \land z \in ℝ^{*}) \to (\exists y \in (A \cap [k, +∞)) (y \in A ⟼ - F (y)) (y) = - z \to z \in F [[k, +∞)])$
66	65	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, +∞)])$
67	29 66	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, +∞)])$
68	28 67	mpd	$⊢ (φ \land z \in ℝ^{} \land - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})) \to z \in F [[k, +∞)]$
69	68	rabssdv	$⊢ φ \to \{z \in ℝ^{} \| - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})\} \subseteq F [[k, +∞)]$
70		ssrab2	$⊢ \{z \in ℝ^{} \| - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})\} \subseteq ℝ^{*}$
71	70	a1i	$⊢ φ \to \{z \in ℝ^{} \| - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})\} \subseteq ℝ^{*}$
72	69 71	ssind	$⊢ φ \to \{z \in ℝ^{} \| - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})\} \subseteq F [[k, +∞)] \cap ℝ^{*}$
73	5	a1i	$⊢ φ \to F [[k, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
74	3	ffnd	$⊢ φ \to F Fn A$
75	74	adantr	$⊢ (φ \land z \in (F [[k, +∞)] \cap ℝ^{*})) \to F Fn A$
76		elinel1	$⊢ z \in (F [[k, +∞)] \cap ℝ^{*}) \to z \in F [[k, +∞)]$
77	76	adantl	$⊢ (φ \land z \in (F [[k, +∞)] \cap ℝ^{*})) \to z \in F [[k, +∞)]$
78		fvelima2	$⊢ (F Fn A \land z \in F [[k, +∞)]) \to \exists y \in (A \cap [k, +∞)) F (y) = z$
79	75 77 78	syl2anc	$⊢ (φ \land z \in (F [[k, +∞)] \cap ℝ^{*})) \to \exists y \in (A \cap [k, +∞)) F (y) = z$
80		elinel2	$⊢ z \in (F [[k, +∞)] \cap ℝ^{}) \to z \in ℝ^{}$
81		eqcom	$⊢ F (y) = z \leftrightarrow z = F (y)$
82	81	bilani	$⊢ (z \in ℝ^{*} \land F (y) = z) \to z = F (y)$
83	82	xnegeqd	$⊢ (z \in ℝ^{*} \land F (y) = z) \to - z = - F (y)$
84	83	ex	$⊢ z \in ℝ^{*} \to (F (y) = z \to - z = - F (y))$
85	84	reximdv	$⊢ z \in ℝ^{*} \to (\exists y \in (A \cap [k, +∞)) F (y) = z \to \exists y \in (A \cap [k, +∞)) - z = - F (y))$
86	80 85	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))$
87	86	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))$
88	79 87	mpd	$⊢ (φ \land z \in (F [[k, +∞)] \cap ℝ^{*})) \to \exists y \in (A \cap [k, +∞)) - z = - F (y)$
89		xnegex	$⊢ - z \in V$
90		elmptima	$⊢ - z \in V \to (- z \in (y \in A ⟼ - F (y)) [[k, +∞)] \leftrightarrow \exists y \in (A \cap [k, +∞)) - z = - F (y))$
91	89 90	ax-mp	$⊢ - z \in (y \in A ⟼ - F (y)) [[k, +∞)] \leftrightarrow \exists y \in (A \cap [k, +∞)) - z = - F (y)$
92	88 91	sylibr	$⊢ (φ \land z \in (F [[k, +∞)] \cap ℝ^{*})) \to - z \in (y \in A ⟼ - F (y)) [[k, +∞)]$
93	73	sselda	$⊢ (φ \land z \in (F [[k, +∞)] \cap ℝ^{})) \to z \in ℝ^{}$
94	93	xnegcld	$⊢ (φ \land z \in (F [[k, +∞)] \cap ℝ^{})) \to - z \in ℝ^{}$
95	92 94	elind	$⊢ (φ \land z \in (F [[k, +∞)] \cap ℝ^{})) \to - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})$
96	73 95	ssrabdv	$⊢ φ \to F [[k, +∞)] \cap ℝ^{} \subseteq \{z \in ℝ^{} \| - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{*})\}$
97	72 96	eqssd	$⊢ φ \to \{z \in ℝ^{} \| - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})\} = F [[k, +∞)] \cap ℝ^{*}$
98	97	infeq1d	$⊢ φ \to inf (\{z \in ℝ^{} \| - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})\} ℝ^{} <) = inf (F [[k, +∞)] \cap ℝ^{} ℝ^{*} <)$
99	98	xnegeqd	$⊢ φ \to - inf (\{z \in ℝ^{} \| - z \in ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{})\} ℝ^{} <) = - inf (F [[k, +∞)] \cap ℝ^{} ℝ^{*} <)$
100	17 99	eqtr2d	$⊢ φ \to - inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) = sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <)$
101	100	mpteq2dv	$⊢ φ \to (k \in ℝ ⟼ - inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
102	101	rneqd	$⊢ φ \to ran (k \in ℝ ⟼ - inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = ran (k \in ℝ ⟼ sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
103	102	infeq1d	$⊢ φ \to inf (ran (k \in ℝ ⟼ - inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) = inf (ran (k \in ℝ ⟼ sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <)$
104	103	xnegeqd	$⊢ φ \to - inf (ran (k \in ℝ ⟼ - inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) = - inf (ran (k \in ℝ ⟼ sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <)$
105	11 104	eqtrd	$⊢ φ \to sup (ran (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) = - inf (ran (k \in ℝ ⟼ sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <)$
106	3 2	fexd	$⊢ φ \to F \in V$
107		eqid	$⊢ (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
108	107	liminfval	$⊢ F \in V \to lim inf (F) = sup (ran (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
109	106 108	syl	$⊢ φ \to lim inf (F) = sup (ran (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
110	2	mptexd	$⊢ φ \to (y \in A ⟼ - F (y)) \in V$
111		eqid	$⊢ (k \in ℝ ⟼ sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
112	111	limsupval	$⊢ (y \in A ⟼ - F (y)) \in V \to lim sup ((y \in A ⟼ - F (y))) = inf (ran (k \in ℝ ⟼ sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
113	110 112	syl	$⊢ φ \to lim sup ((y \in A ⟼ - F (y))) = inf (ran (k \in ℝ ⟼ sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
114	113	xnegeqd	$⊢ φ \to - lim sup ((y \in A ⟼ - F (y))) = - inf (ran (k \in ℝ ⟼ sup ((y \in A ⟼ - F (y)) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
115	105 109 114	3eqtr4d	$⊢ φ \to lim inf (F) = - lim sup ((y \in A ⟼ - F (y)))$
116		nfcv	$⊢ \underline{Ⅎ} x y$
117	1 116	nffv	$⊢ \underline{Ⅎ} x F (y)$
118	117	nfxneg	$⊢ \underline{Ⅎ} x (- F (y))$
119		nfcv	$⊢ \underline{Ⅎ} y (- F (x))$
120		fveq2	$⊢ y = x \to F (y) = F (x)$
121	120	xnegeqd	$⊢ y = x \to - F (y) = - F (x)$
122	118 119 121	cbvmpt	$⊢ (y \in A ⟼ - F (y)) = (x \in A ⟼ - F (x))$
123	122	fveq2i	$⊢ lim sup ((y \in A ⟼ - F (y))) = lim sup ((x \in A ⟼ - F (x)))$
124	123	xnegeqi	$⊢ - lim sup ((y \in A ⟼ - F (y))) = - lim sup ((x \in A ⟼ - F (x)))$
125	124	a1i	$⊢ φ \to - lim sup ((y \in A ⟼ - F (y))) = - lim sup ((x \in A ⟼ - F (x)))$
126	115 125	eqtrd	$⊢ φ \to lim inf (F) = - lim sup ((x \in A ⟼ - F (x)))$

Metamath Proof Explorer

Theorem liminfvalxr

Proof