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

Metamath Proof Explorer

Theorem ftc1a

Description: The Fundamental Theorem of Calculus, part one. The function G formed by varying the right endpoint of an integral of F is continuous if F is integrable. (Contributed by Mario Carneiro, 1-Sep-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 )
ftc1a.f 
|- ( ph -> F : D --> CC )
Assertion ftc1a 
|- ( ph -> G e. ( ( A [,] B ) -cn-> CC ) )

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 ftc1a.f 
 |-  ( ph -> F : D --> CC )
9 1 2 3 4 5 6 7 8 ftc1lem2 
 |-  ( ph -> G : ( A [,] B ) --> CC )
10 fvexd 
 |-  ( ( ( ph /\ e e. RR+ ) /\ w e. D ) -> ( F ` w ) e. _V )
11 8 feqmptd 
 |-  ( ph -> F = ( w e. D |-> ( F ` w ) ) )
12 11 7 eqeltrrd 
 |-  ( ph -> ( w e. D |-> ( F ` w ) ) e. L^1 )
13 12 adantr 
 |-  ( ( ph /\ e e. RR+ ) -> ( w e. D |-> ( F ` w ) ) e. L^1 )
14 simpr 
 |-  ( ( ph /\ e e. RR+ ) -> e e. RR+ )
15 10 13 14 itgcn 
 |-  ( ( ph /\ e e. RR+ ) -> E. d e. RR+ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) )
16 oveq12 
 |-  ( ( s = z /\ r = y ) -> ( s - r ) = ( z - y ) )
17 16 fveq2d 
 |-  ( ( s = z /\ r = y ) -> ( abs ` ( s - r ) ) = ( abs ` ( z - y ) ) )
18 17 breq1d 
 |-  ( ( s = z /\ r = y ) -> ( ( abs ` ( s - r ) ) < d <-> ( abs ` ( z - y ) ) < d ) )
19 fveq2 
 |-  ( s = z -> ( G ` s ) = ( G ` z ) )
20 fveq2 
 |-  ( r = y -> ( G ` r ) = ( G ` y ) )
21 19 20 oveqan12d 
 |-  ( ( s = z /\ r = y ) -> ( ( G ` s ) - ( G ` r ) ) = ( ( G ` z ) - ( G ` y ) ) )
22 21 fveq2d 
 |-  ( ( s = z /\ r = y ) -> ( abs ` ( ( G ` s ) - ( G ` r ) ) ) = ( abs ` ( ( G ` z ) - ( G ` y ) ) ) )
23 22 breq1d 
 |-  ( ( s = z /\ r = y ) -> ( ( abs ` ( ( G ` s ) - ( G ` r ) ) ) < e <-> ( abs ` ( ( G ` z ) - ( G ` y ) ) ) < e ) )
24 18 23 imbi12d 
 |-  ( ( s = z /\ r = y ) -> ( ( ( abs ` ( s - r ) ) < d -> ( abs ` ( ( G ` s ) - ( G ` r ) ) ) < e ) <-> ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( G ` z ) - ( G ` y ) ) ) < e ) ) )
25 24 ancoms 
 |-  ( ( r = y /\ s = z ) -> ( ( ( abs ` ( s - r ) ) < d -> ( abs ` ( ( G ` s ) - ( G ` r ) ) ) < e ) <-> ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( G ` z ) - ( G ` y ) ) ) < e ) ) )
26 oveq12 
 |-  ( ( s = y /\ r = z ) -> ( s - r ) = ( y - z ) )
27 26 fveq2d 
 |-  ( ( s = y /\ r = z ) -> ( abs ` ( s - r ) ) = ( abs ` ( y - z ) ) )
28 27 breq1d 
 |-  ( ( s = y /\ r = z ) -> ( ( abs ` ( s - r ) ) < d <-> ( abs ` ( y - z ) ) < d ) )
29 fveq2 
 |-  ( s = y -> ( G ` s ) = ( G ` y ) )
30 fveq2 
 |-  ( r = z -> ( G ` r ) = ( G ` z ) )
31 29 30 oveqan12d 
 |-  ( ( s = y /\ r = z ) -> ( ( G ` s ) - ( G ` r ) ) = ( ( G ` y ) - ( G ` z ) ) )
32 31 fveq2d 
 |-  ( ( s = y /\ r = z ) -> ( abs ` ( ( G ` s ) - ( G ` r ) ) ) = ( abs ` ( ( G ` y ) - ( G ` z ) ) ) )
