Metamath Proof Explorer

Theorem limsupvaluz2

Description: The superior limit, when the domain of a real-valued function is a set of upper integers, and the superior limit is real. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupvaluz2.m ${⊢}{\phi }\to {M}\in ℤ$
limsupvaluz2.z ${⊢}{Z}={ℤ}_{\ge {M}}$
limsupvaluz2.f ${⊢}{\phi }\to {F}:{Z}⟶ℝ$
limsupvaluz2.r ${⊢}{\phi }\to \mathrm{lim sup}\left({F}\right)\in ℝ$
Assertion limsupvaluz2 ${⊢}{\phi }\to \mathrm{lim sup}\left({F}\right)=sup\left(\mathrm{ran}\left({k}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {k}}}\right),{ℝ}^{*},<\right)\right),ℝ,<\right)$

Proof

Step Hyp Ref Expression
1 limsupvaluz2.m ${⊢}{\phi }\to {M}\in ℤ$
2 limsupvaluz2.z ${⊢}{Z}={ℤ}_{\ge {M}}$
3 limsupvaluz2.f ${⊢}{\phi }\to {F}:{Z}⟶ℝ$
4 limsupvaluz2.r ${⊢}{\phi }\to \mathrm{lim sup}\left({F}\right)\in ℝ$
5 3 frexr ${⊢}{\phi }\to {F}:{Z}⟶{ℝ}^{*}$
6 1 2 5 limsupvaluz ${⊢}{\phi }\to \mathrm{lim sup}\left({F}\right)=sup\left(\mathrm{ran}\left({n}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)$
7 3 adantr ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {F}:{Z}⟶ℝ$
8 id ${⊢}{n}\in {Z}\to {n}\in {Z}$
9 2 8 uzssd2 ${⊢}{n}\in {Z}\to {ℤ}_{\ge {n}}\subseteq {Z}$
10 9 adantl ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {ℤ}_{\ge {n}}\subseteq {Z}$
11 7 10 feqresmpt ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {{F}↾}_{{ℤ}_{\ge {n}}}=\left({m}\in {ℤ}_{\ge {n}}⟼{F}\left({m}\right)\right)$
12 11 rneqd ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right)=\mathrm{ran}\left({m}\in {ℤ}_{\ge {n}}⟼{F}\left({m}\right)\right)$
13 12 supeq1d ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left({m}\in {ℤ}_{\ge {n}}⟼{F}\left({m}\right)\right),{ℝ}^{*},<\right)$
14 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{F}$
15 4 renepnfd ${⊢}{\phi }\to \mathrm{lim sup}\left({F}\right)\ne \mathrm{+\infty }$
16 14 2 3 15 limsupubuz ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\le {x}$
17 16 adantr ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\le {x}$
18 ssralv ${⊢}{ℤ}_{\ge {n}}\subseteq {Z}\to \left(\forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\le {x}\to \forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\le {x}\right)$
19 9 18 syl ${⊢}{n}\in {Z}\to \left(\forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\le {x}\to \forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\le {x}\right)$
20 19 adantl ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \left(\forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\le {x}\to \forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\le {x}\right)$
21 20 reximdv ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \left(\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\le {x}\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\le {x}\right)$
22 17 21 mpd ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\le {x}$
23 nfv ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {n}\in {Z}\right)$
24 2 eluzelz2 ${⊢}{n}\in {Z}\to {n}\in ℤ$
25 uzid ${⊢}{n}\in ℤ\to {n}\in {ℤ}_{\ge {n}}$
26 ne0i ${⊢}{n}\in {ℤ}_{\ge {n}}\to {ℤ}_{\ge {n}}\ne \varnothing$
27 24 25 26 3syl ${⊢}{n}\in {Z}\to {ℤ}_{\ge {n}}\ne \varnothing$
28 27 adantl ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {ℤ}_{\ge {n}}\ne \varnothing$
29 7 adantr ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {F}:{Z}⟶ℝ$
30 10 sselda ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {m}\in {Z}$
31 29 30 ffvelrnd ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {F}\left({m}\right)\in ℝ$
32 23 28 31 supxrre3rnmpt ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \left(sup\left(\mathrm{ran}\left({m}\in {ℤ}_{\ge {n}}⟼{F}\left({m}\right)\right),{ℝ}^{*},<\right)\in ℝ↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\le {x}\right)$
33 22 32 mpbird ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to sup\left(\mathrm{ran}\left({m}\in {ℤ}_{\ge {n}}⟼{F}\left({m}\right)\right),{ℝ}^{*},<\right)\in ℝ$
34 13 33 eqeltrd ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)\in ℝ$
35 34 fmpttd ${⊢}{\phi }\to \left({n}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)\right):{Z}⟶ℝ$
36 35 frnd ${⊢}{\phi }\to \mathrm{ran}\left({n}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)\right)\subseteq ℝ$
37 nfv ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{\phi }$
38 34 elexd ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)\in \mathrm{V}$
39 eqid ${⊢}\left({n}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)\right)=\left({n}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)\right)$
40 1 2 uzn0d ${⊢}{\phi }\to {Z}\ne \varnothing$
41 37 38 39 40 rnmptn0 ${⊢}{\phi }\to \mathrm{ran}\left({n}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)\right)\ne \varnothing$
42 nfcv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{F}$
43 42 1 2 5 limsupre3uz ${⊢}{\phi }\to \left(\mathrm{lim sup}\left({F}\right)\in ℝ↔\left(\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {i}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {j}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}{x}\le {F}\left({j}\right)\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {i}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {j}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {x}\right)\right)$
44 4 43 mpbid ${⊢}{\phi }\to \left(\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {i}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {j}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}{x}\le {F}\left({j}\right)\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {i}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {j}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {x}\right)$
45 44 simpld ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {i}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {j}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}{x}\le {F}\left({j}\right)$
46 simp-4r ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {i}\in {Z}\right)\wedge {j}\in {ℤ}_{\ge {i}}\right)\wedge {x}\le {F}\left({j}\right)\right)\to {x}\in ℝ$
47 46 rexrd ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {i}\in {Z}\right)\wedge {j}\in {ℤ}_{\ge {i}}\right)\wedge {x}\le {F}\left({j}\right)\right)\to {x}\in {ℝ}^{*}$
48 5 3ad2ant1 ${⊢}\left({\phi }\wedge {i}\in {Z}\wedge {j}\in {ℤ}_{\ge {i}}\right)\to {F}:{Z}⟶{ℝ}^{*}$
49 2 uztrn2 ${⊢}\left({i}\in {Z}\wedge {j}\in {ℤ}_{\ge {i}}\right)\to {j}\in {Z}$
50 49 3adant1 ${⊢}\left({\phi }\wedge {i}\in {Z}\wedge {j}\in {ℤ}_{\ge {i}}\right)\to {j}\in {Z}$
51 48 50 ffvelrnd ${⊢}\left({\phi }\wedge {i}\in {Z}\wedge {j}\in {ℤ}_{\ge {i}}\right)\to {F}\left({j}\right)\in {ℝ}^{*}$
52 51 ad5ant134 ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {i}\in {Z}\right)\wedge {j}\in {ℤ}_{\ge {i}}\right)\wedge {x}\le {F}\left({j}\right)\right)\to {F}\left({j}\right)\in {ℝ}^{*}$
53 rnresss ${⊢}\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right)\subseteq \mathrm{ran}{F}$
54 53 a1i ${⊢}\left({\phi }\wedge {i}\in {Z}\right)\to \mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right)\subseteq \mathrm{ran}{F}$
55 3 frnd ${⊢}{\phi }\to \mathrm{ran}{F}\subseteq ℝ$
56 55 adantr ${⊢}\left({\phi }\wedge {i}\in {Z}\right)\to \mathrm{ran}{F}\subseteq ℝ$
57 54 56 sstrd ${⊢}\left({\phi }\wedge {i}\in {Z}\right)\to \mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right)\subseteq ℝ$
58 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
59 58 a1i ${⊢}\left({\phi }\wedge {i}\in {Z}\right)\to ℝ\subseteq {ℝ}^{*}$
60 57 59 sstrd ${⊢}\left({\phi }\wedge {i}\in {Z}\right)\to \mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right)\subseteq {ℝ}^{*}$
61 60 supxrcld ${⊢}\left({\phi }\wedge {i}\in {Z}\right)\to sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)\in {ℝ}^{*}$
62 61 ad5ant13 ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {i}\in {Z}\right)\wedge {j}\in {ℤ}_{\ge {i}}\right)\wedge {x}\le {F}\left({j}\right)\right)\to sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)\in {ℝ}^{*}$
63 simpr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {i}\in {Z}\right)\wedge {j}\in {ℤ}_{\ge {i}}\right)\wedge {x}\le {F}\left({j}\right)\right)\to {x}\le {F}\left({j}\right)$
64 60 3adant3 ${⊢}\left({\phi }\wedge {i}\in {Z}\wedge {j}\in {ℤ}_{\ge {i}}\right)\to \mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right)\subseteq {ℝ}^{*}$
65 fvres ${⊢}{j}\in {ℤ}_{\ge {i}}\to \left({{F}↾}_{{ℤ}_{\ge {i}}}\right)\left({j}\right)={F}\left({j}\right)$
66 65 eqcomd ${⊢}{j}\in {ℤ}_{\ge {i}}\to {F}\left({j}\right)=\left({{F}↾}_{{ℤ}_{\ge {i}}}\right)\left({j}\right)$
67 66 3ad2ant3 ${⊢}\left({\phi }\wedge {i}\in {Z}\wedge {j}\in {ℤ}_{\ge {i}}\right)\to {F}\left({j}\right)=\left({{F}↾}_{{ℤ}_{\ge {i}}}\right)\left({j}\right)$
68 3 ffnd ${⊢}{\phi }\to {F}Fn{Z}$
69 68 adantr ${⊢}\left({\phi }\wedge {i}\in {Z}\right)\to {F}Fn{Z}$
70 id ${⊢}{i}\in {Z}\to {i}\in {Z}$
71 2 70 uzssd2 ${⊢}{i}\in {Z}\to {ℤ}_{\ge {i}}\subseteq {Z}$
72 71 adantl ${⊢}\left({\phi }\wedge {i}\in {Z}\right)\to {ℤ}_{\ge {i}}\subseteq {Z}$
73 fnssres ${⊢}\left({F}Fn{Z}\wedge {ℤ}_{\ge {i}}\subseteq {Z}\right)\to \left({{F}↾}_{{ℤ}_{\ge {i}}}\right)Fn{ℤ}_{\ge {i}}$
74 69 72 73 syl2anc ${⊢}\left({\phi }\wedge {i}\in {Z}\right)\to \left({{F}↾}_{{ℤ}_{\ge {i}}}\right)Fn{ℤ}_{\ge {i}}$
75 74 3adant3 ${⊢}\left({\phi }\wedge {i}\in {Z}\wedge {j}\in {ℤ}_{\ge {i}}\right)\to \left({{F}↾}_{{ℤ}_{\ge {i}}}\right)Fn{ℤ}_{\ge {i}}$
76 simp3 ${⊢}\left({\phi }\wedge {i}\in {Z}\wedge {j}\in {ℤ}_{\ge {i}}\right)\to {j}\in {ℤ}_{\ge {i}}$
77 fnfvelrn ${⊢}\left(\left({{F}↾}_{{ℤ}_{\ge {i}}}\right)Fn{ℤ}_{\ge {i}}\wedge {j}\in {ℤ}_{\ge {i}}\right)\to \left({{F}↾}_{{ℤ}_{\ge {i}}}\right)\left({j}\right)\in \mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right)$
78 75 76 77 syl2anc ${⊢}\left({\phi }\wedge {i}\in {Z}\wedge {j}\in {ℤ}_{\ge {i}}\right)\to \left({{F}↾}_{{ℤ}_{\ge {i}}}\right)\left({j}\right)\in \mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right)$
79 67 78 eqeltrd ${⊢}\left({\phi }\wedge {i}\in {Z}\wedge {j}\in {ℤ}_{\ge {i}}\right)\to {F}\left({j}\right)\in \mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right)$
80 eqid ${⊢}sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)$
81 64 79 80 supxrubd ${⊢}\left({\phi }\wedge {i}\in {Z}\wedge {j}\in {ℤ}_{\ge {i}}\right)\to {F}\left({j}\right)\le sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)$
82 81 ad5ant134 ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {i}\in {Z}\right)\wedge {j}\in {ℤ}_{\ge {i}}\right)\wedge {x}\le {F}\left({j}\right)\right)\to {F}\left({j}\right)\le sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)$
83 47 52 62 63 82 xrletrd ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {i}\in {Z}\right)\wedge {j}\in {ℤ}_{\ge {i}}\right)\wedge {x}\le {F}\left({j}\right)\right)\to {x}\le sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)$
84 83 rexlimdva2 ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {i}\in {Z}\right)\to \left(\exists {j}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}{x}\le {F}\left({j}\right)\to {x}\le sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)\right)$
85 84 ralimdva ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left(\forall {i}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {j}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}{x}\le {F}\left({j}\right)\to \forall {i}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)\right)$
86 85 reximdva ${⊢}{\phi }\to \left(\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {i}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {j}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}{x}\le {F}\left({j}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {i}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)\right)$
87 45 86 mpd ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {i}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)$
88 87 idi ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {i}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)$
89 fveq2 ${⊢}{n}={i}\to {ℤ}_{\ge {n}}={ℤ}_{\ge {i}}$
90 89 reseq2d ${⊢}{n}={i}\to {{F}↾}_{{ℤ}_{\ge {n}}}={{F}↾}_{{ℤ}_{\ge {i}}}$
91 90 rneqd ${⊢}{n}={i}\to \mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right)=\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right)$
92 91 supeq1d ${⊢}{n}={i}\to sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)$
93 eqcom ${⊢}{n}={i}↔{i}={n}$
94 93 imbi1i ${⊢}\left({n}={i}\to sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)\right)↔\left({i}={n}\to sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)\right)$
95 eqcom ${⊢}sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)↔sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)$
96 95 imbi2i ${⊢}\left({i}={n}\to sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)\right)↔\left({i}={n}\to sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)\right)$
97 94 96 bitri ${⊢}\left({n}={i}\to sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)\right)↔\left({i}={n}\to sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)\right)$
98 92 97 mpbi ${⊢}{i}={n}\to sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)$
99 98 breq2d ${⊢}{i}={n}\to \left({x}\le sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)↔{x}\le sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)\right)$
100 99 cbvralv ${⊢}\forall {i}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)↔\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)$
101 100 rexbii ${⊢}\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {i}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right),{ℝ}^{*},<\right)↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)$
102 88 101 sylib ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)$
103 37 38 rnmptbd2 ${⊢}{\phi }\to \left(\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}\left({n}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)\right)\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)$
104 102 103 mpbid ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}\left({n}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)\right)\phantom{\rule{.4em}{0ex}}{x}\le {y}$
105 infxrre ${⊢}\left(\mathrm{ran}\left({n}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)\right)\subseteq ℝ\wedge \mathrm{ran}\left({n}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)\right)\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}\left({n}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)\right)\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to sup\left(\mathrm{ran}\left({n}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left({n}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)\right),ℝ,<\right)$
106 36 41 104 105 syl3anc ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({n}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left({n}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)\right),ℝ,<\right)$
107 fveq2 ${⊢}{n}={k}\to {ℤ}_{\ge {n}}={ℤ}_{\ge {k}}$
108 107 reseq2d ${⊢}{n}={k}\to {{F}↾}_{{ℤ}_{\ge {n}}}={{F}↾}_{{ℤ}_{\ge {k}}}$
109 108 rneqd ${⊢}{n}={k}\to \mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right)=\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {k}}}\right)$
110 109 supeq1d ${⊢}{n}={k}\to sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {k}}}\right),{ℝ}^{*},<\right)$
111 110 cbvmptv ${⊢}\left({n}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)\right)=\left({k}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {k}}}\right),{ℝ}^{*},<\right)\right)$
112 111 rneqi ${⊢}\mathrm{ran}\left({n}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)\right)=\mathrm{ran}\left({k}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {k}}}\right),{ℝ}^{*},<\right)\right)$
113 112 infeq1i ${⊢}sup\left(\mathrm{ran}\left({n}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)\right),ℝ,<\right)=sup\left(\mathrm{ran}\left({k}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {k}}}\right),{ℝ}^{*},<\right)\right),ℝ,<\right)$
114 113 a1i ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({n}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {n}}}\right),{ℝ}^{*},<\right)\right),ℝ,<\right)=sup\left(\mathrm{ran}\left({k}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {k}}}\right),{ℝ}^{*},<\right)\right),ℝ,<\right)$
115 6 106 114 3eqtrd ${⊢}{\phi }\to \mathrm{lim sup}\left({F}\right)=sup\left(\mathrm{ran}\left({k}\in {Z}⟼sup\left(\mathrm{ran}\left({{F}↾}_{{ℤ}_{\ge {k}}}\right),{ℝ}^{*},<\right)\right),ℝ,<\right)$