Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mblfinlem3 Unicode version

Theorem mblfinlem3 26145
Description: Backward direction of ismblfin 26146. (Contributed by Brendan Leahy, 28-Mar-2018.)
Assertion
Ref Expression
mblfinlem3  |-  ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  ->  ( vol * `
 A )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )
Distinct variable group:    y, b, A

Proof of Theorem mblfinlem3
Dummy variables  f 
g  s  u  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltso 9112 . . . 4  |-  <  Or  RR
21a1i 11 . . 3  |-  ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  ->  <  Or  RR )
3 simplr 732 . . 3  |-  ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  ->  ( vol * `
 A )  e.  RR )
4 vex 2919 . . . . . . 7  |-  u  e. 
_V
5 eqeq1 2410 . . . . . . . . 9  |-  ( y  =  u  ->  (
y  =  ( vol `  b )  <->  u  =  ( vol `  b ) ) )
65anbi2d 685 . . . . . . . 8  |-  ( y  =  u  ->  (
( b  C_  A  /\  y  =  ( vol `  b ) )  <-> 
( b  C_  A  /\  u  =  ( vol `  b ) ) ) )
76rexbidv 2687 . . . . . . 7  |-  ( y  =  u  ->  ( E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
C_  A  /\  y  =  ( vol `  b
) )  <->  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  u  =  ( vol `  b ) ) ) )
84, 7elab 3042 . . . . . 6  |-  ( u  e.  { y  |  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  <->  E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
C_  A  /\  u  =  ( vol `  b
) ) )
9 simprl 733 . . . . . . . . 9  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) )  -> 
b  C_  A )
10 ovolss 19334 . . . . . . . . . . 11  |-  ( ( b  C_  A  /\  A  C_  RR )  -> 
( vol * `  b )  <_  ( vol * `  A ) )
11 sstr 3316 . . . . . . . . . . . . 13  |-  ( ( b  C_  A  /\  A  C_  RR )  -> 
b  C_  RR )
12 ovolcl 19327 . . . . . . . . . . . . 13  |-  ( b 
C_  RR  ->  ( vol
* `  b )  e.  RR* )
1311, 12syl 16 . . . . . . . . . . . 12  |-  ( ( b  C_  A  /\  A  C_  RR )  -> 
( vol * `  b )  e.  RR* )
14 ovolcl 19327 . . . . . . . . . . . . 13  |-  ( A 
C_  RR  ->  ( vol
* `  A )  e.  RR* )
1514adantl 453 . . . . . . . . . . . 12  |-  ( ( b  C_  A  /\  A  C_  RR )  -> 
( vol * `  A )  e.  RR* )
16 xrlenlt 9099 . . . . . . . . . . . 12  |-  ( ( ( vol * `  b )  e.  RR*  /\  ( vol * `  A )  e.  RR* )  ->  ( ( vol
* `  b )  <_  ( vol * `  A )  <->  -.  ( vol * `  A )  <  ( vol * `  b ) ) )
1713, 15, 16syl2anc 643 . . . . . . . . . . 11  |-  ( ( b  C_  A  /\  A  C_  RR )  -> 
( ( vol * `  b )  <_  ( vol * `  A )  <->  -.  ( vol * `  A )  <  ( vol * `  b ) ) )
1810, 17mpbid 202 . . . . . . . . . 10  |-  ( ( b  C_  A  /\  A  C_  RR )  ->  -.  ( vol * `  A )  <  ( vol * `  b ) )
1918ancoms 440 . . . . . . . . 9  |-  ( ( A  C_  RR  /\  b  C_  A )  ->  -.  ( vol * `  A
)  <  ( vol * `
 b ) )
209, 19sylan2 461 . . . . . . . 8  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  -.  ( vol * `
 A )  < 
( vol * `  b ) )
21 simprrr 742 . . . . . . . . . 10  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  u  =  ( vol `  b ) )
22 uniretop 18749 . . . . . . . . . . . . . . 15  |-  RR  =  U. ( topGen `  ran  (,) )
2322cldss 17048 . . . . . . . . . . . . . 14  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  b  C_  RR )
24 dfss4 3535 . . . . . . . . . . . . . 14  |-  ( b 
C_  RR  <->  ( RR  \ 
( RR  \  b
) )  =  b )
2523, 24sylib 189 . . . . . . . . . . . . 13  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  ( RR  \  b
) )  =  b )
26 rembl 19388 . . . . . . . . . . . . . 14  |-  RR  e.  dom  vol
2722cldopn 17050 . . . . . . . . . . . . . . 15  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  b )  e.  (
topGen `  ran  (,) )
)
28 opnmbl 19447 . . . . . . . . . . . . . . 15  |-  ( ( RR  \  b )  e.  ( topGen `  ran  (,) )  ->  ( RR  \  b )  e.  dom  vol )
2927, 28syl 16 . . . . . . . . . . . . . 14  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  b )  e.  dom  vol )
30 difmbl 19390 . . . . . . . . . . . . . 14  |-  ( ( RR  e.  dom  vol  /\  ( RR  \  b
)  e.  dom  vol )  ->  ( RR  \ 
( RR  \  b
) )  e.  dom  vol )
3126, 29, 30sylancr 645 . . . . . . . . . . . . 13  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  ( RR  \  b
) )  e.  dom  vol )
3225, 31eqeltrrd 2479 . . . . . . . . . . . 12  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  b  e.  dom  vol )
33 mblvol 19379 . . . . . . . . . . . 12  |-  ( b  e.  dom  vol  ->  ( vol `  b )  =  ( vol * `  b ) )
3432, 33syl 16 . . . . . . . . . . 11  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol `  b )  =  ( vol * `  b
) )
3534ad2antrl 709 . . . . . . . . . 10  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  ( vol `  b
)  =  ( vol
* `  b )
)
3621, 35eqtrd 2436 . . . . . . . . 9  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  u  =  ( vol * `  b
) )
3736breq2d 4184 . . . . . . . 8  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  ( ( vol
* `  A )  <  u  <->  ( vol * `  A )  <  ( vol * `  b ) ) )
3820, 37mtbird 293 . . . . . . 7  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  -.  ( vol * `
 A )  < 
u )
3938rexlimdvaa 2791 . . . . . 6  |-  ( A 
C_  RR  ->  ( E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  u  =  ( vol `  b ) )  ->  -.  ( vol * `  A )  <  u ) )
408, 39syl5bi 209 . . . . 5  |-  ( A 
C_  RR  ->  ( u  e.  { y  |  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  ->  -.  ( vol * `
 A )  < 
u ) )
4140ad2antrr 707 . . . 4  |-  ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  ->  ( u  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  ->  -.  ( vol * `  A
)  <  u )
)
4241imp 419 . . 3  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  u  e. 
{ y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } )  ->  -.  ( vol * `  A )  <  u
)
43 1rp 10572 . . . . . . . . 9  |-  1  e.  RR+
44 eqid 2404 . . . . . . . . . 10  |-  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  =  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)
4544ovolgelb 19329 . . . . . . . . 9  |-  ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR  /\  1  e.  RR+ )  ->  E. f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( A  C_  U.
ran  ( (,)  o.  f )  /\  sup ( ran  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  f ) ) , 
RR* ,  <  )  <_ 
( ( vol * `  A )  +  1 ) ) )
4643, 45mp3an3 1268 . . . . . . . 8  |-  ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  ->  E. f  e.  (
(  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( A  C_  U. ran  ( (,)  o.  f )  /\  sup ( ran  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  f )
) ,  RR* ,  <  )  <_  ( ( vol
* `  A )  +  1 ) ) )
47 elmapi 6997 . . . . . . . . . . 11  |-  ( f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN )  ->  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
48 ssid 3327 . . . . . . . . . . . . . . 15  |-  U. ran  ( (,)  o.  f ) 
C_  U. ran  ( (,) 
o.  f )
4944ovollb 19328 . . . . . . . . . . . . . . 15  |-  ( ( f : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  U. ran  ( (,)  o.  f
)  C_  U. ran  ( (,)  o.  f ) )  ->  ( vol * `  U. ran  ( (,) 
o.  f ) )  <_  sup ( ran  seq  1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) ,  RR* ,  <  ) )
5048, 49mpan2 653 . . . . . . . . . . . . . 14  |-  ( f : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  ( vol * `  U. ran  ( (,)  o.  f ) )  <_  sup ( ran  seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) ) , 
RR* ,  <  ) )
5150adantl 453 . . . . . . . . . . . . 13  |-  ( ( ( vol * `  A )  e.  RR  /\  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )  -> 
( vol * `  U. ran  ( (,)  o.  f ) )  <_  sup ( ran  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  f )
) ,  RR* ,  <  ) )
52 eqid 2404 . . . . . . . . . . . . . . . 16  |-  ( ( abs  o.  -  )  o.  f )  =  ( ( abs  o.  -  )  o.  f )
5352, 44ovolsf 19322 . . . . . . . . . . . . . . 15  |-  ( f : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  seq  1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,)  +oo ) )
54 frn 5556 . . . . . . . . . . . . . . . 16  |-  (  seq  1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,)  +oo )  ->  ran  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  C_  ( 0 [,)  +oo ) )
55 icossxr 10951 . . . . . . . . . . . . . . . 16  |-  ( 0 [,)  +oo )  C_  RR*
5654, 55syl6ss 3320 . . . . . . . . . . . . . . 15  |-  (  seq  1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,)  +oo )  ->  ran  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  C_  RR* )
57 supxrcl 10849 . . . . . . . . . . . . . . 15  |-  ( ran 
seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) )  C_  RR* 
->  sup ( ran  seq  1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) ,  RR* ,  <  )  e.  RR* )
5853, 56, 573syl 19 . . . . . . . . . . . . . 14  |-  ( f : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  sup ( ran  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  f ) ) , 
RR* ,  <  )  e. 
RR* )
59 peano2re 9195 . . . . . . . . . . . . . . 15  |-  ( ( vol * `  A
)  e.  RR  ->  ( ( vol * `  A )  +  1 )  e.  RR )
6059rexrd 9090 . . . . . . . . . . . . . 14  |-  ( ( vol * `  A
)  e.  RR  ->  ( ( vol * `  A )  +  1 )  e.  RR* )
61 rncoss 5095 . . . . . . . . . . . . . . . . . 18  |-  ran  ( (,)  o.  f )  C_  ran  (,)
6261unissi 3998 . . . . . . . . . . . . . . . . 17  |-  U. ran  ( (,)  o.  f ) 
C_  U. ran  (,)
63 unirnioo 10960 . . . . . . . . . . . . . . . . 17  |-  RR  =  U. ran  (,)
6462, 63sseqtr4i 3341 . . . . . . . . . . . . . . . 16  |-  U. ran  ( (,)  o.  f ) 
C_  RR
65 ovolcl 19327 . . . . . . . . . . . . . . . 16  |-  ( U. ran  ( (,)  o.  f
)  C_  RR  ->  ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR* )
6664, 65ax-mp 8 . . . . . . . . . . . . . . 15  |-  ( vol
* `  U. ran  ( (,)  o.  f ) )  e.  RR*
67 xrletr 10704 . . . . . . . . . . . . . . 15  |-  ( ( ( vol * `  U. ran  ( (,)  o.  f ) )  e. 
RR*  /\  sup ( ran  seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) ) , 
RR* ,  <  )  e. 
RR*  /\  ( ( vol * `  A )  +  1 )  e. 
RR* )  ->  (
( ( vol * `  U. ran  ( (,) 
o.  f ) )  <_  sup ( ran  seq  1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) ,  RR* ,  <  )  /\  sup ( ran  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  f ) ) , 
RR* ,  <  )  <_ 
( ( vol * `  A )  +  1 ) )  ->  ( vol * `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol * `  A )  +  1 ) ) )
6866, 67mp3an1 1266 . . . . . . . . . . . . . 14  |-  ( ( sup ( ran  seq  1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) ,  RR* ,  <  )  e.  RR*  /\  ( ( vol * `  A )  +  1 )  e.  RR* )  ->  ( ( ( vol
* `  U. ran  ( (,)  o.  f ) )  <_  sup ( ran  seq  1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) ,  RR* ,  <  )  /\  sup ( ran  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  f ) ) , 
RR* ,  <  )  <_ 
( ( vol * `  A )  +  1 ) )  ->  ( vol * `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol * `  A )  +  1 ) ) )
6958, 60, 68syl2anr 465 . . . . . . . . . . . . 13  |-  ( ( ( vol * `  A )  e.  RR  /\  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )  -> 
( ( ( vol
* `  U. ran  ( (,)  o.  f ) )  <_  sup ( ran  seq  1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) ,  RR* ,  <  )  /\  sup ( ran  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  f ) ) , 
RR* ,  <  )  <_ 
( ( vol * `  A )  +  1 ) )  ->  ( vol * `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol * `  A )  +  1 ) ) )
7051, 69mpand 657 . . . . . . . . . . . 12  |-  ( ( ( vol * `  A )  e.  RR  /\  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )  -> 
( sup ( ran 
seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) ) , 
RR* ,  <  )  <_ 
( ( vol * `  A )  +  1 )  ->  ( vol * `
 U. ran  ( (,)  o.  f ) )  <_  ( ( vol
* `  A )  +  1 ) ) )
7170adantll 695 . . . . . . . . . . 11  |-  ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )  ->  ( sup ( ran  seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) ) , 
RR* ,  <  )  <_ 
( ( vol * `  A )  +  1 )  ->  ( vol * `
 U. ran  ( (,)  o.  f ) )  <_  ( ( vol
* `  A )  +  1 ) ) )
7247, 71sylan2 461 . . . . . . . . . 10  |-  ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) )  ->  ( sup ( ran  seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) ) , 
RR* ,  <  )  <_ 
( ( vol * `  A )  +  1 )  ->  ( vol * `
 U. ran  ( (,)  o.  f ) )  <_  ( ( vol
* `  A )  +  1 ) ) )
7372anim2d 549 . . . . . . . . 9  |-  ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) )  ->  ( ( A 
C_  U. ran  ( (,) 
o.  f )  /\  sup ( ran  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  f )
) ,  RR* ,  <  )  <_  ( ( vol
* `  A )  +  1 ) )  ->  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol * `  A )  +  1 ) ) ) )
7473reximdva 2778 . . . . . . . 8  |-  ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  -> 
( E. f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( A  C_  U.
ran  ( (,)  o.  f )  /\  sup ( ran  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  f ) ) , 
RR* ,  <  )  <_ 
( ( vol * `  A )  +  1 ) )  ->  E. f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol * `  A )  +  1 ) ) ) )
7546, 74mpd 15 . . . . . . 7  |-  ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  ->  E. f  e.  (
(  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )
76 rexex 2725 . . . . . . 7  |-  ( E. f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol * `  A )  +  1 ) )  ->  E. f ( A 
C_  U. ran  ( (,) 
o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )
7775, 76syl 16 . . . . . 6  |-  ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  ->  E. f ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol * `  A )  +  1 ) ) )
7877ad2antrr 707 . . . . 5  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol * `  A ) ) )  ->  E. f ( A 
C_  U. ran  ( (,) 
o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )
79 difss 3434 . . . . . . . . . . . . . 14  |-  ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  f )
8079, 64sstri 3317 . . . . . . . . . . . . 13  |-  ( U. ran  ( (,)  o.  f
)  \  A )  C_  RR
81 ovolcl 19327 . . . . . . . . . . . . 13  |-  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  RR  ->  ( vol * `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e. 
RR* )
8280, 81ax-mp 8 . . . . . . . . . . . 12  |-  ( vol
* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  e.  RR*
8359, 82jctil 524 . . . . . . . . . . 11  |-  ( ( vol * `  A
)  e.  RR  ->  ( ( vol * `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e. 
RR*  /\  ( ( vol * `  A )  +  1 )  e.  RR ) )
8483ad4antlr 714 . . . . . . . . . 10  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  -> 
( ( vol * `  ( U. ran  ( (,)  o.  f )  \  A ) )  e. 
RR*  /\  ( ( vol * `  A )  +  1 )  e.  RR ) )
85 ovolss 19334 . . . . . . . . . . . . . . 15  |-  ( ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  f )  /\  U. ran  ( (,)  o.  f )  C_  RR )  ->  ( vol
* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  <_  ( vol * `
 U. ran  ( (,)  o.  f ) ) )
8679, 64, 85mp2an 654 . . . . . . . . . . . . . 14  |-  ( vol
* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  <_  ( vol * `
 U. ran  ( (,)  o.  f ) )
87 xrletr 10704 . . . . . . . . . . . . . . . 16  |-  ( ( ( vol * `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e. 
RR*  /\  ( vol * `
 U. ran  ( (,)  o.  f ) )  e.  RR*  /\  (
( vol * `  A )  +  1 )  e.  RR* )  ->  ( ( ( vol
* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  <_  ( vol * `
 U. ran  ( (,)  o.  f ) )  /\  ( vol * `  U. ran  ( (,) 
o.  f ) )  <_  ( ( vol
* `  A )  +  1 ) )  ->  ( vol * `  ( U. ran  ( (,)  o.  f )  \  A ) )  <_ 
( ( vol * `  A )  +  1 ) ) )
8882, 66, 87mp3an12 1269 . . . . . . . . . . . . . . 15  |-  ( ( ( vol * `  A )  +  1 )  e.  RR*  ->  ( ( ( vol * `  ( U. ran  ( (,)  o.  f )  \  A ) )  <_ 
( vol * `  U. ran  ( (,)  o.  f ) )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) )  ->  ( vol * `  ( U. ran  ( (,)  o.  f
)  \  A )
)  <_  ( ( vol * `  A )  +  1 ) ) )
8960, 88syl 16 . . . . . . . . . . . . . 14  |-  ( ( vol * `  A
)  e.  RR  ->  ( ( ( vol * `  ( U. ran  ( (,)  o.  f )  \  A ) )  <_ 
( vol * `  U. ran  ( (,)  o.  f ) )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) )  ->  ( vol * `  ( U. ran  ( (,)  o.  f
)  \  A )
)  <_  ( ( vol * `  A )  +  1 ) ) )
9086, 89mpani 658 . . . . . . . . . . . . 13  |-  ( ( vol * `  A
)  e.  RR  ->  ( ( vol * `  U. ran  ( (,)  o.  f ) )  <_ 
( ( vol * `  A )  +  1 )  ->  ( vol * `
 ( U. ran  ( (,)  o.  f ) 
\  A ) )  <_  ( ( vol
* `  A )  +  1 ) ) )
9190ad4antlr 714 . . . . . . . . . . . 12  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  A  C_ 
U. ran  ( (,)  o.  f ) )  -> 
( ( vol * `  U. ran  ( (,) 
o.  f ) )  <_  ( ( vol
* `  A )  +  1 )  -> 
( vol * `  ( U. ran  ( (,) 
o.  f )  \  A ) )  <_ 
( ( vol * `  A )  +  1 ) ) )
9291impr 603 . . . . . . . . . . 11  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  -> 
( vol * `  ( U. ran  ( (,) 
o.  f )  \  A ) )  <_ 
( ( vol * `  A )  +  1 ) )
93 ovolge0 19330 . . . . . . . . . . . 12  |-  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  RR  ->  0  <_  ( vol * `
 ( U. ran  ( (,)  o.  f ) 
\  A ) ) )
9480, 93ax-mp 8 . . . . . . . . . . 11  |-  0  <_  ( vol * `  ( U. ran  ( (,) 
o.  f )  \  A ) )
9592, 94jctil 524 . . . . . . . . . 10  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  -> 
( 0  <_  ( vol * `  ( U. ran  ( (,)  o.  f
)  \  A )
)  /\  ( vol * `
 ( U. ran  ( (,)  o.  f ) 
\  A ) )  <_  ( ( vol
* `  A )  +  1 ) ) )
96 xrrege0 10718 . . . . . . . . . 10  |-  ( ( ( ( vol * `  ( U. ran  ( (,)  o.  f )  \  A ) )  e. 
RR*  /\  ( ( vol * `  A )  +  1 )  e.  RR )  /\  (
0  <_  ( vol * `
 ( U. ran  ( (,)  o.  f ) 
\  A ) )  /\  ( vol * `  ( U. ran  ( (,)  o.  f )  \  A ) )  <_ 
( ( vol * `  A )  +  1 ) ) )  -> 
( vol * `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e.  RR )
9784, 95, 96syl2anc 643 . . . . . . . . 9  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  -> 
( vol * `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e.  RR )
98 resubcl 9321 . . . . . . . . . . . . . 14  |-  ( ( ( vol * `  A )  e.  RR  /\  u  e.  RR )  ->  ( ( vol
* `  A )  -  u )  e.  RR )
9998adantrr 698 . . . . . . . . . . . . 13  |-  ( ( ( vol * `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  ->  (
( vol * `  A )  -  u
)  e.  RR )
100 posdif 9477 . . . . . . . . . . . . . . . 16  |-  ( ( u  e.  RR  /\  ( vol * `  A
)  e.  RR )  ->  ( u  < 
( vol * `  A )  <->  0  <  ( ( vol * `  A )  -  u
) ) )
101100ancoms 440 . . . . . . . . . . . . . . 15  |-  ( ( ( vol * `  A )  e.  RR  /\  u  e.  RR )  ->  ( u  < 
( vol * `  A )  <->  0  <  ( ( vol * `  A )  -  u
) ) )
102101biimpd 199 . . . . . . . . . . . . . 14  |-  ( ( ( vol * `  A )  e.  RR  /\  u  e.  RR )  ->  ( u  < 
( vol * `  A )  ->  0  <  ( ( vol * `  A )  -  u
) ) )
103102impr 603 . . . . . . . . . . . . 13  |-  ( ( ( vol * `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  ->  0  <  ( ( vol * `  A )  -  u
) )
10499, 103elrpd 10602 . . . . . . . . . . . 12  |-  ( ( ( vol * `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  ->  (
( vol * `  A )  -  u
)  e.  RR+ )
105104rphalfcld 10616 . . . . . . . . . . 11  |-  ( ( ( vol * `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  ->  (
( ( vol * `  A )  -  u
)  /  2 )  e.  RR+ )
1063, 105sylan 458 . . . . . . . . . 10  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol * `  A ) ) )  ->  ( ( ( vol * `  A
)  -  u )  /  2 )  e.  RR+ )
107106adantr 452 . . . . . . . . 9  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  -> 
( ( ( vol
* `  A )  -  u )  /  2
)  e.  RR+ )
108 eqid 2404 . . . . . . . . . . 11  |-  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  g )
)  =  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  g )
)
109108ovolgelb 19329 . . . . . . . . . 10  |-  ( ( ( U. ran  ( (,)  o.  f )  \  A )  C_  RR  /\  ( vol * `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e.  RR  /\  ( ( ( vol * `  A )  -  u
)  /  2 )  e.  RR+ )  ->  E. g  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  g )  /\  sup ( ran  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  g ) ) , 
RR* ,  <  )  <_ 
( ( vol * `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol
* `  A )  -  u )  /  2
) ) ) )
11080, 109mp3an1 1266 . . . . . . . . 9  |-  ( ( ( vol * `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e.  RR  /\  ( ( ( vol * `  A )  -  u
)  /  2 )  e.  RR+ )  ->  E. g  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  g )  /\  sup ( ran  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  g ) ) , 
RR* ,  <  )  <_ 
( ( vol * `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol
* `  A )  -  u )  /  2
) ) ) )
11197, 107, 110syl2anc 643 . . . . . . . 8  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  ->  E. g  e.  (
(  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  sup ( ran 
seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  g ) ) , 
RR* ,  <  )  <_ 
( ( vol * `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol
* `  A )  -  u )  /  2
) ) ) )
112 elmapi 6997 . . . . . . . . . . 11  |-  ( g  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN )  ->  g : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
113 ssid 3327 . . . . . . . . . . . . . 14  |-  U. ran  ( (,)  o.  g ) 
C_  U. ran  ( (,) 
o.  g )
114108ovollb 19328 . . . . . . . . . . . . . 14  |-  ( ( g : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  U. ran  ( (,)  o.  g
)  C_  U. ran  ( (,)  o.  g ) )  ->  ( vol * `  U. ran  ( (,) 
o.  g ) )  <_  sup ( ran  seq  1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) ,  RR* ,  <  ) )
115113, 114mpan2 653 . . . . . . . . . . . . 13  |-  ( g : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  ( vol * `  U. ran  ( (,)  o.  g ) )  <_  sup ( ran  seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  g ) ) , 
RR* ,  <  ) )
116115adantl 453 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  /\  g : NN --> (  <_  i^i  ( RR  X.  RR ) ) )  -> 
( vol * `  U. ran  ( (,)  o.  g ) )  <_  sup ( ran  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  g )
) ,  RR* ,  <  ) )
117 eqid 2404 . . . . . . . . . . . . . . 15  |-  ( ( abs  o.  -  )  o.  g )  =  ( ( abs  o.  -  )  o.  g )
118117, 108ovolsf 19322 . . . . . . . . . . . . . 14  |-  ( g : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  seq  1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) : NN --> ( 0 [,)  +oo ) )
119 frn 5556 . . . . . . . . . . . . . . 15  |-  (  seq  1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) : NN --> ( 0 [,)  +oo )  ->  ran  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  g )
)  C_  ( 0 [,)  +oo ) )
120119, 55syl6ss 3320 . . . . . . . . . . . . . 14  |-  (  seq  1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) : NN --> ( 0 [,)  +oo )  ->  ran  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  g )
)  C_  RR* )
121 supxrcl 10849 . . . . . . . . . . . . . 14  |-  ( ran 
seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  g ) )  C_  RR* 
->  sup ( ran  seq  1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) ,  RR* ,  <  )  e.  RR* )
122118, 120, 1213syl 19 . . . . . . . . . . . . 13  |-  ( g : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  sup ( ran  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  g ) ) , 
RR* ,  <  )  e. 
RR* )
12399rehalfcld 10170 . . . . . . . . . . . . . . . . 17  |-  ( ( ( vol * `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  ->  (
( ( vol * `  A )  -  u
)  /  2 )  e.  RR )
1243, 123sylan 458 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol * `  A ) ) )  ->  ( ( ( vol * `  A
)  -  u )  /  2 )  e.  RR )
125124adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  -> 
( ( ( vol
* `  A )  -  u )  /  2
)  e.  RR )
12697, 125readdcld 9071 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  -> 
( ( vol * `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol
* `  A )  -  u )  /  2
) )  e.  RR )
127126rexrd 9090 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  -> 
( ( vol * `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol
* `  A )  -  u )  /  2
) )  e.  RR* )
128 rncoss 5095 . . . . . . . . . . . . . . . . 17  |-  ran  ( (,)  o.  g )  C_  ran  (,)
129128unissi 3998 . . . . . . . . . . . . . . . 16  |-  U. ran  ( (,)  o.  g ) 
C_  U. ran  (,)
130129, 63sseqtr4i 3341 . . . . . . . . . . . . . . 15  |-  U. ran  ( (,)  o.  g ) 
C_  RR
131 ovolcl 19327 . . . . . . . . . . . . . . 15  |-  ( U. ran  ( (,)  o.  g
)  C_  RR  ->  ( vol * `  U. ran  ( (,)  o.  g
) )  e.  RR* )
132130, 131ax-mp 8 . . . . . . . . . . . . . 14  |-  ( vol
* `  U. ran  ( (,)  o.  g ) )  e.  RR*
133 xrletr 10704 . . . . . . . . . . . . . 14  |-  ( ( ( vol * `  U. ran  ( (,)  o.  g ) )  e. 
RR*  /\  sup ( ran  seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  g ) ) , 
RR* ,  <  )  e. 
RR*  /\  ( ( vol * `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) )  e.  RR* )  ->  ( ( ( vol
* `  U. ran  ( (,)  o.  g ) )  <_  sup ( ran  seq  1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) ,  RR* ,  <  )  /\  sup ( ran  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  g ) ) , 
RR* ,  <  )  <_ 
( ( vol * `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol
* `  A )  -  u )  /  2
) ) )  -> 
( vol * `  U. ran  ( (,)  o.  g ) )  <_ 
( ( vol * `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol
* `  A )  -  u )  /  2
) ) ) )
134132, 133mp3an1 1266 . . . . . . . . . . . . 13  |-  ( ( sup ( ran  seq  1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) ,  RR* ,  <  )  e.  RR*  /\  ( ( vol * `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol
* `  A )  -  u )  /  2
) )  e.  RR* )  ->  ( ( ( vol * `  U. ran  ( (,)  o.  g
) )  <_  sup ( ran  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  g ) ) , 
RR* ,  <  )  /\  sup ( ran  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  g )
) ,  RR* ,  <  )  <_  ( ( vol
* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) )  ->  ( vol * `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol * `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) ) )
135122, 127, 134syl2anr 465 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  /\  g : NN --> (  <_  i^i  ( RR  X.  RR ) ) )  -> 
( ( ( vol
* `  U. ran  ( (,)  o.  g ) )  <_  sup ( ran  seq  1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) ,  RR* ,  <  )  /\  sup ( ran  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  g ) ) , 
RR* ,  <  )  <_ 
( ( vol * `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol
* `  A )  -  u )  /  2
) ) )  -> 
( vol * `  U. ran  ( (,)  o.  g ) )  <_ 
( ( vol * `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol
* `  A )  -  u )  /  2
) ) ) )
136116, 135mpand 657 . . . . . . . . . . 11  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  /\  g : NN --> (  <_  i^i  ( RR  X.  RR ) ) )  -> 
( sup ( ran 
seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  g ) ) , 
RR* ,  <  )  <_ 
( ( vol * `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol
* `  A )  -  u )  /  2
) )  ->  ( vol * `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol * `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) ) )
137112, 136sylan2 461 . . . . . . . . . 10  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  /\  g  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) )  ->  ( sup ( ran  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  g )
) ,  RR* ,  <  )  <_  ( ( vol
* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) )  ->  ( vol * `
 U. ran  ( (,)  o.  g ) )  <_  ( ( vol
* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) ) )
138137anim2d 549 . . . . . . . . 9  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  /\  g  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) )  ->  (
( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  U.
ran  ( (,)  o.  g )  /\  sup ( ran  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  g ) ) , 
RR* ,  <  )  <_ 
( ( vol * `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol
* `  A )  -  u )  /  2
) ) )  -> 
( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  U.
ran  ( (,)  o.  g )  /\  ( vol * `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol * `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) ) ) )
139138reximdva 2778 . . . . . . . 8  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  -> 
( E. g  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  g )  /\  sup ( ran  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  g ) ) , 
RR* ,  <  )  <_ 
( ( vol * `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol
* `  A )  -  u )  /  2
) ) )  ->  E. g  e.  (
(  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol * `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol
* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) ) ) )
140111, 139mpd 15 . . . . . . 7  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  ->  E. g  e.  (
(  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol * `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol
* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) ) )
141 rexex 2725 . . . . . . 7  |-  ( E. g  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  g )  /\  ( vol * `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol * `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) )  ->  E. g
( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  U.
ran  ( (,)  o.  g )  /\  ( vol * `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol * `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) ) )
142140, 141syl 16 . . . . . 6  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  ->  E. g ( ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  g )  /\  ( vol * `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol * `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) ) )
14359, 66jctil 524 . . . . . . . . . . . 12  |-  ( ( vol * `  A
)  e.  RR  ->  ( ( vol * `  U. ran  ( (,)  o.  f ) )  e. 
RR*  /\  ( ( vol * `  A )  +  1 )  e.  RR ) )
144143ad3antlr 712 . . . . . . . . . . 11  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol * `  A ) ) )  ->  ( ( vol
* `  U. ran  ( (,)  o.  f ) )  e.  RR*  /\  (
( vol * `  A )  +  1 )  e.  RR ) )
145 ovolge0 19330 . . . . . . . . . . . . . 14  |-  ( U. ran  ( (,)  o.  f
)  C_  RR  ->  0  <_  ( vol * `  U. ran  ( (,) 
o.  f ) ) )
14664, 145ax-mp 8 . . . . . . . . . . . . 13  |-  0  <_  ( vol * `  U. ran  ( (,)  o.  f ) )
147146jctl 526 . . . . . . . . . . . 12  |-  ( ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 )  ->  ( 0  <_  ( vol * `  U. ran  ( (,) 
o.  f ) )  /\  ( vol * `  U. ran  ( (,) 
o.  f ) )  <_  ( ( vol
* `  A )  +  1 ) ) )
148147adantl 453 . . . . . . . . . . 11  |-  ( ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) )  ->  (
0  <_  ( vol * `
 U. ran  ( (,)  o.  f ) )  /\  ( vol * `  U. ran  ( (,) 
o.  f ) )  <_  ( ( vol
* `  A )  +  1 ) ) )
149 xrrege0 10718 . . . . . . . . . . 11  |-  ( ( ( ( vol * `  U. ran  ( (,) 
o.  f ) )  e.  RR*  /\  (
( vol * `  A )  +  1 )  e.  RR )  /\  ( 0  <_ 
( vol * `  U. ran  ( (,)  o.  f ) )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  -> 
( vol * `  U. ran  ( (,)  o.  f ) )  e.  RR )
150144, 148, 149syl2an 464 . . . . . . . . . 10  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  -> 
( vol * `  U. ran  ( (,)  o.  f ) )  e.  RR )
151150, 125resubcld 9421 . . . . . . . . 9  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  -> 
( ( vol * `  U. ran  ( (,) 
o.  f ) )  -  ( ( ( vol * `  A
)  -  u )  /  2 ) )  e.  RR )
152150, 107ltsubrpd 10632 . . . . . . . . 9  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  -> 
( ( vol * `  U. ran  ( (,) 
o.  f ) )  -  ( ( ( vol * `  A
)  -  u )  /  2 ) )  <  ( vol * `  U. ran  ( (,) 
o.  f ) ) )
153 retop 18748 . . . . . . . . . . 11  |-  ( topGen ` 
ran  (,) )  e.  Top
154 retopbas 18747 . . . . . . . . . . . . 13  |-  ran  (,)  e. 
TopBases
155 bastg 16986 . . . . . . . . . . . . 13  |-  ( ran 
(,)  e.  TopBases  ->  ran  (,)  C_  ( topGen `  ran  (,) )
)
156154, 155ax-mp 8 . . . . . . . . . . . 12  |-  ran  (,)  C_  ( topGen `  ran  (,) )
15761, 156sstri 3317 . . . . . . . . . . 11  |-  ran  ( (,)  o.  f )  C_  ( topGen `  ran  (,) )
158 uniopn 16925 . . . . . . . . . . 11  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ran  ( (,)  o.  f )  C_  ( topGen `  ran  (,) )
)  ->  U. ran  ( (,)  o.  f )  e.  ( topGen `  ran  (,) )
)
159153, 157, 158mp2an 654 . . . . . . . . . 10  |-  U. ran  ( (,)  o.  f )  e.  ( topGen `  ran  (,) )
160 mblfinlem 26143 . . . . . . . . . 10  |-  ( ( U. ran  ( (,) 
o.  f )  e.  ( topGen `  ran  (,) )  /\  ( ( vol * `  U. ran  ( (,) 
o.  f ) )  -  ( ( ( vol * `  A
)  -  u )  /  2 ) )  e.  RR  /\  (
( vol * `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol
* `  A )  -  u )  /  2
) )  <  ( vol * `  U. ran  ( (,)  o.  f ) ) )  ->  E. s  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( s  C_  U.
ran  ( (,)  o.  f )  /\  (
( vol * `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol
* `  A )  -  u )  /  2
) )  <  ( vol * `  s ) ) )
161159, 160mp3an1 1266 . . . . . . . . 9  |-  ( ( ( ( vol * `  U. ran  ( (,) 
o.  f ) )  -  ( ( ( vol * `  A
)  -  u )  /  2 ) )  e.  RR  /\  (
( vol * `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol
* `  A )  -  u )  /  2
) )  <  ( vol * `  U. ran  ( (,)  o.  f ) ) )  ->  E. s  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( s  C_  U.
ran  ( (,)  o.  f )  /\  (
( vol * `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol
* `  A )  -  u )  /  2
) )  <  ( vol * `  s ) ) )
162151, 152, 161syl2anc 643 . . . . . . . 8  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  ->  E. s  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( s 
C_  U. ran  ( (,) 
o.  f )  /\  ( ( vol * `  U. ran  ( (,) 
o.  f ) )  -  ( ( ( vol * `  A
)  -  u )  /  2 ) )  <  ( vol * `  s ) ) )
163162adantr 452 . . . . . . 7  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  U.
ran  ( (,)  o.  g )  /\  ( vol * `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol * `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) ) )  ->  E. s  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( s 
C_  U. ran  ( (,) 
o.  f )  /\  ( ( vol * `  U. ran  ( (,) 
o.  f ) )  -  ( ( ( vol * `  A
)  -  u )  /  2 ) )  <  ( vol * `  s ) ) )
164 indif2 3544 . . . . . . . . . . . . . . 15  |-  ( s  i^i  ( RR  \  U. ran  ( (,)  o.  g ) ) )  =  ( ( s  i^i  RR )  \  U. ran  ( (,)  o.  g ) )
16522cldss 17048 . . . . . . . . . . . . . . . . 17  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  s  C_  RR )
166 df-ss 3294 . . . . . . . . . . . . . . . . 17  |-  ( s 
C_  RR  <->  ( s  i^i 
RR )  =  s )
167165, 166sylib 189 . . . . . . . . . . . . . . . 16  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( s  i^i  RR )  =  s )
168167difeq1d 3424 . . . . . . . . . . . . . . 15  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( (
s  i^i  RR )  \  U. ran  ( (,) 
o.  g ) )  =  ( s  \  U. ran  ( (,)  o.  g ) ) )
169164, 168syl5eq 2448 . . . . . . . . . . . . . 14  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( s  i^i  ( RR  \  U. ran  ( (,)  o.  g
) ) )  =  ( s  \  U. ran  ( (,)  o.  g
) ) )
170128, 156sstri 3317 . . . . . . . . . . . . . . . . 17  |-  ran  ( (,)  o.  g )  C_  ( topGen `  ran  (,) )
171 uniopn 16925 . . . . . . . . . . . . . . . . 17  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ran  ( (,)  o.  g )  C_  ( topGen `  ran  (,) )
)  ->  U. ran  ( (,)  o.  g )  e.  ( topGen `  ran  (,) )
)
172153, 170, 171mp2an 654 . . . . . . . . . . . . . . . 16  |-  U. ran  ( (,)  o.  g )  e.  ( topGen `  ran  (,) )
17322opncld 17052 . . . . . . . . . . . . . . . 16  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  U. ran  ( (,)  o.  g )  e.  ( topGen `  ran  (,) ) )  ->  ( RR  \  U. ran  ( (,)  o.  g ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
) )
174153, 172, 173mp2an 654 . . . . . . . . . . . . . . 15  |-  ( RR 
\  U. ran  ( (,) 
o.  g ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
)
175 incld 17062 . . . . . . . . . . . . . . 15  |-  ( ( s  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( RR  \ 
U. ran  ( (,)  o.  g ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
) )  ->  (
s  i^i  ( RR  \ 
U. ran  ( (,)  o.  g ) ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
) )
176174, 175mpan2 653 . . . . . . . . . . . . . 14  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( s  i^i  ( RR  \  U. ran  ( (,)  o.  g
) ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
) )
177169, 176eqeltrrd 2479 . . . . . . . . . . . . 13  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( s  \  U. ran  ( (,) 
o.  g ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
) )
178 simpr 448 . . . . . . . . . . . . . . 15  |-  ( ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  s  C_  U. ran  ( (,)  o.  f ) )  ->  s  C_  U.
ran  ( (,)  o.  f ) )
179 simpl 444 . . . . . . . . . . . . . . 15  |-  ( ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  s  C_  U. ran  ( (,)  o.  f ) )  ->  ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  g ) )
180178, 179ssdif2d 3446 . . . . . . . . . . . . . 14  |-  ( ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  s  C_  U. ran  ( (,)  o.  f ) )  ->  ( s  \  U. ran  ( (,) 
o.  g ) ) 
C_  ( U. ran  ( (,)  o.  f ) 
\  ( U. ran  ( (,)  o.  f ) 
\  A ) ) )
181 dfin4 3541 . . . . . . . . . . . . . . 15  |-  ( U. ran  ( (,)  o.  f
)  i^i  A )  =  ( U. ran  ( (,)  o.  f ) 
\  ( U. ran  ( (,)  o.  f ) 
\  A ) )
182 inss2 3522 . . . . . . . . . . . . . . 15  |-  ( U. ran  ( (,)  o.  f
)  i^i  A )  C_  A
183181, 182eqsstr3i 3339 . . . . . . . . . . . . . 14  |-  ( U. ran  ( (,)  o.  f
)  \  ( U. ran  ( (,)  o.  f
)  \  A )
)  C_  A
184180, 183syl6ss 3320 . . . . . . . . . . . . 13  |-  ( ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  s  C_  U. ran  ( (,)  o.  f ) )  ->  ( s  \  U. ran  ( (,) 
o.  g ) ) 
C_  A )
185 sseq1 3329 . . . . . . . . . . . . . . . 16  |-  ( b  =  ( s  \  U. ran  ( (,)  o.  g ) )  -> 
( b  C_  A  <->  ( s  \  U. ran  ( (,)  o.  g ) )  C_  A )
)
186185anbi1d 686 . . . . . . . . . . . . . . 15  |-  ( b  =  ( s  \  U. ran  ( (,)  o.  g ) )  -> 
( ( b  C_  A  /\  ( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) )  <->  ( (
s  \  U. ran  ( (,)  o.  g ) ) 
C_  A  /\  ( vol `  ( s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b
) ) ) )
187 fveq2 5687 . . . . . . . . . . . . . . . . 17  |-  ( ( s  \  U. ran  ( (,)  o.  g ) )  =  b  -> 
( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) )
188187eqcoms 2407 . . . . . . . . . . . . . . . 16  |-  ( b  =  ( s  \  U. ran  ( (,)  o.  g ) )  -> 
( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) )
189188biantrud 494 . . . . . . . . . . . . . . 15  |-  ( b  =  ( s  \  U. ran  ( (,)  o.  g ) )  -> 
( ( s  \  U. ran  ( (,)  o.  g ) )  C_  A 
<->  ( ( s  \  U. ran  ( (,)  o.  g ) )  C_  A  /\  ( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) ) ) )
190186, 189bitr4d 248 . . . . . . . . . . . . . 14  |-  ( b  =  ( s  \  U. ran  ( (,)  o.  g ) )  -> 
( ( b  C_  A  /\  ( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) )  <->  ( s  \  U. ran  ( (,) 
o.  g ) ) 
C_  A ) )
191190rspcev 3012 . . . . . . . . . . . . 13  |-  ( ( ( s  \  U. ran  ( (,)  o.  g
) )  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  \  U. ran  ( (,)  o.  g
) )  C_  A
)  ->  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  ( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) ) )
192177, 184, 191syl2an 464 . . . . . . . . . . . 12  |-  ( ( s  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( ( U. ran  ( (,)  o.  f )  \  A
)  C_  U. ran  ( (,)  o.  g )  /\  s  C_  U. ran  ( (,)  o.  f ) ) )  ->  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  ( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) ) )
193192an12s 777 . . . . . . . . . . 11  |-  ( ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  /\  s  C_  U.
ran  ( (,)  o.  f ) ) )  ->  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  A  /\  ( vol `  ( s 
\  U. ran  ( (,) 
o.  g ) ) )  =  ( vol `  b ) ) )
194193adantrrr 706 . . . . . . . . . 10  |-  ( ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  /\  ( s  C_ 
U. ran  ( (,)  o.  f )  /\  (
( vol * `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol
* `  A )  -  u )  /  2
) )  <  ( vol * `  s ) ) ) )  ->  E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
C_  A  /\  ( vol `  ( s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b
) ) )
195194adantlr 696 . . . . . . . . 9  |-  ( ( ( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  U.
ran  ( (,)  o.  g )  /\  ( vol * `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol * `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) )  /\  (
s  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( s  C_ 
U. ran  ( (,)  o.  f )  /\  (
( vol * `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol
* `  A )  -  u )  /  2
) )  <  ( vol * `  s ) ) ) )  ->  E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
C_  A  /\  ( vol `  ( s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b
) ) )
196195adantll 695 . . . . . . . 8  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol * `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol * `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol * `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol
* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol
* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol * `  A
)  -  u )  /  2 ) )  <  ( vol * `  s ) ) ) )  ->  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  ( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) ) )
197 difss 3434 . . . . . . . . . . . 12  |-  ( A 
\  ( s  \  U. ran  ( (,)  o.  g ) ) ) 
C_  A
198 ovolsscl 19335 . . . . . . . . . . . 12  |-  ( ( ( A  \  (
s  \  U. ran  ( (,)  o.  g ) ) )  C_  A  /\  A  C_  RR  /\  ( vol * `  A )  e.  RR )  -> 
( vol * `  ( A  \  (
s  \  U. ran  ( (,)  o.  g ) ) ) )  e.  RR )
199197, 198mp3an1 1266 . . . . . . . . . . 11  |-  ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  -> 
( vol * `  ( A  \  (
s  \  U. ran  ( (,)  o.  g ) ) ) )  e.  RR )
200199ad5antr 715 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol * `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol * `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol * `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol
* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol
* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol * `  A
)  -  u )  /  2 ) )  <  ( vol * `  s ) ) ) )  ->  ( vol * `
 ( A  \ 
( s  \  U. ran  ( (,)  o.  g
) ) ) )  e.  RR )
201 simp-6r 748 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol * `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol * `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol * `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol
* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol
* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol * `  A
)  -  u )  /  2 ) )  <  ( vol * `  s ) ) ) )  ->  ( vol * `
 A )  e.  RR )
