# Metamath Proof Explorer

## Theorem ftc1a

Description: The Fundamental Theorem of Calculus, part one. The function G formed by varying the right endpoint of an integral of F is continuous if F is integrable. (Contributed by Mario Carneiro, 1-Sep-2014)

Ref Expression
Hypotheses ftc1.g ${⊢}{G}=\left({x}\in \left[{A},{B}\right]⟼{\int }_{\left({A},{x}\right)}{F}\left({t}\right)d{t}\right)$
ftc1.a ${⊢}{\phi }\to {A}\in ℝ$
ftc1.b ${⊢}{\phi }\to {B}\in ℝ$
ftc1.le ${⊢}{\phi }\to {A}\le {B}$
ftc1.s ${⊢}{\phi }\to \left({A},{B}\right)\subseteq {D}$
ftc1.d ${⊢}{\phi }\to {D}\subseteq ℝ$
ftc1.i ${⊢}{\phi }\to {F}\in {𝐿}^{1}$
ftc1a.f ${⊢}{\phi }\to {F}:{D}⟶ℂ$
Assertion ftc1a ${⊢}{\phi }\to {G}:\left[{A},{B}\right]\underset{cn}{⟶}ℂ$

### Proof

Step Hyp Ref Expression
1 ftc1.g ${⊢}{G}=\left({x}\in \left[{A},{B}\right]⟼{\int }_{\left({A},{x}\right)}{F}\left({t}\right)d{t}\right)$
2 ftc1.a ${⊢}{\phi }\to {A}\in ℝ$
3 ftc1.b ${⊢}{\phi }\to {B}\in ℝ$
4 ftc1.le ${⊢}{\phi }\to {A}\le {B}$
5 ftc1.s ${⊢}{\phi }\to \left({A},{B}\right)\subseteq {D}$
6 ftc1.d ${⊢}{\phi }\to {D}\subseteq ℝ$
7 ftc1.i ${⊢}{\phi }\to {F}\in {𝐿}^{1}$
8 ftc1a.f ${⊢}{\phi }\to {F}:{D}⟶ℂ$
9 1 2 3 4 5 6 7 8 ftc1lem2 ${⊢}{\phi }\to {G}:\left[{A},{B}\right]⟶ℂ$
10 fvexd ${⊢}\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {w}\in {D}\right)\to {F}\left({w}\right)\in \mathrm{V}$
11 8 feqmptd ${⊢}{\phi }\to {F}=\left({w}\in {D}⟼{F}\left({w}\right)\right)$
12 11 7 eqeltrrd ${⊢}{\phi }\to \left({w}\in {D}⟼{F}\left({w}\right)\right)\in {𝐿}^{1}$
13 12 adantr ${⊢}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\to \left({w}\in {D}⟼{F}\left({w}\right)\right)\in {𝐿}^{1}$
14 simpr ${⊢}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\to {e}\in {ℝ}^{+}$
15 10 13 14 itgcn ${⊢}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)$
16 oveq12 ${⊢}\left({s}={z}\wedge {r}={y}\right)\to {s}-{r}={z}-{y}$
17 16 fveq2d ${⊢}\left({s}={z}\wedge {r}={y}\right)\to \left|{s}-{r}\right|=\left|{z}-{y}\right|$
18 17 breq1d ${⊢}\left({s}={z}\wedge {r}={y}\right)\to \left(\left|{s}-{r}\right|<{d}↔\left|{z}-{y}\right|<{d}\right)$
19 fveq2 ${⊢}{s}={z}\to {G}\left({s}\right)={G}\left({z}\right)$
20 fveq2 ${⊢}{r}={y}\to {G}\left({r}\right)={G}\left({y}\right)$
21 19 20 oveqan12d ${⊢}\left({s}={z}\wedge {r}={y}\right)\to {G}\left({s}\right)-{G}\left({r}\right)={G}\left({z}\right)-{G}\left({y}\right)$
22 21 fveq2d ${⊢}\left({s}={z}\wedge {r}={y}\right)\to \left|{G}\left({s}\right)-{G}\left({r}\right)\right|=\left|{G}\left({z}\right)-{G}\left({y}\right)\right|$
23 22 breq1d ${⊢}\left({s}={z}\wedge {r}={y}\right)\to \left(\left|{G}\left({s}\right)-{G}\left({r}\right)\right|<{e}↔\left|{G}\left({z}\right)-{G}\left({y}\right)\right|<{e}\right)$
24 18 23 imbi12d ${⊢}\left({s}={z}\wedge {r}={y}\right)\to \left(\left(\left|{s}-{r}\right|<{d}\to \left|{G}\left({s}\right)-{G}\left({r}\right)\right|<{e}\right)↔\left(\left|{z}-{y}\right|<{d}\to \left|{G}\left({z}\right)-{G}\left({y}\right)\right|<{e}\right)\right)$
25 24 ancoms ${⊢}\left({r}={y}\wedge {s}={z}\right)\to \left(\left(\left|{s}-{r}\right|<{d}\to \left|{G}\left({s}\right)-{G}\left({r}\right)\right|<{e}\right)↔\left(\left|{z}-{y}\right|<{d}\to \left|{G}\left({z}\right)-{G}\left({y}\right)\right|<{e}\right)\right)$
26 oveq12 ${⊢}\left({s}={y}\wedge {r}={z}\right)\to {s}-{r}={y}-{z}$
27 26 fveq2d ${⊢}\left({s}={y}\wedge {r}={z}\right)\to \left|{s}-{r}\right|=\left|{y}-{z}\right|$
28 27 breq1d ${⊢}\left({s}={y}\wedge {r}={z}\right)\to \left(\left|{s}-{r}\right|<{d}↔\left|{y}-{z}\right|<{d}\right)$
29 fveq2 ${⊢}{s}={y}\to {G}\left({s}\right)={G}\left({y}\right)$
30 fveq2 ${⊢}{r}={z}\to {G}\left({r}\right)={G}\left({z}\right)$
31 29 30 oveqan12d ${⊢}\left({s}={y}\wedge {r}={z}\right)\to {G}\left({s}\right)-{G}\left({r}\right)={G}\left({y}\right)-{G}\left({z}\right)$
32 31 fveq2d ${⊢}\left({s}={y}\wedge {r}={z}\right)\to \left|{G}\left({s}\right)-{G}\left({r}\right)\right|=\left|{G}\left({y}\right)-{G}\left({z}\right)\right|$
33 32 breq1d ${⊢}\left({s}={y}\wedge {r}={z}\right)\to \left(\left|{G}\left({s}\right)-{G}\left({r}\right)\right|<{e}↔\left|{G}\left({y}\right)-{G}\left({z}\right)\right|<{e}\right)$
34 28 33 imbi12d ${⊢}\left({s}={y}\wedge {r}={z}\right)\to \left(\left(\left|{s}-{r}\right|<{d}\to \left|{G}\left({s}\right)-{G}\left({r}\right)\right|<{e}\right)↔\left(\left|{y}-{z}\right|<{d}\to \left|{G}\left({y}\right)-{G}\left({z}\right)\right|<{e}\right)\right)$
35 34 ancoms ${⊢}\left({r}={z}\wedge {s}={y}\right)\to \left(\left(\left|{s}-{r}\right|<{d}\to \left|{G}\left({s}\right)-{G}\left({r}\right)\right|<{e}\right)↔\left(\left|{y}-{z}\right|<{d}\to \left|{G}\left({y}\right)-{G}\left({z}\right)\right|<{e}\right)\right)$
36 iccssre ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left[{A},{B}\right]\subseteq ℝ$
37 2 3 36 syl2anc ${⊢}{\phi }\to \left[{A},{B}\right]\subseteq ℝ$
38 37 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\to \left[{A},{B}\right]\subseteq ℝ$
39 37 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\right)\right)\to \left[{A},{B}\right]\subseteq ℝ$
40 simprr ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\right)\right)\to {z}\in \left[{A},{B}\right]$
41 39 40 sseldd ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\right)\right)\to {z}\in ℝ$
42 41 recnd ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\right)\right)\to {z}\in ℂ$
43 simprl ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\right)\right)\to {y}\in \left[{A},{B}\right]$
44 39 43 sseldd ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\right)\right)\to {y}\in ℝ$
45 44 recnd ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\right)\right)\to {y}\in ℂ$
46 42 45 abssubd ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\right)\right)\to \left|{z}-{y}\right|=\left|{y}-{z}\right|$
47 46 breq1d ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\right)\right)\to \left(\left|{z}-{y}\right|<{d}↔\left|{y}-{z}\right|<{d}\right)$
48 9 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\right)\right)\to {G}:\left[{A},{B}\right]⟶ℂ$
49 48 40 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\right)\right)\to {G}\left({z}\right)\in ℂ$
50 48 43 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\right)\right)\to {G}\left({y}\right)\in ℂ$
51 49 50 abssubd ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\right)\right)\to \left|{G}\left({z}\right)-{G}\left({y}\right)\right|=\left|{G}\left({y}\right)-{G}\left({z}\right)\right|$
52 51 breq1d ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\right)\right)\to \left(\left|{G}\left({z}\right)-{G}\left({y}\right)\right|<{e}↔\left|{G}\left({y}\right)-{G}\left({z}\right)\right|<{e}\right)$
53 47 52 imbi12d ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\right)\right)\to \left(\left(\left|{z}-{y}\right|<{d}\to \left|{G}\left({z}\right)-{G}\left({y}\right)\right|<{e}\right)↔\left(\left|{y}-{z}\right|<{d}\to \left|{G}\left({y}\right)-{G}\left({z}\right)\right|<{e}\right)\right)$
54 simpr3 ${⊢}\left({\phi }\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\right)\to {y}\le {z}$
55 2 adantr ${⊢}\left({\phi }\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\right)\to {A}\in ℝ$
56 3 adantr ${⊢}\left({\phi }\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\right)\to {B}\in ℝ$
57 4 adantr ${⊢}\left({\phi }\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\right)\to {A}\le {B}$
58 5 adantr ${⊢}\left({\phi }\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\right)\to \left({A},{B}\right)\subseteq {D}$
59 6 adantr ${⊢}\left({\phi }\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\right)\to {D}\subseteq ℝ$
60 7 adantr ${⊢}\left({\phi }\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\right)\to {F}\in {𝐿}^{1}$
61 8 adantr ${⊢}\left({\phi }\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\right)\to {F}:{D}⟶ℂ$
62 simpr1 ${⊢}\left({\phi }\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\right)\to {y}\in \left[{A},{B}\right]$
63 simpr2 ${⊢}\left({\phi }\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\right)\to {z}\in \left[{A},{B}\right]$
64 1 55 56 57 58 59 60 61 62 63 ftc1lem1 ${⊢}\left(\left({\phi }\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\right)\wedge {y}\le {z}\right)\to {G}\left({z}\right)-{G}\left({y}\right)={\int }_{\left({y},{z}\right)}{F}\left({t}\right)d{t}$
65 54 64 mpdan ${⊢}\left({\phi }\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\right)\to {G}\left({z}\right)-{G}\left({y}\right)={\int }_{\left({y},{z}\right)}{F}\left({t}\right)d{t}$
66 65 adantlr ${⊢}\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\right)\to {G}\left({z}\right)-{G}\left({y}\right)={\int }_{\left({y},{z}\right)}{F}\left({t}\right)d{t}$
67 66 ad2ant2r ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {G}\left({z}\right)-{G}\left({y}\right)={\int }_{\left({y},{z}\right)}{F}\left({t}\right)d{t}$
68 67 fveq2d ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to \left|{G}\left({z}\right)-{G}\left({y}\right)\right|=\left|{\int }_{\left({y},{z}\right)}{F}\left({t}\right)d{t}\right|$
69 fvexd ${⊢}\left(\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\wedge {t}\in \left({y},{z}\right)\right)\to {F}\left({t}\right)\in \mathrm{V}$
70 2 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {A}\in ℝ$
71 70 rexrd ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {A}\in {ℝ}^{*}$
72 simprl1 ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {y}\in \left[{A},{B}\right]$
73 3 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {B}\in ℝ$
74 elicc2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({y}\in \left[{A},{B}\right]↔\left({y}\in ℝ\wedge {A}\le {y}\wedge {y}\le {B}\right)\right)$
75 70 73 74 syl2anc ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to \left({y}\in \left[{A},{B}\right]↔\left({y}\in ℝ\wedge {A}\le {y}\wedge {y}\le {B}\right)\right)$
76 72 75 mpbid ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to \left({y}\in ℝ\wedge {A}\le {y}\wedge {y}\le {B}\right)$
77 76 simp2d ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {A}\le {y}$
78 iooss1 ${⊢}\left({A}\in {ℝ}^{*}\wedge {A}\le {y}\right)\to \left({y},{z}\right)\subseteq \left({A},{z}\right)$
79 71 77 78 syl2anc ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to \left({y},{z}\right)\subseteq \left({A},{z}\right)$
80 73 rexrd ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {B}\in {ℝ}^{*}$
81 simprl2 ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {z}\in \left[{A},{B}\right]$
82 elicc2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({z}\in \left[{A},{B}\right]↔\left({z}\in ℝ\wedge {A}\le {z}\wedge {z}\le {B}\right)\right)$
83 70 73 82 syl2anc ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to \left({z}\in \left[{A},{B}\right]↔\left({z}\in ℝ\wedge {A}\le {z}\wedge {z}\le {B}\right)\right)$
84 81 83 mpbid ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to \left({z}\in ℝ\wedge {A}\le {z}\wedge {z}\le {B}\right)$
85 84 simp3d ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {z}\le {B}$
86 iooss2 ${⊢}\left({B}\in {ℝ}^{*}\wedge {z}\le {B}\right)\to \left({A},{z}\right)\subseteq \left({A},{B}\right)$
87 80 85 86 syl2anc ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to \left({A},{z}\right)\subseteq \left({A},{B}\right)$
88 79 87 sstrd ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to \left({y},{z}\right)\subseteq \left({A},{B}\right)$
89 5 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to \left({A},{B}\right)\subseteq {D}$
90 88 89 sstrd ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to \left({y},{z}\right)\subseteq {D}$
91 ioombl ${⊢}\left({y},{z}\right)\in \mathrm{dom}vol$
92 91 a1i ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to \left({y},{z}\right)\in \mathrm{dom}vol$
93 fvexd ${⊢}\left(\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\wedge {t}\in {D}\right)\to {F}\left({t}\right)\in \mathrm{V}$
94 8 feqmptd ${⊢}{\phi }\to {F}=\left({t}\in {D}⟼{F}\left({t}\right)\right)$
95 94 7 eqeltrrd ${⊢}{\phi }\to \left({t}\in {D}⟼{F}\left({t}\right)\right)\in {𝐿}^{1}$
96 95 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to \left({t}\in {D}⟼{F}\left({t}\right)\right)\in {𝐿}^{1}$
97 90 92 93 96 iblss ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to \left({t}\in \left({y},{z}\right)⟼{F}\left({t}\right)\right)\in {𝐿}^{1}$
98 69 97 itgcl ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {\int }_{\left({y},{z}\right)}{F}\left({t}\right)d{t}\in ℂ$
99 98 abscld ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to \left|{\int }_{\left({y},{z}\right)}{F}\left({t}\right)d{t}\right|\in ℝ$
100 iblmbf ${⊢}\left({t}\in \left({y},{z}\right)⟼{F}\left({t}\right)\right)\in {𝐿}^{1}\to \left({t}\in \left({y},{z}\right)⟼{F}\left({t}\right)\right)\in MblFn$
101 97 100 syl ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to \left({t}\in \left({y},{z}\right)⟼{F}\left({t}\right)\right)\in MblFn$
102 101 69 mbfmptcl ${⊢}\left(\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\wedge {t}\in \left({y},{z}\right)\right)\to {F}\left({t}\right)\in ℂ$
103 102 abscld ${⊢}\left(\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\wedge {t}\in \left({y},{z}\right)\right)\to \left|{F}\left({t}\right)\right|\in ℝ$
104 69 97 iblabs ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to \left({t}\in \left({y},{z}\right)⟼\left|{F}\left({t}\right)\right|\right)\in {𝐿}^{1}$
105 103 104 itgrecl ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {\int }_{\left({y},{z}\right)}\left|{F}\left({t}\right)\right|d{t}\in ℝ$
106 simprl ${⊢}\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\to {e}\in {ℝ}^{+}$
107 106 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {e}\in {ℝ}^{+}$
108 107 rpred ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {e}\in ℝ$
109 69 97 itgabs ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to \left|{\int }_{\left({y},{z}\right)}{F}\left({t}\right)d{t}\right|\le {\int }_{\left({y},{z}\right)}\left|{F}\left({t}\right)\right|d{t}$
110 mblvol ${⊢}\left({y},{z}\right)\in \mathrm{dom}vol\to vol\left(\left({y},{z}\right)\right)={vol}^{*}\left(\left({y},{z}\right)\right)$
111 91 110 ax-mp ${⊢}vol\left(\left({y},{z}\right)\right)={vol}^{*}\left(\left({y},{z}\right)\right)$
112 ioossre ${⊢}\left({y},{z}\right)\subseteq ℝ$
113 ovolcl ${⊢}\left({y},{z}\right)\subseteq ℝ\to {vol}^{*}\left(\left({y},{z}\right)\right)\in {ℝ}^{*}$
114 112 113 mp1i ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {vol}^{*}\left(\left({y},{z}\right)\right)\in {ℝ}^{*}$
115 84 simp1d ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {z}\in ℝ$
116 76 simp1d ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {y}\in ℝ$
117 115 116 resubcld ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {z}-{y}\in ℝ$
118 117 rexrd ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {z}-{y}\in {ℝ}^{*}$
119 simprr ${⊢}\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\to {d}\in {ℝ}^{+}$
120 119 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {d}\in {ℝ}^{+}$
121 120 rpxrd ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {d}\in {ℝ}^{*}$
122 ioossicc ${⊢}\left({y},{z}\right)\subseteq \left[{y},{z}\right]$
123 iccssre ${⊢}\left({y}\in ℝ\wedge {z}\in ℝ\right)\to \left[{y},{z}\right]\subseteq ℝ$
124 116 115 123 syl2anc ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to \left[{y},{z}\right]\subseteq ℝ$
125 ovolss ${⊢}\left(\left({y},{z}\right)\subseteq \left[{y},{z}\right]\wedge \left[{y},{z}\right]\subseteq ℝ\right)\to {vol}^{*}\left(\left({y},{z}\right)\right)\le {vol}^{*}\left(\left[{y},{z}\right]\right)$
126 122 124 125 sylancr ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {vol}^{*}\left(\left({y},{z}\right)\right)\le {vol}^{*}\left(\left[{y},{z}\right]\right)$
127 simprl3 ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {y}\le {z}$
128 ovolicc ${⊢}\left({y}\in ℝ\wedge {z}\in ℝ\wedge {y}\le {z}\right)\to {vol}^{*}\left(\left[{y},{z}\right]\right)={z}-{y}$
129 116 115 127 128 syl3anc ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {vol}^{*}\left(\left[{y},{z}\right]\right)={z}-{y}$
130 126 129 breqtrd ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {vol}^{*}\left(\left({y},{z}\right)\right)\le {z}-{y}$
131 116 115 127 abssubge0d ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to \left|{z}-{y}\right|={z}-{y}$
132 simprr ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to \left|{z}-{y}\right|<{d}$
133 131 132 eqbrtrrd ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {z}-{y}<{d}$
134 114 118 121 130 133 xrlelttrd ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {vol}^{*}\left(\left({y},{z}\right)\right)<{d}$
135 111 134 eqbrtrid ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to vol\left(\left({y},{z}\right)\right)<{d}$
136 sseq1 ${⊢}{u}=\left({y},{z}\right)\to \left({u}\subseteq {D}↔\left({y},{z}\right)\subseteq {D}\right)$
137 fveq2 ${⊢}{u}=\left({y},{z}\right)\to vol\left({u}\right)=vol\left(\left({y},{z}\right)\right)$
138 137 breq1d ${⊢}{u}=\left({y},{z}\right)\to \left(vol\left({u}\right)<{d}↔vol\left(\left({y},{z}\right)\right)<{d}\right)$
139 136 138 anbi12d ${⊢}{u}=\left({y},{z}\right)\to \left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)↔\left(\left({y},{z}\right)\subseteq {D}\wedge vol\left(\left({y},{z}\right)\right)<{d}\right)\right)$
140 2fveq3 ${⊢}{w}={t}\to \left|{F}\left({w}\right)\right|=\left|{F}\left({t}\right)\right|$
141 140 cbvitgv ${⊢}{\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}={\int }_{{u}}\left|{F}\left({t}\right)\right|d{t}$
142 itgeq1 ${⊢}{u}=\left({y},{z}\right)\to {\int }_{{u}}\left|{F}\left({t}\right)\right|d{t}={\int }_{\left({y},{z}\right)}\left|{F}\left({t}\right)\right|d{t}$
143 141 142 syl5eq ${⊢}{u}=\left({y},{z}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}={\int }_{\left({y},{z}\right)}\left|{F}\left({t}\right)\right|d{t}$
144 143 breq1d ${⊢}{u}=\left({y},{z}\right)\to \left({\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}↔{\int }_{\left({y},{z}\right)}\left|{F}\left({t}\right)\right|d{t}<{e}\right)$
145 139 144 imbi12d ${⊢}{u}=\left({y},{z}\right)\to \left(\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)↔\left(\left(\left({y},{z}\right)\subseteq {D}\wedge vol\left(\left({y},{z}\right)\right)<{d}\right)\to {\int }_{\left({y},{z}\right)}\left|{F}\left({t}\right)\right|d{t}<{e}\right)\right)$
146 simplr ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)$
147 145 146 92 rspcdva ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to \left(\left(\left({y},{z}\right)\subseteq {D}\wedge vol\left(\left({y},{z}\right)\right)<{d}\right)\to {\int }_{\left({y},{z}\right)}\left|{F}\left({t}\right)\right|d{t}<{e}\right)$
148 90 135 147 mp2and ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to {\int }_{\left({y},{z}\right)}\left|{F}\left({t}\right)\right|d{t}<{e}$
149 99 105 108 109 148 lelttrd ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to \left|{\int }_{\left({y},{z}\right)}{F}\left({t}\right)d{t}\right|<{e}$
150 68 149 eqbrtrd ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left(\left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\wedge \left|{z}-{y}\right|<{d}\right)\right)\to \left|{G}\left({z}\right)-{G}\left({y}\right)\right|<{e}$
151 150 expr ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\wedge {y}\le {z}\right)\right)\to \left(\left|{z}-{y}\right|<{d}\to \left|{G}\left({z}\right)-{G}\left({y}\right)\right|<{e}\right)$
152 25 35 38 53 151 wlogle ${⊢}\left(\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {z}\in \left[{A},{B}\right]\right)\right)\to \left(\left|{z}-{y}\right|<{d}\to \left|{G}\left({z}\right)-{G}\left({y}\right)\right|<{e}\right)$
153 152 ralrimivva ${⊢}\left(\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\right)\to \forall {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\forall {z}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{z}-{y}\right|<{d}\to \left|{G}\left({z}\right)-{G}\left({y}\right)\right|<{e}\right)$
154 153 ex ${⊢}\left({\phi }\wedge \left({e}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\to \left(\forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\to \forall {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\forall {z}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{z}-{y}\right|<{d}\to \left|{G}\left({z}\right)-{G}\left({y}\right)\right|<{e}\right)\right)$
155 154 anassrs ${⊢}\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {d}\in {ℝ}^{+}\right)\to \left(\forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\to \forall {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\forall {z}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{z}-{y}\right|<{d}\to \left|{G}\left({z}\right)-{G}\left({y}\right)\right|<{e}\right)\right)$
156 155 reximdva ${⊢}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\to \left(\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {D}\wedge vol\left({u}\right)<{d}\right)\to {\int }_{{u}}\left|{F}\left({w}\right)\right|d{w}<{e}\right)\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\forall {z}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{z}-{y}\right|<{d}\to \left|{G}\left({z}\right)-{G}\left({y}\right)\right|<{e}\right)\right)$
157 15 156 mpd ${⊢}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\forall {z}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{z}-{y}\right|<{d}\to \left|{G}\left({z}\right)-{G}\left({y}\right)\right|<{e}\right)$
158 r19.12 ${⊢}\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\forall {z}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{z}-{y}\right|<{d}\to \left|{G}\left({z}\right)-{G}\left({y}\right)\right|<{e}\right)\to \forall {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{z}-{y}\right|<{d}\to \left|{G}\left({z}\right)-{G}\left({y}\right)\right|<{e}\right)$
159 157 158 syl ${⊢}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\to \forall {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{z}-{y}\right|<{d}\to \left|{G}\left({z}\right)-{G}\left({y}\right)\right|<{e}\right)$
160 159 ralrimiva ${⊢}{\phi }\to \forall {e}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{z}-{y}\right|<{d}\to \left|{G}\left({z}\right)-{G}\left({y}\right)\right|<{e}\right)$
161 ralcom ${⊢}\forall {e}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{z}-{y}\right|<{d}\to \left|{G}\left({z}\right)-{G}\left({y}\right)\right|<{e}\right)↔\forall {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\forall {e}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{z}-{y}\right|<{d}\to \left|{G}\left({z}\right)-{G}\left({y}\right)\right|<{e}\right)$
162 160 161 sylib ${⊢}{\phi }\to \forall {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\forall {e}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{z}-{y}\right|<{d}\to \left|{G}\left({z}\right)-{G}\left({y}\right)\right|<{e}\right)$
163 ax-resscn ${⊢}ℝ\subseteq ℂ$
164 37 163 sstrdi ${⊢}{\phi }\to \left[{A},{B}\right]\subseteq ℂ$
165 ssid ${⊢}ℂ\subseteq ℂ$
166 elcncf2 ${⊢}\left(\left[{A},{B}\right]\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to \left({G}:\left[{A},{B}\right]\underset{cn}{⟶}ℂ↔\left({G}:\left[{A},{B}\right]⟶ℂ\wedge \forall {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\forall {e}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{z}-{y}\right|<{d}\to \left|{G}\left({z}\right)-{G}\left({y}\right)\right|<{e}\right)\right)\right)$
167 164 165 166 sylancl ${⊢}{\phi }\to \left({G}:\left[{A},{B}\right]\underset{cn}{⟶}ℂ↔\left({G}:\left[{A},{B}\right]⟶ℂ\wedge \forall {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\forall {e}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{z}-{y}\right|<{d}\to \left|{G}\left({z}\right)-{G}\left({y}\right)\right|<{e}\right)\right)\right)$
168 9 162 167 mpbir2and ${⊢}{\phi }\to {G}:\left[{A},{B}\right]\underset{cn}{⟶}ℂ$