33 32 breq1d 
 |-  ( ( s = y /\ r = z ) -> ( ( abs ` ( ( G ` s ) - ( G ` r ) ) ) < e <-> ( abs ` ( ( G ` y ) - ( G ` z ) ) ) < e ) )
34 28 33 imbi12d 
 |-  ( ( s = y /\ r = z ) -> ( ( ( abs ` ( s - r ) ) < d -> ( abs ` ( ( G ` s ) - ( G ` r ) ) ) < e ) <-> ( ( abs ` ( y - z ) ) < d -> ( abs ` ( ( G ` y ) - ( G ` z ) ) ) < e ) ) )
35 34 ancoms 
 |-  ( ( r = z /\ s = y ) -> ( ( ( abs ` ( s - r ) ) < d -> ( abs ` ( ( G ` s ) - ( G ` r ) ) ) < e ) <-> ( ( abs ` ( y - z ) ) < d -> ( abs ` ( ( G ` y ) - ( G ` z ) ) ) < e ) ) )
36 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
37 2 3 36 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
38 37 ad2antrr 
 |-  ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) -> ( A [,] B ) C_ RR )
39 37 ad3antrrr 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) ) ) -> ( A [,] B ) C_ RR )
40 simprr 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) ) ) -> z e. ( A [,] B ) )
41 39 40 sseldd 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) ) ) -> z e. RR )
42 41 recnd 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) ) ) -> z e. CC )
43 simprl 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) ) ) -> y e. ( A [,] B ) )
44 39 43 sseldd 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) ) ) -> y e. RR )
45 44 recnd 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) ) ) -> y e. CC )
46 42 45 abssubd 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) ) ) -> ( abs ` ( z - y ) ) = ( abs ` ( y - z ) ) )
47 46 breq1d 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) ) ) -> ( ( abs ` ( z - y ) ) < d <-> ( abs ` ( y - z ) ) < d ) )
48 9 ad3antrrr 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) ) ) -> G : ( A [,] B ) --> CC )
49 48 40 ffvelcdmd 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) ) ) -> ( G ` z ) e. CC )
50 48 43 ffvelcdmd 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) ) ) -> ( G ` y ) e. CC )
51 49 50 abssubd 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) ) ) -> ( abs ` ( ( G ` z ) - ( G ` y ) ) ) = ( abs ` ( ( G ` y ) - ( G ` z ) ) ) )
52 51 breq1d 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) ) ) -> ( ( abs ` ( ( G ` z ) - ( G ` y ) ) ) < e <-> ( abs ` ( ( G ` y ) - ( G ` z ) ) ) < e ) )
53 47 52 imbi12d 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) ) ) -> ( ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( G ` z ) - ( G ` y ) ) ) < e ) <-> ( ( abs ` ( y - z ) ) < d -> ( abs ` ( ( G ` y ) - ( G ` z ) ) ) < e ) ) )
54 simpr3 
 |-  ( ( ph /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) ) -> y <_ z )
55 2 adantr 
 |-  ( ( ph /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) ) -> A e. RR )
56 3 adantr 
 |-  ( ( ph /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) ) -> B e. RR )
57 4 adantr 
 |-  ( ( ph /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) ) -> A <_ B )
58 5 adantr 
 |-  ( ( ph /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) ) -> ( A (,) B ) C_ D )
59 6 adantr 
 |-  ( ( ph /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) ) -> D C_ RR )
60 7 adantr 
 |-  ( ( ph /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) ) -> F e. L^1 )
61 8 adantr 
 |-  ( ( ph /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) ) -> F : D --> CC )
62 simpr1 
 |-  ( ( ph /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) ) -> y e. ( A [,] B ) )
63 simpr2 
 |-  ( ( ph /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) ) -> z e. ( A [,] B ) )
64 1 55 56 57 58 59 60 61 62 63 ftc1lem1 
 |-  ( ( ( ph /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) ) /\ y <_ z ) -> ( ( G ` z ) - ( G ` y ) ) = S. ( y (,) z ) ( F ` t ) _d t )
65 54 64 mpdan 
 |-  ( ( ph /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) ) -> ( ( G ` z ) - ( G ` y ) ) = S. ( y (,) z ) ( F ` t ) _d t )
66 65 adantlr 
 |-  ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) ) -> ( ( G ` z ) - ( G ` y ) ) = S. ( y (,) z ) ( F ` t ) _d t )
67 66 ad2ant2r 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( ( G ` z ) - ( G ` y ) ) = S. ( y (,) z ) ( F ` t ) _d t )
68 67 fveq2d 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( abs ` ( ( G ` z ) - ( G ` y ) ) ) = ( abs ` S. ( y (,) z ) ( F ` t ) _d t ) )
69 fvexd 
 |-  ( ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) /\ t e. ( y (,) z ) ) -> ( F ` t ) e. _V )
70 2 ad3antrrr 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> A e. RR )
71 70 rexrd 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> A e. RR* )
72 simprl1 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> y e. ( A [,] B ) )
73 3 ad3antrrr 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> B e. RR )
74 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( y e. ( A [,] B ) <-> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
75 70 73 74 syl2anc 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( y e. ( A [,] B ) <-> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
76 72 75 mpbid 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( y e. RR /\ A <_ y /\ y <_ B ) )
77 76 simp2d 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> A <_ y )
78 iooss1 
 |-  ( ( A e. RR* /\ A <_ y ) -> ( y (,) z ) C_ ( A (,) z ) )
79 71 77 78 syl2anc 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( y (,) z ) C_ ( A (,) z ) )
80 73 rexrd 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> B e. RR* )
81 simprl2 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> z e. ( A [,] B ) )
82 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( z e. ( A [,] B ) <-> ( z e. RR /\ A <_ z /\ z <_ B ) ) )
83 70 73 82 syl2anc 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( z e. ( A [,] B ) <-> ( z e. RR /\ A <_ z /\ z <_ B ) ) )
84 81 83 mpbid 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( z e. RR /\ A <_ z /\ z <_ B ) )
85 84 simp3d 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> z <_ B )
86 iooss2 
 |-  ( ( B e. RR* /\ z <_ B ) -> ( A (,) z ) C_ ( A (,) B ) )
87 80 85 86 syl2anc 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( A (,) z ) C_ ( A (,) B ) )
88 79 87 sstrd 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( y (,) z ) C_ ( A (,) B ) )
89 5 ad3antrrr 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( A (,) B ) C_ D )
90 88 89 sstrd 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( y (,) z ) C_ D )
91 ioombl 
 |-  ( y (,) z ) e. dom vol
92 91 a1i 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( y (,) z ) e. dom vol )
93 fvexd 
 |-  ( ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) /\ t e. D ) -> ( F ` t ) e. _V )
94 8 feqmptd 
 |-  ( ph -> F = ( t e. D |-> ( F ` t ) ) )
95 94 7 eqeltrrd 
 |-  ( ph -> ( t e. D |-> ( F ` t ) ) e. L^1 )
96 95 ad3antrrr 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( t e. D |-> ( F ` t ) ) e. L^1 )
97 90 92 93 96 iblss 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( t e. ( y (,) z ) |-> ( F ` t ) ) e. L^1 )
98 69 97 itgcl 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> S. ( y (,) z ) ( F ` t ) _d t e. CC )
99 98 abscld 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( abs ` S. ( y (,) z ) ( F ` t ) _d t ) e. RR )
100 iblmbf 
 |-  ( ( t e. ( y (,) z ) |-> ( F ` t ) ) e. L^1 -> ( t e. ( y (,) z ) |-> ( F ` t ) ) e. MblFn )
101 97 100 syl 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( t e. ( y (,) z ) |-> ( F ` t ) ) e. MblFn )
102 101 69 mbfmptcl 
 |-  ( ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) /\ t e. ( y (,) z ) ) -> ( F ` t ) e. CC )
103 102 abscld 
 |-  ( ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) /\ t e. ( y (,) z ) ) -> ( abs ` ( F ` t ) ) e. RR )
104 69 97 iblabs 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( t e. ( y (,) z ) |-> ( abs ` ( F ` t ) ) ) e. L^1 )
105 103 104 itgrecl 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> S. ( y (,) z ) ( abs ` ( F ` t ) ) _d t e. RR )
106 simprl 
 |-  ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) -> e e. RR+ )
107 106 ad2antrr 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> e e. RR+ )
108 107 rpred 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> e e. RR )
109 69 97 itgabs 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( abs ` S. ( y (,) z ) ( F ` t ) _d t ) <_ S. ( y (,) z ) ( abs ` ( F ` t ) ) _d t )
110 mblvol 
 |-  ( ( y (,) z ) e. dom vol -> ( vol ` ( y (,) z ) ) = ( vol* ` ( y (,) z ) ) )
111 91 110 ax-mp 
 |-  ( vol ` ( y (,) z ) ) = ( vol* ` ( y (,) z ) )
112 ioossre 
 |-  ( y (,) z ) C_ RR
