xlimliminflimsup

Description: A sequence of extended reals converges if and only if its inferior limit and its superior limit are equal. (Contributed by Glauco Siliprandi, 23-Apr-2023)

	Ref	Expression
Hypotheses	xlimliminflimsup.m	$⊢ φ \to M \in ℤ$
	xlimliminflimsup.z	$⊢ Z = ℤ_{\geq M}$
	xlimliminflimsup.f	$⊢ φ \to F : Z ⟶ ℝ^{*}$
Assertion	xlimliminflimsup	$⊢ φ \to (F \in dom \underset{*}{⇝} \leftrightarrow lim inf (F) = lim sup (F))$

Proof

Step	Hyp	Ref	Expression
1		xlimliminflimsup.m	$⊢ φ \to M \in ℤ$
2		xlimliminflimsup.z	$⊢ Z = ℤ_{\geq M}$
3		xlimliminflimsup.f	$⊢ φ \to F : Z ⟶ ℝ^{*}$
4	1	ad2antrr	$⊢ ((φ \land F \in dom \underset{}{⇝}) \land \underset{}{⇝} (F) \in ℝ) \to M \in ℤ$
5	3	ad2antrr	$⊢ ((φ \land F \in dom \underset{}{⇝}) \land \underset{}{⇝} (F) \in ℝ) \to F : Z ⟶ ℝ^{*}$
6		simpr	$⊢ ((φ \land F \in dom \underset{}{⇝}) \land \underset{}{⇝} (F) \in ℝ) \to \underset{*}{⇝} (F) \in ℝ$
7		xlimdm	$⊢ F \in dom \underset{}{⇝} \leftrightarrow F \underset{}{⇝} \underset{*}{⇝} (F)$
8	7	biimpi	$⊢ F \in dom \underset{}{⇝} \to F \underset{}{⇝} \underset{*}{⇝} (F)$
9	8	ad2antlr	$⊢ ((φ \land F \in dom \underset{}{⇝}) \land \underset{}{⇝} (F) \in ℝ) \to F \underset{}{⇝} \underset{}{⇝} (F)$
10	4 2 5 6 9	xlimxrre	$⊢ ((φ \land F \in dom \underset{}{⇝}) \land \underset{}{⇝} (F) \in ℝ) \to \exists j \in Z ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ$
11	2	eluzelz2	$⊢ j \in Z \to j \in ℤ$
12	11	ad2antlr	$⊢ ((((φ \land F \in dom \underset{}{⇝}) \land \underset{}{⇝} (F) \in ℝ) \land j \in Z) \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ) \to j \in ℤ$
13		eqid	$⊢ ℤ_{\geq j} = ℤ_{\geq j}$
14		simpr	$⊢ ((((φ \land F \in dom \underset{}{⇝}) \land \underset{}{⇝} (F) \in ℝ) \land j \in Z) \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ) \to ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ$
15	14	frexr	$⊢ ((((φ \land F \in dom \underset{}{⇝}) \land \underset{}{⇝} (F) \in ℝ) \land j \in Z) \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ) \to ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ^{*}$
16	9	adantr	$⊢ (((φ \land F \in dom \underset{}{⇝}) \land \underset{}{⇝} (F) \in ℝ) \land j \in Z) \to F \underset{}{⇝} \underset{}{⇝} (F)$
17	2 3	fuzxrpmcn	$⊢ φ \to F \in (ℝ^{*} ↑_{𝑝𝑚} ℂ)$
18	17	ad3antrrr	$⊢ (((φ \land F \in dom \underset{}{⇝}) \land \underset{}{⇝} (F) \in ℝ) \land j \in Z) \to F \in (ℝ^{*} ↑_{𝑝𝑚} ℂ)$
19	11	adantl	$⊢ (((φ \land F \in dom \underset{}{⇝}) \land \underset{}{⇝} (F) \in ℝ) \land j \in Z) \to j \in ℤ$
20	18 19	xlimres	$⊢ (((φ \land F \in dom \underset{}{⇝}) \land \underset{}{⇝} (F) \in ℝ) \land j \in Z) \to (F \underset{}{⇝} \underset{}{⇝} (F) \leftrightarrow ({F ↾}_{ℤ_{\geq j}}) \underset{}{⇝} \underset{}{⇝} (F))$
21	16 20	mpbid	$⊢ (((φ \land F \in dom \underset{}{⇝}) \land \underset{}{⇝} (F) \in ℝ) \land j \in Z) \to ({F ↾}_{ℤ_{\geq j}}) \underset{}{⇝} \underset{}{⇝} (F)$
22	21	adantr	$⊢ ((((φ \land F \in dom \underset{}{⇝}) \land \underset{}{⇝} (F) \in ℝ) \land j \in Z) \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ) \to ({F ↾}_{ℤ_{\geq j}}) \underset{}{⇝} \underset{}{⇝} (F)$
23		simpllr	$⊢ ((((φ \land F \in dom \underset{}{⇝}) \land \underset{}{⇝} (F) \in ℝ) \land j \in Z) \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ) \to \underset{*}{⇝} (F) \in ℝ$
24	12 13 15 22 23	xlimclimdm	$⊢ ((((φ \land F \in dom \underset{}{⇝}) \land \underset{}{⇝} (F) \in ℝ) \land j \in Z) \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ) \to {F ↾}_{ℤ_{\geq j}} \in dom ⇝$
25	12 13 14 24	climliminflimsupd	$⊢ ((((φ \land F \in dom \underset{}{⇝}) \land \underset{}{⇝} (F) \in ℝ) \land j \in Z) \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ) \to lim inf ({F ↾}_{ℤ_{\geq j}}) = lim sup ({F ↾}_{ℤ_{\geq j}})$
26	11	adantl	$⊢ (φ \land j \in Z) \to j \in ℤ$
27	17	elexd	$⊢ φ \to F \in V$
28	27	adantr	$⊢ (φ \land j \in Z) \to F \in V$
29	3	fdmd	$⊢ φ \to dom F = Z$
30	26	ssd	$⊢ φ \to Z \subseteq ℤ$
31	29 30	eqsstrd	$⊢ φ \to dom F \subseteq ℤ$
32	31	adantr	$⊢ (φ \land j \in Z) \to dom F \subseteq ℤ$
33	26 13 28 32	liminfresuz2	$⊢ (φ \land j \in Z) \to lim inf ({F ↾}_{ℤ_{\geq j}}) = lim inf (F)$
34	33	eqcomd	$⊢ (φ \land j \in Z) \to lim inf (F) = lim inf ({F ↾}_{ℤ_{\geq j}})$
35	34	ad5ant14	$⊢ ((((φ \land F \in dom \underset{}{⇝}) \land \underset{}{⇝} (F) \in ℝ) \land j \in Z) \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ) \to lim inf (F) = lim inf ({F ↾}_{ℤ_{\geq j}})$
36	26 13 28 32	limsupresuz2	$⊢ (φ \land j \in Z) \to lim sup ({F ↾}_{ℤ_{\geq j}}) = lim sup (F)$
37	36	eqcomd	$⊢ (φ \land j \in Z) \to lim sup (F) = lim sup ({F ↾}_{ℤ_{\geq j}})$
38	37	ad5ant14	$⊢ ((((φ \land F \in dom \underset{}{⇝}) \land \underset{}{⇝} (F) \in ℝ) \land j \in Z) \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ) \to lim sup (F) = lim sup ({F ↾}_{ℤ_{\geq j}})$
39	25 35 38	3eqtr4d	$⊢ ((((φ \land F \in dom \underset{}{⇝}) \land \underset{}{⇝} (F) \in ℝ) \land j \in Z) \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ) \to lim inf (F) = lim sup (F)$
40	10 39	rexlimddv2	$⊢ ((φ \land F \in dom \underset{}{⇝}) \land \underset{}{⇝} (F) \in ℝ) \to lim inf (F) = lim sup (F)$
41		simpll	$⊢ ((φ \land F \in dom \underset{}{⇝}) \land \underset{}{⇝} (F) = +∞) \to φ$
42	8	adantr	$⊢ (F \in dom \underset{}{⇝} \land \underset{}{⇝} (F) = +∞) \to F \underset{}{⇝} \underset{}{⇝} (F)$
43		simpr	$⊢ (F \in dom \underset{}{⇝} \land \underset{}{⇝} (F) = +∞) \to \underset{*}{⇝} (F) = +∞$
44	42 43	breqtrd	$⊢ (F \in dom \underset{}{⇝} \land \underset{}{⇝} (F) = +∞) \to F \underset{*}{⇝} +∞$
45	44	adantll	$⊢ ((φ \land F \in dom \underset{}{⇝}) \land \underset{}{⇝} (F) = +∞) \to F \underset{*}{⇝} +∞$
46	17	liminfcld	$⊢ φ \to lim inf (F) \in ℝ^{*}$
47	46	adantr	$⊢ (φ \land F \underset{}{⇝} +∞) \to lim inf (F) \in ℝ^{}$
48	17	limsupcld	$⊢ φ \to lim sup (F) \in ℝ^{*}$
49	48	adantr	$⊢ (φ \land F \underset{}{⇝} +∞) \to lim sup (F) \in ℝ^{}$
50	1 2 3	liminflelimsupuz	$⊢ φ \to lim inf (F) \leq lim sup (F)$
51	50	adantr	$⊢ (φ \land F \underset{*}{⇝} +∞) \to lim inf (F) \leq lim sup (F)$
52	49	pnfged	$⊢ (φ \land F \underset{*}{⇝} +∞) \to lim sup (F) \leq +∞$
53	1	adantr	$⊢ (φ \land F \underset{*}{⇝} +∞) \to M \in ℤ$
54	3	adantr	$⊢ (φ \land F \underset{}{⇝} +∞) \to F : Z ⟶ ℝ^{}$
55		simpr	$⊢ (φ \land F \underset{}{⇝} +∞) \to F \underset{}{⇝} +∞$
56	53 2 54 55	xlimpnfliminf	$⊢ (φ \land F \underset{*}{⇝} +∞) \to lim inf (F) = +∞$
57	52 56	breqtrrd	$⊢ (φ \land F \underset{*}{⇝} +∞) \to lim sup (F) \leq lim inf (F)$
58	47 49 51 57	xrletrid	$⊢ (φ \land F \underset{*}{⇝} +∞) \to lim inf (F) = lim sup (F)$
59	41 45 58	syl2anc	$⊢ ((φ \land F \in dom \underset{}{⇝}) \land \underset{}{⇝} (F) = +∞) \to lim inf (F) = lim sup (F)$
60	59	adantlr	$⊢ (((φ \land F \in dom \underset{}{⇝}) \land \neg \underset{}{⇝} (F) \in ℝ) \land \underset{*}{⇝} (F) = +∞) \to lim inf (F) = lim sup (F)$
61		simplll	$⊢ (((φ \land F \in dom \underset{}{⇝}) \land \neg \underset{}{⇝} (F) \in ℝ) \land \neg \underset{*}{⇝} (F) = +∞) \to φ$
62	8	ad2antrr	$⊢ ((F \in dom \underset{}{⇝} \land \neg \underset{}{⇝} (F) \in ℝ) \land \neg \underset{}{⇝} (F) = +∞) \to F \underset{}{⇝} \underset{*}{⇝} (F)$
63		xlimcl	$⊢ F \underset{}{⇝} \underset{}{⇝} (F) \to \underset{}{⇝} (F) \in ℝ^{}$
64	8 63	syl	$⊢ F \in dom \underset{}{⇝} \to \underset{}{⇝} (F) \in ℝ^{*}$
65	64	ad2antrr	$⊢ ((F \in dom \underset{}{⇝} \land \neg \underset{}{⇝} (F) \in ℝ) \land \neg \underset{}{⇝} (F) = +∞) \to \underset{}{⇝} (F) \in ℝ^{*}$
66		simplr	$⊢ ((F \in dom \underset{}{⇝} \land \neg \underset{}{⇝} (F) \in ℝ) \land \neg \underset{}{⇝} (F) = +∞) \to \neg \underset{}{⇝} (F) \in ℝ$
67		neqne	$⊢ \neg \underset{}{⇝} (F) = +∞ \to \underset{}{⇝} (F) \neq +∞$
68	67	adantl	$⊢ ((F \in dom \underset{}{⇝} \land \neg \underset{}{⇝} (F) \in ℝ) \land \neg \underset{}{⇝} (F) = +∞) \to \underset{}{⇝} (F) \neq +∞$
69	65 66 68	xrnpnfmnf	$⊢ ((F \in dom \underset{}{⇝} \land \neg \underset{}{⇝} (F) \in ℝ) \land \neg \underset{}{⇝} (F) = +∞) \to \underset{}{⇝} (F) = −∞$
70	62 69	breqtrd	$⊢ ((F \in dom \underset{}{⇝} \land \neg \underset{}{⇝} (F) \in ℝ) \land \neg \underset{}{⇝} (F) = +∞) \to F \underset{}{⇝} −∞$
71	70	adantlll	$⊢ (((φ \land F \in dom \underset{}{⇝}) \land \neg \underset{}{⇝} (F) \in ℝ) \land \neg \underset{}{⇝} (F) = +∞) \to F \underset{}{⇝} −∞$
72	46	adantr	$⊢ (φ \land F \underset{}{⇝} −∞) \to lim inf (F) \in ℝ^{}$
73	48	adantr	$⊢ (φ \land F \underset{}{⇝} −∞) \to lim sup (F) \in ℝ^{}$
74	50	adantr	$⊢ (φ \land F \underset{*}{⇝} −∞) \to lim inf (F) \leq lim sup (F)$
75	1	adantr	$⊢ (φ \land F \underset{*}{⇝} −∞) \to M \in ℤ$
76	3	adantr	$⊢ (φ \land F \underset{}{⇝} −∞) \to F : Z ⟶ ℝ^{}$
77		simpr	$⊢ (φ \land F \underset{}{⇝} −∞) \to F \underset{}{⇝} −∞$
78	75 2 76 77	xlimmnflimsup	$⊢ (φ \land F \underset{*}{⇝} −∞) \to lim sup (F) = −∞$
79	72	mnfled	$⊢ (φ \land F \underset{*}{⇝} −∞) \to −∞ \leq lim inf (F)$
80	78 79	eqbrtrd	$⊢ (φ \land F \underset{*}{⇝} −∞) \to lim sup (F) \leq lim inf (F)$
81	72 73 74 80	xrletrid	$⊢ (φ \land F \underset{*}{⇝} −∞) \to lim inf (F) = lim sup (F)$
82	61 71 81	syl2anc	$⊢ (((φ \land F \in dom \underset{}{⇝}) \land \neg \underset{}{⇝} (F) \in ℝ) \land \neg \underset{*}{⇝} (F) = +∞) \to lim inf (F) = lim sup (F)$
83	60 82	pm2.61dan	$⊢ ((φ \land F \in dom \underset{}{⇝}) \land \neg \underset{}{⇝} (F) \in ℝ) \to lim inf (F) = lim sup (F)$
84	40 83	pm2.61dan	$⊢ (φ \land F \in dom \underset{*}{⇝}) \to lim inf (F) = lim sup (F)$
85	27	adantr	$⊢ (φ \land lim sup (F) = −∞) \to F \in V$
86		mnfxr	$⊢ −∞ \in ℝ^{*}$
87	86	a1i	$⊢ (φ \land lim sup (F) = −∞) \to −∞ \in ℝ^{*}$
88		simpr	$⊢ (φ \land lim sup (F) = −∞) \to lim sup (F) = −∞$
89	1	adantr	$⊢ (φ \land lim sup (F) = −∞) \to M \in ℤ$
90	3	adantr	$⊢ (φ \land lim sup (F) = −∞) \to F : Z ⟶ ℝ^{*}$
91	89 2 90	xlimmnflimsup2	$⊢ (φ \land lim sup (F) = −∞) \to (F \underset{*}{⇝} −∞ \leftrightarrow lim sup (F) = −∞)$
92	88 91	mpbird	$⊢ (φ \land lim sup (F) = −∞) \to F \underset{*}{⇝} −∞$
93	85 87 92	breldmd	$⊢ (φ \land lim sup (F) = −∞) \to F \in dom \underset{*}{⇝}$
94	93	adantlr	$⊢ ((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) = −∞) \to F \in dom \underset{*}{⇝}$
95	1	ad2antrr	$⊢ ((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \in ℝ) \to M \in ℤ$
96	3	ad2antrr	$⊢ ((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \in ℝ) \to F : Z ⟶ ℝ^{*}$
97		simpr	$⊢ ((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \in ℝ) \to lim sup (F) \in ℝ$
98	97	renepnfd	$⊢ ((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \in ℝ) \to lim sup (F) \neq +∞$
99		simplr	$⊢ ((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \in ℝ) \to lim inf (F) = lim sup (F)$
100	99 97	eqeltrd	$⊢ ((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \in ℝ) \to lim inf (F) \in ℝ$
101	100	renemnfd	$⊢ ((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \in ℝ) \to lim inf (F) \neq −∞$
102	95 2 96 98 101	liminflimsupxrre	$⊢ ((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \in ℝ) \to \exists m \in Z ({F ↾}_{ℤ_{\geq m}}) : ℤ_{\geq m} ⟶ ℝ$
103	2	eluzelz2	$⊢ m \in Z \to m \in ℤ$
104	103	ad2antlr	$⊢ ((((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \in ℝ) \land m \in Z) \land ({F ↾}_{ℤ_{\geq m}}) : ℤ_{\geq m} ⟶ ℝ) \to m \in ℤ$
105		eqid	$⊢ ℤ_{\geq m} = ℤ_{\geq m}$
106		simpr	$⊢ ((((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \in ℝ) \land m \in Z) \land ({F ↾}_{ℤ_{\geq m}}) : ℤ_{\geq m} ⟶ ℝ) \to ({F ↾}_{ℤ_{\geq m}}) : ℤ_{\geq m} ⟶ ℝ$
107		simplll	$⊢ (((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \in ℝ) \land m \in Z) \to φ$
108		simpl	$⊢ (lim inf (F) = lim sup (F) \land lim sup (F) \in ℝ) \to lim inf (F) = lim sup (F)$
109		simpr	$⊢ (lim inf (F) = lim sup (F) \land lim sup (F) \in ℝ) \to lim sup (F) \in ℝ$
110	108 109	eqeltrd	$⊢ (lim inf (F) = lim sup (F) \land lim sup (F) \in ℝ) \to lim inf (F) \in ℝ$
111	110	ad4ant23	$⊢ (((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \in ℝ) \land m \in Z) \to lim inf (F) \in ℝ$
112		simpr	$⊢ (((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \in ℝ) \land m \in Z) \to m \in Z$
113	103	3ad2ant3	$⊢ (φ \land lim inf (F) \in ℝ \land m \in Z) \to m \in ℤ$
114	27	3ad2ant1	$⊢ (φ \land lim inf (F) \in ℝ \land m \in Z) \to F \in V$
115	31	3ad2ant1	$⊢ (φ \land lim inf (F) \in ℝ \land m \in Z) \to dom F \subseteq ℤ$
116	113 105 114 115	liminfresuz2	$⊢ (φ \land lim inf (F) \in ℝ \land m \in Z) \to lim inf ({F ↾}_{ℤ_{\geq m}}) = lim inf (F)$
117		simp2	$⊢ (φ \land lim inf (F) \in ℝ \land m \in Z) \to lim inf (F) \in ℝ$
118	116 117	eqeltrd	$⊢ (φ \land lim inf (F) \in ℝ \land m \in Z) \to lim inf ({F ↾}_{ℤ_{\geq m}}) \in ℝ$
119	107 111 112 118	syl3anc	$⊢ (((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \in ℝ) \land m \in Z) \to lim inf ({F ↾}_{ℤ_{\geq m}}) \in ℝ$
120	119	adantr	$⊢ ((((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \in ℝ) \land m \in Z) \land ({F ↾}_{ℤ_{\geq m}}) : ℤ_{\geq m} ⟶ ℝ) \to lim inf ({F ↾}_{ℤ_{\geq m}}) \in ℝ$
121		simp2	$⊢ (φ \land lim inf (F) = lim sup (F) \land m \in Z) \to lim inf (F) = lim sup (F)$
122	103	adantl	$⊢ (φ \land m \in Z) \to m \in ℤ$
123	27	adantr	$⊢ (φ \land m \in Z) \to F \in V$
124	31	adantr	$⊢ (φ \land m \in Z) \to dom F \subseteq ℤ$
125	122 105 123 124	liminfresuz2	$⊢ (φ \land m \in Z) \to lim inf ({F ↾}_{ℤ_{\geq m}}) = lim inf (F)$
126	125	3adant2	$⊢ (φ \land lim inf (F) = lim sup (F) \land m \in Z) \to lim inf ({F ↾}_{ℤ_{\geq m}}) = lim inf (F)$
127	122 105 123 124	limsupresuz2	$⊢ (φ \land m \in Z) \to lim sup ({F ↾}_{ℤ_{\geq m}}) = lim sup (F)$
128	127	3adant2	$⊢ (φ \land lim inf (F) = lim sup (F) \land m \in Z) \to lim sup ({F ↾}_{ℤ_{\geq m}}) = lim sup (F)$
129	121 126 128	3eqtr4d	$⊢ (φ \land lim inf (F) = lim sup (F) \land m \in Z) \to lim inf ({F ↾}_{ℤ_{\geq m}}) = lim sup ({F ↾}_{ℤ_{\geq m}})$
130	129	ad5ant124	$⊢ ((((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \in ℝ) \land m \in Z) \land ({F ↾}_{ℤ_{\geq m}}) : ℤ_{\geq m} ⟶ ℝ) \to lim inf ({F ↾}_{ℤ_{\geq m}}) = lim sup ({F ↾}_{ℤ_{\geq m}})$
131	104 105 106	climliminflimsup3	$⊢ ((((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \in ℝ) \land m \in Z) \land ({F ↾}_{ℤ_{\geq m}}) : ℤ_{\geq m} ⟶ ℝ) \to ({F ↾}_{ℤ_{\geq m}} \in dom ⇝ \leftrightarrow (lim inf ({F ↾}_{ℤ_{\geq m}}) \in ℝ \land lim inf ({F ↾}_{ℤ_{\geq m}}) = lim sup ({F ↾}_{ℤ_{\geq m}})))$
132	120 130 131	mpbir2and	$⊢ ((((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \in ℝ) \land m \in Z) \land ({F ↾}_{ℤ_{\geq m}}) : ℤ_{\geq m} ⟶ ℝ) \to {F ↾}_{ℤ_{\geq m}} \in dom ⇝$
133	104 105 106 132	dmclimxlim	$⊢ ((((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \in ℝ) \land m \in Z) \land ({F ↾}_{ℤ_{\geq m}}) : ℤ_{\geq m} ⟶ ℝ) \to {F ↾}_{ℤ_{\geq m}} \in dom \underset{*}{⇝}$
134	17	ad4antr	$⊢ ((((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \in ℝ) \land m \in Z) \land ({F ↾}_{ℤ_{\geq m}}) : ℤ_{\geq m} ⟶ ℝ) \to F \in (ℝ^{*} ↑_{𝑝𝑚} ℂ)$
135	134 104	xlimresdm	$⊢ ((((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \in ℝ) \land m \in Z) \land ({F ↾}_{ℤ_{\geq m}}) : ℤ_{\geq m} ⟶ ℝ) \to (F \in dom \underset{}{⇝} \leftrightarrow {F ↾}_{ℤ_{\geq m}} \in dom \underset{}{⇝})$
136	133 135	mpbird	$⊢ ((((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \in ℝ) \land m \in Z) \land ({F ↾}_{ℤ_{\geq m}}) : ℤ_{\geq m} ⟶ ℝ) \to F \in dom \underset{*}{⇝}$
137	102 136	rexlimddv2	$⊢ ((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \in ℝ) \to F \in dom \underset{*}{⇝}$
138	137	adantlr	$⊢ (((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \neq −∞) \land lim sup (F) \in ℝ) \to F \in dom \underset{*}{⇝}$
139		simpll	$⊢ (((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \neq −∞) \land \neg lim sup (F) \in ℝ) \to (φ \land lim inf (F) = lim sup (F))$
140		simpllr	$⊢ (((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \neq −∞) \land \neg lim sup (F) \in ℝ) \to lim inf (F) = lim sup (F)$
141	48	ad2antrr	$⊢ ((φ \land lim sup (F) \neq −∞) \land \neg lim sup (F) \in ℝ) \to lim sup (F) \in ℝ^{*}$
142		simpr	$⊢ ((φ \land lim sup (F) \neq −∞) \land \neg lim sup (F) \in ℝ) \to \neg lim sup (F) \in ℝ$
143		simplr	$⊢ ((φ \land lim sup (F) \neq −∞) \land \neg lim sup (F) \in ℝ) \to lim sup (F) \neq −∞$
144	141 142 143	xrnmnfpnf	$⊢ ((φ \land lim sup (F) \neq −∞) \land \neg lim sup (F) \in ℝ) \to lim sup (F) = +∞$
145	144	adantllr	$⊢ (((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \neq −∞) \land \neg lim sup (F) \in ℝ) \to lim sup (F) = +∞$
146	140 145	eqtrd	$⊢ (((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \neq −∞) \land \neg lim sup (F) \in ℝ) \to lim inf (F) = +∞$
147	27	adantr	$⊢ (φ \land lim inf (F) = +∞) \to F \in V$
148		pnfxr	$⊢ +∞ \in ℝ^{*}$
149	148	a1i	$⊢ (φ \land lim inf (F) = +∞) \to +∞ \in ℝ^{*}$
150	1 2 3	xlimpnfliminf2	$⊢ φ \to (F \underset{*}{⇝} +∞ \leftrightarrow lim inf (F) = +∞)$
151	150	biimpar	$⊢ (φ \land lim inf (F) = +∞) \to F \underset{*}{⇝} +∞$
152	147 149 151	breldmd	$⊢ (φ \land lim inf (F) = +∞) \to F \in dom \underset{*}{⇝}$
153	152	adantlr	$⊢ ((φ \land lim inf (F) = lim sup (F)) \land lim inf (F) = +∞) \to F \in dom \underset{*}{⇝}$
154	139 146 153	syl2anc	$⊢ (((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \neq −∞) \land \neg lim sup (F) \in ℝ) \to F \in dom \underset{*}{⇝}$
155	138 154	pm2.61dan	$⊢ ((φ \land lim inf (F) = lim sup (F)) \land lim sup (F) \neq −∞) \to F \in dom \underset{*}{⇝}$
156	94 155	pm2.61dane	$⊢ (φ \land lim inf (F) = lim sup (F)) \to F \in dom \underset{*}{⇝}$
157	84 156	impbida	$⊢ φ \to (F \in dom \underset{*}{⇝} \leftrightarrow lim inf (F) = lim sup (F))$

Metamath Proof Explorer

Theorem xlimliminflimsup

Proof