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

Theorem itg2addnclem 31420
Description: An alternate expression for the  S.2 integral that includes an arbitrarily small but strictly positive "buffer zone" wherever the simple function is nonzero. (Contributed by Brendan Leahy, 10-Oct-2017.) (Revised by Brendan Leahy, 10-Mar-2018.)
Hypothesis
Ref Expression
itg2addnclem.1  |-  L  =  { x  |  E. g  e.  dom  S.1 ( E. y  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  oR  <_  F  /\  x  =  ( S.1 `  g
) ) }
Assertion
Ref Expression
itg2addnclem  |-  ( F : RR --> ( 0 [,] +oo )  -> 
( S.2 `  F )  =  sup ( L ,  RR* ,  <  )
)
Distinct variable group:    x, y, z, g, F
Allowed substitution hints:    L( x, y, z, g)

Proof of Theorem itg2addnclem
Dummy variables  s  u  f  a  b are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2402 . . 3  |-  { x  |  E. f  e.  dom  S.1 ( f  oR  <_  F  /\  x  =  ( S.1 `  f
) ) }  =  { x  |  E. f  e.  dom  S.1 (
f  oR  <_  F  /\  x  =  ( S.1 `  f ) ) }
21itg2val 22319 . 2  |-  ( F : RR --> ( 0 [,] +oo )  -> 
( S.2 `  F )  =  sup ( { x  |  E. f  e.  dom  S.1 ( f  oR  <_  F  /\  x  =  ( S.1 `  f ) ) } ,  RR* ,  <  )
)
3 itg2addnclem.1 . . . 4  |-  L  =  { x  |  E. g  e.  dom  S.1 ( E. y  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  oR  <_  F  /\  x  =  ( S.1 `  g
) ) }
43supeq1i 7860 . . 3  |-  sup ( L ,  RR* ,  <  )  =  sup ( { x  |  E. g  e.  dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  y ) ) )  oR  <_  F  /\  x  =  ( S.1 `  g ) ) } ,  RR* ,  <  )
5 xrltso 11318 . . . . 5  |-  <  Or  RR*
65a1i 11 . . . 4  |-  ( F : RR --> ( 0 [,] +oo )  ->  <  Or  RR* )
7 simprr 758 . . . . . . . 8  |-  ( ( f  e.  dom  S.1  /\  ( f  oR  <_  F  /\  x  =  ( S.1 `  f
) ) )  ->  x  =  ( S.1 `  f ) )
8 itg1cl 22276 . . . . . . . . . 10  |-  ( f  e.  dom  S.1  ->  ( S.1 `  f )  e.  RR )
98rexrd 9593 . . . . . . . . 9  |-  ( f  e.  dom  S.1  ->  ( S.1 `  f )  e.  RR* )
109adantr 463 . . . . . . . 8  |-  ( ( f  e.  dom  S.1  /\  ( f  oR  <_  F  /\  x  =  ( S.1 `  f
) ) )  -> 
( S.1 `  f )  e.  RR* )
117, 10eqeltrd 2490 . . . . . . 7  |-  ( ( f  e.  dom  S.1  /\  ( f  oR  <_  F  /\  x  =  ( S.1 `  f
) ) )  ->  x  e.  RR* )
1211rexlimiva 2891 . . . . . 6  |-  ( E. f  e.  dom  S.1 ( f  oR  <_  F  /\  x  =  ( S.1 `  f
) )  ->  x  e.  RR* )
1312abssi 3513 . . . . 5  |-  { x  |  E. f  e.  dom  S.1 ( f  oR  <_  F  /\  x  =  ( S.1 `  f
) ) }  C_  RR*
14 supxrcl 11477 . . . . 5  |-  ( { x  |  E. f  e.  dom  S.1 ( f  oR  <_  F  /\  x  =  ( S.1 `  f ) ) } 
C_  RR*  ->  sup ( { x  |  E. f  e.  dom  S.1 (
f  oR  <_  F  /\  x  =  ( S.1 `  f ) ) } ,  RR* ,  <  )  e.  RR* )
1513, 14mp1i 13 . . . 4  |-  ( F : RR --> ( 0 [,] +oo )  ->  sup ( { x  |  E. f  e.  dom  S.1 ( f  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  )  e. 
RR* )
16 fveq1 5804 . . . . . . . . . . . . . . . 16  |-  ( g  =  f  ->  (
g `  z )  =  ( f `  z ) )
1716eqeq1d 2404 . . . . . . . . . . . . . . 15  |-  ( g  =  f  ->  (
( g `  z
)  =  0  <->  (
f `  z )  =  0 ) )
1816oveq1d 6249 . . . . . . . . . . . . . . 15  |-  ( g  =  f  ->  (
( g `  z
)  +  y )  =  ( ( f `
 z )  +  y ) )
1917, 18ifbieq2d 3909 . . . . . . . . . . . . . 14  |-  ( g  =  f  ->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) )  =  if ( ( f `  z
)  =  0 ,  0 ,  ( ( f `  z )  +  y ) ) )
2019mpteq2dv 4481 . . . . . . . . . . . . 13  |-  ( g  =  f  ->  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  =  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  y ) ) ) )
2120breq1d 4404 . . . . . . . . . . . 12  |-  ( g  =  f  ->  (
( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  oR  <_  F  <->  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  y ) ) )  oR  <_  F
) )
2221rexbidv 2917 . . . . . . . . . . 11  |-  ( g  =  f  ->  ( E. y  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  oR  <_  F  <->  E. y  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  y ) ) )  oR  <_  F
) )
23 fveq2 5805 . . . . . . . . . . . 12  |-  ( g  =  f  ->  ( S.1 `  g )  =  ( S.1 `  f
) )
2423eqeq2d 2416 . . . . . . . . . . 11  |-  ( g  =  f  ->  (
x  =  ( S.1 `  g )  <->  x  =  ( S.1 `  f ) ) )
2522, 24anbi12d 709 . . . . . . . . . 10  |-  ( g  =  f  ->  (
( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  oR  <_  F  /\  x  =  ( S.1 `  g
) )  <->  ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z
)  =  0 ,  0 ,  ( ( f `  z )  +  y ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f ) ) ) )
2625cbvrexv 3034 . . . . . . . . 9  |-  ( E. g  e.  dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  oR  <_  F  /\  x  =  ( S.1 `  g
) )  <->  E. f  e.  dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  y ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f ) ) )
27 breq2 4398 . . . . . . . . . . . . . . . . 17  |-  ( 0  =  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  y ) )  -> 
( ( f `  z )  <_  0  <->  ( f `  z )  <_  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  y ) ) ) )
28 breq2 4398 . . . . . . . . . . . . . . . . 17  |-  ( ( ( f `  z
)  +  y )  =  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  y ) )  -> 
( ( f `  z )  <_  (
( f `  z
)  +  y )  <-> 
( f `  z
)  <_  if (
( f `  z
)  =  0 ,  0 ,  ( ( f `  z )  +  y ) ) ) )
29 id 22 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f `  z )  =  0  ->  (
f `  z )  =  0 )
30 0le0 10586 . . . . . . . . . . . . . . . . . . 19  |-  0  <_  0
3129, 30syl6eqbr 4431 . . . . . . . . . . . . . . . . . 18  |-  ( ( f `  z )  =  0  ->  (
f `  z )  <_  0 )
3231adantl 464 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( f  e. 
dom  S.1  /\  y  e.  RR+ )  /\  z  e.  RR )  /\  (
f `  z )  =  0 )  -> 
( f `  z
)  <_  0 )
33 rpge0 11195 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  RR+  ->  0  <_ 
y )
3433ad2antlr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( f  e.  dom  S.1 
/\  y  e.  RR+ )  /\  z  e.  RR )  ->  0  <_  y
)
35 i1ff 22267 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  e.  dom  S.1  ->  f : RR --> RR )
3635ffvelrnda 5965 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( f  e.  dom  S.1  /\  z  e.  RR )  ->  ( f `  z )  e.  RR )
3736adantlr 713 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( f  e.  dom  S.1 
/\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( f `  z )  e.  RR )
38 rpre 11189 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  RR+  ->  y  e.  RR )
3938ad2antlr 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( f  e.  dom  S.1 
/\  y  e.  RR+ )  /\  z  e.  RR )  ->  y  e.  RR )
4037, 39addge01d 10100 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( f  e.  dom  S.1 
/\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( 0  <_ 
y  <->  ( f `  z )  <_  (
( f `  z
)  +  y ) ) )
4134, 40mpbid 210 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( f  e.  dom  S.1 
/\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( f `  z )  <_  (
( f `  z
)  +  y ) )
4241adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( f  e. 
dom  S.1  /\  y  e.  RR+ )  /\  z  e.  RR )  /\  -.  ( f `  z
)  =  0 )  ->  ( f `  z )  <_  (
( f `  z
)  +  y ) )
4327, 28, 32, 42ifbothda 3919 . . . . . . . . . . . . . . . 16  |-  ( ( ( f  e.  dom  S.1 
/\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( f `  z )  <_  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  y ) ) )
4443adantlll 716 . . . . . . . . . . . . . . 15  |-  ( ( ( ( F : RR
--> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  (
f `  z )  <_  if ( ( f `
 z )  =  0 ,  0 ,  ( ( f `  z )  +  y ) ) )
4535ad2antlr 725 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F : RR --> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  f : RR --> RR )
4645ffvelrnda 5965 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( F : RR
--> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  (
f `  z )  e.  RR )
4746rexrd 9593 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( F : RR
--> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  (
f `  z )  e.  RR* )
48 0re 9546 . . . . . . . . . . . . . . . . . 18  |-  0  e.  RR
4938ad2antlr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( F : RR
--> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  y  e.  RR )
5046, 49readdcld 9573 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F : RR
--> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  (
( f `  z
)  +  y )  e.  RR )
51 ifcl 3926 . . . . . . . . . . . . . . . . . 18  |-  ( ( 0  e.  RR  /\  ( ( f `  z )  +  y )  e.  RR )  ->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  y ) )  e.  RR )
5248, 50, 51sylancr 661 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( F : RR
--> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  y ) )  e.  RR )
5352rexrd 9593 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( F : RR
--> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  y ) )  e.  RR* )
54 iccssxr 11578 . . . . . . . . . . . . . . . . . . 19  |-  ( 0 [,] +oo )  C_  RR*
55 fss 5678 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  ( 0 [,] +oo )  C_  RR* )  ->  F : RR --> RR* )
5654, 55mpan2 669 . . . . . . . . . . . . . . . . . 18  |-  ( F : RR --> ( 0 [,] +oo )  ->  F : RR --> RR* )
5756ad2antrr 724 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F : RR --> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  F : RR
--> RR* )
5857ffvelrnda 5965 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( F : RR
--> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( F `  z )  e.  RR* )
59 xrletr 11332 . . . . . . . . . . . . . . . 16  |-  ( ( ( f `  z
)  e.  RR*  /\  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  y ) )  e.  RR*  /\  ( F `  z )  e.  RR* )  ->  (
( ( f `  z )  <_  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  y ) )  /\  if ( ( f `  z
)  =  0 ,  0 ,  ( ( f `  z )  +  y ) )  <_  ( F `  z ) )  -> 
( f `  z
)  <_  ( F `  z ) ) )
6047, 53, 58, 59syl3anc 1230 . . . . . . . . . . . . . . 15  |-  ( ( ( ( F : RR
--> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  (
( ( f `  z )  <_  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  y ) )  /\  if ( ( f `  z
)  =  0 ,  0 ,  ( ( f `  z )  +  y ) )  <_  ( F `  z ) )  -> 
( f `  z
)  <_  ( F `  z ) ) )
6144, 60mpand 673 . . . . . . . . . . . . . 14  |-  ( ( ( ( F : RR
--> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  y ) )  <_  ( F `  z )  ->  (
f `  z )  <_  ( F `  z
) ) )
6261ralimdva 2811 . . . . . . . . . . . . 13  |-  ( ( ( F : RR --> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  ( A. z  e.  RR  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  y ) )  <_  ( F `  z )  ->  A. z  e.  RR  ( f `  z )  <_  ( F `  z )
) )
63 reex 9533 . . . . . . . . . . . . . . 15  |-  RR  e.  _V
6463a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( F : RR --> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  RR  e.  _V )
65 eqidd 2403 . . . . . . . . . . . . . 14  |-  ( ( ( F : RR --> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  ( z  e.  RR  |->  if ( ( f `  z
)  =  0 ,  0 ,  ( ( f `  z )  +  y ) ) )  =  ( z  e.  RR  |->  if ( ( f `  z
)  =  0 ,  0 ,  ( ( f `  z )  +  y ) ) ) )
66 id 22 . . . . . . . . . . . . . . . 16  |-  ( F : RR --> ( 0 [,] +oo )  ->  F : RR --> ( 0 [,] +oo ) )
6766feqmptd 5858 . . . . . . . . . . . . . . 15  |-  ( F : RR --> ( 0 [,] +oo )  ->  F  =  ( z  e.  RR  |->  ( F `  z ) ) )
6867ad2antrr 724 . . . . . . . . . . . . . 14  |-  ( ( ( F : RR --> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  F  =  ( z  e.  RR  |->  ( F `  z ) ) )
6964, 52, 58, 65, 68ofrfval2 6495 . . . . . . . . . . . . 13  |-  ( ( ( F : RR --> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  ( ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  y ) ) )  oR  <_  F  <->  A. z  e.  RR  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  y ) )  <_ 
( F `  z
) ) )
7035feqmptd 5858 . . . . . . . . . . . . . . 15  |-  ( f  e.  dom  S.1  ->  f  =  ( z  e.  RR  |->  ( f `  z ) ) )
7170ad2antlr 725 . . . . . . . . . . . . . 14  |-  ( ( ( F : RR --> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  f  =  ( z  e.  RR  |->  ( f `  z
) ) )
7264, 46, 58, 71, 68ofrfval2 6495 . . . . . . . . . . . . 13  |-  ( ( ( F : RR --> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  ( f  oR  <_  F  <->  A. z  e.  RR  (
f `  z )  <_  ( F `  z
) ) )
7362, 69, 723imtr4d 268 . . . . . . . . . . . 12  |-  ( ( ( F : RR --> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  ( ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  y ) ) )  oR  <_  F  ->  f  oR  <_  F ) )
7473rexlimdva 2895 . . . . . . . . . . 11  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  ->  ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  y ) ) )  oR  <_  F  ->  f  oR  <_  F ) )
7574anim1d 562 . . . . . . . . . 10  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  ->  ( ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  y ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f ) )  ->  ( f  oR  <_  F  /\  x  =  ( S.1 `  f ) ) ) )
7675reximdva 2878 . . . . . . . . 9  |-  ( F : RR --> ( 0 [,] +oo )  -> 
( E. f  e. 
dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  y ) ) )  oR  <_  F  /\  x  =  ( S.1 `  f ) )  ->  E. f  e.  dom  S.1 ( f  oR  <_  F  /\  x  =  ( S.1 `  f
) ) ) )
7726, 76syl5bi 217 . . . . . . . 8  |-  ( F : RR --> ( 0 [,] +oo )  -> 
( E. g  e. 
dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  y ) ) )  oR  <_  F  /\  x  =  ( S.1 `  g ) )  ->  E. f  e.  dom  S.1 ( f  oR  <_  F  /\  x  =  ( S.1 `  f
) ) ) )
7877ss2abdv 3511 . . . . . . 7  |-  ( F : RR --> ( 0 [,] +oo )  ->  { x  |  E. g  e.  dom  S.1 ( E. y  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  oR  <_  F  /\  x  =  ( S.1 `  g
) ) }  C_  { x  |  E. f  e.  dom  S.1 ( f  oR  <_  F  /\  x  =  ( S.1 `  f ) ) } )
7978sseld 3440 . . . . . 6  |-  ( F : RR --> ( 0 [,] +oo )  -> 
( b  e.  {
x  |  E. g  e.  dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  y ) ) )  oR  <_  F  /\  x  =  ( S.1 `  g ) ) }  ->  b  e.  { x  |  E. f  e.  dom  S.1 ( f  oR  <_  F  /\  x  =  ( S.1 `  f ) ) } ) )
80 simp3r 1026 . . . . . . . . . . 11  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  f  e.  dom  S.1  /\  ( f  oR  <_  F  /\  x  =  ( S.1 `  f
) ) )  ->  x  =  ( S.1 `  f ) )
8193ad2ant2 1019 . . . . . . . . . . 11  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  f  e.  dom  S.1  /\  ( f  oR  <_  F  /\  x  =  ( S.1 `  f
) ) )  -> 
( S.1 `  f )  e.  RR* )
8280, 81eqeltrd 2490 . . . . . . . . . 10  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  f  e.  dom  S.1  /\  ( f  oR  <_  F  /\  x  =  ( S.1 `  f
) ) )  ->  x  e.  RR* )
8382rexlimdv3a 2897 . . . . . . . . 9  |-  ( F : RR --> ( 0 [,] +oo )  -> 
( E. f  e. 
dom  S.1 ( f  oR  <_  F  /\  x  =  ( S.1 `  f ) )  ->  x  e.  RR* ) )
8483abssdv 3512 . . . . . . . 8  |-  ( F : RR --> ( 0 [,] +oo )  ->  { x  |  E. f  e.  dom  S.1 (
f  oR  <_  F  /\  x  =  ( S.1 `  f ) ) }  C_  RR* )
85 xrsupss 11471 . . . . . . . 8  |-  ( { x  |  E. f  e.  dom  S.1 ( f  oR  <_  F  /\  x  =  ( S.1 `  f ) ) } 
C_  RR*  ->  E. a  e.  RR*  ( A. b  e.  { x  |  E. f  e.  dom  S.1 (
f  oR  <_  F  /\  x  =  ( S.1 `  f ) ) }  -.  a  <  b  /\  A. b  e.  RR*  ( b  < 
a  ->  E. s  e.  { x  |  E. f  e.  dom  S.1 (
f  oR  <_  F  /\  x  =  ( S.1 `  f ) ) } b  < 
s ) ) )
8684, 85syl 17 . . . . . . 7  |-  ( F : RR --> ( 0 [,] +oo )  ->  E. a  e.  RR*  ( A. b  e.  { x  |  E. f  e.  dom  S.1 ( f  oR  <_  F  /\  x  =  ( S.1 `  f
) ) }  -.  a  <  b  /\  A. b  e.  RR*  ( b  <  a  ->  E. s  e.  { x  |  E. f  e.  dom  S.1 (
f  oR  <_  F  /\  x  =  ( S.1 `  f ) ) } b  < 
s ) ) )
876, 86supub 7872 . . . . . 6  |-  ( F : RR --> ( 0 [,] +oo )  -> 
( b  e.  {
x  |  E. f  e.  dom  S.1 ( f  oR  <_  F  /\  x  =  ( S.1 `  f ) ) }  ->  -.  sup ( { x  |  E. f  e.  dom  S.1 (
f  oR  <_  F  /\  x  =  ( S.1 `  f ) ) } ,  RR* ,  <  )  <  b
) )
8879, 87syld 42 . . . . 5  |-  ( F : RR --> ( 0 [,] +oo )  -> 
( b  e.  {
x  |  E. g  e.  dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  y ) ) )  oR  <_  F  /\  x  =  ( S.1 `  g ) ) }  ->  -.  sup ( { x  |  E. f  e.  dom  S.1 (
f  oR  <_  F  /\  x  =  ( S.1 `  f ) ) } ,  RR* ,  <  )  <  b
) )
8988imp 427 . . . 4  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  b  e.  { x  |  E. g  e.  dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  oR  <_  F  /\  x  =  ( S.1 `  g
) ) } )  ->  -.  sup ( { x  |  E. f  e.  dom  S.1 (
f  oR  <_  F  /\  x  =  ( S.1 `  f ) ) } ,  RR* ,  <  )  <  b
)
90 supxrlub 11488 . . . . . . . 8  |-  ( ( { x  |  E. f  e.  dom  S.1 (
f  oR  <_  F  /\  x  =  ( S.1 `  f ) ) }  C_  RR*  /\  b  e.  RR* )  ->  (
b  <  sup ( { x  |  E. f  e.  dom  S.1 (
f  oR  <_  F  /\  x  =  ( S.1 `  f ) ) } ,  RR* ,  <  )  <->  E. s  e.  { x  |  E. f  e.  dom  S.1 (
f  oR  <_  F  /\  x  =  ( S.1 `  f ) ) } b  < 
s ) )
9113, 90mpan 668 . . . . . . 7  |-  ( b  e.  RR*  ->  ( b  <  sup ( { x  |  E. f  e.  dom  S.1 ( f  oR  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  )  <->  E. s  e.  { x  |  E. f  e.  dom  S.1 (
f  oR  <_  F  /\  x  =  ( S.1 `  f ) ) } b  < 
s ) )
9291adantl 464 . . . . . 6  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  b  e.  RR* )  -> 
( b  <  sup ( { x  |  E. f  e.  dom  S.1 (
f  oR  <_  F  /\  x  =  ( S.1 `  f ) ) } ,  RR* ,  <  )  <->  E. s  e.  { x  |  E. f  e.  dom  S.1 (
f  oR  <_  F  /\  x  =  ( S.1 `  f ) ) } b  < 
s ) )
93 simprrr 767 . . . . . . . . . . . . . . 15  |-  ( ( ( F : RR --> ( 0 [,] +oo )  /\  b  e.  RR* )  /\  ( f  e. 
dom  S.1  /\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  ->  s  =  ( S.1 `  f
) )
9493breq2d 4406 . . . . . . . . . . . . . 14  |-  ( ( ( F : RR --> ( 0 [,] +oo )  /\  b  e.  RR* )  /\  ( f  e. 
dom  S.1  /\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  ->  (
b  <  s  <->  b  <  ( S.1 `  f ) ) )
95 simplll 760 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( F : RR
--> ( 0 [,] +oo )  /\  b  e.  RR* )  /\  ( f  e. 
dom  S.1  /\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  /\  b  <  ( S.1 `  f
) )  ->  F : RR --> ( 0 [,] +oo ) )
96 i1f0 22278 . . . . . . . . . . . . . . . . . . 19  |-  ( RR 
X.  { 0 } )  e.  dom  S.1
97 2rp 11188 . . . . . . . . . . . . . . . . . . . . 21  |-  2  e.  RR+
9897ne0ii 3744 . . . . . . . . . . . . . . . . . . . 20  |-  RR+  =/=  (/)
99 ffvelrn 5963 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  z  e.  RR )  ->  ( F `  z
)  e.  ( 0 [,] +oo ) )
100 elxrge0 11600 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F `  z )  e.  ( 0 [,] +oo )  <->  ( ( F `
 z )  e. 
