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

Metamath Proof Explorer

Theorem volcn

Description: The function formed by restricting a measurable set to a closed interval with a varying endpoint produces an increasing continuous function on the reals. (Contributed by Mario Carneiro, 30-Aug-2014)

Ref Expression
Hypothesis volcn.1 
|- F = ( x e. RR |-> ( vol ` ( A i^i ( B [,] x ) ) ) )
Assertion volcn 
|- ( ( A e. dom vol /\ B e. RR ) -> F e. ( RR -cn-> RR ) )

Proof

Step Hyp Ref Expression
1 volcn.1 
 |-  F = ( x e. RR |-> ( vol ` ( A i^i ( B [,] x ) ) ) )
2 simpll 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ x e. RR ) -> A e. dom vol )
3 iccmbl 
 |-  ( ( B e. RR /\ x e. RR ) -> ( B [,] x ) e. dom vol )
4 3 adantll 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ x e. RR ) -> ( B [,] x ) e. dom vol )
5 inmbl 
 |-  ( ( A e. dom vol /\ ( B [,] x ) e. dom vol ) -> ( A i^i ( B [,] x ) ) e. dom vol )
6 2 4 5 syl2anc 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ x e. RR ) -> ( A i^i ( B [,] x ) ) e. dom vol )
7 mblvol 
 |-  ( ( A i^i ( B [,] x ) ) e. dom vol -> ( vol ` ( A i^i ( B [,] x ) ) ) = ( vol* ` ( A i^i ( B [,] x ) ) ) )
8 6 7 syl 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ x e. RR ) -> ( vol ` ( A i^i ( B [,] x ) ) ) = ( vol* ` ( A i^i ( B [,] x ) ) ) )
9 inss2 
 |-  ( A i^i ( B [,] x ) ) C_ ( B [,] x )
10 mblss 
 |-  ( ( B [,] x ) e. dom vol -> ( B [,] x ) C_ RR )
11 4 10 syl 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ x e. RR ) -> ( B [,] x ) C_ RR )
12 mblvol 
 |-  ( ( B [,] x ) e. dom vol -> ( vol ` ( B [,] x ) ) = ( vol* ` ( B [,] x ) ) )
