liminflimsupclim

Description: A sequence of real numbers converges if its inferior limit is real, and it is greater than or equal to the superior limit (in such a case, they are actually equal, see liminflelimsupuz ). (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	liminflimsupclim.1	$⊢ φ \to M \in ℤ$
	liminflimsupclim.2	$⊢ Z = ℤ_{\geq M}$
	liminflimsupclim.3	$⊢ φ \to F : Z ⟶ ℝ$
	liminflimsupclim.4	$⊢ φ \to lim inf (F) \in ℝ$
	liminflimsupclim.5	$⊢ φ \to lim sup (F) \leq lim inf (F)$
Assertion	liminflimsupclim	$⊢ φ \to F \in dom ⇝$

Proof

Step	Hyp	Ref	Expression
1		liminflimsupclim.1	$⊢ φ \to M \in ℤ$
2		liminflimsupclim.2	$⊢ Z = ℤ_{\geq M}$
3		liminflimsupclim.3	$⊢ φ \to F : Z ⟶ ℝ$
4		liminflimsupclim.4	$⊢ φ \to lim inf (F) \in ℝ$
5		liminflimsupclim.5	$⊢ φ \to lim sup (F) \leq lim inf (F)$
6		climrel	$⊢ Rel ⇝$
7	6	a1i	$⊢ φ \to Rel ⇝$
8	2	fvexi	$⊢ Z \in V$
9	8	a1i	$⊢ φ \to Z \in V$
10	3 9	fexd	$⊢ φ \to F \in V$
11	10	limsupcld	$⊢ φ \to lim sup (F) \in ℝ^{*}$
12	4	rexrd	$⊢ φ \to lim inf (F) \in ℝ^{*}$
13	3	frexr	$⊢ φ \to F : Z ⟶ ℝ^{*}$
14	1 2 13	liminflelimsupuz	$⊢ φ \to lim inf (F) \leq lim sup (F)$
15	11 12 5 14	xrletrid	$⊢ φ \to lim sup (F) = lim inf (F)$
16	15 4	eqeltrd	$⊢ φ \to lim sup (F) \in ℝ$
17	16	recnd	$⊢ φ \to lim sup (F) \in ℂ$
18		nfcv	$⊢ \underline{Ⅎ} k F$
19	1	adantr	$⊢ (φ \land x \in ℝ^{+}) \to M \in ℤ$
20	3	adantr	$⊢ (φ \land x \in ℝ^{+}) \to F : Z ⟶ ℝ$
21	4	adantr	$⊢ (φ \land x \in ℝ^{+}) \to lim inf (F) \in ℝ$
22		simpr	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ^{+}$
23	18 19 2 20 21 22	liminflt	$⊢ (φ \land x \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} lim inf (F) < F (k) + x$
24	21	ad2antrr	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to lim inf (F) \in ℝ$
25	3	ad2antrr	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to F : Z ⟶ ℝ$
26	2	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
27	26	adantll	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to k \in Z$
28	25 27	ffvelrnd	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to F (k) \in ℝ$
29	28	adantllr	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to F (k) \in ℝ$
30	22	ad2antrr	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to x \in ℝ^{+}$
31		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
32	30 31	syl	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to x \in ℝ$
33	24 29 32	ltsubadd2d	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to (lim inf (F) - F (k) < x \leftrightarrow lim inf (F) < F (k) + x)$
34	33	bicomd	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to (lim inf (F) < F (k) + x \leftrightarrow lim inf (F) - F (k) < x)$
35	28	recnd	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to F (k) \in ℂ$
36	15	eqcomd	$⊢ φ \to lim inf (F) = lim sup (F)$
37	36 17	eqeltrd	$⊢ φ \to lim inf (F) \in ℂ$
38	37	ad2antrr	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to lim inf (F) \in ℂ$
39	35 38	negsubdi2d	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to - (F (k) - lim inf (F)) = lim inf (F) - F (k)$
40	39	breq1d	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to (- (F (k) - lim inf (F)) < x \leftrightarrow lim inf (F) - F (k) < x)$
41	40	adantllr	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to (- (F (k) - lim inf (F)) < x \leftrightarrow lim inf (F) - F (k) < x)$
42	41	bicomd	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to (lim inf (F) - F (k) < x \leftrightarrow - (F (k) - lim inf (F)) < x)$
43	29 24	resubcld	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to F (k) - lim inf (F) \in ℝ$
44		ltnegcon1	$⊢ (F (k) - lim inf (F) \in ℝ \land x \in ℝ) \to (- (F (k) - lim inf (F)) < x \leftrightarrow - x < F (k) - lim inf (F))$
45	43 32 44	syl2anc	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to (- (F (k) - lim inf (F)) < x \leftrightarrow - x < F (k) - lim inf (F))$
46	42 45	bitrd	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to (lim inf (F) - F (k) < x \leftrightarrow - x < F (k) - lim inf (F))$
47	36	oveq2d	$⊢ φ \to F (k) - lim inf (F) = F (k) - lim sup (F)$
48	47	breq2d	$⊢ φ \to (- x < F (k) - lim inf (F) \leftrightarrow - x < F (k) - lim sup (F))$
49	48	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to (- x < F (k) - lim inf (F) \leftrightarrow - x < F (k) - lim sup (F))$
50	34 46 49	3bitrd	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to (lim inf (F) < F (k) + x \leftrightarrow - x < F (k) - lim sup (F))$
51	50	ralbidva	$⊢ ((φ \land x \in ℝ^{+}) \land j \in Z) \to (\forall k \in ℤ_{\geq j} lim inf (F) < F (k) + x \leftrightarrow \forall k \in ℤ_{\geq j} - x < F (k) - lim sup (F))$
52	51	rexbidva	$⊢ (φ \land x \in ℝ^{+}) \to (\exists j \in Z \forall k \in ℤ_{\geq j} lim inf (F) < F (k) + x \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} - x < F (k) - lim sup (F))$
53	23 52	mpbid	$⊢ (φ \land x \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} - x < F (k) - lim sup (F)$
54	16	adantr	$⊢ (φ \land x \in ℝ^{+}) \to lim sup (F) \in ℝ$
55	18 19 2 20 54 22	limsupgt	$⊢ (φ \land x \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) - x < lim sup (F)$
56	54	ad2antrr	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to lim sup (F) \in ℝ$
57		ltsub23	$⊢ (F (k) \in ℝ \land x \in ℝ \land lim sup (F) \in ℝ) \to (F (k) - x < lim sup (F) \leftrightarrow F (k) - lim sup (F) < x)$
58	29 32 56 57	syl3anc	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to (F (k) - x < lim sup (F) \leftrightarrow F (k) - lim sup (F) < x)$
59	58	ralbidva	$⊢ ((φ \land x \in ℝ^{+}) \land j \in Z) \to (\forall k \in ℤ_{\geq j} F (k) - x < lim sup (F) \leftrightarrow \forall k \in ℤ_{\geq j} F (k) - lim sup (F) < x)$
60	59	rexbidva	$⊢ (φ \land x \in ℝ^{+}) \to (\exists j \in Z \forall k \in ℤ_{\geq j} F (k) - x < lim sup (F) \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} F (k) - lim sup (F) < x)$
61	55 60	mpbid	$⊢ (φ \land x \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) - lim sup (F) < x$
62	53 61	jca	$⊢ (φ \land x \in ℝ^{+}) \to (\exists j \in Z \forall k \in ℤ_{\geq j} - x < F (k) - lim sup (F) \land \exists j \in Z \forall k \in ℤ_{\geq j} F (k) - lim sup (F) < x)$
63	2	rexanuz2	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} (- x < F (k) - lim sup (F) \land F (k) - lim sup (F) < x) \leftrightarrow (\exists j \in Z \forall k \in ℤ_{\geq j} - x < F (k) - lim sup (F) \land \exists j \in Z \forall k \in ℤ_{\geq j} F (k) - lim sup (F) < x)$
64	62 63	sylibr	$⊢ (φ \land x \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} (- x < F (k) - lim sup (F) \land F (k) - lim sup (F) < x)$
65		simplll	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to φ$
66		simpllr	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to x \in ℝ^{+}$
67	26	adantll	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to k \in Z$
68		simpr	$⊢ (((φ \land x \in ℝ^{+}) \land k \in Z) \land (- x < F (k) - lim sup (F) \land F (k) - lim sup (F) < x)) \to (- x < F (k) - lim sup (F) \land F (k) - lim sup (F) < x)$
69	3	ffvelrnda	$⊢ (φ \land k \in Z) \to F (k) \in ℝ$
70	16	adantr	$⊢ (φ \land k \in Z) \to lim sup (F) \in ℝ$
71	69 70	resubcld	$⊢ (φ \land k \in Z) \to F (k) - lim sup (F) \in ℝ$
72	71	adantlr	$⊢ ((φ \land x \in ℝ^{+}) \land k \in Z) \to F (k) - lim sup (F) \in ℝ$
73	31	ad2antlr	$⊢ ((φ \land x \in ℝ^{+}) \land k \in Z) \to x \in ℝ$
74		abslt	$⊢ (F (k) - lim sup (F) \in ℝ \land x \in ℝ) \to (\|F (k) - lim sup (F)\| < x \leftrightarrow (- x < F (k) - lim sup (F) \land F (k) - lim sup (F) < x))$
75	72 73 74	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land k \in Z) \to (\|F (k) - lim sup (F)\| < x \leftrightarrow (- x < F (k) - lim sup (F) \land F (k) - lim sup (F) < x))$
76	75	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land k \in Z) \land (- x < F (k) - lim sup (F) \land F (k) - lim sup (F) < x)) \to (\|F (k) - lim sup (F)\| < x \leftrightarrow (- x < F (k) - lim sup (F) \land F (k) - lim sup (F) < x))$
77	68 76	mpbird	$⊢ (((φ \land x \in ℝ^{+}) \land k \in Z) \land (- x < F (k) - lim sup (F) \land F (k) - lim sup (F) < x)) \to \|F (k) - lim sup (F)\| < x$
78	77	ex	$⊢ ((φ \land x \in ℝ^{+}) \land k \in Z) \to ((- x < F (k) - lim sup (F) \land F (k) - lim sup (F) < x) \to \|F (k) - lim sup (F)\| < x)$
79	65 66 67 78	syl21anc	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to ((- x < F (k) - lim sup (F) \land F (k) - lim sup (F) < x) \to \|F (k) - lim sup (F)\| < x)$
80	79	ralimdva	$⊢ ((φ \land x \in ℝ^{+}) \land j \in Z) \to (\forall k \in ℤ_{\geq j} (- x < F (k) - lim sup (F) \land F (k) - lim sup (F) < x) \to \forall k \in ℤ_{\geq j} \|F (k) - lim sup (F)\| < x)$
81	80	reximdva	$⊢ (φ \land x \in ℝ^{+}) \to (\exists j \in Z \forall k \in ℤ_{\geq j} (- x < F (k) - lim sup (F) \land F (k) - lim sup (F) < x) \to \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - lim sup (F)\| < x)$
82	64 81	mpd	$⊢ (φ \land x \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - lim sup (F)\| < x$
83	82	ralrimiva	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - lim sup (F)\| < x$
84	17 83	jca	$⊢ φ \to (lim sup (F) \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - lim sup (F)\| < x)$
85		ax-resscn	$⊢ ℝ \subseteq ℂ$
86	85	a1i	$⊢ φ \to ℝ \subseteq ℂ$
87	3 86	fssd	$⊢ φ \to F : Z ⟶ ℂ$
88	18 1 2 87	climuz	$⊢ φ \to (F ⇝ lim sup (F) \leftrightarrow (lim sup (F) \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - lim sup (F)\| < x))$
89	84 88	mpbird	$⊢ φ \to F ⇝ lim sup (F)$
90		releldm	$⊢ (Rel ⇝ \land F ⇝ lim sup (F)) \to F \in dom ⇝$
91	7 89 90	syl2anc	$⊢ φ \to F \in dom ⇝$

Metamath Proof Explorer

Theorem liminflimsupclim

Proof