202 simpl 444 . . . . . . . . . . 11  |-  ( ( u  e.  RR  /\  u  <  ( vol * `  A ) )  ->  u  e.  RR )
203202ad4antlr 714 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol * `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol * `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol * `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol
* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol
* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol * `  A
)  -  u )  /  2 ) )  <  ( vol * `  s ) ) ) )  ->  u  e.  RR )
204 difdif2 3558 . . . . . . . . . . . 12  |-  ( A 
\  ( s  \  U. ran  ( (,)  o.  g ) ) )  =  ( ( A 
\  s )  u.  ( A  i^i  U. ran  ( (,)  o.  g
) ) )
205204fveq2i 5690 . . . . . . . . . . 11  |-  ( vol
* `  ( A  \  ( s  \  U. ran  ( (,)  o.  g
) ) ) )  =  ( vol * `  ( ( A  \ 
s )  u.  ( A  i^i  U. ran  ( (,)  o.  g ) ) ) )
206 difss 3434 . . . . . . . . . . . . . . 15  |-  ( A 
\  s )  C_  A
207 inss1 3521 . . . . . . . . . . . . . . 15  |-  ( A  i^i  U. ran  ( (,)  o.  g ) ) 
C_  A
208206, 207unssi 3482 . . . . . . . . . . . . . 14  |-  ( ( A  \  s )  u.  ( A  i^i  U.
ran  ( (,)  o.  g ) ) ) 
C_  A
209 ovolsscl 19335 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  \ 
s )  u.  ( A  i^i  U. ran  ( (,)  o.  g ) ) )  C_  A  /\  A  C_  RR  /\  ( vol * `  A )  e.  RR )  -> 
( vol * `  ( ( A  \ 
s )  u.  ( A  i^i  U. ran  ( (,)  o.  g ) ) ) )  e.  RR )
210208, 209mp3an1 1266 . . . . . . . . . . . . 13  |-  ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  -> 
( vol * `  ( ( A  \ 
s )  u.  ( A  i^i  U. ran  ( (,)  o.  g ) ) ) )  e.  RR )
211210ad5antr 715 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol * `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol * `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol * `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol
* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol
* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol * `  A
)  -  u )  /  2 ) )  <  ( vol * `  s ) ) ) )  ->  ( vol * `
 ( ( A 
\  s )  u.  ( A  i^i  U. ran  ( (,)  o.  g
) ) ) )  e.  RR )
212 ovolsscl 19335 . . . . . . . . . . . . . . 15  |-  ( ( ( A  \  s
)  C_  A  /\  A  C_  RR  /\  ( vol * `  A )  e.  RR )  -> 
( vol * `  ( A  \  s
) )  e.  RR )
213206, 212mp3an1 1266 . . . . . . . . . . . . . 14  |-  ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  -> 
( vol * `  ( A  \  s
) )  e.  RR )
214213ad5antr 715 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol * `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol * `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol * `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol
* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol
* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol * `  A
)  -  u )  /  2 ) )  <  ( vol * `  s ) ) ) )  ->  ( vol * `
 ( A  \ 
s ) )  e.  RR )
215 ovolsscl 19335 . . . . . . . . . . . . . . 15  |-  ( ( ( A  i^i  U. ran  ( (,)  o.  g
) )  C_  A  /\  A  C_  RR  /\  ( vol * `  A
)  e.  RR )  ->  ( vol * `  ( A  i^i  U. ran  ( (,)  o.  g
) ) )  e.  RR )
216207, 215mp3an1 1266 . . . . . . . . . . . . . 14  |-  ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  -> 
( vol * `  ( A  i^i  U. ran  ( (,)  o.  g ) ) )  e.  RR )
217216ad5antr 715 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol * `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol * `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol * `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol
* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol
* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol * `  A
)  -  u )  /  2 ) )  <  ( vol * `  s ) ) ) )  ->  ( vol * `
 ( A  i^i  U.
ran  ( (,)  o.  g ) ) )  e.  RR )
218214, 217readdcld 9071 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol * `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol * `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol * `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol
* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol
* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol * `  A
)  -  u )  /  2 ) )  <  ( vol * `  s ) ) ) )  ->  ( ( vol * `  ( A 
\  s ) )  +  ( vol * `  ( A  i^i  U. ran  ( (,)  o.  g
) ) ) )  e.  RR )
2193, 202, 98syl2an 464 . . . . . . . . . . . . 13  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol * `  A ) ) )  ->  ( ( vol
* `  A )  -  u )  e.  RR )
220219ad3antrrr 711 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol * `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol * `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol * `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol
* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol
* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol * `  A
)  -  u )  /  2 ) )  <  ( vol * `  s ) ) ) )  ->  ( ( vol * `  A )  -  u )  e.  RR )
221 ssdifss 3438 . . . . . . . . . . . . . . 15  |-  ( A 
C_  RR  ->  ( A 
\  s )  C_  RR )
222221adantr 452 . . . . . . . . . . . . . 14  |-  ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  -> 
( A  \  s
)  C_  RR )
223 ssinss1 3529 . . . . . . . . . . . . . . 15  |-  ( A 
C_  RR  ->  ( A  i^i  U. ran  ( (,)  o.  g ) ) 
C_  RR )
224223adantr 452 . . . . . . . . . . . . . 14  |-  ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  -> 
( A  i^i  U. ran  ( (,)  o.  g
) )  C_  RR )
225 ovolun 19348 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  \ 
s )  C_  RR  /\  ( vol * `  ( A  \  s
) )  e.  RR )  /\  ( ( A  i^i  U. ran  ( (,)  o.  g ) ) 
C_  RR  /\  ( vol * `  ( A  i^i  U. ran  ( (,)  o.  g ) ) )  e.  RR ) )  ->  ( vol * `
 ( ( A 
\  s )  u.  ( A  i^i  U. ran  ( (,)  o.  g
) ) ) )  <_  ( ( vol
* `  ( A  \  s ) )  +  ( vol * `  ( A  i^i  U. ran  ( (,)  o.  g ) ) ) ) )
226222, 213, 224, 216, 225syl22anc 1185 . . . . . . . . . . . . 13  |-  ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  -> 
( vol * `  ( ( A  \ 
s )  u.  ( A  i^i  U. ran  ( (,)  o.  g ) ) ) )  <_  (
( vol * `  ( A  \  s
) )  +  ( vol * `  ( A  i^i  U. ran  ( (,)  o.  g ) ) ) ) )
227226ad5antr 715 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol * `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol * `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol * `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol
* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol
* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol * `  A
)  -  u )  /  2 ) )  <  ( vol * `  s ) ) ) )  ->  ( vol * `
 ( ( A 
\  s )  u.  ( A  i^i  U. ran  ( (,)  o.  g
) ) ) )  <_  ( ( vol
* `  ( A  \  s ) )  +  ( vol * `  ( A  i^i  U. ran  ( (,)  o.  g ) ) ) ) )
228124ad2antrr 707 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  U.
ran  ( (,)  o.  g )  /\  ( vol * `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol * `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) ) )  -> 
( ( ( vol
* `  A )  -  u )  /  2
)  e.  RR )
229228adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol * `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol * `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol * `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol
* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol
* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol * `  A
)  -  u )  /  2 ) )  <  ( vol * `  s ) ) ) )  ->  ( (
( vol * `  A )  -  u
)  /  2 )  e.  RR )
230150ad2antrr 707 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol * `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol * `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol * `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol
* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol
* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol * `  A
)  -  u )  /  2 ) )  <  ( vol * `  s ) ) ) )  ->  ( vol * `
 U. ran  ( (,)  o.  f ) )  e.  RR )
231 simprl 733 . . . . . . . . . . . . . . . . 17  |-  ( ( s  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( s  C_ 
U. ran  ( (,)  o.  f )  /\  (
( vol * `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol
* `  A )  -  u )  /  2
) )  <  ( vol * `  s ) ) )  ->  s  C_ 
U. ran  ( (,)  o.  f ) )
232150adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  <_  (
( vol * `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  U.
ran  ( (,)  o.  g )  /\  ( vol * `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol * `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) ) )  -> 
( vol * `  U. ran  ( (,)  o.  f ) )  e.  RR )
233 ovolsscl 19335 . . . . . . . . . . . . . . . . . 18  |-  ( ( s  C_  U. ran  ( (,)  o.  f )  /\  U.
ran  ( (,)  o.  f )  C_  RR  /\  ( vol * `  U. ran  ( (,)  o.  f ) )  e.  RR )  ->  ( vol * `  s )  e.  RR )
23464, 233mp3an2 1267 . . . . . . . . . . . . . . . . 17  |-  ( ( s  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR )  ->  ( vol * `  s )  e.  RR )
235231, 232, 234syl2anr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol * `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol * `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol * `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol
* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol * `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol
* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol * `