Metamath Proof Explorer

Theorem ftc1cnnclem

Description: Lemma for ftc1cnnc ; cf. ftc1lem4 . The stronger assumptions of ftc1cn are exploited to make use of weaker theorems. (Contributed by Brendan Leahy, 19-Nov-2017)

Ref Expression
Hypotheses ftc1cnnc.g ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
ftc1cnnc.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ftc1cnnc.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ftc1cnnc.le ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
ftc1cnnc.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
ftc1cnnc.i ⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
ftc1cnnclem.c ⊢ ( 𝜑 → 𝑐 ∈ ( 𝐴 (,) 𝐵 ) )
ftc1cnnclem.h ⊢ 𝐻 = ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑧 − 𝑐 ) ) )
ftc1cnnclem.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
ftc1cnnclem.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
ftc1cnnclem.fc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( abs ‘ ( 𝑦 − 𝑐 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 ) )
ftc1cnnclem.x1 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 [,] 𝐵 ) )
ftc1cnnclem.x2 ⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝑐 ) ) < 𝑅 )
ftc1cnnclem.y1 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 [,] 𝐵 ) )
ftc1cnnclem.y2 ⊢ ( 𝜑 → ( abs ‘ ( 𝑌 − 𝑐 ) ) < 𝑅 )
Assertion ftc1cnnclem ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 )

Proof

