liminflelimsuplem

Description: The superior limit is greater than or equal to the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	liminflelimsuplem.1	$⊢ φ \to F \in V$
	liminflelimsuplem.2	$⊢ φ \to \forall k \in ℝ \exists j \in [k, +∞) F [[j, +∞)] \cap ℝ^{*} \neq \emptyset$
Assertion	liminflelimsuplem	$⊢ φ \to lim inf (F) \leq lim sup (F)$

Proof

Step	Hyp	Ref	Expression
1		liminflelimsuplem.1	$⊢ φ \to F \in V$
2		liminflelimsuplem.2	$⊢ φ \to \forall k \in ℝ \exists j \in [k, +∞) F [[j, +∞)] \cap ℝ^{*} \neq \emptyset$
3		inss2	$⊢ F [[i, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
4		infxrcl	$⊢ F [[i, +∞)] \cap ℝ^{} \subseteq ℝ^{} \to inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
5	3 4	ax-mp	$⊢ inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
6	5	a1i	$⊢ (((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \land F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{}$
7		inss2	$⊢ F [[j, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
8		infxrcl	$⊢ F [[j, +∞)] \cap ℝ^{} \subseteq ℝ^{} \to inf (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
9	7 8	ax-mp	$⊢ inf (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
10	9	a1i	$⊢ (((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \land F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to inf (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{}$
11		inss2	$⊢ F [[l, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
12	11	supxrcli	$⊢ sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
13	12	a1i	$⊢ (((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \land F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{}$
14		rexr	$⊢ i \in ℝ \to i \in ℝ^{*}$
15	14	ad2antrr	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to i \in ℝ^{*}$
16		pnfxr	$⊢ +∞ \in ℝ^{*}$
17	16	a1i	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to +∞ \in ℝ^{*}$
18		simpr	$⊢ (i \in ℝ \land l \in ℝ) \to l \in ℝ$
19		simpl	$⊢ (i \in ℝ \land l \in ℝ) \to i \in ℝ$
20	18 19	ifcld	$⊢ (i \in ℝ \land l \in ℝ) \to if (i \leq l, l, i) \in ℝ$
21	20	rexrd	$⊢ (i \in ℝ \land l \in ℝ) \to if (i \leq l, l, i) \in ℝ^{*}$
22	21	adantr	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to if (i \leq l, l, i) \in ℝ^{*}$
23		icossxr	$⊢ [if (i \leq l, l, i), +∞) \subseteq ℝ^{*}$
24	23	sseli	$⊢ j \in [if (i \leq l, l, i), +∞) \to j \in ℝ^{*}$
25	24	adantl	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to j \in ℝ^{*}$
26		max1	$⊢ (i \in ℝ \land l \in ℝ) \to i \leq if (i \leq l, l, i)$
27	26	adantr	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to i \leq if (i \leq l, l, i)$
28		simpr	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to j \in [if (i \leq l, l, i), +∞)$
29	22 17 28	icogelbd	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to if (i \leq l, l, i) \leq j$
30	15 22 25 27 29	xrletrd	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to i \leq j$
31	15 17 30	icossico2d	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to [j, +∞) \subseteq [i, +∞)$
32	31	imass2d	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to F [[j, +∞)] \subseteq F [[i, +∞)]$
33	32	ssrind	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to F [[j, +∞)] \cap ℝ^{} \subseteq F [[i, +∞)] \cap ℝ^{}$
34		infxrss	$⊢ (F [[j, +∞)] \cap ℝ^{} \subseteq F [[i, +∞)] \cap ℝ^{} \land F [[i, +∞)] \cap ℝ^{} \subseteq ℝ^{}) \to inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq inf (F [[j, +∞)] \cap ℝ^{} ℝ^{} <)$
35	33 3 34	sylancl	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq inf (F [[j, +∞)] \cap ℝ^{} ℝ^{} <)$
36	35	adantr	$⊢ (((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \land F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq inf (F [[j, +∞)] \cap ℝ^{} ℝ^{*} <)$
37	7	supxrcli	$⊢ sup (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
38	37	a1i	$⊢ (((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \land F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to sup (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{}$
39	7	a1i	$⊢ (((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \land F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to F [[j, +∞)] \cap ℝ^{} \subseteq ℝ^{*}$
40		simpr	$⊢ (((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \land F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to F [[j, +∞)] \cap ℝ^{} \neq \emptyset$
41	39 40	infxrlesupxr	$⊢ (((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \land F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to inf (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[j, +∞)] \cap ℝ^{} ℝ^{*} <)$
42		rexr	$⊢ l \in ℝ \to l \in ℝ^{*}$
43	42	ad2antlr	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to l \in ℝ^{*}$
44		max2	$⊢ (i \in ℝ \land l \in ℝ) \to l \leq if (i \leq l, l, i)$
45	44	adantr	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to l \leq if (i \leq l, l, i)$
46	43 22 25 45 29	xrletrd	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to l \leq j$
47	43 17 46	icossico2d	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to [j, +∞) \subseteq [l, +∞)$
48	47	imass2d	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to F [[j, +∞)] \subseteq F [[l, +∞)]$
49	48	ssrind	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to F [[j, +∞)] \cap ℝ^{} \subseteq F [[l, +∞)] \cap ℝ^{}$
50	11	a1i	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to F [[l, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
51	49 50	xrsupssd	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to sup (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <)$
52	51	adantr	$⊢ (((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \land F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to sup (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[l, +∞)] \cap ℝ^{} ℝ^{*} <)$
53	10 38 13 41 52	xrletrd	$⊢ (((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \land F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to inf (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[l, +∞)] \cap ℝ^{} ℝ^{*} <)$
54	6 10 13 36 53	xrletrd	$⊢ (((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \land F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[l, +∞)] \cap ℝ^{} ℝ^{*} <)$
55	54	ad5ant2345	$⊢ ((((φ \land i \in ℝ) \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \land F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[l, +∞)] \cap ℝ^{} ℝ^{*} <)$
56		oveq1	$⊢ k = if (i \leq l, l, i) \to [k, +∞) = [if (i \leq l, l, i), +∞)$
57	56	rexeqdv	$⊢ k = if (i \leq l, l, i) \to (\exists j \in [k, +∞) F [[j, +∞)] \cap ℝ^{} \neq \emptyset \leftrightarrow \exists j \in [if (i \leq l, l, i), +∞) F [[j, +∞)] \cap ℝ^{} \neq \emptyset)$
58	2	ad2antrr	$⊢ ((φ \land i \in ℝ) \land l \in ℝ) \to \forall k \in ℝ \exists j \in [k, +∞) F [[j, +∞)] \cap ℝ^{*} \neq \emptyset$
59	20	adantll	$⊢ ((φ \land i \in ℝ) \land l \in ℝ) \to if (i \leq l, l, i) \in ℝ$
60	57 58 59	rspcdva	$⊢ ((φ \land i \in ℝ) \land l \in ℝ) \to \exists j \in [if (i \leq l, l, i), +∞) F [[j, +∞)] \cap ℝ^{*} \neq \emptyset$
61	55 60	r19.29a	$⊢ ((φ \land i \in ℝ) \land l \in ℝ) \to inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <)$
62	61	ralrimiva	$⊢ (φ \land i \in ℝ) \to \forall l \in ℝ inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <)$
63		nfv	$⊢ Ⅎ l φ$
64		xrltso	$⊢ < Or ℝ^{*}$
65	64	supex	$⊢ sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <) \in V$
66	65	a1i	$⊢ (φ \land l \in ℝ) \to sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <) \in V$
67		breq2	$⊢ y = sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <) \to (inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq y \leftrightarrow inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <))$
68	63 66 67	ralrnmpt3	$⊢ φ \to (\forall y \in ran (l \in ℝ ⟼ sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <)) inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq y \leftrightarrow \forall l \in ℝ inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <))$
69	68	adantr	$⊢ (φ \land i \in ℝ) \to (\forall y \in ran (l \in ℝ ⟼ sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <)) inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq y \leftrightarrow \forall l \in ℝ inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <))$
70	62 69	mpbird	$⊢ (φ \land i \in ℝ) \to \forall y \in ran (l \in ℝ ⟼ sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <)) inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq y$
71		oveq1	$⊢ l = i \to [l, +∞) = [i, +∞)$
72	71	imaeq2d	$⊢ l = i \to F [[l, +∞)] = F [[i, +∞)]$
73	72	ineq1d	$⊢ l = i \to F [[l, +∞)] \cap ℝ^{} = F [[i, +∞)] \cap ℝ^{}$
74	73	supeq1d	$⊢ l = i \to sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <) = sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)$
75	74	cbvmptv	$⊢ (l \in ℝ ⟼ sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <)) = (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <))$
76	75	rneqi	$⊢ ran (l \in ℝ ⟼ sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <)) = ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <))$
77	76	raleqi	$⊢ \forall y \in ran (l \in ℝ ⟼ sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <)) inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq y \leftrightarrow \forall y \in ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq y$
78	70 77	sylib	$⊢ (φ \land i \in ℝ) \to \forall y \in ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq y$
79	3	supxrcli	$⊢ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
80	79	rgenw	$⊢ \forall i \in ℝ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
81		eqid	$⊢ (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) = (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <))$
82	81	rnmptss	$⊢ \forall i \in ℝ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{} \to ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) \subseteq ℝ^{}$
83	80 82	ax-mp	$⊢ ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) \subseteq ℝ^{*}$
84	83	a1i	$⊢ (φ \land i \in ℝ) \to ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) \subseteq ℝ^{*}$
85		infxrgelb	$⊢ (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) \subseteq ℝ^{} \land inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{}) \to (inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) \leftrightarrow \forall y \in ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) inf (F [[i, +∞)] \cap ℝ^{} ℝ^{*} <) \leq y)$
86	84 5 85	sylancl	$⊢ (φ \land i \in ℝ) \to (inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) \leftrightarrow \forall y \in ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) inf (F [[i, +∞)] \cap ℝ^{} ℝ^{*} <) \leq y)$
87	78 86	mpbird	$⊢ (φ \land i \in ℝ) \to inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
88	87	ralrimiva	$⊢ φ \to \forall i \in ℝ inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
89		nfv	$⊢ Ⅎ i φ$
90		nfcv	$⊢ \underline{Ⅎ} i ℝ$
91		nfmpt1	$⊢ \underline{Ⅎ} i (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <))$
92	91	nfrn	$⊢ \underline{Ⅎ} i ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <))$
93		nfcv	$⊢ \underline{Ⅎ} i ℝ^{*}$
94		nfcv	$⊢ \underline{Ⅎ} i <$
95	92 93 94	nfinf	$⊢ \underline{Ⅎ} i inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
96	5	a1i	$⊢ (φ \land i \in ℝ) \to inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
97		infxrcl	$⊢ ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) \subseteq ℝ^{} \to inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) \in ℝ^{*}$
98	83 97	ax-mp	$⊢ inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) \in ℝ^{}$
99	98	a1i	$⊢ φ \to inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) \in ℝ^{}$
100	89 90 95 96 99	supxrleubrnmptf	$⊢ φ \to (sup (ran (i \in ℝ ⟼ inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) \leq inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) \leftrightarrow \forall i \in ℝ inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <))$
101	88 100	mpbird	$⊢ φ \to sup (ran (i \in ℝ ⟼ inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) \leq inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <)$
102		eqid	$⊢ (i \in ℝ ⟼ inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) = (i \in ℝ ⟼ inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <))$
103	1 102	liminfvald	$⊢ φ \to lim inf (F) = sup (ran (i \in ℝ ⟼ inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
104	1 81	limsupvald	$⊢ φ \to lim sup (F) = inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
105	101 103 104	3brtr4d	$⊢ φ \to lim inf (F) \leq lim sup (F)$

Metamath Proof Explorer

Theorem liminflelimsuplem

Proof