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 ffvelrn
 |-  ( ( F : RR --> RR /\ y e. RR ) -> ( F ` y ) e. RR )
51 ffvelrn
 |-  ( ( 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 ffvelrnd
 |-  ( ( ( ( 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 ffvelrnd
 |-  ( ( ( ( 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 ) )