Step Hyp Ref Expression
1 ftc1cnnc.g ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
2 ftc1cnnc.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 ftc1cnnc.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 ftc1cnnc.le ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
5 ftc1cnnc.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
6 ftc1cnnc.i ⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
7 ftc1cnnclem.c ⊢ ( 𝜑 → 𝑐 ∈ ( 𝐴 (,) 𝐵 ) )
8 ftc1cnnclem.h ⊢ 𝐻 = ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑧 − 𝑐 ) ) )
9 ftc1cnnclem.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
10 ftc1cnnclem.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
11 ftc1cnnclem.fc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( abs ‘ ( 𝑦 − 𝑐 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 ) )
12 ftc1cnnclem.x1 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 [,] 𝐵 ) )
13 ftc1cnnclem.x2 ⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝑐 ) ) < 𝑅 )
14 ftc1cnnclem.y1 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 [,] 𝐵 ) )
15 ftc1cnnclem.y2 ⊢ ( 𝜑 → ( abs ‘ ( 𝑌 − 𝑐 ) ) < 𝑅 )
16 ovexd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ∈ V )
17 2 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
18 3 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
19 elicc1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑋 ∈ ℝ* ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵 ) ) )
20 19 biimpa ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑋 ∈ ℝ* ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵 ) )
21 20 simp2d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ 𝑋 )
22 17 18 12 21 syl21anc ⊢ ( 𝜑 → 𝐴 ≤ 𝑋 )
23 iccleub ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑌 ≤ 𝐵 )
24 17 18 14 23 syl3anc ⊢ ( 𝜑 → 𝑌 ≤ 𝐵 )
25 ioossioo ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝑋 ∧ 𝑌 ≤ 𝐵 ) ) → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝐵 ) )
26 17 18 22 24 25 syl22anc ⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝐵 ) )
27 26 sselda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑡 ∈ ( 𝐴 (,) 𝐵 ) )
28 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
29 5 28 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
30 29 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
31 27 30 syldan ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
32 ioombl ⊢ ( 𝑋 (,) 𝑌 ) ∈ dom vol
33 32 a1i ⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ∈ dom vol )
34 fvexd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ V )
35 29 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑡 ) ) )
36 35 6 eqeltrrd ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
37 26 33 34 36 iblss ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
38 29 7 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑐 ) ∈ ℂ )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐹 ‘ 𝑐 ) ∈ ℂ )
40 fconstmpt ⊢ ( ( 𝑋 (,) 𝑌 ) × { ( 𝐹 ‘ 𝑐 ) } ) = ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝑐 ) )
41 mblvol ⊢ ( ( 𝑋 (,) 𝑌 ) ∈ dom vol → ( vol ‘ ( 𝑋 (,) 𝑌 ) ) = ( vol* ‘ ( 𝑋 (,) 𝑌 ) ) )
42 32 41 ax-mp ⊢ ( vol ‘ ( 𝑋 (,) 𝑌 ) ) = ( vol* ‘ ( 𝑋 (,) 𝑌 ) )
43 ioossicc ⊢ ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 )
44 43 a1i ⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 ) )
45 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
46 2 3 45 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
47 46 12 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
48 46 14 sseldd ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
49 iccmbl ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝑋 [,] 𝑌 ) ∈ dom vol )
50 47 48 49 syl2anc ⊢ ( 𝜑 → ( 𝑋 [,] 𝑌 ) ∈ dom vol )
51 mblss ⊢ ( ( 𝑋 [,] 𝑌 ) ∈ dom vol → ( 𝑋 [,] 𝑌 ) ⊆ ℝ )
52 50 51 syl ⊢ ( 𝜑 → ( 𝑋 [,] 𝑌 ) ⊆ ℝ )
53 mblvol ⊢ ( ( 𝑋 [,] 𝑌 ) ∈ dom vol → ( vol ‘ ( 𝑋 [,] 𝑌 ) ) = ( vol* ‘ ( 𝑋 [,] 𝑌 ) ) )
54 50 53 syl ⊢ ( 𝜑 → ( vol ‘ ( 𝑋 [,] 𝑌 ) ) = ( vol* ‘ ( 𝑋 [,] 𝑌 ) ) )
55 iccvolcl ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( vol ‘ ( 𝑋 [,] 𝑌 ) ) ∈ ℝ )
56 47 48 55 syl2anc ⊢ ( 𝜑 → ( vol ‘ ( 𝑋 [,] 𝑌 ) ) ∈ ℝ )
57 54 56 eqeltrrd ⊢ ( 𝜑 → ( vol* ‘ ( 𝑋 [,] 𝑌 ) ) ∈ ℝ )
58 ovolsscl ⊢ ( ( ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 ) ∧ ( 𝑋 [,] 𝑌 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑋 [,] 𝑌 ) ) ∈ ℝ ) → ( vol* ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ )
59 44 52 57 58 syl3anc ⊢ ( 𝜑 → ( vol* ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ )
60 42 59 eqeltrid ⊢ ( 𝜑 → ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ )
61 iblconst ⊢ ( ( ( 𝑋 (,) 𝑌 ) ∈ dom vol ∧ ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℂ ) → ( ( 𝑋 (,) 𝑌 ) × { ( 𝐹 ‘ 𝑐 ) } ) ∈ 𝐿1 )
62 33 60 38 61 syl3anc ⊢ ( 𝜑 → ( ( 𝑋 (,) 𝑌 ) × { ( 𝐹 ‘ 𝑐 ) } ) ∈ 𝐿1 )
63 40 62 eqeltrrid ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝑐 ) ) ∈ 𝐿1 )
64 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
65 64 subcn ⊢ − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
66 65 a1i ⊢ ( 𝜑 → − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
67 29 26 feqresmpt ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) = ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝑡 ) ) )
68 rescncf ⊢ ( ( 𝑋 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝐵 ) → ( 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) → ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ) )
69 26 5 68 sylc ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
70 67 69 eqeltrrd ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
71 ioossre ⊢ ( 𝑋 (,) 𝑌 ) ⊆ ℝ
72 ax-resscn ⊢ ℝ ⊆ ℂ
73 71 72 sstri ⊢ ( 𝑋 (,) 𝑌 ) ⊆ ℂ
74 ssid ⊢ ℂ ⊆ ℂ
75 cncfmptc ⊢ ( ( ( 𝐹 ‘ 𝑐 ) ∈ ℂ ∧ ( 𝑋 (,) 𝑌 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝑐 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
76 73 74 75 mp3an23 ⊢ ( ( 𝐹 ‘ 𝑐 ) ∈ ℂ → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝑐 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
77 38 76 syl ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝑐 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
78 64 66 70 77 cncfmpt2f ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
79 cnmbf ⊢ ( ( ( 𝑋 (,) 𝑌 ) ∈ dom vol ∧ ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ) → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ∈ MblFn )
80 32 78 79 sylancr ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ∈ MblFn )
81 31 37 39 63 80 iblsubnc ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ∈ 𝐿1 )
82 16 81 itgcl ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ∈ ℂ )
83 82 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ∈ ℂ )
84 48 47 resubcld ⊢ ( 𝜑 → ( 𝑌 − 𝑋 ) ∈ ℝ )
85 84 recnd ⊢ ( 𝜑 → ( 𝑌 − 𝑋 ) ∈ ℂ )
86 85 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝑌 − 𝑋 ) ∈ ℂ )
87 47 48 posdifd ⊢ ( 𝜑 → ( 𝑋 < 𝑌 ↔ 0 < ( 𝑌 − 𝑋 ) ) )
88 87 biimpa ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 0 < ( 𝑌 − 𝑋 ) )
89 88 gt0ne0d ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝑌 − 𝑋 ) ≠ 0 )
90 83 86 89 divcld ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) ∈ ℂ )
91 38 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝐹 ‘ 𝑐 ) ∈ ℂ )
92 ltle ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝑋 < 𝑌 → 𝑋 ≤ 𝑌 ) )
93 47 48 92 syl2anc ⊢ ( 𝜑 → ( 𝑋 < 𝑌 → 𝑋 ≤ 𝑌 ) )
94 93 imp ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 𝑋 ≤ 𝑌 )
95 ssidd ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 ) )
96 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
97 96 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
98 1 2 3 4 95 97 6 29 12 14 ftc1lem1 ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
99 94 98 syldan ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
100 31 39 npcand ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) + ( 𝐹 ‘ 𝑐 ) ) = ( 𝐹 ‘ 𝑡 ) )
101 100 itgeq2dv ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) + ( 𝐹 ‘ 𝑐 ) ) d 𝑡 = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
102 31 39 subcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ∈ ℂ )
103 100 mpteq2dva ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) + ( 𝐹 ‘ 𝑐 ) ) ) = ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝑡 ) ) )
104 103 67 eqtr4d ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) + ( 𝐹 ‘ 𝑐 ) ) ) = ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) )
105 iblmbf ⊢ ( 𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn )
106 6 105 syl ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
107 mbfres ⊢ ( ( 𝐹 ∈ MblFn ∧ ( 𝑋 (,) 𝑌 ) ∈ dom vol ) → ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ∈ MblFn )
108 106 32 107 sylancl ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ∈ MblFn )
109 104 108 eqeltrd ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) + ( 𝐹 ‘ 𝑐 ) ) ) ∈ MblFn )
110 102 81 39 63 109 itgaddnc ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) + ( 𝐹 ‘ 𝑐 ) ) d 𝑡 = ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑐 ) d 𝑡 ) )
111 101 110 eqtr3d ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑐 ) d 𝑡 ) )
112 111 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑐 ) d 𝑡 ) )
113 itgconst ⊢ ( ( ( 𝑋 (,) 𝑌 ) ∈ dom vol ∧ ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℂ ) → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑐 ) d 𝑡 = ( ( 𝐹 ‘ 𝑐 ) · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) )
114 33 60 38 113 syl3anc ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑐 ) d 𝑡 = ( ( 𝐹 ‘ 𝑐 ) · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) )
115 114 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑐 ) d 𝑡 = ( ( 𝐹 ‘ 𝑐 ) · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) )
116 47 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 𝑋 ∈ ℝ )
117 48 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 𝑌 ∈ ℝ )
118 ovolioo ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ 𝑋 ≤ 𝑌 ) → ( vol* ‘ ( 𝑋 (,) 𝑌 ) ) = ( 𝑌 − 𝑋 ) )
119 116 117 94 118 syl3anc ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( vol* ‘ ( 𝑋 (,) 𝑌 ) ) = ( 𝑌 − 𝑋 ) )
120 42 119 syl5eq ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( vol ‘ ( 𝑋 (,) 𝑌 ) ) = ( 𝑌 − 𝑋 ) )
121 120 oveq2d ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( 𝐹 ‘ 𝑐 ) · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) = ( ( 𝐹 ‘ 𝑐 ) · ( 𝑌 − 𝑋 ) ) )
122 115 121 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑐 ) d 𝑡 = ( ( 𝐹 ‘ 𝑐 ) · ( 𝑌 − 𝑋 ) ) )
123 122 oveq2d ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑐 ) d 𝑡 ) = ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 + ( ( 𝐹 ‘ 𝑐 ) · ( 𝑌 − 𝑋 ) ) ) )
124 99 112 123 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) = ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 + ( ( 𝐹 ‘ 𝑐 ) · ( 𝑌 − 𝑋 ) ) ) )
125 124 oveq1d ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) = ( ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 + ( ( 𝐹 ‘ 𝑐 ) · ( 𝑌 − 𝑋 ) ) ) / ( 𝑌 − 𝑋 ) ) )
126 91 86 mulcld ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( 𝐹 ‘ 𝑐 ) · ( 𝑌 − 𝑋 ) ) ∈ ℂ )
127 83 126 86 89 divdird ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 + ( ( 𝐹 ‘ 𝑐 ) · ( 𝑌 − 𝑋 ) ) ) / ( 𝑌 − 𝑋 ) ) = ( ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) + ( ( ( 𝐹 ‘ 𝑐 ) · ( 𝑌 − 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) ) )
128 91 86 89 divcan4d ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ( 𝐹 ‘ 𝑐 ) · ( 𝑌 − 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) = ( 𝐹 ‘ 𝑐 ) )
129 128 oveq2d ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) + ( ( ( 𝐹 ‘ 𝑐 ) · ( 𝑌 − 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) ) = ( ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) + ( 𝐹 ‘ 𝑐 ) ) )
130 125 127 129 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) = ( ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) + ( 𝐹 ‘ 𝑐 ) ) )
131 90 91 130 mvrraddd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) − ( 𝐹 ‘ 𝑐 ) ) = ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) )
132 131 fveq2d ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) − ( 𝐹 ‘ 𝑐 ) ) ) = ( abs ‘ ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) ) )
133 83 86 89 absdivd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) ) = ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) / ( abs ‘ ( 𝑌 − 𝑋 ) ) ) )
134 84 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝑌 − 𝑋 ) ∈ ℝ )
135 0re ⊢ 0 ∈ ℝ
136 ltle ⊢ ( ( 0 ∈ ℝ ∧ ( 𝑌 − 𝑋 ) ∈ ℝ ) → ( 0 < ( 𝑌 − 𝑋 ) → 0 ≤ ( 𝑌 − 𝑋 ) ) )
137 135 134 136 sylancr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 0 < ( 𝑌 − 𝑋 ) → 0 ≤ ( 𝑌 − 𝑋 ) ) )
138 88 137 mpd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 0 ≤ ( 𝑌 − 𝑋 ) )
139 134 138 absidd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ( 𝑌 − 𝑋 ) ) = ( 𝑌 − 𝑋 ) )
140 139 oveq2d ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) / ( abs ‘ ( 𝑌 − 𝑋 ) ) ) = ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) / ( 𝑌 − 𝑋 ) ) )
141 132 133 140 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) − ( 𝐹 ‘ 𝑐 ) ) ) = ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) / ( 𝑌 − 𝑋 ) ) )
142 83 abscld ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) ∈ ℝ )
143 102 abscld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ∈ ℝ )
144 cncfss ⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ℂ –cn→ ℝ ) ⊆ ( ℂ –cn→ ℂ ) )
145 72 74 144 mp2an ⊢ ( ℂ –cn→ ℝ ) ⊆ ( ℂ –cn→ ℂ )
146 abscncf ⊢ abs ∈ ( ℂ –cn→ ℝ )
147 145 146 sselii ⊢ abs ∈ ( ℂ –cn→ ℂ )
148 147 a1i ⊢ ( 𝜑 → abs ∈ ( ℂ –cn→ ℂ ) )
149 148 78 cncfmpt1f ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
150 cnmbf ⊢ ( ( ( 𝑋 (,) 𝑌 ) ∈ dom vol ∧ ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ) → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ MblFn )
151 32 149 150 sylancr ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ MblFn )
152 16 81 151 iblabsnc ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ 𝐿1 )
153 143 152 itgrecl ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 ∈ ℝ )
154 153 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 ∈ ℝ )
155 9 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
156 84 155 remulcld ⊢ ( 𝜑 → ( ( 𝑌 − 𝑋 ) · 𝐸 ) ∈ ℝ )
157 156 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( 𝑌 − 𝑋 ) · 𝐸 ) ∈ ℝ )
158 82 cjcld ⊢ ( 𝜑 → ( ∗ ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) ∈ ℂ )
159 cncfmptc ⊢ ( ( ( ∗ ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) ∈ ℂ ∧ ( 𝑋 (,) 𝑌 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ∗ ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
160 73 74 159 mp3an23 ⊢ ( ( ∗ ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) ∈ ℂ → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ∗ ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
161 158 160 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ∗ ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
162 nfcv ⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) )
163 nfcsb1v ⊢ Ⅎ 𝑡 ⦋ 𝑥 / 𝑡 ⦌ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) )
164 csbeq1a ⊢ ( 𝑡 = 𝑥 → ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) = ⦋ 𝑥 / 𝑡 ⦌ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) )
165 162 163 164 cbvmpt ⊢ ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ⦋ 𝑥 / 𝑡 ⦌ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) )
166 165 78 eqeltrrid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ⦋ 𝑥 / 𝑡 ⦌ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
167 161 166 mulcncf ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( ∗ ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) · ⦋ 𝑥 / 𝑡 ⦌ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
168 cnmbf ⊢ ( ( ( 𝑋 (,) 𝑌 ) ∈ dom vol ∧ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( ∗ ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) · ⦋ 𝑥 / 𝑡 ⦌ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ) → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( ∗ ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) · ⦋ 𝑥 / 𝑡 ⦌ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ MblFn )
169 32 167 168 sylancr ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( ∗ ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) · ⦋ 𝑥 / 𝑡 ⦌ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ MblFn )
170 102 81 151 169 itgabsnc ⊢ ( 𝜑 → ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) ≤ ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 )
171 170 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) ≤ ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 )
172 simpr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 𝑋 < 𝑌 )
173 155 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐸 ∈ ℝ )
174 fconstmpt ⊢ ( ( 𝑋 (,) 𝑌 ) × { 𝐸 } ) = ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 )
175 9 rpcnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
176 iblconst ⊢ ( ( ( 𝑋 (,) 𝑌 ) ∈ dom vol ∧ ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ ∧ 𝐸 ∈ ℂ ) → ( ( 𝑋 (,) 𝑌 ) × { 𝐸 } ) ∈ 𝐿1 )
177 33 60 175 176 syl3anc ⊢ ( 𝜑 → ( ( 𝑋 (,) 𝑌 ) × { 𝐸 } ) ∈ 𝐿1 )
178 174 177 eqeltrrid ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∈ 𝐿1 )
179 cncfmptc ⊢ ( ( 𝐸 ∈ ℂ ∧ ( 𝑋 (,) 𝑌 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
180 73 74 179 mp3an23 ⊢ ( 𝐸 ∈ ℂ → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
181 175 180 syl ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
182 64 66 181 149 cncfmpt2f ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
183 cnmbf ⊢ ( ( ( 𝑋 (,) 𝑌 ) ∈ dom vol ∧ ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ) → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ) ∈ MblFn )
184 32 182 183 sylancr ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ) ∈ MblFn )
185 173 178 143 152 184 iblsubnc ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ) ∈ 𝐿1 )
186 185 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ) ∈ 𝐿1 )
187 11 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝑐 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 ) )
188 187 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝑐 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 ) )
189 96 7 sseldi ⊢ ( 𝜑 → 𝑐 ∈ ℝ )
190 10 rpred ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
191 189 190 resubcld ⊢ ( 𝜑 → ( 𝑐 − 𝑅 ) ∈ ℝ )
192 191 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝑐 − 𝑅 ) ∈ ℝ )
193 47 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑋 ∈ ℝ )
194 elioore ⊢ ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) → 𝑡 ∈ ℝ )
195 194 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑡 ∈ ℝ )
196 47 189 190 absdifltd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 − 𝑐 ) ) < 𝑅 ↔ ( ( 𝑐 − 𝑅 ) < 𝑋 ∧ 𝑋 < ( 𝑐 + 𝑅 ) ) ) )
197 13 196 mpbid ⊢ ( 𝜑 → ( ( 𝑐 − 𝑅 ) < 𝑋 ∧ 𝑋 < ( 𝑐 + 𝑅 ) ) )
198 197 simpld ⊢ ( 𝜑 → ( 𝑐 − 𝑅 ) < 𝑋 )
199 198 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝑐 − 𝑅 ) < 𝑋 )
200 eliooord ⊢ ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) → ( 𝑋 < 𝑡 ∧ 𝑡 < 𝑌 ) )
201 200 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝑋 < 𝑡 ∧ 𝑡 < 𝑌 ) )
202 201 simpld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑋 < 𝑡 )
203 192 193 195 199 202 lttrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝑐 − 𝑅 ) < 𝑡 )
204 48 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑌 ∈ ℝ )
205 189 190 readdcld ⊢ ( 𝜑 → ( 𝑐 + 𝑅 ) ∈ ℝ )
206 205 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝑐 + 𝑅 ) ∈ ℝ )
207 201 simprd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑡 < 𝑌 )
208 48 189 190 absdifltd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑌 − 𝑐 ) ) < 𝑅 ↔ ( ( 𝑐 − 𝑅 ) < 𝑌 ∧ 𝑌 < ( 𝑐 + 𝑅 ) ) ) )
209 15 208 mpbid ⊢ ( 𝜑 → ( ( 𝑐 − 𝑅 ) < 𝑌 ∧ 𝑌 < ( 𝑐 + 𝑅 ) ) )
210 209 simprd ⊢ ( 𝜑 → 𝑌 < ( 𝑐 + 𝑅 ) )
211 210 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑌 < ( 𝑐 + 𝑅 ) )
212 195 204 206 207 211 lttrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑡 < ( 𝑐 + 𝑅 ) )
213 189 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑐 ∈ ℝ )
214 190 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑅 ∈ ℝ )
215 195 213 214 absdifltd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( abs ‘ ( 𝑡 − 𝑐 ) ) < 𝑅 ↔ ( ( 𝑐 − 𝑅 ) < 𝑡 ∧ 𝑡 < ( 𝑐 + 𝑅 ) ) ) )
216 203 212 215 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( abs ‘ ( 𝑡 − 𝑐 ) ) < 𝑅 )
217 fvoveq1 ⊢ ( 𝑦 = 𝑡 → ( abs ‘ ( 𝑦 − 𝑐 ) ) = ( abs ‘ ( 𝑡 − 𝑐 ) ) )
218 217 breq1d ⊢ ( 𝑦 = 𝑡 → ( ( abs ‘ ( 𝑦 − 𝑐 ) ) < 𝑅 ↔ ( abs ‘ ( 𝑡 − 𝑐 ) ) < 𝑅 ) )
219 218 imbrov2fvoveq ⊢ ( 𝑦 = 𝑡 → ( ( ( abs ‘ ( 𝑦 − 𝑐 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 ) ↔ ( ( abs ‘ ( 𝑡 − 𝑐 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 ) ) )
220 219 rspcv ⊢ ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) → ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝑐 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 ) → ( ( abs ‘ ( 𝑡 − 𝑐 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 ) ) )
221 27 188 216 220 syl3c ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 )
222 difrp ⊢ ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ∈ ℝ ∧ 𝐸 ∈ ℝ ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 ↔ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ ℝ+ ) )
223 143 173 222 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 ↔ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ ℝ+ ) )
224 221 223 mpbid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ ℝ+ )
225 224 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑋 < 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ ℝ+ )
226 182 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
227 172 186 225 226 itggt0cn ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 0 < ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) d 𝑡 )
228 173 178 143 152 184 itgsubnc ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) d 𝑡 = ( ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 ) )
229 228 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) d 𝑡 = ( ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 ) )
230 itgconst ⊢ ( ( ( 𝑋 (,) 𝑌 ) ∈ dom vol ∧ ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ ∧ 𝐸 ∈ ℂ ) → ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 = ( 𝐸 · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) )
231 33 60 175 230 syl3anc ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 = ( 𝐸 · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) )
232 231 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 = ( 𝐸 · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) )
233 120 oveq2d ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝐸 · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) = ( 𝐸 · ( 𝑌 − 𝑋 ) ) )
234 175 85 mulcomd ⊢ ( 𝜑 → ( 𝐸 · ( 𝑌 − 𝑋 ) ) = ( ( 𝑌 − 𝑋 ) · 𝐸 ) )
235 234 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝐸 · ( 𝑌 − 𝑋 ) ) = ( ( 𝑌 − 𝑋 ) · 𝐸 ) )
236 232 233 235 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 = ( ( 𝑌 − 𝑋 ) · 𝐸 ) )
237 236 oveq1d ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 ) = ( ( ( 𝑌 − 𝑋 ) · 𝐸 ) − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 ) )
238 229 237 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) d 𝑡 = ( ( ( 𝑌 − 𝑋 ) · 𝐸 ) − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 ) )
239 227 238 breqtrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 0 < ( ( ( 𝑌 − 𝑋 ) · 𝐸 ) − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 ) )
240 153 156 posdifd ⊢ ( 𝜑 → ( ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 < ( ( 𝑌 − 𝑋 ) · 𝐸 ) ↔ 0 < ( ( ( 𝑌 − 𝑋 ) · 𝐸 ) − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 ) ) )
241 240 biimpar ⊢ ( ( 𝜑 ∧ 0 < ( ( ( 𝑌 − 𝑋 ) · 𝐸 ) − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 ) ) → ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 < ( ( 𝑌 − 𝑋 ) · 𝐸 ) )
242 239 241 syldan ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 < ( ( 𝑌 − 𝑋 ) · 𝐸 ) )
243 142 154 157 171 242 lelttrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) < ( ( 𝑌 − 𝑋 ) · 𝐸 ) )
244 155 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 𝐸 ∈ ℝ )
245 ltdivmul ⊢ ( ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) ∈ ℝ ∧ 𝐸 ∈ ℝ ∧ ( ( 𝑌 − 𝑋 ) ∈ ℝ ∧ 0 < ( 𝑌 − 𝑋 ) ) ) → ( ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) / ( 𝑌 − 𝑋 ) ) < 𝐸 ↔ ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) < ( ( 𝑌 − 𝑋 ) · 𝐸 ) ) )
246 142 244 134 88 245 syl112anc ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) / ( 𝑌 − 𝑋 ) ) < 𝐸 ↔ ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) < ( ( 𝑌 − 𝑋 ) · 𝐸 ) ) )
247 243 246 mpbird ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) / ( 𝑌 − 𝑋 ) ) < 𝐸 )
248 141 247 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 )