# Metamath Proof Explorer

## Theorem ftc1lem4

Description: Lemma for ftc1 . (Contributed by Mario Carneiro, 31-Aug-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}$
ftc1.c ${⊢}{\phi }\to {C}\in \left({A},{B}\right)$
ftc1.f ${⊢}{\phi }\to {F}\in \left({K}\mathrm{CnP}{L}\right)\left({C}\right)$
ftc1.j ${⊢}{J}={L}{↾}_{𝑡}ℝ$
ftc1.k ${⊢}{K}={L}{↾}_{𝑡}{D}$
ftc1.l ${⊢}{L}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
ftc1.h ${⊢}{H}=\left({z}\in \left(\left[{A},{B}\right]\setminus \left\{{C}\right\}\right)⟼\frac{{G}\left({z}\right)-{G}\left({C}\right)}{{z}-{C}}\right)$
ftc1.e ${⊢}{\phi }\to {E}\in {ℝ}^{+}$
ftc1.r ${⊢}{\phi }\to {R}\in {ℝ}^{+}$
ftc1.fc ${⊢}\left({\phi }\wedge {y}\in {D}\right)\to \left(\left|{y}-{C}\right|<{R}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{E}\right)$
ftc1.x1 ${⊢}{\phi }\to {X}\in \left[{A},{B}\right]$
ftc1.x2 ${⊢}{\phi }\to \left|{X}-{C}\right|<{R}$
ftc1.y1 ${⊢}{\phi }\to {Y}\in \left[{A},{B}\right]$
ftc1.y2 ${⊢}{\phi }\to \left|{Y}-{C}\right|<{R}$
Assertion ftc1lem4 ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to \left|\left(\frac{{G}\left({Y}\right)-{G}\left({X}\right)}{{Y}-{X}}\right)-{F}\left({C}\right)\right|<{E}$

### 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 ftc1.c ${⊢}{\phi }\to {C}\in \left({A},{B}\right)$
9 ftc1.f ${⊢}{\phi }\to {F}\in \left({K}\mathrm{CnP}{L}\right)\left({C}\right)$
10 ftc1.j ${⊢}{J}={L}{↾}_{𝑡}ℝ$
11 ftc1.k ${⊢}{K}={L}{↾}_{𝑡}{D}$
12 ftc1.l ${⊢}{L}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
13 ftc1.h ${⊢}{H}=\left({z}\in \left(\left[{A},{B}\right]\setminus \left\{{C}\right\}\right)⟼\frac{{G}\left({z}\right)-{G}\left({C}\right)}{{z}-{C}}\right)$
14 ftc1.e ${⊢}{\phi }\to {E}\in {ℝ}^{+}$
15 ftc1.r ${⊢}{\phi }\to {R}\in {ℝ}^{+}$
16 ftc1.fc ${⊢}\left({\phi }\wedge {y}\in {D}\right)\to \left(\left|{y}-{C}\right|<{R}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{E}\right)$
17 ftc1.x1 ${⊢}{\phi }\to {X}\in \left[{A},{B}\right]$
18 ftc1.x2 ${⊢}{\phi }\to \left|{X}-{C}\right|<{R}$
19 ftc1.y1 ${⊢}{\phi }\to {Y}\in \left[{A},{B}\right]$
20 ftc1.y2 ${⊢}{\phi }\to \left|{Y}-{C}\right|<{R}$
21 ovexd ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to {F}\left({t}\right)-{F}\left({C}\right)\in \mathrm{V}$
22 2 rexrd ${⊢}{\phi }\to {A}\in {ℝ}^{*}$
23 elicc2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({X}\in \left[{A},{B}\right]↔\left({X}\in ℝ\wedge {A}\le {X}\wedge {X}\le {B}\right)\right)$
24 2 3 23 syl2anc ${⊢}{\phi }\to \left({X}\in \left[{A},{B}\right]↔\left({X}\in ℝ\wedge {A}\le {X}\wedge {X}\le {B}\right)\right)$
25 17 24 mpbid ${⊢}{\phi }\to \left({X}\in ℝ\wedge {A}\le {X}\wedge {X}\le {B}\right)$
26 25 simp2d ${⊢}{\phi }\to {A}\le {X}$
27 iooss1 ${⊢}\left({A}\in {ℝ}^{*}\wedge {A}\le {X}\right)\to \left({X},{Y}\right)\subseteq \left({A},{Y}\right)$
28 22 26 27 syl2anc ${⊢}{\phi }\to \left({X},{Y}\right)\subseteq \left({A},{Y}\right)$
29 3 rexrd ${⊢}{\phi }\to {B}\in {ℝ}^{*}$
30 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)$
31 2 3 30 syl2anc ${⊢}{\phi }\to \left({Y}\in \left[{A},{B}\right]↔\left({Y}\in ℝ\wedge {A}\le {Y}\wedge {Y}\le {B}\right)\right)$
32 19 31 mpbid ${⊢}{\phi }\to \left({Y}\in ℝ\wedge {A}\le {Y}\wedge {Y}\le {B}\right)$
33 32 simp3d ${⊢}{\phi }\to {Y}\le {B}$
34 iooss2 ${⊢}\left({B}\in {ℝ}^{*}\wedge {Y}\le {B}\right)\to \left({A},{Y}\right)\subseteq \left({A},{B}\right)$
35 29 33 34 syl2anc ${⊢}{\phi }\to \left({A},{Y}\right)\subseteq \left({A},{B}\right)$
36 28 35 sstrd ${⊢}{\phi }\to \left({X},{Y}\right)\subseteq \left({A},{B}\right)$
37 36 5 sstrd ${⊢}{\phi }\to \left({X},{Y}\right)\subseteq {D}$
38 37 sselda ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to {t}\in {D}$
39 1 2 3 4 5 6 7 8 9 10 11 12 ftc1lem3 ${⊢}{\phi }\to {F}:{D}⟶ℂ$
40 39 ffvelrnda ${⊢}\left({\phi }\wedge {t}\in {D}\right)\to {F}\left({t}\right)\in ℂ$
41 38 40 syldan ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to {F}\left({t}\right)\in ℂ$
42 ioombl ${⊢}\left({X},{Y}\right)\in \mathrm{dom}vol$
43 42 a1i ${⊢}{\phi }\to \left({X},{Y}\right)\in \mathrm{dom}vol$
44 fvexd ${⊢}\left({\phi }\wedge {t}\in {D}\right)\to {F}\left({t}\right)\in \mathrm{V}$
45 39 feqmptd ${⊢}{\phi }\to {F}=\left({t}\in {D}⟼{F}\left({t}\right)\right)$
46 45 7 eqeltrrd ${⊢}{\phi }\to \left({t}\in {D}⟼{F}\left({t}\right)\right)\in {𝐿}^{1}$
47 37 43 44 46 iblss ${⊢}{\phi }\to \left({t}\in \left({X},{Y}\right)⟼{F}\left({t}\right)\right)\in {𝐿}^{1}$
48 5 8 sseldd ${⊢}{\phi }\to {C}\in {D}$
49 39 48 ffvelrnd ${⊢}{\phi }\to {F}\left({C}\right)\in ℂ$
50 49 adantr ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to {F}\left({C}\right)\in ℂ$
51 fconstmpt ${⊢}\left({X},{Y}\right)×\left\{{F}\left({C}\right)\right\}=\left({t}\in \left({X},{Y}\right)⟼{F}\left({C}\right)\right)$
52 mblvol ${⊢}\left({X},{Y}\right)\in \mathrm{dom}vol\to vol\left(\left({X},{Y}\right)\right)={vol}^{*}\left(\left({X},{Y}\right)\right)$
53 42 52 ax-mp ${⊢}vol\left(\left({X},{Y}\right)\right)={vol}^{*}\left(\left({X},{Y}\right)\right)$
54 ioossicc ${⊢}\left({X},{Y}\right)\subseteq \left[{X},{Y}\right]$
55 54 a1i ${⊢}{\phi }\to \left({X},{Y}\right)\subseteq \left[{X},{Y}\right]$
56 iccssre ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left[{A},{B}\right]\subseteq ℝ$
57 2 3 56 syl2anc ${⊢}{\phi }\to \left[{A},{B}\right]\subseteq ℝ$
58 57 17 sseldd ${⊢}{\phi }\to {X}\in ℝ$
59 57 19 sseldd ${⊢}{\phi }\to {Y}\in ℝ$
60 iccmbl ${⊢}\left({X}\in ℝ\wedge {Y}\in ℝ\right)\to \left[{X},{Y}\right]\in \mathrm{dom}vol$
61 58 59 60 syl2anc ${⊢}{\phi }\to \left[{X},{Y}\right]\in \mathrm{dom}vol$
62 mblss ${⊢}\left[{X},{Y}\right]\in \mathrm{dom}vol\to \left[{X},{Y}\right]\subseteq ℝ$
63 61 62 syl ${⊢}{\phi }\to \left[{X},{Y}\right]\subseteq ℝ$
64 mblvol ${⊢}\left[{X},{Y}\right]\in \mathrm{dom}vol\to vol\left(\left[{X},{Y}\right]\right)={vol}^{*}\left(\left[{X},{Y}\right]\right)$
65 61 64 syl ${⊢}{\phi }\to vol\left(\left[{X},{Y}\right]\right)={vol}^{*}\left(\left[{X},{Y}\right]\right)$
66 iccvolcl ${⊢}\left({X}\in ℝ\wedge {Y}\in ℝ\right)\to vol\left(\left[{X},{Y}\right]\right)\in ℝ$
67 58 59 66 syl2anc ${⊢}{\phi }\to vol\left(\left[{X},{Y}\right]\right)\in ℝ$
68 65 67 eqeltrrd ${⊢}{\phi }\to {vol}^{*}\left(\left[{X},{Y}\right]\right)\in ℝ$
69 ovolsscl ${⊢}\left(\left({X},{Y}\right)\subseteq \left[{X},{Y}\right]\wedge \left[{X},{Y}\right]\subseteq ℝ\wedge {vol}^{*}\left(\left[{X},{Y}\right]\right)\in ℝ\right)\to {vol}^{*}\left(\left({X},{Y}\right)\right)\in ℝ$
70 55 63 68 69 syl3anc ${⊢}{\phi }\to {vol}^{*}\left(\left({X},{Y}\right)\right)\in ℝ$
71 53 70 eqeltrid ${⊢}{\phi }\to vol\left(\left({X},{Y}\right)\right)\in ℝ$
72 iblconst ${⊢}\left(\left({X},{Y}\right)\in \mathrm{dom}vol\wedge vol\left(\left({X},{Y}\right)\right)\in ℝ\wedge {F}\left({C}\right)\in ℂ\right)\to \left({X},{Y}\right)×\left\{{F}\left({C}\right)\right\}\in {𝐿}^{1}$
73 43 71 49 72 syl3anc ${⊢}{\phi }\to \left({X},{Y}\right)×\left\{{F}\left({C}\right)\right\}\in {𝐿}^{1}$
74 51 73 eqeltrrid ${⊢}{\phi }\to \left({t}\in \left({X},{Y}\right)⟼{F}\left({C}\right)\right)\in {𝐿}^{1}$
75 41 47 50 74 iblsub ${⊢}{\phi }\to \left({t}\in \left({X},{Y}\right)⟼{F}\left({t}\right)-{F}\left({C}\right)\right)\in {𝐿}^{1}$
76 21 75 itgcl ${⊢}{\phi }\to {\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}\in ℂ$
77 76 adantr ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}\in ℂ$
78 59 58 resubcld ${⊢}{\phi }\to {Y}-{X}\in ℝ$
79 78 adantr ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {Y}-{X}\in ℝ$
80 79 recnd ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {Y}-{X}\in ℂ$
81 58 59 posdifd ${⊢}{\phi }\to \left({X}<{Y}↔0<{Y}-{X}\right)$
82 81 biimpa ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to 0<{Y}-{X}$
83 82 gt0ne0d ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {Y}-{X}\ne 0$
84 77 80 83 divcld ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to \frac{{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}}{{Y}-{X}}\in ℂ$
85 49 adantr ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {F}\left({C}\right)\in ℂ$
86 ltle ${⊢}\left({X}\in ℝ\wedge {Y}\in ℝ\right)\to \left({X}<{Y}\to {X}\le {Y}\right)$
87 58 59 86 syl2anc ${⊢}{\phi }\to \left({X}<{Y}\to {X}\le {Y}\right)$
88 87 imp ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {X}\le {Y}$
89 1 2 3 4 5 6 7 39 17 19 ftc1lem1 ${⊢}\left({\phi }\wedge {X}\le {Y}\right)\to {G}\left({Y}\right)-{G}\left({X}\right)={\int }_{\left({X},{Y}\right)}{F}\left({t}\right)d{t}$
90 88 89 syldan ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {G}\left({Y}\right)-{G}\left({X}\right)={\int }_{\left({X},{Y}\right)}{F}\left({t}\right)d{t}$
91 41 50 npcand ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to {F}\left({t}\right)-{F}\left({C}\right)+{F}\left({C}\right)={F}\left({t}\right)$
92 91 itgeq2dv ${⊢}{\phi }\to {\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)+{F}\left({C}\right)\right)d{t}={\int }_{\left({X},{Y}\right)}{F}\left({t}\right)d{t}$
93 41 50 subcld ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to {F}\left({t}\right)-{F}\left({C}\right)\in ℂ$
94 93 75 50 74 itgadd ${⊢}{\phi }\to {\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)+{F}\left({C}\right)\right)d{t}={\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}+{\int }_{\left({X},{Y}\right)}{F}\left({C}\right)d{t}$
95 92 94 eqtr3d ${⊢}{\phi }\to {\int }_{\left({X},{Y}\right)}{F}\left({t}\right)d{t}={\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}+{\int }_{\left({X},{Y}\right)}{F}\left({C}\right)d{t}$
96 95 adantr ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {\int }_{\left({X},{Y}\right)}{F}\left({t}\right)d{t}={\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}+{\int }_{\left({X},{Y}\right)}{F}\left({C}\right)d{t}$
97 itgconst ${⊢}\left(\left({X},{Y}\right)\in \mathrm{dom}vol\wedge vol\left(\left({X},{Y}\right)\right)\in ℝ\wedge {F}\left({C}\right)\in ℂ\right)\to {\int }_{\left({X},{Y}\right)}{F}\left({C}\right)d{t}={F}\left({C}\right)vol\left(\left({X},{Y}\right)\right)$
98 43 71 49 97 syl3anc ${⊢}{\phi }\to {\int }_{\left({X},{Y}\right)}{F}\left({C}\right)d{t}={F}\left({C}\right)vol\left(\left({X},{Y}\right)\right)$
99 98 adantr ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {\int }_{\left({X},{Y}\right)}{F}\left({C}\right)d{t}={F}\left({C}\right)vol\left(\left({X},{Y}\right)\right)$
100 58 adantr ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {X}\in ℝ$
101 59 adantr ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {Y}\in ℝ$
102 ovolioo ${⊢}\left({X}\in ℝ\wedge {Y}\in ℝ\wedge {X}\le {Y}\right)\to {vol}^{*}\left(\left({X},{Y}\right)\right)={Y}-{X}$
103 100 101 88 102 syl3anc ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {vol}^{*}\left(\left({X},{Y}\right)\right)={Y}-{X}$
104 53 103 syl5eq ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to vol\left(\left({X},{Y}\right)\right)={Y}-{X}$
105 104 oveq2d ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {F}\left({C}\right)vol\left(\left({X},{Y}\right)\right)={F}\left({C}\right)\left({Y}-{X}\right)$
106 99 105 eqtrd ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {\int }_{\left({X},{Y}\right)}{F}\left({C}\right)d{t}={F}\left({C}\right)\left({Y}-{X}\right)$
107 106 oveq2d ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}+{\int }_{\left({X},{Y}\right)}{F}\left({C}\right)d{t}={\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}+{F}\left({C}\right)\left({Y}-{X}\right)$
108 90 96 107 3eqtrd ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {G}\left({Y}\right)-{G}\left({X}\right)={\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}+{F}\left({C}\right)\left({Y}-{X}\right)$
109 108 oveq1d ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to \frac{{G}\left({Y}\right)-{G}\left({X}\right)}{{Y}-{X}}=\frac{{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}+{F}\left({C}\right)\left({Y}-{X}\right)}{{Y}-{X}}$
110 85 80 mulcld ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {F}\left({C}\right)\left({Y}-{X}\right)\in ℂ$
111 77 110 80 83 divdird ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to \frac{{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}+{F}\left({C}\right)\left({Y}-{X}\right)}{{Y}-{X}}=\left(\frac{{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}}{{Y}-{X}}\right)+\left(\frac{{F}\left({C}\right)\left({Y}-{X}\right)}{{Y}-{X}}\right)$
112 85 80 83 divcan4d ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to \frac{{F}\left({C}\right)\left({Y}-{X}\right)}{{Y}-{X}}={F}\left({C}\right)$
113 112 oveq2d ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to \left(\frac{{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}}{{Y}-{X}}\right)+\left(\frac{{F}\left({C}\right)\left({Y}-{X}\right)}{{Y}-{X}}\right)=\left(\frac{{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}}{{Y}-{X}}\right)+{F}\left({C}\right)$
114 109 111 113 3eqtrd ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to \frac{{G}\left({Y}\right)-{G}\left({X}\right)}{{Y}-{X}}=\left(\frac{{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}}{{Y}-{X}}\right)+{F}\left({C}\right)$
115 84 85 114 mvrraddd ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to \left(\frac{{G}\left({Y}\right)-{G}\left({X}\right)}{{Y}-{X}}\right)-{F}\left({C}\right)=\frac{{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}}{{Y}-{X}}$
116 115 fveq2d ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to \left|\left(\frac{{G}\left({Y}\right)-{G}\left({X}\right)}{{Y}-{X}}\right)-{F}\left({C}\right)\right|=\left|\frac{{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}}{{Y}-{X}}\right|$
117 77 80 83 absdivd ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to \left|\frac{{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}}{{Y}-{X}}\right|=\frac{\left|{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}\right|}{\left|{Y}-{X}\right|}$
118 0re ${⊢}0\in ℝ$
119 ltle ${⊢}\left(0\in ℝ\wedge {Y}-{X}\in ℝ\right)\to \left(0<{Y}-{X}\to 0\le {Y}-{X}\right)$
120 118 79 119 sylancr ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to \left(0<{Y}-{X}\to 0\le {Y}-{X}\right)$
121 82 120 mpd ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to 0\le {Y}-{X}$
122 79 121 absidd ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to \left|{Y}-{X}\right|={Y}-{X}$
123 122 oveq2d ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to \frac{\left|{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}\right|}{\left|{Y}-{X}\right|}=\frac{\left|{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}\right|}{{Y}-{X}}$
124 116 117 123 3eqtrd ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to \left|\left(\frac{{G}\left({Y}\right)-{G}\left({X}\right)}{{Y}-{X}}\right)-{F}\left({C}\right)\right|=\frac{\left|{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}\right|}{{Y}-{X}}$
125 76 abscld ${⊢}{\phi }\to \left|{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}\right|\in ℝ$
126 125 adantr ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to \left|{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}\right|\in ℝ$
127 93 abscld ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to \left|{F}\left({t}\right)-{F}\left({C}\right)\right|\in ℝ$
128 21 75 iblabs ${⊢}{\phi }\to \left({t}\in \left({X},{Y}\right)⟼\left|{F}\left({t}\right)-{F}\left({C}\right)\right|\right)\in {𝐿}^{1}$
129 127 128 itgrecl ${⊢}{\phi }\to {\int }_{\left({X},{Y}\right)}\left|{F}\left({t}\right)-{F}\left({C}\right)\right|d{t}\in ℝ$
130 129 adantr ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {\int }_{\left({X},{Y}\right)}\left|{F}\left({t}\right)-{F}\left({C}\right)\right|d{t}\in ℝ$
131 14 rpred ${⊢}{\phi }\to {E}\in ℝ$
132 78 131 remulcld ${⊢}{\phi }\to \left({Y}-{X}\right){E}\in ℝ$
133 132 adantr ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to \left({Y}-{X}\right){E}\in ℝ$
134 93 75 itgabs ${⊢}{\phi }\to \left|{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}\right|\le {\int }_{\left({X},{Y}\right)}\left|{F}\left({t}\right)-{F}\left({C}\right)\right|d{t}$
135 134 adantr ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to \left|{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}\right|\le {\int }_{\left({X},{Y}\right)}\left|{F}\left({t}\right)-{F}\left({C}\right)\right|d{t}$
136 82 104 breqtrrd ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to 0
137 131 adantr ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to {E}\in ℝ$
138 fconstmpt ${⊢}\left({X},{Y}\right)×\left\{{E}\right\}=\left({t}\in \left({X},{Y}\right)⟼{E}\right)$
139 131 recnd ${⊢}{\phi }\to {E}\in ℂ$
140 iblconst ${⊢}\left(\left({X},{Y}\right)\in \mathrm{dom}vol\wedge vol\left(\left({X},{Y}\right)\right)\in ℝ\wedge {E}\in ℂ\right)\to \left({X},{Y}\right)×\left\{{E}\right\}\in {𝐿}^{1}$
141 43 71 139 140 syl3anc ${⊢}{\phi }\to \left({X},{Y}\right)×\left\{{E}\right\}\in {𝐿}^{1}$
142 138 141 eqeltrrid ${⊢}{\phi }\to \left({t}\in \left({X},{Y}\right)⟼{E}\right)\in {𝐿}^{1}$
143 137 142 127 128 iblsub ${⊢}{\phi }\to \left({t}\in \left({X},{Y}\right)⟼{E}-\left|{F}\left({t}\right)-{F}\left({C}\right)\right|\right)\in {𝐿}^{1}$
144 143 adantr ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to \left({t}\in \left({X},{Y}\right)⟼{E}-\left|{F}\left({t}\right)-{F}\left({C}\right)\right|\right)\in {𝐿}^{1}$
145 6 48 sseldd ${⊢}{\phi }\to {C}\in ℝ$
146 15 rpred ${⊢}{\phi }\to {R}\in ℝ$
147 145 146 resubcld ${⊢}{\phi }\to {C}-{R}\in ℝ$
148 147 adantr ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to {C}-{R}\in ℝ$
149 58 adantr ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to {X}\in ℝ$
150 37 6 sstrd ${⊢}{\phi }\to \left({X},{Y}\right)\subseteq ℝ$
151 150 sselda ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to {t}\in ℝ$
152 58 145 146 absdifltd ${⊢}{\phi }\to \left(\left|{X}-{C}\right|<{R}↔\left({C}-{R}<{X}\wedge {X}<{C}+{R}\right)\right)$
153 18 152 mpbid ${⊢}{\phi }\to \left({C}-{R}<{X}\wedge {X}<{C}+{R}\right)$
154 153 simpld ${⊢}{\phi }\to {C}-{R}<{X}$
155 154 adantr ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to {C}-{R}<{X}$
156 eliooord ${⊢}{t}\in \left({X},{Y}\right)\to \left({X}<{t}\wedge {t}<{Y}\right)$
157 156 adantl ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to \left({X}<{t}\wedge {t}<{Y}\right)$
158 157 simpld ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to {X}<{t}$
159 148 149 151 155 158 lttrd ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to {C}-{R}<{t}$
160 59 adantr ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to {Y}\in ℝ$
161 145 146 readdcld ${⊢}{\phi }\to {C}+{R}\in ℝ$
162 161 adantr ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to {C}+{R}\in ℝ$
163 157 simprd ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to {t}<{Y}$
164 59 145 146 absdifltd ${⊢}{\phi }\to \left(\left|{Y}-{C}\right|<{R}↔\left({C}-{R}<{Y}\wedge {Y}<{C}+{R}\right)\right)$
165 20 164 mpbid ${⊢}{\phi }\to \left({C}-{R}<{Y}\wedge {Y}<{C}+{R}\right)$
166 165 simprd ${⊢}{\phi }\to {Y}<{C}+{R}$
167 166 adantr ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to {Y}<{C}+{R}$
168 151 160 162 163 167 lttrd ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to {t}<{C}+{R}$
169 145 adantr ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to {C}\in ℝ$
170 146 adantr ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to {R}\in ℝ$
171 151 169 170 absdifltd ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to \left(\left|{t}-{C}\right|<{R}↔\left({C}-{R}<{t}\wedge {t}<{C}+{R}\right)\right)$
172 159 168 171 mpbir2and ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to \left|{t}-{C}\right|<{R}$
173 fvoveq1 ${⊢}{y}={t}\to \left|{y}-{C}\right|=\left|{t}-{C}\right|$
174 173 breq1d ${⊢}{y}={t}\to \left(\left|{y}-{C}\right|<{R}↔\left|{t}-{C}\right|<{R}\right)$
175 174 imbrov2fvoveq ${⊢}{y}={t}\to \left(\left(\left|{y}-{C}\right|<{R}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{E}\right)↔\left(\left|{t}-{C}\right|<{R}\to \left|{F}\left({t}\right)-{F}\left({C}\right)\right|<{E}\right)\right)$
176 16 ralrimiva ${⊢}{\phi }\to \forall {y}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left|{y}-{C}\right|<{R}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{E}\right)$
177 176 adantr ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to \forall {y}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left|{y}-{C}\right|<{R}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{E}\right)$
178 175 177 38 rspcdva ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to \left(\left|{t}-{C}\right|<{R}\to \left|{F}\left({t}\right)-{F}\left({C}\right)\right|<{E}\right)$
179 172 178 mpd ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to \left|{F}\left({t}\right)-{F}\left({C}\right)\right|<{E}$
180 difrp ${⊢}\left(\left|{F}\left({t}\right)-{F}\left({C}\right)\right|\in ℝ\wedge {E}\in ℝ\right)\to \left(\left|{F}\left({t}\right)-{F}\left({C}\right)\right|<{E}↔{E}-\left|{F}\left({t}\right)-{F}\left({C}\right)\right|\in {ℝ}^{+}\right)$
181 127 137 180 syl2anc ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to \left(\left|{F}\left({t}\right)-{F}\left({C}\right)\right|<{E}↔{E}-\left|{F}\left({t}\right)-{F}\left({C}\right)\right|\in {ℝ}^{+}\right)$
182 179 181 mpbid ${⊢}\left({\phi }\wedge {t}\in \left({X},{Y}\right)\right)\to {E}-\left|{F}\left({t}\right)-{F}\left({C}\right)\right|\in {ℝ}^{+}$
183 182 adantlr ${⊢}\left(\left({\phi }\wedge {X}<{Y}\right)\wedge {t}\in \left({X},{Y}\right)\right)\to {E}-\left|{F}\left({t}\right)-{F}\left({C}\right)\right|\in {ℝ}^{+}$
184 136 144 183 itggt0 ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to 0<{\int }_{\left({X},{Y}\right)}\left({E}-\left|{F}\left({t}\right)-{F}\left({C}\right)\right|\right)d{t}$
185 137 142 127 128 itgsub ${⊢}{\phi }\to {\int }_{\left({X},{Y}\right)}\left({E}-\left|{F}\left({t}\right)-{F}\left({C}\right)\right|\right)d{t}={\int }_{\left({X},{Y}\right)}{E}d{t}-{\int }_{\left({X},{Y}\right)}\left|{F}\left({t}\right)-{F}\left({C}\right)\right|d{t}$
186 185 adantr ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {\int }_{\left({X},{Y}\right)}\left({E}-\left|{F}\left({t}\right)-{F}\left({C}\right)\right|\right)d{t}={\int }_{\left({X},{Y}\right)}{E}d{t}-{\int }_{\left({X},{Y}\right)}\left|{F}\left({t}\right)-{F}\left({C}\right)\right|d{t}$
187 itgconst ${⊢}\left(\left({X},{Y}\right)\in \mathrm{dom}vol\wedge vol\left(\left({X},{Y}\right)\right)\in ℝ\wedge {E}\in ℂ\right)\to {\int }_{\left({X},{Y}\right)}{E}d{t}={E}vol\left(\left({X},{Y}\right)\right)$
188 43 71 139 187 syl3anc ${⊢}{\phi }\to {\int }_{\left({X},{Y}\right)}{E}d{t}={E}vol\left(\left({X},{Y}\right)\right)$
189 188 adantr ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {\int }_{\left({X},{Y}\right)}{E}d{t}={E}vol\left(\left({X},{Y}\right)\right)$
190 104 oveq2d ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {E}vol\left(\left({X},{Y}\right)\right)={E}\left({Y}-{X}\right)$
191 78 recnd ${⊢}{\phi }\to {Y}-{X}\in ℂ$
192 139 191 mulcomd ${⊢}{\phi }\to {E}\left({Y}-{X}\right)=\left({Y}-{X}\right){E}$
193 192 adantr ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {E}\left({Y}-{X}\right)=\left({Y}-{X}\right){E}$
194 189 190 193 3eqtrd ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {\int }_{\left({X},{Y}\right)}{E}d{t}=\left({Y}-{X}\right){E}$
195 194 oveq1d ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {\int }_{\left({X},{Y}\right)}{E}d{t}-{\int }_{\left({X},{Y}\right)}\left|{F}\left({t}\right)-{F}\left({C}\right)\right|d{t}=\left({Y}-{X}\right){E}-{\int }_{\left({X},{Y}\right)}\left|{F}\left({t}\right)-{F}\left({C}\right)\right|d{t}$
196 186 195 eqtrd ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {\int }_{\left({X},{Y}\right)}\left({E}-\left|{F}\left({t}\right)-{F}\left({C}\right)\right|\right)d{t}=\left({Y}-{X}\right){E}-{\int }_{\left({X},{Y}\right)}\left|{F}\left({t}\right)-{F}\left({C}\right)\right|d{t}$
197 184 196 breqtrd ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to 0<\left({Y}-{X}\right){E}-{\int }_{\left({X},{Y}\right)}\left|{F}\left({t}\right)-{F}\left({C}\right)\right|d{t}$
198 129 132 posdifd ${⊢}{\phi }\to \left({\int }_{\left({X},{Y}\right)}\left|{F}\left({t}\right)-{F}\left({C}\right)\right|d{t}<\left({Y}-{X}\right){E}↔0<\left({Y}-{X}\right){E}-{\int }_{\left({X},{Y}\right)}\left|{F}\left({t}\right)-{F}\left({C}\right)\right|d{t}\right)$
199 198 biimpar ${⊢}\left({\phi }\wedge 0<\left({Y}-{X}\right){E}-{\int }_{\left({X},{Y}\right)}\left|{F}\left({t}\right)-{F}\left({C}\right)\right|d{t}\right)\to {\int }_{\left({X},{Y}\right)}\left|{F}\left({t}\right)-{F}\left({C}\right)\right|d{t}<\left({Y}-{X}\right){E}$
200 197 199 syldan ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {\int }_{\left({X},{Y}\right)}\left|{F}\left({t}\right)-{F}\left({C}\right)\right|d{t}<\left({Y}-{X}\right){E}$
201 126 130 133 135 200 lelttrd ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to \left|{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}\right|<\left({Y}-{X}\right){E}$
202 77 abscld ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to \left|{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}\right|\in ℝ$
203 131 adantr ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to {E}\in ℝ$
204 ltdivmul ${⊢}\left(\left|{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}\right|\in ℝ\wedge {E}\in ℝ\wedge \left({Y}-{X}\in ℝ\wedge 0<{Y}-{X}\right)\right)\to \left(\frac{\left|{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}\right|}{{Y}-{X}}<{E}↔\left|{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}\right|<\left({Y}-{X}\right){E}\right)$
205 202 203 79 82 204 syl112anc ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to \left(\frac{\left|{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}\right|}{{Y}-{X}}<{E}↔\left|{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}\right|<\left({Y}-{X}\right){E}\right)$
206 201 205 mpbird ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to \frac{\left|{\int }_{\left({X},{Y}\right)}\left({F}\left({t}\right)-{F}\left({C}\right)\right)d{t}\right|}{{Y}-{X}}<{E}$
207 124 206 eqbrtrd ${⊢}\left({\phi }\wedge {X}<{Y}\right)\to \left|\left(\frac{{G}\left({Y}\right)-{G}\left({X}\right)}{{Y}-{X}}\right)-{F}\left({C}\right)\right|<{E}$