RR*  /\  0  <_  ( F `  z ) ) )
10199, 100sylib 196 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  z  e.  RR )  ->  ( ( F `  z )  e.  RR*  /\  0  <_  ( F `  z ) ) )
102101simprd 461 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  z  e.  RR )  ->  0  <_  ( F `  z ) )
103102ralrimiva 2817 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F : RR --> ( 0 [,] +oo )  ->  A. z  e.  RR  0  <_  ( F `  z ) )
10463a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F : RR --> ( 0 [,] +oo )  ->  RR  e.  _V )
105 c0ex 9540 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  0  e.  _V
106105a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  z  e.  RR )  ->  0  e.  _V )
107 eqidd 2403 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F : RR --> ( 0 [,] +oo )  -> 
( z  e.  RR  |->  0 )  =  ( z  e.  RR  |->  0 ) )
108104, 106, 99, 107, 67ofrfval2 6495 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F : RR --> ( 0 [,] +oo )  -> 
( ( z  e.  RR  |->  0 )  oR  <_  F  <->  A. z  e.  RR  0  <_  ( F `  z )
) )
109103, 108mpbird 232 . . . . . . . . . . . . . . . . . . . . 21  |-  ( F : RR --> ( 0 [,] +oo )  -> 
( z  e.  RR  |->  0 )  oR  <_  F )
110109ralrimivw 2818 . . . . . . . . . . . . . . . . . . . 20  |-  ( F : RR --> ( 0 [,] +oo )  ->  A. y  e.  RR+  (
z  e.  RR  |->  0 )  oR  <_  F )
111 r19.2z 3861 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
RR+  =/=  (/)  /\  A. y  e.  RR+  ( z  e.  RR  |->  0 )  oR  <_  F
)  ->  E. y  e.  RR+  ( z  e.  RR  |->  0 )  oR  <_  F )
11298, 110, 111sylancr 661 . . . . . . . . . . . . . . . . . . 19  |-  ( F : RR --> ( 0 [,] +oo )  ->  E. y  e.  RR+  (
z  e.  RR  |->  0 )  oR  <_  F )
113 fveq2 5805 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( S.1 `  g
)  =  ( S.1 `  ( RR  X.  {
0 } ) ) )
114 itg10 22279 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( S.1 `  ( RR  X.  {
0 } ) )  =  0
115113, 114syl6req 2460 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( g  =  ( RR  X.  { 0 } )  ->  0  =  ( S.1 `  g ) )
116115biantrud 505 . . . . . . . . . . . . . . . . . . . . 21  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  y ) ) )  oR  <_  F  <->  ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  oR  <_  F  /\  0  =  ( S.1 `  g
) ) ) )
117 fveq1 5804 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( g `  z )  =  ( ( RR  X.  {
0 } ) `  z ) )
118105fvconst2 6063 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  e.  RR  ->  (
( RR  X.  {
0 } ) `  z )  =  0 )
119117, 118sylan9eq 2463 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( g  =  ( RR 
X.  { 0 } )  /\  z  e.  RR )  ->  (
g `  z )  =  0 )
120 iftrue 3890 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( g `  z )  =  0  ->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) )  =  0 )
121119, 120syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( g  =  ( RR 
X.  { 0 } )  /\  z  e.  RR )  ->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) )  =  0 )
122121mpteq2dva 4480 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  y ) ) )  =  ( z  e.  RR  |->  0 ) )
123122breq1d 4404 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( ( z  e.  RR  |->  if ( ( g `  z
)  =  0 ,  0 ,  ( ( g `  z )  +  y ) ) )  oR  <_  F 
<->  ( z  e.  RR  |->  0 )  oR  <_  F ) )
124123rexbidv 2917 . . . . . . . . . . . . . . . . . . . . 21  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  y ) ) )  oR  <_  F  <->  E. y  e.  RR+  (
z  e.  RR  |->  0 )  oR  <_  F ) )
125116, 124bitr3d 255 . . . . . . . . . . . . . . . . . . . 20  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( ( E. y  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  oR  <_  F  /\  0  =  ( S.1 `  g
) )  <->  E. y  e.  RR+  ( z  e.  RR  |->  0 )  oR  <_  F )
)
126125rspcev 3159 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( RR  X.  {
0 } )  e. 
dom  S.1  /\  E. y  e.  RR+  ( z  e.  RR  |->  0 )  oR  <_  F )  ->  E. g  e.  dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  oR  <_  F  /\  0  =  ( S.1 `  g
) ) )
12796, 112, 126sylancr 661 . . . . . . . . . . . . . . . . . 18  |-  ( F : RR --> ( 0 [,] +oo )  ->  E. g  e.  dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  oR  <_  F  /\  0  =  ( S.1 `  g
) ) )
128 id 22 . . . . . . . . . . . . . . . . . . 19  |-  ( b  = -oo  ->  b  = -oo )
129 mnflt 11304 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  e.  RR  -> -oo  <  0 )
13048, 129mp1i 13 . . . . . . . . . . . . . . . . . . 19  |-  ( b  = -oo  -> -oo  <  0 )
131128, 130eqbrtrd 4414 . . . . . . . . . . . . . . . . . 18  |-  ( b  = -oo  ->  b  <  0 )
132 eqeq1 2406 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  0  ->  (
a  =  ( S.1 `  g )  <->  0  =  ( S.1 `  g ) ) )
133132anbi2d 702 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  0  ->  (
( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  oR  <_  F  /\  a  =  ( S.1 `  g
) )  <->  ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z
)  =  0 ,  0 ,  ( ( g `  z )  +  y ) ) )  oR  <_  F  /\  0  =  ( S.1 `  g ) ) ) )
134133rexbidv 2917 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  0  ->  ( E. g  e.  dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  oR  <_  F  /\  a  =  ( S.1 `  g
) )  <->  E. g  e.  dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  y ) ) )  oR  <_  F  /\  0  =  ( S.1 `  g ) ) ) )
135 breq2 4398 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  0  ->  (
b  <  a  <->  b  <  0 ) )
136134, 135anbi12d 709 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  0  ->  (
( E. g  e. 
dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  y ) ) )  oR  <_  F  /\  a  =  ( S.1 `  g ) )  /\  b  <  a
)  <->  ( E. g  e.  dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  y ) ) )  oR  <_  F  /\  0  =  ( S.1 `  g ) )  /\  b  <  0
) ) )
137105, 136spcev 3150 . . . . . . . . . . . . . . . . . 18  |-  ( ( E. g  e.  dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  oR  <_  F  /\  0  =  ( S.1 `  g
) )  /\  b  <  0 )  ->  E. a
( E. g  e. 
dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  y ) ) )  oR  <_  F  /\  a  =  ( S.1 `  g ) )  /\  b  <  a
) )
138127, 131, 137syl2an 475 . . . . . . . . . . . . . . . . 17  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  b  = -oo )  ->  E. a ( E. g  e.  dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  oR  <_  F  /\  a  =  ( S.1 `  g
) )  /\  b  <  a ) )
13995, 138sylan 469 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( F : RR --> ( 0 [,] +oo )  /\  b  e.  RR* )  /\  ( f  e.  dom  S.1 
/\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  /\  b  < 
( S.1 `  f ) )  /\  b  = -oo )  ->  E. a
( E. g  e. 
dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  y ) ) )  oR  <_  F  /\  a  =  ( S.1 `  g ) )  /\  b  <  a
) )
140 simp-4r 769 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( F : RR --> ( 0 [,] +oo )  /\  b  e.  RR* )  /\  ( f  e.  dom  S.1 
/\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  /\  b  < 
( S.1 `  f ) )  /\  b  =/= -oo )  ->  b  e. 
RR* )
1418adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f  e.  dom  S.1  /\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f
) ) )  -> 
( S.1 `  f )  e.  RR )
142141ad3antlr 729 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( F : RR --> ( 0 [,] +oo )  /\  b  e.  RR* )  /\  ( f  e.  dom  S.1 
/\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  /\  b  < 
( S.1 `  f ) )  /\  b  =/= -oo )  ->  ( S.1 `  f )  e.  RR )
143 simpllr 761 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( F : RR
--> ( 0 [,] +oo )  /\  b  e.  RR* )  /\  ( f  e. 
dom  S.1  /\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  /\  b  <  ( S.1 `  f
) )  ->  b  e.  RR* )
144 ngtmnft 11339 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( b  e.  RR*  ->  ( b  = -oo  <->  -. -oo  <  b ) )
145144biimprd 223 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  e.  RR*  ->  ( -. -oo  <  b  ->  b  = -oo ) )
146145necon1ad 2619 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  e.  RR*  ->  ( b  =/= -oo  -> -oo  <  b ) )
147146imp 427 . . . . . . . . . . . . . . . . . . 19  |-  ( ( b  e.  RR*  /\  b  =/= -oo )  -> -oo  <  b )
148143, 147sylan 469 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( F : RR --> ( 0 [,] +oo )  /\  b  e.  RR* )  /\  ( f  e.  dom  S.1 
/\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  /\  b  < 
( S.1 `  f ) )  /\  b  =/= -oo )  -> -oo  <  b )
149 simpr 459 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  b  e.  RR* )  -> 
b  e.  RR* )
1509adantr 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( f  e.  dom  S.1  /\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f
) ) )  -> 
( S.1 `  f )  e.  RR* )
151149, 150anim12i 564 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( F : RR --> ( 0 [,] +oo )  /\  b  e.  RR* )  /\  ( f  e. 
dom  S.1  /\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  ->  (
b  e.  RR*  /\  ( S.1 `  f )  e. 
RR* ) )
152 xrltle 11326 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( b  e.  RR*  /\  ( S.1 `  f )  e. 
RR* )  ->  (
b  <  ( S.1 `  f )  ->  b  <_  ( S.1 `  f
) ) )
153152imp 427 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( b  e.  RR*  /\  ( S.1 `  f
)  e.  RR* )  /\  b  <  ( S.1 `  f ) )  -> 
b  <_  ( S.1 `  f ) )
154151, 153sylan 469 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( F : RR
--> ( 0 [,] +oo )  /\  b  e.  RR* )  /\  ( f  e. 
dom  S.1  /\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  /\  b  <  ( S.1 `  f
) )  ->  b  <_  ( S.1 `  f
) )
155154adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( F : RR --> ( 0 [,] +oo )  /\  b  e.  RR* )  /\  ( f  e.  dom  S.1 
/\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  /\  b  < 
( S.1 `  f ) )  /\  b  =/= -oo )  ->  b  <_ 
( S.1 `  f ) )
156 xrre 11341 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( b  e.  RR*  /\  ( S.1 `  f
)  e.  RR )  /\  ( -oo  <  b  /\  b  <_  ( S.1 `  f ) ) )  ->  b  e.  RR )
157140, 142, 148, 155, 156syl22anc 1231 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( F : RR --> ( 0 [,] +oo )  /\  b  e.  RR* )  /\  ( f  e.  dom  S.1 
/\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  /\  b  < 
( S.1 `  f ) )  /\  b  =/= -oo )  ->  b  e.  RR )
158127ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( F : RR
--> ( 0 [,] +oo )  /\  ( f  e. 
dom  S.1  /\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  /\  (
b  <  ( S.1 `  f )  /\  b  e.  RR ) )  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  ->  E. g  e.  dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  oR  <_  F  /\  0  =  ( S.1 `  g
) ) )
159 simplrl 762 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( F : RR
--> ( 0 [,] +oo )  /\  ( f  e. 
dom  S.1  /\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  /\  (
b  <  ( S.1 `  f )  /\  b  e.  RR ) )  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
b  <  ( S.1 `  f ) )
160 simplrl 762 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( F : RR --> ( 0 [,] +oo )  /\  ( f  e. 
dom  S.1  /\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  /\  (
b  <  ( S.1 `  f )  /\  b  e.  RR ) )  -> 
f  e.  dom  S.1 )
161 simpl 455 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( f  e.  dom  S.1  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
f  e.  dom  S.1 )
162 cnvimass 5298 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( `' f " ( ran  f  \  { 0 } ) )  C_  dom  f
163 fdm 5674 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f : RR --> RR  ->  dom  f  =  RR )
16435, 163syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f  e.  dom  S.1  ->  dom  f  =  RR )
165162, 164syl5sseq 3489 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f  e.  dom  S.1  ->  ( `' f " ( ran  f  \  { 0 } ) )  C_  RR )
166165adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( f  e.  dom  S.1  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
( `' f "
( ran  f  \  { 0 } ) )  C_  RR )
167 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( f  e.  dom  S.1  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )
168163eqcomd 2410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( f : RR --> RR  ->  RR  =  dom  f )
169 ffun 5672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( f : RR --> RR  ->  Fun  f )
170 difpreima 5949 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( Fun  f  ->  ( `' f " ( ran  f  \  { 0 } ) )  =  ( ( `' f " ran  f )  \  ( `' f " {
0 } ) ) )
171169, 170syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( f : RR --> RR  ->  ( `' f " ( ran  f  \  { 0 } ) )  =  ( ( `' f
" ran  f )  \  ( `' f
" { 0 } ) ) )
172 cnvimarndm 5299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( `' f " ran  f
)  =  dom  f
173172difeq1i 3556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( `' f " ran  f )  \  ( `' f " {
0 } ) )  =  ( dom  f  \  ( `' f
" { 0 } ) )
174171, 173syl6eq 2459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( f : RR --> RR  ->  ( `' f " ( ran  f  \  { 0 } ) )  =  ( dom  f  \ 
( `' f " { 0 } ) ) )
175168, 174difeq12d 3561 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( f : RR --> RR  ->  ( RR  \  ( `' f " ( ran  f  \  { 0 } ) ) )  =  ( dom  f  \  ( dom  f  \  ( `' f
" { 0 } ) ) ) )
176 cnvimass 5298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( `' f " { 0 } )  C_  dom  f
177 dfss4 3683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( `' f " {
0 } )  C_  dom  f  <->  ( dom  f  \  ( dom  f  \  ( `' f
" { 0 } ) ) )  =  ( `' f " { 0 } ) )
178176, 177mpbi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( dom  f  \  ( dom  f  \  ( `' f " { 0 } ) ) )  =  ( `' f
" { 0 } )
179175, 178syl6eq 2459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( f : RR --> RR  ->  ( RR  \  ( `' f " ( ran  f  \  { 0 } ) ) )  =  ( `' f
" { 0 } ) )
180179eleq2d 2472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( f : RR --> RR  ->  ( z  e.  ( RR 
\  ( `' f
" ( ran  f  \  { 0 } ) ) )  <->  z  e.  ( `' f " {
0 } ) ) )
181 ffn 5670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( f : RR --> RR  ->  f  Fn  RR )
182 fniniseg 5942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( f  Fn  RR  ->  (
z  e.  ( `' f " { 0 } )  <->  ( z  e.  RR  /\  ( f `
 z )  =  0 ) ) )
183 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( z  e.  RR  /\  ( f `  z
)  =  0 )  ->  ( f `  z )  =  0 )
184182, 183syl6bi 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( f  Fn  RR  ->  (
z  e.  ( `' f " { 0 } )  ->  (
f `  z )  =  0 ) )
185181, 184syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( f : RR --> RR  ->  ( z  e.  ( `' f " { 0 } )  ->  (
f `  z )  =  0 ) )
186180, 185sylbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f : RR --> RR  ->  ( z  e.  ( RR 
\  ( `' f
" ( ran  f  \  { 0 } ) ) )  ->  (
f `  z )  =  0 ) )
18735, 186syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f  e.  dom  S.1  ->  ( z  e.  ( RR 
\  ( `' f
" ( ran  f  \  { 0 } ) ) )  ->  (
f `  z )  =  0 ) )
188187imp 427 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( f  e.  dom  S.1  /\  z  e.  ( RR 
\  ( `' f
" ( ran  f  \  { 0 } ) ) ) )  -> 
( f `  z
)  =  0 )
189188adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( f  e.  dom  S.1 
/\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =  0 )  /\  z  e.  ( RR  \  ( `' f " ( ran  f  \  { 0 } ) ) ) )  ->  ( f `  z )  =  0 )
190161, 166, 167, 189itg10a 22301 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( f  e.  dom  S.1  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
( S.1 `  f )  =  0 )
191160, 190sylan 469 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( F : RR
--> ( 0 [,] +oo )  /\  ( f  e. 
dom  S.1  /\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  /\  (
b  <  ( S.1 `  f )  /\  b  e.  RR ) )  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
( S.1 `  f )  =  0 )
192159, 191breqtrd 4418 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( F : RR
--> ( 0 [,] +oo )  /\  ( f  e. 
dom  S.1  /\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  /\  (
b  <  ( S.1 `  f )  /\  b  e.  RR ) )  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
b  <  0 )
193158, 192, 137syl2anc 659 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( F : RR
--> ( 0 [,] +oo )  /\  ( f  e. 
dom  S.1  /\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  /\  (
b  <  ( S.1 `  f )  /\  b  e.  RR ) )  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  ->  E. a ( E. g  e.  dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  y ) ) )  oR  <_  F  /\  a  =  ( S.1 `  g ) )  /\  b  <  a
) )
194 simprl 756 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  ( f  e.  dom  S.1 
/\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  ->  f  e.  dom  S.1 )
195 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( b  <  ( S.1 `  f )  /\  b  e.  RR )  ->  b  e.  RR )
196194, 195anim12i 564 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( F : RR --> ( 0 [,] +oo )  /\  ( f  e. 
dom  S.1  /\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  /\  (
b  <  ( S.1 `  f )  /\  b  e.  RR ) )  -> 
( f  e.  dom  S.1 
/\  b  e.  RR ) )
19763a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  RR  e.  _V )
198 fvex 5815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( f `
 u )  e. 
_V
199198a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( f  e. 
dom  S.1  /\  b  e.  RR )  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =/=  0 )  /\  u  e.  RR )  ->  ( f `  u
)  e.  _V )
200 ovex 6262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) )  e.  _V
201200, 105ifex 3952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 )  e. 
_V
202201a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( f  e. 
dom  S.1  /\  b  e.  RR )  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =/=  0 )  /\  u  e.  RR )  ->  if ( u  e.  ( `' f "
( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ,  0 )  e.  _V )
20335feqmptd 5858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( f  e.  dom  S.1  ->  f  =  ( u  e.  RR  |->  ( f `  u ) ) )
204203ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  f  =  ( u  e.  RR  |->  ( f `  u
) ) )
205 eqidd 2403 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( u  e.  RR  |->  if ( u  e.  ( `' f
" ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) )  =  ( u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) ) )
206197, 199, 202, 204, 205offval2 6494 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( f  oF  -  (
u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) ) )  =  ( u  e.  RR  |->  ( ( f `  u )  -  if ( u  e.  ( `' f
" ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) ) ) )
207 ovif2 6317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( f `  u )  -  if ( u  e.  ( `' f
" ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) )  =  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( f `  u )  -  (
( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ) ,  ( ( f `  u )  -  0 ) )
208172, 163syl5eq 2455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( f : RR --> RR  ->  ( `' f " ran  f )  =  RR )
209208difeq1d 3559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( f : RR --> RR  ->  ( ( `' f " ran  f )  \  ( `' f " {
0 } ) )  =  ( RR  \ 
( `' f " { 0 } ) ) )
210171, 209eqtrd 2443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( f : RR --> RR  ->  ( `' f " ( ran  f  \  { 0 } ) )  =  ( RR  \  ( `' f " {
0 } ) ) )
211210eleq2d 2472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( f : RR --> RR  ->  ( u  e.  ( `' f " ( ran  f  \  { 0 } ) )  <->  u  e.  ( RR  \  ( `' f " {
0 } ) ) ) )
21235, 211syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( f  e.  dom  S.1  ->  ( u  e.  ( `' f " ( ran  f  \  { 0 } ) )  <->  u  e.  ( RR  \  ( `' f " {
0 } ) ) ) )
213212ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( f  e. 
dom  S.1  /\  b  e.  RR )  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =/=  0 )  /\  u  e.  RR )  ->  ( u  e.  ( `' f " ( ran  f  \  { 0 } ) )  <->  u  e.  ( RR  \  ( `' f " {
0 } ) ) ) )
214 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( f  e. 
dom  S.1  /\  b  e.  RR )  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =/=  0 )  /\  u  e.  RR )  ->  u  e.  RR )
215214biantrurd 506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( f  e. 
dom  S.1  /\  b  e.  RR )  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =/=  0 )  /\  u  e.  RR )  ->  ( -.  u  e.  ( `' f " { 0 } )  <-> 
( u  e.  RR  /\ 
-.  u  e.  ( `' f " {
0 } ) ) ) )
216 eldif 3423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( u  e.  ( RR  \ 
( `' f " { 0 } ) )  <->  ( u  e.  RR  /\  -.  u  e.  ( `' f " { 0 } ) ) )
217215, 216syl6bbr 263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( f  e. 
dom  S.1  /\  b  e.  RR )  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =/=  0 )  /\  u  e.  RR )  ->  ( -.  u  e.  ( `' f " { 0 } )  <-> 
u  e.  ( RR 
\  ( `' f
" { 0 } ) ) ) )
218213, 217bitr4d 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( f  e. 
dom  S.1  /\  b  e.  RR )  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =/=  0 )  /\  u  e.  RR )  ->  ( u  e.  ( `' f " ( ran  f  \  { 0 } ) )  <->  -.  u  e.  ( `' f " { 0 } ) ) )
219218con2bid 327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( f  e. 
dom  S.1  /\  b  e.  RR )  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =/=  0 )  /\  u  e.  RR )  ->  ( u  e.  ( `' f " {
0 } )  <->  -.  u  e.  ( `' f "
( ran  f  \  { 0 } ) ) ) )
220 fniniseg 5942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( f  Fn  RR  ->  (
u  e.  ( `' f " { 0 } )  <->  ( u  e.  RR  /\  ( f `
 u )  =  0 ) ) )