113 ovolcl 
 |-  ( ( y (,) z ) C_ RR -> ( vol* ` ( y (,) z ) ) e. RR* )
114 112 113 mp1i 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( vol* ` ( y (,) z ) ) e. RR* )
115 84 simp1d 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> z e. RR )
116 76 simp1d 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> y e. RR )
117 115 116 resubcld 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( z - y ) e. RR )
118 117 rexrd 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( z - y ) e. RR* )
119 simprr 
 |-  ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) -> d e. RR+ )
120 119 ad2antrr 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> d e. RR+ )
121 120 rpxrd 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> d e. RR* )
122 ioossicc 
 |-  ( y (,) z ) C_ ( y [,] z )
123 iccssre 
 |-  ( ( y e. RR /\ z e. RR ) -> ( y [,] z ) C_ RR )
124 116 115 123 syl2anc 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( y [,] z ) C_ RR )
125 ovolss 
 |-  ( ( ( y (,) z ) C_ ( y [,] z ) /\ ( y [,] z ) C_ RR ) -> ( vol* ` ( y (,) z ) ) <_ ( vol* ` ( y [,] z ) ) )
126 122 124 125 sylancr 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( vol* ` ( y (,) z ) ) <_ ( vol* ` ( y [,] z ) ) )
127 simprl3 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> y <_ z )
128 ovolicc 
 |-  ( ( y e. RR /\ z e. RR /\ y <_ z ) -> ( vol* ` ( y [,] z ) ) = ( z - y ) )
129 116 115 127 128 syl3anc 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( vol* ` ( y [,] z ) ) = ( z - y ) )
130 126 129 breqtrd 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( vol* ` ( y (,) z ) ) <_ ( z - y ) )
131 116 115 127 abssubge0d 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( abs ` ( z - y ) ) = ( z - y ) )
132 simprr 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( abs ` ( z - y ) ) < d )
133 131 132 eqbrtrrd 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( z - y ) < d )
134 114 118 121 130 133 xrlelttrd 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( vol* ` ( y (,) z ) ) < d )
135 111 134 eqbrtrid 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( vol ` ( y (,) z ) ) < d )
136 sseq1 
 |-  ( u = ( y (,) z ) -> ( u C_ D <-> ( y (,) z ) C_ D ) )
137 fveq2 
 |-  ( u = ( y (,) z ) -> ( vol ` u ) = ( vol ` ( y (,) z ) ) )
138 137 breq1d 
 |-  ( u = ( y (,) z ) -> ( ( vol ` u ) < d <-> ( vol ` ( y (,) z ) ) < d ) )
139 136 138 anbi12d 
 |-  ( u = ( y (,) z ) -> ( ( u C_ D /\ ( vol ` u ) < d ) <-> ( ( y (,) z ) C_ D /\ ( vol ` ( y (,) z ) ) < d ) ) )
140 2fveq3 
 |-  ( w = t -> ( abs ` ( F ` w ) ) = ( abs ` ( F ` t ) ) )
141 140 cbvitgv 
 |-  S. u ( abs ` ( F ` w ) ) _d w = S. u ( abs ` ( F ` t ) ) _d t
142 itgeq1 
 |-  ( u = ( y (,) z ) -> S. u ( abs ` ( F ` t ) ) _d t = S. ( y (,) z ) ( abs ` ( F ` t ) ) _d t )
143 141 142 eqtrid 
 |-  ( u = ( y (,) z ) -> S. u ( abs ` ( F ` w ) ) _d w = S. ( y (,) z ) ( abs ` ( F ` t ) ) _d t )
144 143 breq1d 
 |-  ( u = ( y (,) z ) -> ( S. u ( abs ` ( F ` w ) ) _d w < e <-> S. ( y (,) z ) ( abs ` ( F ` t ) ) _d t < e ) )
145 139 144 imbi12d 
 |-  ( u = ( y (,) z ) -> ( ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) <-> ( ( ( y (,) z ) C_ D /\ ( vol ` ( y (,) z ) ) < d ) -> S. ( y (,) z ) ( abs ` ( F ` t ) ) _d t < e ) ) )
146 simplr 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) )
147 145 146 92 rspcdva 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( ( ( y (,) z ) C_ D /\ ( vol ` ( y (,) z ) ) < d ) -> S. ( y (,) z ) ( abs ` ( F ` t ) ) _d t < e ) )
148 90 135 147 mp2and 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> S. ( y (,) z ) ( abs ` ( F ` t ) ) _d t < e )
149 99 105 108 109 148 lelttrd 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( abs ` S. ( y (,) z ) ( F ` t ) _d t ) < e )
150 68 149 eqbrtrd 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) /\ ( abs ` ( z - y ) ) < d ) ) -> ( abs ` ( ( G ` z ) - ( G ` y ) ) ) < e )
151 150 expr 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) /\ y <_ z ) ) -> ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( G ` z ) - ( G ` y ) ) ) < e ) )
152 25 35 38 53 151 wlogle 
 |-  ( ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) /\ ( y e. ( A [,] B ) /\ z e. ( A [,] B ) ) ) -> ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( G ` z ) - ( G ` y ) ) ) < e ) )
153 152 ralrimivva 
 |-  ( ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) /\ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) ) -> A. y e. ( A [,] B ) A. z e. ( A [,] B ) ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( G ` z ) - ( G ` y ) ) ) < e ) )
154 153 ex 
 |-  ( ( ph /\ ( e e. RR+ /\ d e. RR+ ) ) -> ( A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) -> A. y e. ( A [,] B ) A. z e. ( A [,] B ) ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( G ` z ) - ( G ` y ) ) ) < e ) ) )
155 154 anassrs 
 |-  ( ( ( ph /\ e e. RR+ ) /\ d e. RR+ ) -> ( A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) -> A. y e. ( A [,] B ) A. z e. ( A [,] B ) ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( G ` z ) - ( G ` y ) ) ) < e ) ) )
156 155 reximdva 
 |-  ( ( ph /\ e e. RR+ ) -> ( E. d e. RR+ A. u e. dom vol ( ( u C_ D /\ ( vol ` u ) < d ) -> S. u ( abs ` ( F ` w ) ) _d w < e ) -> E. d e. RR+ A. y e. ( A [,] B ) A. z e. ( A [,] B ) ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( G ` z ) - ( G ` y ) ) ) < e ) ) )
