# Metamath Proof Explorer

## Theorem 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 ${⊢}{\phi }\to {M}\in ℤ$
liminflimsupclim.2 ${⊢}{Z}={ℤ}_{\ge {M}}$
liminflimsupclim.3 ${⊢}{\phi }\to {F}:{Z}⟶ℝ$
liminflimsupclim.4 ${⊢}{\phi }\to \mathrm{lim inf}\left({F}\right)\in ℝ$
liminflimsupclim.5 ${⊢}{\phi }\to \mathrm{lim sup}\left({F}\right)\le \mathrm{lim inf}\left({F}\right)$
Assertion liminflimsupclim ${⊢}{\phi }\to {F}\in \mathrm{dom}⇝$

### Proof

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