22135, 181, 2203syl 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( f  e.  dom  S.1  ->  ( u  e.  ( `' f " { 0 } )  <->  ( u  e.  RR  /\  ( f `
 u )  =  0 ) ) )
222221ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( f  e. 
dom  S.1  /\  b  e.  RR )  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =/=  0 )  /\  u  e.  RR )  ->  ( u  e.  ( `' f " {
0 } )  <->  ( u  e.  RR  /\  ( f `
 u )  =  0 ) ) )
223219, 222bitr3d 255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( f  e. 
dom  S.1  /\  b  e.  RR )  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =/=  0 )  /\  u  e.  RR )  ->  ( -.  u  e.  ( `' f "
( ran  f  \  { 0 } ) )  <->  ( u  e.  RR  /\  ( f `
 u )  =  0 ) ) )
224 oveq1 6241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( f `  u )  =  0  ->  (
( f `  u
)  -  0 )  =  ( 0  -  0 ) )
225 0m0e0 10606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( 0  -  0 )  =  0
226224, 225syl6eq 2459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( f `  u )  =  0  ->  (
( f `  u
)  -  0 )  =  0 )
227226adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( u  e.  RR  /\  ( f `  u
)  =  0 )  ->  ( ( f `
 u )  - 
0 )  =  0 )
228223, 227syl6bi 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( f  e. 
dom  S.1  /\  b  e.  RR )  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =/=  0 )  /\  u  e.  RR )  ->  ( -.  u  e.  ( `' f "
( ran  f  \  { 0 } ) )  ->  ( (
f `  u )  -  0 )  =  0 ) )
229228imp 427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( f  e.  dom  S.1  /\  b  e.  RR )  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =/=  0 )  /\  u  e.  RR )  /\  -.  u  e.  ( `' f " ( ran  f  \  { 0 } ) ) )  ->  ( ( f `
 u )  - 
