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 ) ) |