This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ftc1lem4

Description: Lemma for ftc1 . (Contributed by Mario Carneiro, 31-Aug-2014)

Ref Expression
Hypotheses ftc1.g ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
ftc1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ftc1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ftc1.le ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
ftc1.s ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
ftc1.d ⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
ftc1.i ⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
ftc1.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 (,) 𝐵 ) )
ftc1.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ 𝐶 ) )
ftc1.j ⊢ 𝐽 = ( 𝐿 ↾t ℝ )
ftc1.k ⊢ 𝐾 = ( 𝐿 ↾t 𝐷 )
ftc1.l ⊢ 𝐿 = ( TopOpen ‘ ℂfld )
ftc1.h ⊢ 𝐻 = ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) )
ftc1.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
ftc1.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
ftc1.fc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 ) )
ftc1.x1 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 [,] 𝐵 ) )
ftc1.x2 ⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝐶 ) ) < 𝑅 )
ftc1.y1 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 [,] 𝐵 ) )
ftc1.y2 ⊢ ( 𝜑 → ( abs ‘ ( 𝑌 − 𝐶 ) ) < 𝑅 )
Assertion ftc1lem4 ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 )

Proof

Step Hyp Ref Expression
1 ftc1.g ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
2 ftc1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 ftc1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 ftc1.le ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
5 ftc1.s ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
6 ftc1.d ⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
7 ftc1.i ⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
8 ftc1.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 (,) 𝐵 ) )
9 ftc1.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ 𝐶 ) )
10 ftc1.j ⊢ 𝐽 = ( 𝐿 ↾t ℝ )
11 ftc1.k ⊢ 𝐾 = ( 𝐿 ↾t 𝐷 )
12 ftc1.l ⊢ 𝐿 = ( TopOpen ‘ ℂfld )
13 ftc1.h ⊢ 𝐻 = ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) )
14 ftc1.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
15 ftc1.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
16 ftc1.fc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 ) )
17 ftc1.x1 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 [,] 𝐵 ) )
18 ftc1.x2 ⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝐶 ) ) < 𝑅 )
19 ftc1.y1 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 [,] 𝐵 ) )
20 ftc1.y2 ⊢ ( 𝜑 → ( abs ‘ ( 𝑌 − 𝐶 ) ) < 𝑅 )
21 ovexd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ∈ V )
22 2 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
23 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵 ) ) )
24 2 3 23 syl2anc ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵 ) ) )
25 17 24 mpbid ⊢ ( 𝜑 → ( 𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵 ) )
26 25 simp2d ⊢ ( 𝜑 → 𝐴 ≤ 𝑋 )
27 iooss1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝑋 ) → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝑌 ) )
28 22 26 27 syl2anc ⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝑌 ) )
29 3 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
30 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑌 ∈ ℝ ∧ 𝐴 ≤ 𝑌 ∧ 𝑌 ≤ 𝐵 ) ) )
31 2 3 30 syl2anc ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑌 ∈ ℝ ∧ 𝐴 ≤ 𝑌 ∧ 𝑌 ≤ 𝐵 ) ) )
32 19 31 mpbid ⊢ ( 𝜑 → ( 𝑌 ∈ ℝ ∧ 𝐴 ≤ 𝑌 ∧ 𝑌 ≤ 𝐵 ) )
33 32 simp3d ⊢ ( 𝜑 → 𝑌 ≤ 𝐵 )
34 iooss2 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑌 ≤ 𝐵 ) → ( 𝐴 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝐵 ) )
35 29 33 34 syl2anc ⊢ ( 𝜑 → ( 𝐴 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝐵 ) )
36 28 35 sstrd ⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝐵 ) )
37 36 5 sstrd ⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ 𝐷 )
38 37 sselda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑡 ∈ 𝐷 )
39 1 2 3 4 5 6 7 8 9 10 11 12 ftc1lem3 ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )
40 39 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
41 38 40 syldan ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
42 ioombl ⊢ ( 𝑋 (,) 𝑌 ) ∈ dom vol
43 42 a1i ⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ∈ dom vol )
44 fvexd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ V )
45 39 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) ) )
46 45 7 eqeltrrd ⊢ ( 𝜑 → ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
47 37 43 44 46 iblss ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
48 5 8 sseldd ⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )
49 39 48 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
50 49 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
51 fconstmpt ⊢ ( ( 𝑋 (,) 𝑌 ) × { ( 𝐹 ‘ 𝐶 ) } ) = ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝐶 ) )
52 mblvol ⊢ ( ( 𝑋 (,) 𝑌 ) ∈ dom vol → ( vol ‘ ( 𝑋 (,) 𝑌 ) ) = ( vol* ‘ ( 𝑋 (,) 𝑌 ) ) )
53 42 52 ax-mp ⊢ ( vol ‘ ( 𝑋 (,) 𝑌 ) ) = ( vol* ‘ ( 𝑋 (,) 𝑌 ) )
54 ioossicc ⊢ ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 )
55 54 a1i ⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 ) )
56 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
57 2 3 56 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
58 57 17 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
59 57 19 sseldd ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
60 iccmbl ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝑋 [,] 𝑌 ) ∈ dom vol )
61 58 59 60 syl2anc ⊢ ( 𝜑 → ( 𝑋 [,] 𝑌 ) ∈ dom vol )
62 mblss ⊢ ( ( 𝑋 [,] 𝑌 ) ∈ dom vol → ( 𝑋 [,] 𝑌 ) ⊆ ℝ )
63 61 62 syl ⊢ ( 𝜑 → ( 𝑋 [,] 𝑌 ) ⊆ ℝ )
64 mblvol ⊢ ( ( 𝑋 [,] 𝑌 ) ∈ dom vol → ( vol ‘ ( 𝑋 [,] 𝑌 ) ) = ( vol* ‘ ( 𝑋 [,] 𝑌 ) ) )
65 61 64 syl ⊢ ( 𝜑 → ( vol ‘ ( 𝑋 [,] 𝑌 ) ) = ( vol* ‘ ( 𝑋 [,] 𝑌 ) ) )
66 iccvolcl ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( vol ‘ ( 𝑋 [,] 𝑌 ) ) ∈ ℝ )
67 58 59 66 syl2anc ⊢ ( 𝜑 → ( vol ‘ ( 𝑋 [,] 𝑌 ) ) ∈ ℝ )
68 65 67 eqeltrrd ⊢ ( 𝜑 → ( vol* ‘ ( 𝑋 [,] 𝑌 ) ) ∈ ℝ )
69 ovolsscl ⊢ ( ( ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 ) ∧ ( 𝑋 [,] 𝑌 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑋 [,] 𝑌 ) ) ∈ ℝ ) → ( vol* ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ )
70 55 63 68 69 syl3anc ⊢ ( 𝜑 → ( vol* ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ )
71 53 70 eqeltrid ⊢ ( 𝜑 → ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ )
72 iblconst ⊢ ( ( ( 𝑋 (,) 𝑌 ) ∈ dom vol ∧ ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐶 ) ∈ ℂ ) → ( ( 𝑋 (,) 𝑌 ) × { ( 𝐹 ‘ 𝐶 ) } ) ∈ 𝐿1 )
73 43 71 49 72 syl3anc ⊢ ( 𝜑 → ( ( 𝑋 (,) 𝑌 ) × { ( 𝐹 ‘ 𝐶 ) } ) ∈ 𝐿1 )
74 51 73 eqeltrrid ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝐶 ) ) ∈ 𝐿1 )
75 41 47 50 74 iblsub ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ∈ 𝐿1 )
76 21 75 itgcl ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ∈ ℂ )
77 76 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ∈ ℂ )
78 59 58 resubcld ⊢ ( 𝜑 → ( 𝑌 − 𝑋 ) ∈ ℝ )
79 78 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝑌 − 𝑋 ) ∈ ℝ )
80 79 recnd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝑌 − 𝑋 ) ∈ ℂ )
81 58 59 posdifd ⊢ ( 𝜑 → ( 𝑋 < 𝑌 ↔ 0 < ( 𝑌 − 𝑋 ) ) )
82 81 biimpa ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 0 < ( 𝑌 − 𝑋 ) )
83 82 gt0ne0d ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝑌 − 𝑋 ) ≠ 0 )
84 77 80 83 divcld ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) ∈ ℂ )
85 49 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
86 ltle ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝑋 < 𝑌 → 𝑋 ≤ 𝑌 ) )
87 58 59 86 syl2anc ⊢ ( 𝜑 → ( 𝑋 < 𝑌 → 𝑋 ≤ 𝑌 ) )
88 87 imp ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 𝑋 ≤ 𝑌 )
89 1 2 3 4 5 6 7 39 17 19 ftc1lem1 ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
90 88 89 syldan ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
91 41 50 npcand ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) + ( 𝐹 ‘ 𝐶 ) ) = ( 𝐹 ‘ 𝑡 ) )
92 91 itgeq2dv ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) + ( 𝐹 ‘ 𝐶 ) ) d 𝑡 = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
93 41 50 subcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ∈ ℂ )
94 93 75 50 74 itgadd ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) + ( 𝐹 ‘ 𝐶 ) ) d 𝑡 = ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝐶 ) d 𝑡 ) )
95 92 94 eqtr3d ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝐶 ) d 𝑡 ) )
96 95 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝐶 ) d 𝑡 ) )
97 itgconst ⊢ ( ( ( 𝑋 (,) 𝑌 ) ∈ dom vol ∧ ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐶 ) ∈ ℂ ) → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝐶 ) d 𝑡 = ( ( 𝐹 ‘ 𝐶 ) · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) )
98 43 71 49 97 syl3anc ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝐶 ) d 𝑡 = ( ( 𝐹 ‘ 𝐶 ) · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) )
99 98 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝐶 ) d 𝑡 = ( ( 𝐹 ‘ 𝐶 ) · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) )
100 58 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 𝑋 ∈ ℝ )
101 59 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 𝑌 ∈ ℝ )
102 ovolioo ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ 𝑋 ≤ 𝑌 ) → ( vol* ‘ ( 𝑋 (,) 𝑌 ) ) = ( 𝑌 − 𝑋 ) )
103 100 101 88 102 syl3anc ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( vol* ‘ ( 𝑋 (,) 𝑌 ) ) = ( 𝑌 − 𝑋 ) )
104 53 103 eqtrid ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( vol ‘ ( 𝑋 (,) 𝑌 ) ) = ( 𝑌 − 𝑋 ) )
105 104 oveq2d ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( 𝐹 ‘ 𝐶 ) · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) = ( ( 𝐹 ‘ 𝐶 ) · ( 𝑌 − 𝑋 ) ) )
106 99 105 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝐶 ) d 𝑡 = ( ( 𝐹 ‘ 𝐶 ) · ( 𝑌 − 𝑋 ) ) )
107 106 oveq2d ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝐶 ) d 𝑡 ) = ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 + ( ( 𝐹 ‘ 𝐶 ) · ( 𝑌 − 𝑋 ) ) ) )
108 90 96 107 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) = ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 + ( ( 𝐹 ‘ 𝐶 ) · ( 𝑌 − 𝑋 ) ) ) )
109 108 oveq1d ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) = ( ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 + ( ( 𝐹 ‘ 𝐶 ) · ( 𝑌 − 𝑋 ) ) ) / ( 𝑌 − 𝑋 ) ) )
110 85 80 mulcld ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( 𝐹 ‘ 𝐶 ) · ( 𝑌 − 𝑋 ) ) ∈ ℂ )
111 77 110 80 83 divdird ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 + ( ( 𝐹 ‘ 𝐶 ) · ( 𝑌 − 𝑋 ) ) ) / ( 𝑌 − 𝑋 ) ) = ( ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) + ( ( ( 𝐹 ‘ 𝐶 ) · ( 𝑌 − 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) ) )
112 85 80 83 divcan4d ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ( 𝐹 ‘ 𝐶 ) · ( 𝑌 − 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) = ( 𝐹 ‘ 𝐶 ) )
113 112 oveq2d ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) + ( ( ( 𝐹 ‘ 𝐶 ) · ( 𝑌 − 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) ) = ( ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) + ( 𝐹 ‘ 𝐶 ) ) )
114 109 111 113 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) = ( ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) + ( 𝐹 ‘ 𝐶 ) ) )
115 84 85 114 mvrraddd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) − ( 𝐹 ‘ 𝐶 ) ) = ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) )
116 115 fveq2d ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) = ( abs ‘ ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) ) )
117 77 80 83 absdivd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) ) = ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) / ( abs ‘ ( 𝑌 − 𝑋 ) ) ) )
118 0re ⊢ 0 ∈ ℝ
119 ltle ⊢ ( ( 0 ∈ ℝ ∧ ( 𝑌 − 𝑋 ) ∈ ℝ ) → ( 0 < ( 𝑌 − 𝑋 ) → 0 ≤ ( 𝑌 − 𝑋 ) ) )
120 118 79 119 sylancr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 0 < ( 𝑌 − 𝑋 ) → 0 ≤ ( 𝑌 − 𝑋 ) ) )
121 82 120 mpd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 0 ≤ ( 𝑌 − 𝑋 ) )
122 79 121 absidd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ( 𝑌 − 𝑋 ) ) = ( 𝑌 − 𝑋 ) )
123 122 oveq2d ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) / ( abs ‘ ( 𝑌 − 𝑋 ) ) ) = ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) / ( 𝑌 − 𝑋 ) ) )
124 116 117 123 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) = ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) / ( 𝑌 − 𝑋 ) ) )
125 76 abscld ⊢ ( 𝜑 → ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) ∈ ℝ )
126 125 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) ∈ ℝ )
127 93 abscld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ∈ ℝ )
128 21 75 iblabs ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) ∈ 𝐿1 )
129 127 128 itgrecl ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 ∈ ℝ )
130 129 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 ∈ ℝ )
131 14 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
132 78 131 remulcld ⊢ ( 𝜑 → ( ( 𝑌 − 𝑋 ) · 𝐸 ) ∈ ℝ )
133 132 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( 𝑌 − 𝑋 ) · 𝐸 ) ∈ ℝ )
134 93 75 itgabs ⊢ ( 𝜑 → ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) ≤ ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 )
135 134 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) ≤ ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 )
136 82 104 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 0 < ( vol ‘ ( 𝑋 (,) 𝑌 ) ) )
137 131 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐸 ∈ ℝ )
138 fconstmpt ⊢ ( ( 𝑋 (,) 𝑌 ) × { 𝐸 } ) = ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 )
139 131 recnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
140 iblconst ⊢ ( ( ( 𝑋 (,) 𝑌 ) ∈ dom vol ∧ ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ ∧ 𝐸 ∈ ℂ ) → ( ( 𝑋 (,) 𝑌 ) × { 𝐸 } ) ∈ 𝐿1 )
141 43 71 139 140 syl3anc ⊢ ( 𝜑 → ( ( 𝑋 (,) 𝑌 ) × { 𝐸 } ) ∈ 𝐿1 )
142 138 141 eqeltrrid ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∈ 𝐿1 )
143 137 142 127 128 iblsub ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) ) ∈ 𝐿1 )
144 143 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) ) ∈ 𝐿1 )
145 6 48 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
146 15 rpred ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
147 145 146 resubcld ⊢ ( 𝜑 → ( 𝐶 − 𝑅 ) ∈ ℝ )
148 147 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐶 − 𝑅 ) ∈ ℝ )
149 58 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑋 ∈ ℝ )
150 37 6 sstrd ⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ ℝ )
151 150 sselda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑡 ∈ ℝ )
152 58 145 146 absdifltd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 − 𝐶 ) ) < 𝑅 ↔ ( ( 𝐶 − 𝑅 ) < 𝑋 ∧ 𝑋 < ( 𝐶 + 𝑅 ) ) ) )
153 18 152 mpbid ⊢ ( 𝜑 → ( ( 𝐶 − 𝑅 ) < 𝑋 ∧ 𝑋 < ( 𝐶 + 𝑅 ) ) )
154 153 simpld ⊢ ( 𝜑 → ( 𝐶 − 𝑅 ) < 𝑋 )
155 154 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐶 − 𝑅 ) < 𝑋 )
156 eliooord ⊢ ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) → ( 𝑋 < 𝑡 ∧ 𝑡 < 𝑌 ) )
157 156 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝑋 < 𝑡 ∧ 𝑡 < 𝑌 ) )
158 157 simpld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑋 < 𝑡 )
159 148 149 151 155 158 lttrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐶 − 𝑅 ) < 𝑡 )
160 59 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑌 ∈ ℝ )
161 145 146 readdcld ⊢ ( 𝜑 → ( 𝐶 + 𝑅 ) ∈ ℝ )
162 161 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐶 + 𝑅 ) ∈ ℝ )
163 157 simprd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑡 < 𝑌 )
164 59 145 146 absdifltd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑌 − 𝐶 ) ) < 𝑅 ↔ ( ( 𝐶 − 𝑅 ) < 𝑌 ∧ 𝑌 < ( 𝐶 + 𝑅 ) ) ) )
165 20 164 mpbid ⊢ ( 𝜑 → ( ( 𝐶 − 𝑅 ) < 𝑌 ∧ 𝑌 < ( 𝐶 + 𝑅 ) ) )
166 165 simprd ⊢ ( 𝜑 → 𝑌 < ( 𝐶 + 𝑅 ) )
167 166 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑌 < ( 𝐶 + 𝑅 ) )
168 151 160 162 163 167 lttrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑡 < ( 𝐶 + 𝑅 ) )
169 145 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐶 ∈ ℝ )
170 146 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑅 ∈ ℝ )
171 151 169 170 absdifltd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( abs ‘ ( 𝑡 − 𝐶 ) ) < 𝑅 ↔ ( ( 𝐶 − 𝑅 ) < 𝑡 ∧ 𝑡 < ( 𝐶 + 𝑅 ) ) ) )
172 159 168 171 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( abs ‘ ( 𝑡 − 𝐶 ) ) < 𝑅 )
173 fvoveq1 ⊢ ( 𝑦 = 𝑡 → ( abs ‘ ( 𝑦 − 𝐶 ) ) = ( abs ‘ ( 𝑡 − 𝐶 ) ) )
174 173 breq1d ⊢ ( 𝑦 = 𝑡 → ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑅 ↔ ( abs ‘ ( 𝑡 − 𝐶 ) ) < 𝑅 ) )
175 174 imbrov2fvoveq ⊢ ( 𝑦 = 𝑡 → ( ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 ) ↔ ( ( abs ‘ ( 𝑡 − 𝐶 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 ) ) )
176 16 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 ) )
177 176 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 ) )
178 175 177 38 rspcdva ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( abs ‘ ( 𝑡 − 𝐶 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 ) )
179 172 178 mpd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 )
180 difrp ⊢ ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ∈ ℝ ∧ 𝐸 ∈ ℝ ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 ↔ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) ∈ ℝ+ ) )
181 127 137 180 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 ↔ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) ∈ ℝ+ ) )
182 179 181 mpbid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) ∈ ℝ+ )
183 182 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑋 < 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) ∈ ℝ+ )
184 136 144 183 itggt0 ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 0 < ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) d 𝑡 )
185 137 142 127 128 itgsub ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) d 𝑡 = ( ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 ) )
186 185 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) d 𝑡 = ( ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 ) )
187 itgconst ⊢ ( ( ( 𝑋 (,) 𝑌 ) ∈ dom vol ∧ ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ ∧ 𝐸 ∈ ℂ ) → ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 = ( 𝐸 · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) )
188 43 71 139 187 syl3anc ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 = ( 𝐸 · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) )
189 188 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 = ( 𝐸 · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) )
190 104 oveq2d ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝐸 · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) = ( 𝐸 · ( 𝑌 − 𝑋 ) ) )
191 78 recnd ⊢ ( 𝜑 → ( 𝑌 − 𝑋 ) ∈ ℂ )
192 139 191 mulcomd ⊢ ( 𝜑 → ( 𝐸 · ( 𝑌 − 𝑋 ) ) = ( ( 𝑌 − 𝑋 ) · 𝐸 ) )
193 192 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝐸 · ( 𝑌 − 𝑋 ) ) = ( ( 𝑌 − 𝑋 ) · 𝐸 ) )
194 189 190 193 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 = ( ( 𝑌 − 𝑋 ) · 𝐸 ) )
195 194 oveq1d ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 ) = ( ( ( 𝑌 − 𝑋 ) · 𝐸 ) − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 ) )
196 186 195 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) d 𝑡 = ( ( ( 𝑌 − 𝑋 ) · 𝐸 ) − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 ) )
197 184 196 breqtrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 0 < ( ( ( 𝑌 − 𝑋 ) · 𝐸 ) − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 ) )
198 129 132 posdifd ⊢ ( 𝜑 → ( ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 < ( ( 𝑌 − 𝑋 ) · 𝐸 ) ↔ 0 < ( ( ( 𝑌 − 𝑋 ) · 𝐸 ) − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 ) ) )
199 198 biimpar ⊢ ( ( 𝜑 ∧ 0 < ( ( ( 𝑌 − 𝑋 ) · 𝐸 ) − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 ) ) → ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 < ( ( 𝑌 − 𝑋 ) · 𝐸 ) )
200 197 199 syldan ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 < ( ( 𝑌 − 𝑋 ) · 𝐸 ) )
201 126 130 133 135 200 lelttrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) < ( ( 𝑌 − 𝑋 ) · 𝐸 ) )
202 77 abscld ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) ∈ ℝ )
203 131 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 𝐸 ∈ ℝ )
204 ltdivmul ⊢ ( ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) ∈ ℝ ∧ 𝐸 ∈ ℝ ∧ ( ( 𝑌 − 𝑋 ) ∈ ℝ ∧ 0 < ( 𝑌 − 𝑋 ) ) ) → ( ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) / ( 𝑌 − 𝑋 ) ) < 𝐸 ↔ ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) < ( ( 𝑌 − 𝑋 ) · 𝐸 ) ) )
205 202 203 79 82 204 syl112anc ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) / ( 𝑌 − 𝑋 ) ) < 𝐸 ↔ ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) < ( ( 𝑌 − 𝑋 ) · 𝐸 ) ) )
206 201 205 mpbird ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) / ( 𝑌 − 𝑋 ) ) < 𝐸 )
207 124 206 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 )