0 )  =  0 )
230229ifeq2da 3915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( f  e. 
dom  S.1  /\  b  e.  RR )  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =/=  0 )  /\  u  e.  RR )  ->  if ( u  e.  ( `' f "
( ran  f  \  { 0 } ) ) ,  ( ( f `  u )  -  ( ( ( S.1 `  f )  -  b )  / 
( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ) ,  ( ( f `  u )  -  0 ) )  =  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( f `  u )  -  (
( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ) ,  0 ) )
231207, 230syl5eq 2455 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( f  e. 
dom  S.1  /\  b  e.  RR )  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =/=  0 )  /\  u  e.  RR )  ->  ( ( f `  u )  -  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) )  =  if ( u  e.  ( `' f
" ( ran  f  \  { 0 } ) ) ,  ( ( f `  u )  -  ( ( ( S.1 `  f )  -  b )  / 
( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ) ,  0 ) )
232231mpteq2dva 4480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( u  e.  RR  |->  ( ( f `
 u )  -  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) ) )  =  ( u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( f `  u )  -  (
( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ) ,  0 ) ) )
233206, 232eqtrd 2443 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( f  oF  -  (
u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) ) )  =  ( u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( f `  u )  -  (
( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ) ,  0 ) ) )
234 simpll 752 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  f  e.  dom  S.1 )
235200a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( f  e. 
dom  S.1  /\  b  e.  RR )  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =/=  0 )  /\  u  e.  RR )  ->  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) )  e.  _V )
236 1ex 9541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  1  e.  _V
237236, 105ifex 3952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  1 ,  0 )  e.  _V
238237a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( f  e. 
dom  S.1  /\  b  e.  RR )  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =/=  0 )  /\  u  e.  RR )  ->  if ( u  e.  ( `' f "
( ran  f  \  { 0 } ) ) ,  1 ,  0 )  e.  _V )
239 fconstmpt 4986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( RR 
X.  { ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) } )  =  ( u  e.  RR  |->  ( ( ( S.1 `  f )  -  b )  / 
( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) )
240239a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( RR  X.  { ( ( ( S.1 `  f )  -  b )  / 
( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) } )  =  ( u  e.  RR  |->  ( ( ( S.1 `  f )  -  b )  / 
( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ) )
241 eqidd 2403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( u  e.  RR  |->  if ( u  e.  ( `' f
" ( ran  f  \  { 0 } ) ) ,  1 ,  0 ) )  =  ( u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  1 ,  0 ) ) )
242197, 235, 238, 240, 241offval2 6494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( ( RR  X.  { ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) } )  oF  x.  (
u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  1 ,  0 ) ) )  =  ( u  e.  RR  |->  ( ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) )  x.  if ( u  e.  ( `' f
" ( ran  f  \  { 0 } ) ) ,  1 ,  0 ) ) ) )
243 ovif2 6317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) )  x.  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  1 ,  0 ) )  =  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( ( S.1 `  f )  -  b )  / 
( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) )  x.  1 ) ,  ( ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) )  x.  0 ) )
244 resubcl 9839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( S.1 `  f
)  e.  RR  /\  b  e.  RR )  ->  ( ( S.1 `  f
)  -  b )  e.  RR )
2458, 244sylan 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( f  e.  dom  S.1  /\  b  e.  RR )  ->  ( ( S.1 `  f )  -  b
)  e.  RR )
246245adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( ( S.1 `  f )  -  b )  e.  RR )
247 2re 10566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  2  e.  RR
248 i1fima 22269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( f  e.  dom  S.1  ->  ( `' f " ( ran  f  \  { 0 } ) )  e. 
dom  vol )
249 mblvol 22125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( `' f " ( ran  f  \  { 0 } ) )  e. 
dom  vol  ->  ( vol `  ( `' f "
( ran  f  \  { 0 } ) ) )  =  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) )
250248, 249syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( f  e.  dom  S.1  ->  ( vol `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) ) )
251 neldifsn 4098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  -.  0  e.  ( ran  f  \  { 0 } )
252 i1fima2 22270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( f  e.  dom  S.1  /\ 
-.  0  e.  ( ran  f  \  {
0 } ) )  ->  ( vol `  ( `' f " ( ran  f  \  { 0 } ) ) )  e.  RR )
253251, 252mpan2 669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( f  e.  dom  S.1  ->  ( vol `  ( `' f " ( ran  f  \  { 0 } ) ) )  e.  RR )
254250, 253eqeltrrd 2491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( f  e.  dom  S.1  ->  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  e.  RR )
255 remulcl 9527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( 2  e.  RR  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  e.  RR )  -> 
( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) )  e.  RR )
256247, 254, 255sylancr 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( f  e.  dom  S.1  ->  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) )  e.  RR )
257256ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( 2  x.  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) ) )  e.  RR )
258 2cnd 10569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  2  e.  CC )
259254ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( vol* `  ( `' f
" ( ran  f  \  { 0 } ) ) )  e.  RR )
260259recnd 9572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( vol* `  ( `' f
" ( ran  f  \  { 0 } ) ) )  e.  CC )
261 2ne0 10589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  2  =/=  0
262261a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  2  =/=  0 )
263 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( vol* `  ( `' f
" ( ran  f  \  { 0 } ) ) )  =/=  0
)
264258, 260, 262, 263mulne0d 10162 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( 2  x.  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) ) )  =/=  0 )
265246, 257, 264redivcld 10333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( (
( S.1 `  f )  -  b )  / 
( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) )  e.  RR )
266265recnd 9572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( (
( S.1 `  f )  -  b )  / 
( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) )  e.  CC )
267266mulid1d 9563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( (
( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) )  x.  1 )  =  ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) )
268266mul01d 9733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( (
( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) )  x.  0 )  =  0 )
269267, 268ifeq12d 3904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  if (
u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( ( S.1 `  f )  -  b )  / 
( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) )  x.  1 ) ,  ( ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) )  x.  0 ) )  =  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) )
270243, 269syl5eq 2455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( (
( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) )  x.  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  1 ,  0 ) )  =  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) )
271270mpteq2dv 4481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( u  e.  RR  |->  ( ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) )  x.  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  1 ,  0 ) ) )  =  ( u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) ) )
272242, 271eqtrd 2443 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( ( RR  X.  { ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) } )  oF  x.  (
u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  1 ,  0 ) ) )  =  ( u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) ) )
273 eqid 2402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  1 ,  0 ) )  =  ( u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  1 ,  0 ) )
274273i1f1 22281 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( `' f "
( ran  f  \  { 0 } ) )  e.  dom  vol  /\  ( vol `  ( `' f " ( ran  f  \  { 0 } ) ) )  e.  RR )  -> 
( u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  1 ,  0 ) )  e.  dom  S.1 )
275248, 253, 274syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( f  e.  dom  S.1  ->  ( u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  1 ,  0 ) )  e.  dom  S.1 )
276275ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( u  e.  RR  |->  if ( u  e.  ( `' f
" ( ran  f  \  { 0 } ) ) ,  1 ,  0 ) )  e. 
dom  S.1 )
277276, 265i1fmulc 22294 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( ( RR  X.  { ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) } )  oF  x.  (
u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  1 ,  0 ) ) )  e.  dom  S.1 )
278272, 277eqeltrrd 2491 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( u  e.  RR  |->  if ( u  e.  ( `' f
" ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) )  e.  dom  S.1 )
279 i1fsub 22299 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( f  e.  dom  S.1  /\  ( u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) )  e.  dom  S.1 )  ->  ( f  oF  -  ( u  e.  RR  |->  if ( u  e.  ( `' f
" ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) ) )  e. 
dom  S.1 )
280234, 278, 279syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( f  oF  -  (
u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) ) )  e.  dom  S.1 )
281233, 280eqeltrrd 2491 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( u  e.  RR  |->  if ( u  e.  ( `' f
" ( ran  f  \  { 0 } ) ) ,  ( ( f `  u )  -  ( ( ( S.1 `  f )  -  b )  / 
( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ) ,  0 ) )  e. 
dom  S.1 )
282 eleq1 2474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( u  =  z  ->  (
u  e.  ( `' f " ( ran  f  \  { 0 } ) )  <->  z  e.  ( `' f " ( ran  f  \  { 0 } ) ) ) )
283 fveq2 5805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( u  =  z  ->  (
f `  u )  =  ( f `  z ) )
284283oveq1d 6249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( u  =  z  ->  (
( f `  u
)  -  ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) )  =  ( ( f `  z )  -  (
( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ) )
285282, 284ifbieq1d 3907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( u  =  z  ->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( f `  u )  -  (
( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ) ,  0 )  =  if ( z  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( f `  z )  -  (
( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ) ,  0 ) )
286 eqid 2402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( f `  u )  -  (
( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ) ,  0 ) )  =  ( u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( f `  u )  -  (
( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ) ,  0 ) )
287 ovex 6262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( f `  z )  -  ( ( ( S.1 `  f )  -  b )  / 
( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) )  e. 
_V
288287, 105ifex 3952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  if ( z  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( f `  z )  -  (
( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ) ,  0 )  e.  _V
289285, 286, 288fvmpt 5888 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( z  e.  RR  ->  (
( u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( f `  u )  -  (
( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ) ,  0 ) ) `  z )  =  if ( z  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( f `  z )  -  (
( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ) ,  0 ) )
290289breq2d 4406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  e.  RR  ->  (
0  <_  ( (
u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( f `  u )  -  (
( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ) ,  0 ) ) `  z )  <->  0  <_  if ( z  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( f `  z )  -  (
( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ) ,  0 ) ) )
291290, 289ifbieq1d 3907 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  e.  RR  ->  if ( 0  <_  (
( u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( f `  u )  -  (
( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ) ,  0 ) ) `  z ) ,  ( ( u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( f `  u )  -  (
( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ) ,  0 ) ) `  z ) ,  0 )  =  if ( 0  <_  if (
z  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( f `  z )  -  (
( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ) ,  0 ) ,  if ( z  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( f `  z )  -  (
( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ) ,  0 ) ,  0 ) )
292 iftrue 3890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 0  <_  ( (
f `  z )  -  ( ( ( S.1 `  f )  -  b )  / 
( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )