# Metamath Proof Explorer

## Theorem ioodvbdlimc1lem1

Description: If F has bounded derivative on ( A (,) B ) then a sequence of points in its image converges to its limsup . (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 3-Oct-2020)

Ref Expression
Hypotheses ioodvbdlimc1lem1.a ${⊢}{\phi }\to {A}\in ℝ$
ioodvbdlimc1lem1.b ${⊢}{\phi }\to {B}\in ℝ$
ioodvbdlimc1lem1.altb ${⊢}{\phi }\to {A}<{B}$
ioodvbdlimc1lem1.f ${⊢}{\phi }\to {F}:\left({A},{B}\right)\underset{cn}{⟶}ℝ$
ioodvbdlimc1lem1.dmdv ${⊢}{\phi }\to \mathrm{dom}{{F}}_{ℝ}^{\prime }=\left({A},{B}\right)$
ioodvbdlimc1lem1.dvbd ${⊢}{\phi }\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in \left({A},{B}\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({x}\right)\right|\le {y}$
ioodvbdlimc1lem1.m ${⊢}{\phi }\to {M}\in ℤ$
ioodvbdlimc1lem1.r ${⊢}{\phi }\to {R}:{ℤ}_{\ge {M}}⟶\left({A},{B}\right)$
ioodvbdlimc1lem1.s ${⊢}{S}=\left({j}\in {ℤ}_{\ge {M}}⟼{F}\left({R}\left({j}\right)\right)\right)$
ioodvbdlimc1lem1.rcnv ${⊢}{\phi }\to {R}\in \mathrm{dom}⇝$
ioodvbdlimc1lem1.k ${⊢}{K}=sup\left(\left\{{k}\in {ℤ}_{\ge {M}}|\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\right\},ℝ,<\right)$
Assertion ioodvbdlimc1lem1 ${⊢}{\phi }\to {S}⇝\mathrm{lim sup}\left({S}\right)$

### Proof

Step Hyp Ref Expression
1 ioodvbdlimc1lem1.a ${⊢}{\phi }\to {A}\in ℝ$
2 ioodvbdlimc1lem1.b ${⊢}{\phi }\to {B}\in ℝ$
3 ioodvbdlimc1lem1.altb ${⊢}{\phi }\to {A}<{B}$
4 ioodvbdlimc1lem1.f ${⊢}{\phi }\to {F}:\left({A},{B}\right)\underset{cn}{⟶}ℝ$
5 ioodvbdlimc1lem1.dmdv ${⊢}{\phi }\to \mathrm{dom}{{F}}_{ℝ}^{\prime }=\left({A},{B}\right)$
6 ioodvbdlimc1lem1.dvbd ${⊢}{\phi }\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in \left({A},{B}\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({x}\right)\right|\le {y}$
7 ioodvbdlimc1lem1.m ${⊢}{\phi }\to {M}\in ℤ$
8 ioodvbdlimc1lem1.r ${⊢}{\phi }\to {R}:{ℤ}_{\ge {M}}⟶\left({A},{B}\right)$
9 ioodvbdlimc1lem1.s ${⊢}{S}=\left({j}\in {ℤ}_{\ge {M}}⟼{F}\left({R}\left({j}\right)\right)\right)$
10 ioodvbdlimc1lem1.rcnv ${⊢}{\phi }\to {R}\in \mathrm{dom}⇝$
11 ioodvbdlimc1lem1.k ${⊢}{K}=sup\left(\left\{{k}\in {ℤ}_{\ge {M}}|\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\right\},ℝ,<\right)$
12 eqid ${⊢}{ℤ}_{\ge {M}}={ℤ}_{\ge {M}}$
13 cncff ${⊢}{F}:\left({A},{B}\right)\underset{cn}{⟶}ℝ\to {F}:\left({A},{B}\right)⟶ℝ$
14 4 13 syl ${⊢}{\phi }\to {F}:\left({A},{B}\right)⟶ℝ$
15 14 adantr ${⊢}\left({\phi }\wedge {j}\in {ℤ}_{\ge {M}}\right)\to {F}:\left({A},{B}\right)⟶ℝ$
16 8 ffvelrnda ${⊢}\left({\phi }\wedge {j}\in {ℤ}_{\ge {M}}\right)\to {R}\left({j}\right)\in \left({A},{B}\right)$
17 15 16 ffvelrnd ${⊢}\left({\phi }\wedge {j}\in {ℤ}_{\ge {M}}\right)\to {F}\left({R}\left({j}\right)\right)\in ℝ$
18 17 9 fmptd ${⊢}{\phi }\to {S}:{ℤ}_{\ge {M}}⟶ℝ$
19 ssrab2 ${⊢}\left\{{k}\in {ℤ}_{\ge {M}}|\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\right\}\subseteq {ℤ}_{\ge {M}}$
20 rpre ${⊢}{x}\in {ℝ}^{+}\to {x}\in ℝ$
21 20 adantl ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {x}\in ℝ$
22 2fveq3 ${⊢}{z}={x}\to \left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|=\left|{{F}}_{ℝ}^{\prime }\left({x}\right)\right|$
23 22 cbvmptv ${⊢}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right)=\left({x}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({x}\right)\right|\right)$
24 23 rneqi ${⊢}\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right)=\mathrm{ran}\left({x}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({x}\right)\right|\right)$
25 24 supeq1i ${⊢}sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)=sup\left(\mathrm{ran}\left({x}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({x}\right)\right|\right),ℝ,<\right)$
26 ioomidp ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \frac{{A}+{B}}{2}\in \left({A},{B}\right)$
27 1 2 3 26 syl3anc ${⊢}{\phi }\to \frac{{A}+{B}}{2}\in \left({A},{B}\right)$
28 27 ne0d ${⊢}{\phi }\to \left({A},{B}\right)\ne \varnothing$
29 ioossre ${⊢}\left({A},{B}\right)\subseteq ℝ$
30 29 a1i ${⊢}{\phi }\to \left({A},{B}\right)\subseteq ℝ$
31 dvfre ${⊢}\left({F}:\left({A},{B}\right)⟶ℝ\wedge \left({A},{B}\right)\subseteq ℝ\right)\to {{F}}_{ℝ}^{\prime }:\mathrm{dom}{{F}}_{ℝ}^{\prime }⟶ℝ$
32 14 30 31 syl2anc ${⊢}{\phi }\to {{F}}_{ℝ}^{\prime }:\mathrm{dom}{{F}}_{ℝ}^{\prime }⟶ℝ$
33 5 feq2d ${⊢}{\phi }\to \left({{F}}_{ℝ}^{\prime }:\mathrm{dom}{{F}}_{ℝ}^{\prime }⟶ℝ↔{{F}}_{ℝ}^{\prime }:\left({A},{B}\right)⟶ℝ\right)$
34 32 33 mpbid ${⊢}{\phi }\to {{F}}_{ℝ}^{\prime }:\left({A},{B}\right)⟶ℝ$
35 ax-resscn ${⊢}ℝ\subseteq ℂ$
36 35 a1i ${⊢}{\phi }\to ℝ\subseteq ℂ$
37 34 36 fssd ${⊢}{\phi }\to {{F}}_{ℝ}^{\prime }:\left({A},{B}\right)⟶ℂ$
38 37 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {{F}}_{ℝ}^{\prime }\left({x}\right)\in ℂ$
39 38 abscld ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to \left|{{F}}_{ℝ}^{\prime }\left({x}\right)\right|\in ℝ$
40 eqid ${⊢}\left({x}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({x}\right)\right|\right)=\left({x}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({x}\right)\right|\right)$
41 eqid ${⊢}sup\left(\mathrm{ran}\left({x}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({x}\right)\right|\right),ℝ,<\right)=sup\left(\mathrm{ran}\left({x}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({x}\right)\right|\right),ℝ,<\right)$
42 28 39 6 40 41 suprnmpt ${⊢}{\phi }\to \left(sup\left(\mathrm{ran}\left({x}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({x}\right)\right|\right),ℝ,<\right)\in ℝ\wedge \forall {x}\in \left({A},{B}\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({x}\right)\right|\le sup\left(\mathrm{ran}\left({x}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({x}\right)\right|\right),ℝ,<\right)\right)$
43 42 simpld ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({x}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({x}\right)\right|\right),ℝ,<\right)\in ℝ$
44 25 43 eqeltrid ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)\in ℝ$
45 44 adantr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)\in ℝ$
46 peano2re ${⊢}sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)\in ℝ\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1\in ℝ$
47 45 46 syl ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1\in ℝ$
48 0red ${⊢}{\phi }\to 0\in ℝ$
49 1red ${⊢}{\phi }\to 1\in ℝ$
50 48 49 readdcld ${⊢}{\phi }\to 0+1\in ℝ$
51 44 46 syl ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1\in ℝ$
52 48 ltp1d ${⊢}{\phi }\to 0<0+1$
53 37 27 ffvelrnd ${⊢}{\phi }\to {{F}}_{ℝ}^{\prime }\left(\frac{{A}+{B}}{2}\right)\in ℂ$
54 53 abscld ${⊢}{\phi }\to \left|{{F}}_{ℝ}^{\prime }\left(\frac{{A}+{B}}{2}\right)\right|\in ℝ$
55 53 absge0d ${⊢}{\phi }\to 0\le \left|{{F}}_{ℝ}^{\prime }\left(\frac{{A}+{B}}{2}\right)\right|$
56 42 simprd ${⊢}{\phi }\to \forall {x}\in \left({A},{B}\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({x}\right)\right|\le sup\left(\mathrm{ran}\left({x}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({x}\right)\right|\right),ℝ,<\right)$
57 2fveq3 ${⊢}{y}={x}\to \left|{{F}}_{ℝ}^{\prime }\left({y}\right)\right|=\left|{{F}}_{ℝ}^{\prime }\left({x}\right)\right|$
58 25 a1i ${⊢}{y}={x}\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)=sup\left(\mathrm{ran}\left({x}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({x}\right)\right|\right),ℝ,<\right)$
59 57 58 breq12d ${⊢}{y}={x}\to \left(\left|{{F}}_{ℝ}^{\prime }\left({y}\right)\right|\le sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)↔\left|{{F}}_{ℝ}^{\prime }\left({x}\right)\right|\le sup\left(\mathrm{ran}\left({x}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({x}\right)\right|\right),ℝ,<\right)\right)$
60 59 cbvralvw ${⊢}\forall {y}\in \left({A},{B}\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({y}\right)\right|\le sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)↔\forall {x}\in \left({A},{B}\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({x}\right)\right|\le sup\left(\mathrm{ran}\left({x}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({x}\right)\right|\right),ℝ,<\right)$
61 56 60 sylibr ${⊢}{\phi }\to \forall {y}\in \left({A},{B}\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({y}\right)\right|\le sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)$
62 2fveq3 ${⊢}{y}=\frac{{A}+{B}}{2}\to \left|{{F}}_{ℝ}^{\prime }\left({y}\right)\right|=\left|{{F}}_{ℝ}^{\prime }\left(\frac{{A}+{B}}{2}\right)\right|$
63 62 breq1d ${⊢}{y}=\frac{{A}+{B}}{2}\to \left(\left|{{F}}_{ℝ}^{\prime }\left({y}\right)\right|\le sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)↔\left|{{F}}_{ℝ}^{\prime }\left(\frac{{A}+{B}}{2}\right)\right|\le sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)\right)$
64 63 rspcva ${⊢}\left(\frac{{A}+{B}}{2}\in \left({A},{B}\right)\wedge \forall {y}\in \left({A},{B}\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({y}\right)\right|\le sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)\right)\to \left|{{F}}_{ℝ}^{\prime }\left(\frac{{A}+{B}}{2}\right)\right|\le sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)$
65 27 61 64 syl2anc ${⊢}{\phi }\to \left|{{F}}_{ℝ}^{\prime }\left(\frac{{A}+{B}}{2}\right)\right|\le sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)$
66 48 54 44 55 65 letrd ${⊢}{\phi }\to 0\le sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)$
67 48 44 49 66 leadd1dd ${⊢}{\phi }\to 0+1\le sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1$
68 48 50 51 52 67 ltletrd ${⊢}{\phi }\to 0
69 68 gt0ne0d ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1\ne 0$
70 69 adantr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1\ne 0$
71 21 47 70 redivcld ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\in ℝ$
72 rpgt0 ${⊢}{x}\in {ℝ}^{+}\to 0<{x}$
73 72 adantl ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to 0<{x}$
74 68 adantr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to 0
75 21 47 73 74 divgt0d ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to 0<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}$
76 71 75 elrpd ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\in {ℝ}^{+}$
77 7 adantr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {M}\in ℤ$
78 10 adantr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {R}\in \mathrm{dom}⇝$
79 12 climcau ${⊢}\left({M}\in ℤ\wedge {R}\in \mathrm{dom}⇝\right)\to \forall {w}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {k}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<{w}$
80 77 78 79 syl2anc ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \forall {w}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {k}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<{w}$
81 breq2 ${⊢}{w}=\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\to \left(\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<{w}↔\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\right)$
82 81 rexralbidv ${⊢}{w}=\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\to \left(\exists {k}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<{w}↔\exists {k}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\right)$
83 82 rspcva ${⊢}\left(\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\in {ℝ}^{+}\wedge \forall {w}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {k}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<{w}\right)\to \exists {k}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}$
84 76 80 83 syl2anc ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \exists {k}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}$
85 rabn0 ${⊢}\left\{{k}\in {ℤ}_{\ge {M}}|\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\right\}\ne \varnothing ↔\exists {k}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}$
86 84 85 sylibr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left\{{k}\in {ℤ}_{\ge {M}}|\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\right\}\ne \varnothing$
87 infssuzcl ${⊢}\left(\left\{{k}\in {ℤ}_{\ge {M}}|\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\right\}\subseteq {ℤ}_{\ge {M}}\wedge \left\{{k}\in {ℤ}_{\ge {M}}|\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\right\}\ne \varnothing \right)\to sup\left(\left\{{k}\in {ℤ}_{\ge {M}}|\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\right\},ℝ,<\right)\in \left\{{k}\in {ℤ}_{\ge {M}}|\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\right\}$
88 19 86 87 sylancr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to sup\left(\left\{{k}\in {ℤ}_{\ge {M}}|\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\right\},ℝ,<\right)\in \left\{{k}\in {ℤ}_{\ge {M}}|\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\right\}$
89 11 88 eqeltrid ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {K}\in \left\{{k}\in {ℤ}_{\ge {M}}|\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\right\}$
90 19 89 sseldi ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {K}\in {ℤ}_{\ge {M}}$
91 2fveq3 ${⊢}{j}={i}\to {F}\left({R}\left({j}\right)\right)={F}\left({R}\left({i}\right)\right)$
92 uzss ${⊢}{K}\in {ℤ}_{\ge {M}}\to {ℤ}_{\ge {K}}\subseteq {ℤ}_{\ge {M}}$
93 90 92 syl ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {ℤ}_{\ge {K}}\subseteq {ℤ}_{\ge {M}}$
94 93 sselda ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to {i}\in {ℤ}_{\ge {M}}$
95 14 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to {F}:\left({A},{B}\right)⟶ℝ$
96 8 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to {R}:{ℤ}_{\ge {M}}⟶\left({A},{B}\right)$
97 96 94 ffvelrnd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to {R}\left({i}\right)\in \left({A},{B}\right)$
98 95 97 ffvelrnd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to {F}\left({R}\left({i}\right)\right)\in ℝ$
99 9 91 94 98 fvmptd3 ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to {S}\left({i}\right)={F}\left({R}\left({i}\right)\right)$
100 2fveq3 ${⊢}{j}={K}\to {F}\left({R}\left({j}\right)\right)={F}\left({R}\left({K}\right)\right)$
101 90 adantr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to {K}\in {ℤ}_{\ge {M}}$
102 96 101 ffvelrnd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to {R}\left({K}\right)\in \left({A},{B}\right)$
103 95 102 ffvelrnd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to {F}\left({R}\left({K}\right)\right)\in ℝ$
104 9 100 101 103 fvmptd3 ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to {S}\left({K}\right)={F}\left({R}\left({K}\right)\right)$
105 99 104 oveq12d ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to {S}\left({i}\right)-{S}\left({K}\right)={F}\left({R}\left({i}\right)\right)-{F}\left({R}\left({K}\right)\right)$
106 105 fveq2d ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to \left|{S}\left({i}\right)-{S}\left({K}\right)\right|=\left|{F}\left({R}\left({i}\right)\right)-{F}\left({R}\left({K}\right)\right)\right|$
107 98 recnd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to {F}\left({R}\left({i}\right)\right)\in ℂ$
108 103 recnd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to {F}\left({R}\left({K}\right)\right)\in ℂ$
109 107 108 subcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to {F}\left({R}\left({i}\right)\right)-{F}\left({R}\left({K}\right)\right)\in ℂ$
110 109 abscld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to \left|{F}\left({R}\left({i}\right)\right)-{F}\left({R}\left({K}\right)\right)\right|\in ℝ$
111 110 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to \left|{F}\left({R}\left({i}\right)\right)-{F}\left({R}\left({K}\right)\right)\right|\in ℝ$
112 44 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)\in ℝ$
113 112 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)\in ℝ$
114 8 adantr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {R}:{ℤ}_{\ge {M}}⟶\left({A},{B}\right)$
115 114 90 ffvelrnd ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {R}\left({K}\right)\in \left({A},{B}\right)$
116 29 115 sseldi ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {R}\left({K}\right)\in ℝ$
117 116 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to {R}\left({K}\right)\in ℝ$
118 29 97 sseldi ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to {R}\left({i}\right)\in ℝ$
119 118 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to {R}\left({i}\right)\in ℝ$
120 117 119 resubcld ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to {R}\left({K}\right)-{R}\left({i}\right)\in ℝ$
121 113 120 remulcld ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)\left({R}\left({K}\right)-{R}\left({i}\right)\right)\in ℝ$
122 20 ad3antlr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to {x}\in ℝ$
123 107 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to {F}\left({R}\left({i}\right)\right)\in ℂ$
124 108 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to {F}\left({R}\left({K}\right)\right)\in ℂ$
125 123 124 abssubd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to \left|{F}\left({R}\left({i}\right)\right)-{F}\left({R}\left({K}\right)\right)\right|=\left|{F}\left({R}\left({K}\right)\right)-{F}\left({R}\left({i}\right)\right)\right|$
126 1 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to {A}\in ℝ$
127 2 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to {B}\in ℝ$
128 95 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to {F}:\left({A},{B}\right)⟶ℝ$
129 5 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to \mathrm{dom}{{F}}_{ℝ}^{\prime }=\left({A},{B}\right)$
130 61 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to \forall {y}\in \left({A},{B}\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({y}\right)\right|\le sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)$
131 97 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to {R}\left({i}\right)\in \left({A},{B}\right)$
132 118 rexrd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to {R}\left({i}\right)\in {ℝ}^{*}$
133 132 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to {R}\left({i}\right)\in {ℝ}^{*}$
134 2 rexrd ${⊢}{\phi }\to {B}\in {ℝ}^{*}$
135 134 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to {B}\in {ℝ}^{*}$
136 135 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to {B}\in {ℝ}^{*}$
137 simpr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to {R}\left({i}\right)<{R}\left({K}\right)$
138 1 rexrd ${⊢}{\phi }\to {A}\in {ℝ}^{*}$
139 138 adantr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {A}\in {ℝ}^{*}$
140 134 adantr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {B}\in {ℝ}^{*}$
141 iooltub ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {R}\left({K}\right)\in \left({A},{B}\right)\right)\to {R}\left({K}\right)<{B}$
142 139 140 115 141 syl3anc ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {R}\left({K}\right)<{B}$
143 142 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to {R}\left({K}\right)<{B}$
144 133 136 117 137 143 eliood ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to {R}\left({K}\right)\in \left({R}\left({i}\right),{B}\right)$
145 126 127 128 129 113 130 131 144 dvbdfbdioolem1 ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to \left(\left|{F}\left({R}\left({K}\right)\right)-{F}\left({R}\left({i}\right)\right)\right|\le sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)\left({R}\left({K}\right)-{R}\left({i}\right)\right)\wedge \left|{F}\left({R}\left({K}\right)\right)-{F}\left({R}\left({i}\right)\right)\right|\le sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)\left({B}-{A}\right)\right)$
146 145 simpld ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to \left|{F}\left({R}\left({K}\right)\right)-{F}\left({R}\left({i}\right)\right)\right|\le sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)\left({R}\left({K}\right)-{R}\left({i}\right)\right)$
147 125 146 eqbrtrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to \left|{F}\left({R}\left({i}\right)\right)-{F}\left({R}\left({K}\right)\right)\right|\le sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)\left({R}\left({K}\right)-{R}\left({i}\right)\right)$
148 113 46 syl ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1\in ℝ$
149 148 120 remulcld ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to \left(sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1\right)\left({R}\left({K}\right)-{R}\left({i}\right)\right)\in ℝ$
150 119 117 posdifd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to \left({R}\left({i}\right)<{R}\left({K}\right)↔0<{R}\left({K}\right)-{R}\left({i}\right)\right)$
151 137 150 mpbid ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to 0<{R}\left({K}\right)-{R}\left({i}\right)$
152 120 151 elrpd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to {R}\left({K}\right)-{R}\left({i}\right)\in {ℝ}^{+}$
153 113 ltp1d ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)
154 113 148 152 153 ltmul1dd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)\left({R}\left({K}\right)-{R}\left({i}\right)\right)<\left(sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1\right)\left({R}\left({K}\right)-{R}\left({i}\right)\right)$
155 29 102 sseldi ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to {R}\left({K}\right)\in ℝ$
156 118 155 resubcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to {R}\left({i}\right)-{R}\left({K}\right)\in ℝ$
157 156 recnd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to {R}\left({i}\right)-{R}\left({K}\right)\in ℂ$
158 157 abscld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to \left|{R}\left({i}\right)-{R}\left({K}\right)\right|\in ℝ$
159 158 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to \left|{R}\left({i}\right)-{R}\left({K}\right)\right|\in ℝ$
160 71 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to \frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\in ℝ$
161 120 leabsd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to {R}\left({K}\right)-{R}\left({i}\right)\le \left|{R}\left({K}\right)-{R}\left({i}\right)\right|$
162 117 recnd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to {R}\left({K}\right)\in ℂ$
163 118 recnd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to {R}\left({i}\right)\in ℂ$
164 163 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to {R}\left({i}\right)\in ℂ$
165 162 164 abssubd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to \left|{R}\left({K}\right)-{R}\left({i}\right)\right|=\left|{R}\left({i}\right)-{R}\left({K}\right)\right|$
166 161 165 breqtrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to {R}\left({K}\right)-{R}\left({i}\right)\le \left|{R}\left({i}\right)-{R}\left({K}\right)\right|$
167 fveq2 ${⊢}{k}={K}\to {ℤ}_{\ge {k}}={ℤ}_{\ge {K}}$
168 fveq2 ${⊢}{k}={K}\to {R}\left({k}\right)={R}\left({K}\right)$
169 168 oveq2d ${⊢}{k}={K}\to {R}\left({i}\right)-{R}\left({k}\right)={R}\left({i}\right)-{R}\left({K}\right)$
170 169 fveq2d ${⊢}{k}={K}\to \left|{R}\left({i}\right)-{R}\left({k}\right)\right|=\left|{R}\left({i}\right)-{R}\left({K}\right)\right|$
171 170 breq1d ${⊢}{k}={K}\to \left(\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}↔\left|{R}\left({i}\right)-{R}\left({K}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\right)$
172 167 171 raleqbidv ${⊢}{k}={K}\to \left(\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}↔\forall {i}\in {ℤ}_{\ge {K}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({K}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\right)$
173 172 elrab ${⊢}{K}\in \left\{{k}\in {ℤ}_{\ge {M}}|\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({k}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\right\}↔\left({K}\in {ℤ}_{\ge {M}}\wedge \forall {i}\in {ℤ}_{\ge {K}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({K}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\right)$
174 89 173 sylib ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left({K}\in {ℤ}_{\ge {M}}\wedge \forall {i}\in {ℤ}_{\ge {K}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({K}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\right)$
175 174 simprd ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \forall {i}\in {ℤ}_{\ge {K}}\phantom{\rule{.4em}{0ex}}\left|{R}\left({i}\right)-{R}\left({K}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}$
176 175 r19.21bi ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to \left|{R}\left({i}\right)-{R}\left({K}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}$
177 176 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to \left|{R}\left({i}\right)-{R}\left({K}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}$
178 120 159 160 166 177 lelttrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to {R}\left({K}\right)-{R}\left({i}\right)<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}$
179 51 68 elrpd ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1\in {ℝ}^{+}$
180 179 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1\in {ℝ}^{+}$
181 120 122 180 ltmuldiv2d ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to \left(\left(sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1\right)\left({R}\left({K}\right)-{R}\left({i}\right)\right)<{x}↔{R}\left({K}\right)-{R}\left({i}\right)<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\right)$
182 178 181 mpbird ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to \left(sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1\right)\left({R}\left({K}\right)-{R}\left({i}\right)\right)<{x}$
183 121 149 122 154 182 lttrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)\left({R}\left({K}\right)-{R}\left({i}\right)\right)<{x}$
184 111 121 122 147 183 lelttrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)<{R}\left({K}\right)\right)\to \left|{F}\left({R}\left({i}\right)\right)-{F}\left({R}\left({K}\right)\right)\right|<{x}$
185 fveq2 ${⊢}{R}\left({i}\right)={R}\left({K}\right)\to {F}\left({R}\left({i}\right)\right)={F}\left({R}\left({K}\right)\right)$
186 185 oveq1d ${⊢}{R}\left({i}\right)={R}\left({K}\right)\to {F}\left({R}\left({i}\right)\right)-{F}\left({R}\left({K}\right)\right)={F}\left({R}\left({K}\right)\right)-{F}\left({R}\left({K}\right)\right)$
187 108 subidd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to {F}\left({R}\left({K}\right)\right)-{F}\left({R}\left({K}\right)\right)=0$
188 186 187 sylan9eqr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)={R}\left({K}\right)\right)\to {F}\left({R}\left({i}\right)\right)-{F}\left({R}\left({K}\right)\right)=0$
189 188 abs00bd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)={R}\left({K}\right)\right)\to \left|{F}\left({R}\left({i}\right)\right)-{F}\left({R}\left({K}\right)\right)\right|=0$
190 72 ad3antlr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)={R}\left({K}\right)\right)\to 0<{x}$
191 189 190 eqbrtrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({i}\right)={R}\left({K}\right)\right)\to \left|{F}\left({R}\left({i}\right)\right)-{F}\left({R}\left({K}\right)\right)\right|<{x}$
192 191 adantlr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge ¬{R}\left({i}\right)<{R}\left({K}\right)\right)\wedge {R}\left({i}\right)={R}\left({K}\right)\right)\to \left|{F}\left({R}\left({i}\right)\right)-{F}\left({R}\left({K}\right)\right)\right|<{x}$
193 simpll ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge ¬{R}\left({i}\right)<{R}\left({K}\right)\right)\wedge ¬{R}\left({i}\right)={R}\left({K}\right)\right)\to \left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)$
194 155 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge ¬{R}\left({i}\right)<{R}\left({K}\right)\right)\wedge ¬{R}\left({i}\right)={R}\left({K}\right)\right)\to {R}\left({K}\right)\in ℝ$
195 118 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge ¬{R}\left({i}\right)<{R}\left({K}\right)\right)\wedge ¬{R}\left({i}\right)={R}\left({K}\right)\right)\to {R}\left({i}\right)\in ℝ$
196 id ${⊢}{R}\left({K}\right)={R}\left({i}\right)\to {R}\left({K}\right)={R}\left({i}\right)$
197 196 eqcomd ${⊢}{R}\left({K}\right)={R}\left({i}\right)\to {R}\left({i}\right)={R}\left({K}\right)$
198 197 necon3bi ${⊢}¬{R}\left({i}\right)={R}\left({K}\right)\to {R}\left({K}\right)\ne {R}\left({i}\right)$
199 198 adantl ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge ¬{R}\left({i}\right)<{R}\left({K}\right)\right)\wedge ¬{R}\left({i}\right)={R}\left({K}\right)\right)\to {R}\left({K}\right)\ne {R}\left({i}\right)$
200 simplr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge ¬{R}\left({i}\right)<{R}\left({K}\right)\right)\wedge ¬{R}\left({i}\right)={R}\left({K}\right)\right)\to ¬{R}\left({i}\right)<{R}\left({K}\right)$
201 194 195 199 200 lttri5d ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge ¬{R}\left({i}\right)<{R}\left({K}\right)\right)\wedge ¬{R}\left({i}\right)={R}\left({K}\right)\right)\to {R}\left({K}\right)<{R}\left({i}\right)$
202 110 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to \left|{F}\left({R}\left({i}\right)\right)-{F}\left({R}\left({K}\right)\right)\right|\in ℝ$
203 112 156 remulcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)\left({R}\left({i}\right)-{R}\left({K}\right)\right)\in ℝ$
204 203 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)\left({R}\left({i}\right)-{R}\left({K}\right)\right)\in ℝ$
205 20 ad3antlr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to {x}\in ℝ$
206 1 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to {A}\in ℝ$
207 2 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to {B}\in ℝ$
208 95 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to {F}:\left({A},{B}\right)⟶ℝ$
209 5 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to \mathrm{dom}{{F}}_{ℝ}^{\prime }=\left({A},{B}\right)$
210 44 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)\in ℝ$
211 61 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to \forall {y}\in \left({A},{B}\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({y}\right)\right|\le sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)$
212 102 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to {R}\left({K}\right)\in \left({A},{B}\right)$
213 116 rexrd ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {R}\left({K}\right)\in {ℝ}^{*}$
214 213 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to {R}\left({K}\right)\in {ℝ}^{*}$
215 207 rexrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to {B}\in {ℝ}^{*}$
216 118 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to {R}\left({i}\right)\in ℝ$
217 simpr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to {R}\left({K}\right)<{R}\left({i}\right)$
218 138 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to {A}\in {ℝ}^{*}$
219 iooltub ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {R}\left({i}\right)\in \left({A},{B}\right)\right)\to {R}\left({i}\right)<{B}$
220 218 135 97 219 syl3anc ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to {R}\left({i}\right)<{B}$
221 220 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to {R}\left({i}\right)<{B}$
222 214 215 216 217 221 eliood ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to {R}\left({i}\right)\in \left({R}\left({K}\right),{B}\right)$
223 206 207 208 209 210 211 212 222 dvbdfbdioolem1 ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to \left(\left|{F}\left({R}\left({i}\right)\right)-{F}\left({R}\left({K}\right)\right)\right|\le sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)\left({R}\left({i}\right)-{R}\left({K}\right)\right)\wedge \left|{F}\left({R}\left({i}\right)\right)-{F}\left({R}\left({K}\right)\right)\right|\le sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)\left({B}-{A}\right)\right)$
224 223 simpld ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to \left|{F}\left({R}\left({i}\right)\right)-{F}\left({R}\left({K}\right)\right)\right|\le sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)\left({R}\left({i}\right)-{R}\left({K}\right)\right)$
225 1red ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to 1\in ℝ$
226 210 225 readdcld ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1\in ℝ$
227 155 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to {R}\left({K}\right)\in ℝ$
228 216 227 resubcld ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to {R}\left({i}\right)-{R}\left({K}\right)\in ℝ$
229 226 228 remulcld ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to \left(sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1\right)\left({R}\left({i}\right)-{R}\left({K}\right)\right)\in ℝ$
230 210 46 syl ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1\in ℝ$
231 227 216 posdifd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to \left({R}\left({K}\right)<{R}\left({i}\right)↔0<{R}\left({i}\right)-{R}\left({K}\right)\right)$
232 217 231 mpbid ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to 0<{R}\left({i}\right)-{R}\left({K}\right)$
233 228 232 elrpd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to {R}\left({i}\right)-{R}\left({K}\right)\in {ℝ}^{+}$
234 210 ltp1d ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)
235 210 230 233 234 ltmul1dd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)\left({R}\left({i}\right)-{R}\left({K}\right)\right)<\left(sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1\right)\left({R}\left({i}\right)-{R}\left({K}\right)\right)$
236 158 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to \left|{R}\left({i}\right)-{R}\left({K}\right)\right|\in ℝ$
237 71 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to \frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\in ℝ$
238 228 leabsd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to {R}\left({i}\right)-{R}\left({K}\right)\le \left|{R}\left({i}\right)-{R}\left({K}\right)\right|$
239 176 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to \left|{R}\left({i}\right)-{R}\left({K}\right)\right|<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}$
240 228 236 237 238 239 lelttrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to {R}\left({i}\right)-{R}\left({K}\right)<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}$
241 179 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1\in {ℝ}^{+}$
242 228 205 241 ltmuldiv2d ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to \left(\left(sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1\right)\left({R}\left({i}\right)-{R}\left({K}\right)\right)<{x}↔{R}\left({i}\right)-{R}\left({K}\right)<\frac{{x}}{sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1}\right)$
243 240 242 mpbird ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to \left(sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)+1\right)\left({R}\left({i}\right)-{R}\left({K}\right)\right)<{x}$
244 204 229 205 235 243 lttrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to sup\left(\mathrm{ran}\left({z}\in \left({A},{B}\right)⟼\left|{{F}}_{ℝ}^{\prime }\left({z}\right)\right|\right),ℝ,<\right)\left({R}\left({i}\right)-{R}\left({K}\right)\right)<{x}$
245 202 204 205 224 244 lelttrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge {R}\left({K}\right)<{R}\left({i}\right)\right)\to \left|{F}\left({R}\left({i}\right)\right)-{F}\left({R}\left({K}\right)\right)\right|<{x}$
246 193 201 245 syl2anc ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge ¬{R}\left({i}\right)<{R}\left({K}\right)\right)\wedge ¬{R}\left({i}\right)={R}\left({K}\right)\right)\to \left|{F}\left({R}\left({i}\right)\right)-{F}\left({R}\left({K}\right)\right)\right|<{x}$
247 192 246 pm2.61dan ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\wedge ¬{R}\left({i}\right)<{R}\left({K}\right)\right)\to \left|{F}\left({R}\left({i}\right)\right)-{F}\left({R}\left({K}\right)\right)\right|<{x}$
248 184 247 pm2.61dan ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to \left|{F}\left({R}\left({i}\right)\right)-{F}\left({R}\left({K}\right)\right)\right|<{x}$
249 106 248 eqbrtrd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {i}\in {ℤ}_{\ge {K}}\right)\to \left|{S}\left({i}\right)-{S}\left({K}\right)\right|<{x}$
250 249 ralrimiva ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \forall {i}\in {ℤ}_{\ge {K}}\phantom{\rule{.4em}{0ex}}\left|{S}\left({i}\right)-{S}\left({K}\right)\right|<{x}$
251 fveq2 ${⊢}{k}={K}\to {S}\left({k}\right)={S}\left({K}\right)$
252 251 oveq2d ${⊢}{k}={K}\to {S}\left({i}\right)-{S}\left({k}\right)={S}\left({i}\right)-{S}\left({K}\right)$
253 252 fveq2d ${⊢}{k}={K}\to \left|{S}\left({i}\right)-{S}\left({k}\right)\right|=\left|{S}\left({i}\right)-{S}\left({K}\right)\right|$
254 253 breq1d ${⊢}{k}={K}\to \left(\left|{S}\left({i}\right)-{S}\left({k}\right)\right|<{x}↔\left|{S}\left({i}\right)-{S}\left({K}\right)\right|<{x}\right)$
255 167 254 raleqbidv ${⊢}{k}={K}\to \left(\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{S}\left({i}\right)-{S}\left({k}\right)\right|<{x}↔\forall {i}\in {ℤ}_{\ge {K}}\phantom{\rule{.4em}{0ex}}\left|{S}\left({i}\right)-{S}\left({K}\right)\right|<{x}\right)$
256 255 rspcev ${⊢}\left({K}\in {ℤ}_{\ge {M}}\wedge \forall {i}\in {ℤ}_{\ge {K}}\phantom{\rule{.4em}{0ex}}\left|{S}\left({i}\right)-{S}\left({K}\right)\right|<{x}\right)\to \exists {k}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{S}\left({i}\right)-{S}\left({k}\right)\right|<{x}$
257 90 250 256 syl2anc ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \exists {k}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{S}\left({i}\right)-{S}\left({k}\right)\right|<{x}$
258 257 ralrimiva ${⊢}{\phi }\to \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {k}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}\forall {i}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\left|{S}\left({i}\right)-{S}\left({k}\right)\right|<{x}$
259 12 18 258 caurcvg ${⊢}{\phi }\to {S}⇝\mathrm{lim sup}\left({S}\right)$