157 15 156 mpd 
 |-  ( ( ph /\ e e. RR+ ) -> E. d e. RR+ A. y e. ( A [,] B ) A. z e. ( A [,] B ) ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( G ` z ) - ( G ` y ) ) ) < e ) )
158 r19.12 
 |-  ( E. d e. RR+ A. y e. ( A [,] B ) A. z e. ( A [,] B ) ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( G ` z ) - ( G ` y ) ) ) < e ) -> A. y e. ( A [,] B ) E. d e. RR+ A. z e. ( A [,] B ) ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( G ` z ) - ( G ` y ) ) ) < e ) )
159 157 158 syl 
 |-  ( ( ph /\ e e. RR+ ) -> A. y e. ( A [,] B ) E. d e. RR+ A. z e. ( A [,] B ) ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( G ` z ) - ( G ` y ) ) ) < e ) )
160 159 ralrimiva 
 |-  ( ph -> A. e e. RR+ A. y e. ( A [,] B ) E. d e. RR+ A. z e. ( A [,] B ) ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( G ` z ) - ( G ` y ) ) ) < e ) )
161 ralcom 
 |-  ( A. e e. RR+ A. y e. ( A [,] B ) E. d e. RR+ A. z e. ( A [,] B ) ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( G ` z ) - ( G ` y ) ) ) < e ) <-> A. y e. ( A [,] B ) A. e e. RR+ E. d e. RR+ A. z e. ( A [,] B ) ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( G ` z ) - ( G ` y ) ) ) < e ) )
162 160 161 sylib 
 |-  ( ph -> A. y e. ( A [,] B ) A. e e. RR+ E. d e. RR+ A. z e. ( A [,] B ) ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( G ` z ) - ( G ` y ) ) ) < e ) )
163 ax-resscn 
 |-  RR C_ CC
164 37 163 sstrdi 
 |-  ( ph -> ( A [,] B ) C_ CC )
165 ssid 
 |-  CC C_ CC
166 elcncf2 
 |-  ( ( ( A [,] B ) C_ CC /\ CC C_ CC ) -> ( G e. ( ( A [,] B ) -cn-> CC ) <-> ( G : ( A [,] B ) --> CC /\ A. y e. ( A [,] B ) A. e e. RR+ E. d e. RR+ A. z e. ( A [,] B ) ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( G ` z ) - ( G ` y ) ) ) < e ) ) ) )
167 164 165 166 sylancl 
 |-  ( ph -> ( G e. ( ( A [,] B ) -cn-> CC ) <-> ( G : ( A [,] B ) --> CC /\ A. y e. ( A [,] B ) A. e e. RR+ E. d e. RR+ A. z e. ( A [,] B ) ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( G ` z ) - ( G ` y ) ) ) < e ) ) ) )
168 9 162 167 mpbir2and 
 |-  ( ph -> G e. ( ( A [,] B ) -cn-> CC ) )