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 
|- G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )
ftc1cnnc.a 
|- ( ph -> A e. RR )
ftc1cnnc.b 
|- ( ph -> B e. RR )
ftc1cnnc.le 
|- ( ph -> A <_ B )
ftc1cnnc.f 
|- ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
ftc1cnnc.i 
|- ( ph -> F e. L^1 )
ftc1cnnclem.c 
|- ( ph -> c e. ( A (,) B ) )
ftc1cnnclem.h 
|- H = ( z e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` z ) - ( G ` c ) ) / ( z - c ) ) )
ftc1cnnclem.e 
|- ( ph -> E e. RR+ )
ftc1cnnclem.r 
|- ( ph -> R e. RR+ )
ftc1cnnclem.fc 
|- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( abs ` ( y - c ) ) < R -> ( abs ` ( ( F ` y ) - ( F ` c ) ) ) < E ) )
ftc1cnnclem.x1 
|- ( ph -> X e. ( A [,] B ) )
ftc1cnnclem.x2 
|- ( ph -> ( abs ` ( X - c ) ) < R )
ftc1cnnclem.y1 
|- ( ph -> Y e. ( A [,] B ) )
ftc1cnnclem.y2 
|- ( ph -> ( abs ` ( Y - c ) ) < R )
Assertion ftc1cnnclem 
|- ( ( ph /\ X < Y ) -> ( abs ` ( ( ( ( G ` Y ) - ( G ` X ) ) / ( Y - X ) ) - ( F ` c ) ) ) < E )

Proof

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