Metamath Proof Explorer

Theorem ftc1lem4

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

Ref Expression
Hypotheses ftc1.g 
|- G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )
ftc1.a 
|- ( ph -> A e. RR )
ftc1.b 
|- ( ph -> B e. RR )
ftc1.le 
|- ( ph -> A <_ B )
ftc1.s 
|- ( ph -> ( A (,) B ) C_ D )
ftc1.d 
|- ( ph -> D C_ RR )
ftc1.i 
|- ( ph -> F e. L^1 )
ftc1.c 
|- ( ph -> C e. ( A (,) B ) )
ftc1.f 
|- ( ph -> F e. ( ( K CnP L ) ` C ) )
ftc1.j 
|- J = ( L |`t RR )
ftc1.k 
|- K = ( L |`t D )
ftc1.l 
|- L = ( TopOpen ` CCfld )
ftc1.h 
|- H = ( z e. ( ( A [,] B ) \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) )
ftc1.e 
|- ( ph -> E e. RR+ )
ftc1.r 
|- ( ph -> R e. RR+ )
ftc1.fc 
|- ( ( ph /\ y e. D ) -> ( ( abs ` ( y - C ) ) < R -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < E ) )
ftc1.x1 
|- ( ph -> X e. ( A [,] B ) )
ftc1.x2 
|- ( ph -> ( abs ` ( X - C ) ) < R )
ftc1.y1 
|- ( ph -> Y e. ( A [,] B ) )
ftc1.y2 
|- ( ph -> ( abs ` ( Y - C ) ) < R )
Assertion ftc1lem4 
|- ( ( ph /\ X < Y ) -> ( abs ` ( ( ( ( G ` Y ) - ( G ` X ) ) / ( Y - X ) ) - ( F ` C ) ) ) < E )

Proof

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