13 4 12 syl 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ x e. RR ) -> ( vol ` ( B [,] x ) ) = ( vol* ` ( B [,] x ) ) )
14 iccvolcl 
 |-  ( ( B e. RR /\ x e. RR ) -> ( vol ` ( B [,] x ) ) e. RR )
15 14 adantll 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ x e. RR ) -> ( vol ` ( B [,] x ) ) e. RR )
16 13 15 eqeltrrd 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ x e. RR ) -> ( vol* ` ( B [,] x ) ) e. RR )
17 ovolsscl 
 |-  ( ( ( A i^i ( B [,] x ) ) C_ ( B [,] x ) /\ ( B [,] x ) C_ RR /\ ( vol* ` ( B [,] x ) ) e. RR ) -> ( vol* ` ( A i^i ( B [,] x ) ) ) e. RR )
18 9 11 16 17 mp3an2i 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ x e. RR ) -> ( vol* ` ( A i^i ( B [,] x ) ) ) e. RR )
19 8 18 eqeltrd 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ x e. RR ) -> ( vol ` ( A i^i ( B [,] x ) ) ) e. RR )
20 19 1 fmptd 
 |-  ( ( A e. dom vol /\ B e. RR ) -> F : RR --> RR )
21 simprr 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y e. RR /\ e e. RR+ ) ) -> e e. RR+ )
22 oveq12 
 |-  ( ( v = z /\ u = y ) -> ( v - u ) = ( z - y ) )
23 22 ancoms 
 |-  ( ( u = y /\ v = z ) -> ( v - u ) = ( z - y ) )
24 23 fveq2d 
 |-  ( ( u = y /\ v = z ) -> ( abs ` ( v - u ) ) = ( abs ` ( z - y ) ) )
25 24 breq1d 
 |-  ( ( u = y /\ v = z ) -> ( ( abs ` ( v - u ) ) < e <-> ( abs ` ( z - y ) ) < e ) )
26 fveq2 
 |-  ( v = z -> ( F ` v ) = ( F ` z ) )
27 fveq2 
 |-  ( u = y -> ( F ` u ) = ( F ` y ) )
28 26 27 oveqan12rd 
 |-  ( ( u = y /\ v = z ) -> ( ( F ` v ) - ( F ` u ) ) = ( ( F ` z ) - ( F ` y ) ) )
29 28 fveq2d 
 |-  ( ( u = y /\ v = z ) -> ( abs ` ( ( F ` v ) - ( F ` u ) ) ) = ( abs ` ( ( F ` z ) - ( F ` y ) ) ) )
30 29 breq1d 
 |-  ( ( u = y /\ v = z ) -> ( ( abs ` ( ( F ` v ) - ( F ` u ) ) ) < e <-> ( abs ` ( ( F ` z ) - ( F ` y ) ) ) < e ) )
31 25 30 imbi12d 
 |-  ( ( u = y /\ v = z ) -> ( ( ( abs ` ( v - u ) ) < e -> ( abs ` ( ( F ` v ) - ( F ` u ) ) ) < e ) <-> ( ( abs ` ( z - y ) ) < e -> ( abs ` ( ( F ` z ) - ( F ` y ) ) ) < e ) ) )
32 oveq12 
 |-  ( ( v = y /\ u = z ) -> ( v - u ) = ( y - z ) )
33 32 ancoms 
 |-  ( ( u = z /\ v = y ) -> ( v - u ) = ( y - z ) )
34 33 fveq2d 
 |-  ( ( u = z /\ v = y ) -> ( abs ` ( v - u ) ) = ( abs ` ( y - z ) ) )
35 34 breq1d 
 |-  ( ( u = z /\ v = y ) -> ( ( abs ` ( v - u ) ) < e <-> ( abs ` ( y - z ) ) < e ) )
36 fveq2 
 |-  ( v = y -> ( F ` v ) = ( F ` y ) )
37 fveq2 
 |-  ( u = z -> ( F ` u ) = ( F ` z ) )
38 36 37 oveqan12rd 
 |-  ( ( u = z /\ v = y ) -> ( ( F ` v ) - ( F ` u ) ) = ( ( F ` y ) - ( F ` z ) ) )
39 38 fveq2d 
 |-  ( ( u = z /\ v = y ) -> ( abs ` ( ( F ` v ) - ( F ` u ) ) ) = ( abs ` ( ( F ` y ) - ( F ` z ) ) ) )
40 39 breq1d 
 |-  ( ( u = z /\ v = y ) -> ( ( abs ` ( ( F ` v ) - ( F ` u ) ) ) < e <-> ( abs ` ( ( F ` y ) - ( F ` z ) ) ) < e ) )
41 35 40 imbi12d 
 |-  ( ( u = z /\ v = y ) -> ( ( ( abs ` ( v - u ) ) < e -> ( abs ` ( ( F ` v ) - ( F ` u ) ) ) < e ) <-> ( ( abs ` ( y - z ) ) < e -> ( abs ` ( ( F ` y ) - ( F ` z ) ) ) < e ) ) )
42 ssidd 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) -> RR C_ RR )
43 recn 
 |-  ( z e. RR -> z e. CC )
44 recn 
 |-  ( y e. RR -> y e. CC )
45 abssub 
 |-  ( ( z e. CC /\ y e. CC ) -> ( abs ` ( z - y ) ) = ( abs ` ( y - z ) ) )
46 43 44 45 syl2anr 
 |-  ( ( y e. RR /\ z e. RR ) -> ( abs ` ( z - y ) ) = ( abs ` ( y - z ) ) )
47 46 adantl 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR ) ) -> ( abs ` ( z - y ) ) = ( abs ` ( y - z ) ) )
48 47 breq1d 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR ) ) -> ( ( abs ` ( z - y ) ) < e <-> ( abs ` ( y - z ) ) < e ) )
49 20 adantr 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) -> F : RR --> RR )
50 ffvelcdm 
 |-  ( ( F : RR --> RR /\ y e. RR ) -> ( F ` y ) e. RR )
51 ffvelcdm 
 |-  ( ( F : RR --> RR /\ z e. RR ) -> ( F ` z ) e. RR )
52 50 51 anim12dan 
 |-  ( ( F : RR --> RR /\ ( y e. RR /\ z e. RR ) ) -> ( ( F ` y ) e. RR /\ ( F ` z ) e. RR ) )
53 49 52 sylan 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR ) ) -> ( ( F ` y ) e. RR /\ ( F ` z ) e. RR ) )
54 recn 
 |-  ( ( F ` z ) e. RR -> ( F ` z ) e. CC )
55 recn 
 |-  ( ( F ` y ) e. RR -> ( F ` y ) e. CC )
56 abssub 
 |-  ( ( ( F ` z ) e. CC /\ ( F ` y ) e. CC ) -> ( abs ` ( ( F ` z ) - ( F ` y ) ) ) = ( abs ` ( ( F ` y ) - ( F ` z ) ) ) )
57 54 55 56 syl2anr 
 |-  ( ( ( F ` y ) e. RR /\ ( F ` z ) e. RR ) -> ( abs ` ( ( F ` z ) - ( F ` y ) ) ) = ( abs ` ( ( F ` y ) - ( F ` z ) ) ) )
58 53 57 syl 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR ) ) -> ( abs ` ( ( F ` z ) - ( F ` y ) ) ) = ( abs ` ( ( F ` y ) - ( F ` z ) ) ) )
59 58 breq1d 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR ) ) -> ( ( abs ` ( ( F ` z ) - ( F ` y ) ) ) < e <-> ( abs ` ( ( F ` y ) - ( F ` z ) ) ) < e ) )
60 48 59 imbi12d 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR ) ) -> ( ( ( abs ` ( z - y ) ) < e -> ( abs ` ( ( F ` z ) - ( F ` y ) ) ) < e ) <-> ( ( abs ` ( y - z ) ) < e -> ( abs ` ( ( F ` y ) - ( F ` z ) ) ) < e ) ) )
61 simpr2 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> z e. RR )
62 oveq2 
 |-  ( x = z -> ( B [,] x ) = ( B [,] z ) )
63 62 ineq2d 
 |-  ( x = z -> ( A i^i ( B [,] x ) ) = ( A i^i ( B [,] z ) ) )
64 63 fveq2d 
 |-  ( x = z -> ( vol ` ( A i^i ( B [,] x ) ) ) = ( vol ` ( A i^i ( B [,] z ) ) ) )
65 fvex 
 |-  ( vol ` ( A i^i ( B [,] z ) ) ) e. _V
66 64 1 65 fvmpt 
 |-  ( z e. RR -> ( F ` z ) = ( vol ` ( A i^i ( B [,] z ) ) ) )
67 61 66 syl 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( F ` z ) = ( vol ` ( A i^i ( B [,] z ) ) ) )
68 simplll 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> A e. dom vol )
69 simplr 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) -> B e. RR )
70 69 adantr 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> B e. RR )
71 iccmbl 
 |-  ( ( B e. RR /\ z e. RR ) -> ( B [,] z ) e. dom vol )
72 70 61 71 syl2anc 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( B [,] z ) e. dom vol )
73 inmbl 
 |-  ( ( A e. dom vol /\ ( B [,] z ) e. dom vol ) -> ( A i^i ( B [,] z ) ) e. dom vol )
74 68 72 73 syl2anc 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( A i^i ( B [,] z ) ) e. dom vol )
75 mblvol 
 |-  ( ( A i^i ( B [,] z ) ) e. dom vol -> ( vol ` ( A i^i ( B [,] z ) ) ) = ( vol* ` ( A i^i ( B [,] z ) ) ) )
76 74 75 syl 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( vol ` ( A i^i ( B [,] z ) ) ) = ( vol* ` ( A i^i ( B [,] z ) ) ) )
77 67 76 eqtrd 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( F ` z ) = ( vol* ` ( A i^i ( B [,] z ) ) ) )
78 simpr1 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> y e. RR )
79 oveq2 
 |-  ( x = y -> ( B [,] x ) = ( B [,] y ) )
80 79 ineq2d 
 |-  ( x = y -> ( A i^i ( B [,] x ) ) = ( A i^i ( B [,] y ) ) )
81 80 fveq2d 
 |-  ( x = y -> ( vol ` ( A i^i ( B [,] x ) ) ) = ( vol ` ( A i^i ( B [,] y ) ) ) )
82 fvex 
 |-  ( vol ` ( A i^i ( B [,] y ) ) ) e. _V
83 81 1 82 fvmpt 
 |-  ( y e. RR -> ( F ` y ) = ( vol ` ( A i^i ( B [,] y ) ) ) )
84 78 83 syl 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( F ` y ) = ( vol ` ( A i^i ( B [,] y ) ) ) )
85 simp1 
 |-  ( ( y e. RR /\ z e. RR /\ y <_ z ) -> y e. RR )
86 iccmbl 
 |-  ( ( B e. RR /\ y e. RR ) -> ( B [,] y ) e. dom vol )
87 69 85 86 syl2an 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( B [,] y ) e. dom vol )
88 inmbl 
 |-  ( ( A e. dom vol /\ ( B [,] y ) e. dom vol ) -> ( A i^i ( B [,] y ) ) e. dom vol )
89 68 87 88 syl2anc 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( A i^i ( B [,] y ) ) e. dom vol )
90 mblvol 
 |-  ( ( A i^i ( B [,] y ) ) e. dom vol -> ( vol ` ( A i^i ( B [,] y ) ) ) = ( vol* ` ( A i^i ( B [,] y ) ) ) )
91 89 90 syl 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( vol ` ( A i^i ( B [,] y ) ) ) = ( vol* ` ( A i^i ( B [,] y ) ) ) )
92 84 91 eqtrd 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( F ` y ) = ( vol* ` ( A i^i ( B [,] y ) ) ) )
93 77 92 oveq12d 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( ( F ` z ) - ( F ` y ) ) = ( ( vol* ` ( A i^i ( B [,] z ) ) ) - ( vol* ` ( A i^i ( B [,] y ) ) ) ) )
94 49 adantr 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> F : RR --> RR )
95 94 61 ffvelcdmd 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( F ` z ) e. RR )
96 77 95 eqeltrrd 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( vol* ` ( A i^i ( B [,] z ) ) ) e. RR )
97 70 leidd 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> B <_ B )
98 simpr3 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> y <_ z )
99 iccss 
 |-  ( ( ( B e. RR /\ z e. RR ) /\ ( B <_ B /\ y <_ z ) ) -> ( B [,] y ) C_ ( B [,] z ) )
100 70 61 97 98 99 syl22anc 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( B [,] y ) C_ ( B [,] z ) )
101 sslin 
 |-  ( ( B [,] y ) C_ ( B [,] z ) -> ( A i^i ( B [,] y ) ) C_ ( A i^i ( B [,] z ) ) )
102 100 101 syl 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( A i^i ( B [,] y ) ) C_ ( A i^i ( B [,] z ) ) )
103 mblss 
 |-  ( ( A i^i ( B [,] z ) ) e. dom vol -> ( A i^i ( B [,] z ) ) C_ RR )
104 74 103 syl 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( A i^i ( B [,] z ) ) C_ RR )
105 102 104 sstrd 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( A i^i ( B [,] y ) ) C_ RR )
106 iccssre 
 |-  ( ( y e. RR /\ z e. RR ) -> ( y [,] z ) C_ RR )
107 78 61 106 syl2anc 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( y [,] z ) C_ RR )
108 105 107 unssd 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( ( A i^i ( B [,] y ) ) u. ( y [,] z ) ) C_ RR )
109 94 78 ffvelcdmd 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( F ` y ) e. RR )
110 92 109 eqeltrrd 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( vol* ` ( A i^i ( B [,] y ) ) ) e. RR )
111 61 78 resubcld 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( z - y ) e. RR )
112 110 111 readdcld 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( ( vol* ` ( A i^i ( B [,] y ) ) ) + ( z - y ) ) e. RR )
113 ovolicc 
 |-  ( ( y e. RR /\ z e. RR /\ y <_ z ) -> ( vol* ` ( y [,] z ) ) = ( z - y ) )
114 113 adantl 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( vol* ` ( y [,] z ) ) = ( z - y ) )
115 114 111 eqeltrd 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( vol* ` ( y [,] z ) ) e. RR )
116 ovolun 
 |-  ( ( ( ( A i^i ( B [,] y ) ) C_ RR /\ ( vol* ` ( A i^i ( B [,] y ) ) ) e. RR ) /\ ( ( y [,] z ) C_ RR /\ ( vol* ` ( y [,] z ) ) e. RR ) ) -> ( vol* ` ( ( A i^i ( B [,] y ) ) u. ( y [,] z ) ) ) <_ ( ( vol* ` ( A i^i ( B [,] y ) ) ) + ( vol* ` ( y [,] z ) ) ) )
117 105 110 107 115 116 syl22anc 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( vol* ` ( ( A i^i ( B [,] y ) ) u. ( y [,] z ) ) ) <_ ( ( vol* ` ( A i^i ( B [,] y ) ) ) + ( vol* ` ( y [,] z ) ) ) )
118 114 oveq2d 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( ( vol* ` ( A i^i ( B [,] y ) ) ) + ( vol* ` ( y [,] z ) ) ) = ( ( vol* ` ( A i^i ( B [,] y ) ) ) + ( z - y ) ) )
119 117 118 breqtrd 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( vol* ` ( ( A i^i ( B [,] y ) ) u. ( y [,] z ) ) ) <_ ( ( vol* ` ( A i^i ( B [,] y ) ) ) + ( z - y ) ) )
120 ovollecl 
 |-  ( ( ( ( A i^i ( B [,] y ) ) u. ( y [,] z ) ) C_ RR /\ ( ( vol* ` ( A i^i ( B [,] y ) ) ) + ( z - y ) ) e. RR /\ ( vol* ` ( ( A i^i ( B [,] y ) ) u. ( y [,] z ) ) ) <_ ( ( vol* ` ( A i^i ( B [,] y ) ) ) + ( z - y ) ) ) -> ( vol* ` ( ( A i^i ( B [,] y ) ) u. ( y [,] z ) ) ) e. RR )
121 108 112 119 120 syl3anc 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( vol* ` ( ( A i^i ( B [,] y ) ) u. ( y [,] z ) ) ) e. RR )
122 70 adantr 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) /\ B <_ y ) -> B e. RR )
123 61 adantr 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) /\ B <_ y ) -> z e. RR )
124 78 adantr 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) /\ B <_ y ) -> y e. RR )
125 simpr 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) /\ B <_ y ) -> B <_ y )
126 98 adantr 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) /\ B <_ y ) -> y <_ z )
127 simp2 
 |-  ( ( y e. RR /\ z e. RR /\ y <_ z ) -> z e. RR )
128 elicc2 
 |-  ( ( B e. RR /\ z e. RR ) -> ( y e. ( B [,] z ) <-> ( y e. RR /\ B <_ y /\ y <_ z ) ) )
129 69 127 128 syl2an 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( y e. ( B [,] z ) <-> ( y e. RR /\ B <_ y /\ y <_ z ) ) )
130 129 adantr 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) /\ B <_ y ) -> ( y e. ( B [,] z ) <-> ( y e. RR /\ B <_ y /\ y <_ z ) ) )
131 124 125 126 130 mpbir3and 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) /\ B <_ y ) -> y e. ( B [,] z ) )
132 iccsplit 
 |-  ( ( B e. RR /\ z e. RR /\ y e. ( B [,] z ) ) -> ( B [,] z ) = ( ( B [,] y ) u. ( y [,] z ) ) )
133 122 123 131 132 syl3anc 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) /\ B <_ y ) -> ( B [,] z ) = ( ( B [,] y ) u. ( y [,] z ) ) )
134 eqimss 
 |-  ( ( B [,] z ) = ( ( B [,] y ) u. ( y [,] z ) ) -> ( B [,] z ) C_ ( ( B [,] y ) u. ( y [,] z ) ) )
135 133 134 syl 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) /\ B <_ y ) -> ( B [,] z ) C_ ( ( B [,] y ) u. ( y [,] z ) ) )
136 78 adantr 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) /\ y <_ B ) -> y e. RR )
137 61 adantr 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) /\ y <_ B ) -> z e. RR )
138 simpr 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) /\ y <_ B ) -> y <_ B )
139 137 leidd 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) /\ y <_ B ) -> z <_ z )
140 iccss 
 |-  ( ( ( y e. RR /\ z e. RR ) /\ ( y <_ B /\ z <_ z ) ) -> ( B [,] z ) C_ ( y [,] z ) )
141 136 137 138 139 140 syl22anc 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) /\ y <_ B ) -> ( B [,] z ) C_ ( y [,] z ) )
142 ssun4 
 |-  ( ( B [,] z ) C_ ( y [,] z ) -> ( B [,] z ) C_ ( ( B [,] y ) u. ( y [,] z ) ) )
143 141 142 syl 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) /\ y <_ B ) -> ( B [,] z ) C_ ( ( B [,] y ) u. ( y [,] z ) ) )
144 70 78 135 143 lecasei 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( B [,] z ) C_ ( ( B [,] y ) u. ( y [,] z ) ) )
145 sslin 
 |-  ( ( B [,] z ) C_ ( ( B [,] y ) u. ( y [,] z ) ) -> ( A i^i ( B [,] z ) ) C_ ( A i^i ( ( B [,] y ) u. ( y [,] z ) ) ) )
146 144 145 syl 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( A i^i ( B [,] z ) ) C_ ( A i^i ( ( B [,] y ) u. ( y [,] z ) ) ) )
147 indi 
 |-  ( A i^i ( ( B [,] y ) u. ( y [,] z ) ) ) = ( ( A i^i ( B [,] y ) ) u. ( A i^i ( y [,] z ) ) )
148 inss2 
 |-  ( A i^i ( y [,] z ) ) C_ ( y [,] z )
149 unss2 
 |-  ( ( A i^i ( y [,] z ) ) C_ ( y [,] z ) -> ( ( A i^i ( B [,] y ) ) u. ( A i^i ( y [,] z ) ) ) C_ ( ( A i^i ( B [,] y ) ) u. ( y [,] z ) ) )
150 148 149 ax-mp 
 |-  ( ( A i^i ( B [,] y ) ) u. ( A i^i ( y [,] z ) ) ) C_ ( ( A i^i ( B [,] y ) ) u. ( y [,] z ) )
151 147 150 eqsstri 
 |-  ( A i^i ( ( B [,] y ) u. ( y [,] z ) ) ) C_ ( ( A i^i ( B [,] y ) ) u. ( y [,] z ) )
152 146 151 sstrdi 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( A i^i ( B [,] z ) ) C_ ( ( A i^i ( B [,] y ) ) u. ( y [,] z ) ) )
153 ovolss 
 |-  ( ( ( A i^i ( B [,] z ) ) C_ ( ( A i^i ( B [,] y ) ) u. ( y [,] z ) ) /\ ( ( A i^i ( B [,] y ) ) u. ( y [,] z ) ) C_ RR ) -> ( vol* ` ( A i^i ( B [,] z ) ) ) <_ ( vol* ` ( ( A i^i ( B [,] y ) ) u. ( y [,] z ) ) ) )
154 152 108 153 syl2anc 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( vol* ` ( A i^i ( B [,] z ) ) ) <_ ( vol* ` ( ( A i^i ( B [,] y ) ) u. ( y [,] z ) ) ) )
155 96 121 112 154 119 letrd 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( vol* ` ( A i^i ( B [,] z ) ) ) <_ ( ( vol* ` ( A i^i ( B [,] y ) ) ) + ( z - y ) ) )
156 96 110 111 lesubadd2d 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( ( ( vol* ` ( A i^i ( B [,] z ) ) ) - ( vol* ` ( A i^i ( B [,] y ) ) ) ) <_ ( z - y ) <-> ( vol* ` ( A i^i ( B [,] z ) ) ) <_ ( ( vol* ` ( A i^i ( B [,] y ) ) ) + ( z - y ) ) ) )
157 155 156 mpbird 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( ( vol* ` ( A i^i ( B [,] z ) ) ) - ( vol* ` ( A i^i ( B [,] y ) ) ) ) <_ ( z - y ) )
158 93 157 eqbrtrd 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( ( F ` z ) - ( F ` y ) ) <_ ( z - y ) )
159 95 109 resubcld 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( ( F ` z ) - ( F ` y ) ) e. RR )
160 simplr 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> e e. RR+ )
161 160 rpred 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> e e. RR )
162 lelttr 
 |-  ( ( ( ( F ` z ) - ( F ` y ) ) e. RR /\ ( z - y ) e. RR /\ e e. RR ) -> ( ( ( ( F ` z ) - ( F ` y ) ) <_ ( z - y ) /\ ( z - y ) < e ) -> ( ( F ` z ) - ( F ` y ) ) < e ) )
163 159 111 161 162 syl3anc 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( ( ( ( F ` z ) - ( F ` y ) ) <_ ( z - y ) /\ ( z - y ) < e ) -> ( ( F ` z ) - ( F ` y ) ) < e ) )
164 158 163 mpand 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( ( z - y ) < e -> ( ( F ` z ) - ( F ` y ) ) < e ) )
165 abssubge0 
 |-  ( ( y e. RR /\ z e. RR /\ y <_ z ) -> ( abs ` ( z - y ) ) = ( z - y ) )
166 165 adantl 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( abs ` ( z - y ) ) = ( z - y ) )
167 166 breq1d 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( ( abs ` ( z - y ) ) < e <-> ( z - y ) < e ) )
168 ovolss 
 |-  ( ( ( A i^i ( B [,] y ) ) C_ ( A i^i ( B [,] z ) ) /\ ( A i^i ( B [,] z ) ) C_ RR ) -> ( vol* ` ( A i^i ( B [,] y ) ) ) <_ ( vol* ` ( A i^i ( B [,] z ) ) ) )
169 102 104 168 syl2anc 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( vol* ` ( A i^i ( B [,] y ) ) ) <_ ( vol* ` ( A i^i ( B [,] z ) ) ) )
170 169 92 77 3brtr4d 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( F ` y ) <_ ( F ` z ) )
171 109 95 170 abssubge0d 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( abs ` ( ( F ` z ) - ( F ` y ) ) ) = ( ( F ` z ) - ( F ` y ) ) )
172 171 breq1d 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( ( abs ` ( ( F ` z ) - ( F ` y ) ) ) < e <-> ( ( F ` z ) - ( F ` y ) ) < e ) )
173 164 167 172 3imtr4d 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR /\ y <_ z ) ) -> ( ( abs ` ( z - y ) ) < e -> ( abs ` ( ( F ` z ) - ( F ` y ) ) ) < e ) )
174 31 41 42 60 173 wlogle 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ ( y e. RR /\ z e. RR ) ) -> ( ( abs ` ( z - y ) ) < e -> ( abs ` ( ( F ` z ) - ( F ` y ) ) ) < e ) )
175 174 anassrs 
 |-  ( ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ y e. RR ) /\ z e. RR ) -> ( ( abs ` ( z - y ) ) < e -> ( abs ` ( ( F ` z ) - ( F ` y ) ) ) < e ) )
176 175 ralrimiva 
 |-  ( ( ( ( A e. dom vol /\ B e. RR ) /\ e e. RR+ ) /\ y e. RR ) -> A. z e. RR ( ( abs ` ( z - y ) ) < e -> ( abs ` ( ( F ` z ) - ( F ` y ) ) ) < e ) )
177 176 anasss 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( e e. RR+ /\ y e. RR ) ) -> A. z e. RR ( ( abs ` ( z - y ) ) < e -> ( abs ` ( ( F ` z ) - ( F ` y ) ) ) < e ) )
178 177 ancom2s 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y e. RR /\ e e. RR+ ) ) -> A. z e. RR ( ( abs ` ( z - y ) ) < e -> ( abs ` ( ( F ` z ) - ( F ` y ) ) ) < e ) )
179 breq2 
 |-  ( d = e -> ( ( abs ` ( z - y ) ) < d <-> ( abs ` ( z - y ) ) < e ) )
180 179 rspceaimv 
 |-  ( ( e e. RR+ /\ A. z e. RR ( ( abs ` ( z - y ) ) < e -> ( abs ` ( ( F ` z ) - ( F ` y ) ) ) < e ) ) -> E. d e. RR+ A. z e. RR ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( F ` z ) - ( F ` y ) ) ) < e ) )
181 21 178 180 syl2anc 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y e. RR /\ e e. RR+ ) ) -> E. d e. RR+ A. z e. RR ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( F ` z ) - ( F ` y ) ) ) < e ) )
182 181 ralrimivva 
 |-  ( ( A e. dom vol /\ B e. RR ) -> A. y e. RR A. e e. RR+ E. d e. RR+ A. z e. RR ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( F ` z ) - ( F ` y ) ) ) < e ) )
183 ax-resscn 
 |-  RR C_ CC
184 elcncf2 
 |-  ( ( RR C_ CC /\ RR C_ CC ) -> ( F e. ( RR -cn-> RR ) <-> ( F : RR --> RR /\ A. y e. RR A. e e. RR+ E. d e. RR+ A. z e. RR ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( F ` z ) - ( F ` y ) ) ) < e ) ) ) )
185 183 183 184 mp2an 
 |-  ( F e. ( RR -cn-> RR ) <-> ( F : RR --> RR /\ A. y e. RR A. e e. RR+ E. d e. RR+ A. z e. RR ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( F ` z ) - ( F ` y ) ) ) < e ) ) )
186 20 182 185 sylanbrc 
 |-  ( ( A e. dom vol /\ B e. RR ) -> F e. ( RR -cn-> RR ) )