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

Theorem itg2addnclem 28396
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 2438 . . 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 21181 . 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 7689 . . 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 11110 . . . . 5  |-  <  Or  RR*
65a1i 11 . . . 4  |-  ( F : RR --> ( 0 [,] +oo )  ->  <  Or  RR* )
7 simprr 756 . . . . . . . 8  |-  ( ( f  e.  dom  S.1  /\  ( f  oR  <_  F  /\  x  =  ( S.1 `  f
) ) )  ->  x  =  ( S.1 `  f ) )
8 itg1cl 21138 . . . . . . . . . 10  |-  ( f  e.  dom  S.1  ->  ( S.1 `  f )  e.  RR )
98rexrd 9425 . . . . . . . . 9  |-  ( f  e.  dom  S.1  ->  ( S.1 `  f )  e.  RR* )
109adantr 465 . . . . . . . 8  |-  ( ( f  e.  dom  S.1  /\  ( f  oR  <_  F  /\  x  =  ( S.1 `  f
) ) )  -> 
( S.1 `  f )  e.  RR* )
117, 10eqeltrd 2512 . . . . . . 7  |-  ( ( f  e.  dom  S.1  /\  ( f  oR  <_  F  /\  x  =  ( S.1 `  f
) ) )  ->  x  e.  RR* )
1211rexlimiva 2831 . . . . . 6  |-  ( E. f  e.  dom  S.1 ( f  oR  <_  F  /\  x  =  ( S.1 `  f
) )  ->  x  e.  RR* )
1312abssi 3422 . . . . 5  |-  { x  |  E. f  e.  dom  S.1 ( f  oR  <_  F  /\  x  =  ( S.1 `  f
) ) }  C_  RR*
14 supxrcl 11269 . . . . 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 12 . . . 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 5685 . . . . . . . . . . . . . . . 16  |-  ( g  =  f  ->  (
g `  z )  =  ( f `  z ) )
1716eqeq1d 2446 . . . . . . . . . . . . . . 15  |-  ( g  =  f  ->  (
( g `  z
)  =  0  <->  (
f `  z )  =  0 ) )
1816oveq1d 6101 . . . . . . . . . . . . . . 15  |-  ( g  =  f  ->  (
( g `  z
)  +  y )  =  ( ( f `
 z )  +  y ) )
1917, 18ifbieq2d 3809 . . . . . . . . . . . . . 14  |-  ( g  =  f  ->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) )  =  if ( ( f `  z
)  =  0 ,  0 ,  ( ( f `  z )  +  y ) ) )
2019mpteq2dv 4374 . . . . . . . . . . . . 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 4297 . . . . . . . . . . . 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 2731 . . . . . . . . . . 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 5686 . . . . . . . . . . . 12  |-  ( g  =  f  ->  ( S.1 `  g )  =  ( S.1 `  f
) )
2423eqeq2d 2449 . . . . . . . . . . 11  |-  ( g  =  f  ->  (
x  =  ( S.1 `  g )  <->  x  =  ( S.1 `  f ) ) )
2522, 24anbi12d 710 . . . . . . . . . 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 2943 . . . . . . . . 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 4291 . . . . . . . . . . . . . . . . 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 4291 . . . . . . . . . . . . . . . . 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 10403 . . . . . . . . . . . . . . . . . . 19  |-  0  <_  0
3129, 30syl6eqbr 4324 . . . . . . . . . . . . . . . . . 18  |-  ( ( f `  z )  =  0  ->  (
f `  z )  <_  0 )
3231adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( f  e. 
dom  S.1  /\  y  e.  RR+ )  /\  z  e.  RR )  /\  (
f `  z )  =  0 )  -> 
( f `  z
)  <_  0 )
33 rpge0 10995 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  RR+  ->  0  <_ 
y )
3433ad2antlr 726 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( f  e.  dom  S.1 
/\  y  e.  RR+ )  /\  z  e.  RR )  ->  0  <_  y
)
35 i1ff 21129 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  e.  dom  S.1  ->  f : RR --> RR )
3635ffvelrnda 5838 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( f  e.  dom  S.1  /\  z  e.  RR )  ->  ( f `  z )  e.  RR )
3736adantlr 714 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( f  e.  dom  S.1 
/\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( f `  z )  e.  RR )
38 rpre 10989 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  RR+  ->  y  e.  RR )
3938ad2antlr 726 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( f  e.  dom  S.1 
/\  y  e.  RR+ )  /\  z  e.  RR )  ->  y  e.  RR )
4037, 39addge01d 9919 . . . . . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( f  e. 
dom  S.1  /\  y  e.  RR+ )  /\  z  e.  RR )  /\  -.  ( f `  z
)  =  0 )  ->  ( f `  z )  <_  (
( f `  z
)  +  y ) )
4327, 28, 32, 42ifbothda 3819 . . . . . . . . . . . . . . . 16  |-  ( ( ( f  e.  dom  S.1 
/\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( f `  z )  <_  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  y ) ) )
4443adantlll 717 . . . . . . . . . . . . . . 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 726 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F : RR --> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  f : RR --> RR )
4645ffvelrnda 5838 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( F : RR
--> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  (
f `  z )  e.  RR )
4746rexrd 9425 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( F : RR
--> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  (
f `  z )  e.  RR* )
48 0re 9378 . . . . . . . . . . . . . . . . . 18  |-  0  e.  RR
4938ad2antlr 726 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( F : RR
--> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  y  e.  RR )
5046, 49readdcld 9405 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F : RR
--> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  (
( f `  z
)  +  y )  e.  RR )
51 ifcl 3826 . . . . . . . . . . . . . . . . . 18  |-  ( ( 0  e.  RR  /\  ( ( f `  z )  +  y )  e.  RR )  ->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  y ) )  e.  RR )
5248, 50, 51sylancr 663 . . . . . . . . . . . . . . . . 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 9425 . . . . . . . . . . . . . . . 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 11370 . . . . . . . . . . . . . . . . . . 19  |-  ( 0 [,] +oo )  C_  RR*
55 fss 5562 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  ( 0 [,] +oo )  C_  RR* )  ->  F : RR --> RR* )
5654, 55mpan2 671 . . . . . . . . . . . . . . . . . 18  |-  ( F : RR --> ( 0 [,] +oo )  ->  F : RR --> RR* )
5756ad2antrr 725 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F : RR --> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  F : RR
--> RR* )
5857ffvelrnda 5838 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( F : RR
--> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( F `  z )  e.  RR* )
59 xrletr 11124 . . . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . . . 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 675 . . . . . . . . . . . . . 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 2789 . . . . . . . . . . . . 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 9365 . . . . . . . . . . . . . . 15  |-  RR  e.  _V
6463a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( F : RR --> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  RR  e.  _V )
65 eqidd 2439 . . . . . . . . . . . . . 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 5739 . . . . . . . . . . . . . . 15  |-  ( F : RR --> ( 0 [,] +oo )  ->  F  =  ( z  e.  RR  |->  ( F `  z ) ) )
6867ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( F : RR --> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  F  =  ( z  e.  RR  |->  ( F `  z ) ) )
6964, 52, 58, 65, 68ofrfval2 6332 . . . . . . . . . . . . 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 5739 . . . . . . . . . . . . . . 15  |-  ( f  e.  dom  S.1  ->  f  =  ( z  e.  RR  |->  ( f `  z ) ) )
7170ad2antlr 726 . . . . . . . . . . . . . 14  |-  ( ( ( F : RR --> ( 0 [,] +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  f  =  ( z  e.  RR  |->  ( f `  z
) ) )
7264, 46, 58, 71, 68ofrfval2 6332 . . . . . . . . . . . . 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 2836 . . . . . . . . . . 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 564 . . . . . . . . . 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 2823 . . . . . . . . 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 3420 . . . . . . 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 3350 . . . . . 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 1017 . . . . . . . . . . 11  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  f  e.  dom  S.1  /\  ( f  oR  <_  F  /\  x  =  ( S.1 `  f
) ) )  ->  x  =  ( S.1 `  f ) )
8193ad2ant2 1010 . . . . . . . . . . 11  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  f  e.  dom  S.1  /\  ( f  oR  <_  F  /\  x  =  ( S.1 `  f
) ) )  -> 
( S.1 `  f )  e.  RR* )
8280, 81eqeltrd 2512 . . . . . . . . . 10  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  f  e.  dom  S.1  /\  ( f  oR  <_  F  /\  x  =  ( S.1 `  f
) ) )  ->  x  e.  RR* )
8382rexlimdv3a 2838 . . . . . . . . 9  |-  ( F : RR --> ( 0 [,] +oo )  -> 
( E. f  e. 
dom  S.1 ( f  oR  <_  F  /\  x  =  ( S.1 `  f ) )  ->  x  e.  RR* ) )
8483abssdv 3421 . . . . . . . 8  |-  ( F : RR --> ( 0 [,] +oo )  ->  { x  |  E. f  e.  dom  S.1 (
f  oR  <_  F  /\  x  =  ( S.1 `  f ) ) }  C_  RR* )
85 xrsupss 11263 . . . . . . . 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 16 . . . . . . 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 7701 . . . . . 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 44 . . . . 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 429 . . . 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 11280 . . . . . . . 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 670 . . . . . . 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 466 . . . . . 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 764 . . . . . . . . . . . . . . 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 4299 . . . . . . . . . . . . . 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 757 . . . . . . . . . . . . . . . . 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 21140 . . . . . . . . . . . . . . . . . . 19  |-  ( RR 
X.  { 0 } )  e.  dom  S.1
97 2rp 10988 . . . . . . . . . . . . . . . . . . . . 21  |-  2  e.  RR+
98 ne0i 3638 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 2  e.  RR+  ->  RR+  =/=  (/) )
9997, 98ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  RR+  =/=  (/)
100 ffvelrn 5836 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  z  e.  RR )  ->  ( F `  z
)  e.  ( 0 [,] +oo ) )
101 elxrge0 11386 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F `  z )  e.  ( 0 [,] +oo )  <->  ( ( F `
 z )  e. 
RR*  /\  0  <_  ( F `  z ) ) )
102100, 101sylib 196 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  z  e.  RR )  ->  ( ( F `  z )  e.  RR*  /\  0  <_  ( F `  z ) ) )
103102simprd 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  z  e.  RR )  ->  0  <_  ( F `  z ) )
104103ralrimiva 2794 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F : RR --> ( 0 [,] +oo )  ->  A. z  e.  RR  0  <_  ( F `  z ) )
10563a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F : RR --> ( 0 [,] +oo )  ->  RR  e.  _V )
106 c0ex 9372 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  0  e.  _V
107106a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  z  e.  RR )  ->  0  e.  _V )
108 eqidd 2439 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F : RR --> ( 0 [,] +oo )  -> 
( z  e.  RR  |->  0 )  =  ( z  e.  RR  |->  0 ) )
109105, 107, 100, 108, 67ofrfval2 6332 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F : RR --> ( 0 [,] +oo )  -> 
( ( z  e.  RR  |->  0 )  oR  <_  F  <->  A. z  e.  RR  0  <_  ( F `  z )
) )
110104, 109mpbird 232 . . . . . . . . . . . . . . . . . . . . 21  |-  ( F : RR --> ( 0 [,] +oo )  -> 
( z  e.  RR  |->  0 )  oR  <_  F )
111110ralrimivw 2795 . . . . . . . . . . . . . . . . . . . 20  |-  ( F : RR --> ( 0 [,] +oo )  ->  A. y  e.  RR+  (
z  e.  RR  |->  0 )  oR  <_  F )
112 r19.2z 3764 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
RR+  =/=  (/)  /\  A. y  e.  RR+  ( z  e.  RR  |->  0 )  oR  <_  F
)  ->  E. y  e.  RR+  ( z  e.  RR  |->  0 )  oR  <_  F )
11399, 111, 112sylancr 663 . . . . . . . . . . . . . . . . . . 19  |-  ( F : RR --> ( 0 [,] +oo )  ->  E. y  e.  RR+  (
z  e.  RR  |->  0 )  oR  <_  F )
114 fveq2 5686 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( S.1 `  g
)  =  ( S.1 `  ( RR  X.  {
0 } ) ) )
115 itg10 21141 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( S.1 `  ( RR  X.  {
0 } ) )  =  0
116114, 115syl6req 2487 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( g  =  ( RR  X.  { 0 } )  ->  0  =  ( S.1 `  g ) )
117116biantrud 507 . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
118 fveq1 5685 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( g `  z )  =  ( ( RR  X.  {
0 } ) `  z ) )
119106fvconst2 5928 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  e.  RR  ->  (
( RR  X.  {
0 } ) `  z )  =  0 )
120118, 119sylan9eq 2490 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( g  =  ( RR 
X.  { 0 } )  /\  z  e.  RR )  ->  (
g `  z )  =  0 )
121 iftrue 3792 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( g `  z )  =  0  ->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) )  =  0 )
122120, 121syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( g  =  ( RR 
X.  { 0 } )  /\  z  e.  RR )  ->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) )  =  0 )
123122mpteq2dva 4373 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  y ) ) )  =  ( z  e.  RR  |->  0 ) )
124123breq1d 4297 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( ( z  e.  RR  |->  if ( ( g `  z
)  =  0 ,  0 ,  ( ( g `  z )  +  y ) ) )  oR  <_  F 
<->  ( z  e.  RR  |->  0 )  oR  <_  F ) )
125124rexbidv 2731 . . . . . . . . . . . . . . . . . . . . 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 ) )
126117, 125bitr3d 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 )
)
127126rspcev 3068 . . . . . . . . . . . . . . . . . . 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
) ) )
12896, 113, 127sylancr 663 . . . . . . . . . . . . . . . . . 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
) ) )
129 id 22 . . . . . . . . . . . . . . . . . . 19  |-  ( b  = -oo  ->  b  = -oo )
130 mnflt 11096 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  e.  RR  -> -oo  <  0 )
13148, 130mp1i 12 . . . . . . . . . . . . . . . . . . 19  |-  ( b  = -oo  -> -oo  <  0 )
132129, 131eqbrtrd 4307 . . . . . . . . . . . . . . . . . 18  |-  ( b  = -oo  ->  b  <  0 )
133 eqeq1 2444 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  0  ->  (
a  =  ( S.1 `  g )  <->  0  =  ( S.1 `  g ) ) )
134133anbi2d 703 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
135134rexbidv 2731 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
136 breq2 4291 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  0  ->  (
b  <  a  <->  b  <  0 ) )
137135, 136anbi12d 710 . . . . . . . . . . . . . . . . . . 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
) ) )
138106, 137spcev 3059 . . . . . . . . . . . . . . . . . 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
) )
139128, 132, 138syl2an 477 . . . . . . . . . . . . . . . . 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 ) )
14095, 139sylan 471 . . . . . . . . . . . . . . . 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
) )
141 simp-4r 766 . . . . . . . . . . . . . . . . . 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* )
1428adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f  e.  dom  S.1  /\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f
) ) )  -> 
( S.1 `  f )  e.  RR )
143142ad3antlr 730 . . . . . . . . . . . . . . . . . 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 )
144 simpllr 758 . . . . . . . . . . . . . . . . . . 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* )
145 ngtmnft 11131 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( b  e.  RR*  ->  ( b  = -oo  <->  -. -oo  <  b ) )
146145biimprd 223 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  e.  RR*  ->  ( -. -oo  <  b  ->  b  = -oo ) )
147146necon1ad 2673 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  e.  RR*  ->  ( b  =/= -oo  -> -oo  <  b ) )
148147imp 429 . . . . . . . . . . . . . . . . . . 19  |-  ( ( b  e.  RR*  /\  b  =/= -oo )  -> -oo  <  b )
149144, 148sylan 471 . . . . . . . . . . . . . . . . . 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 )
150 simpr 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  b  e.  RR* )  -> 
b  e.  RR* )
1519adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( f  e.  dom  S.1  /\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f
) ) )  -> 
( S.1 `  f )  e.  RR* )
152150, 151anim12i 566 . . . . . . . . . . . . . . . . . . . 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* ) )
153 xrltle 11118 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( b  e.  RR*  /\  ( S.1 `  f )  e. 
RR* )  ->  (
b  <  ( S.1 `  f )  ->  b  <_  ( S.1 `  f
) ) )
154153imp 429 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( b  e.  RR*  /\  ( S.1 `  f
)  e.  RR* )  /\  b  <  ( S.1 `  f ) )  -> 
b  <_  ( S.1 `  f ) )
155152, 154sylan 471 . . . . . . . . . . . . . . . . . . 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
) )
156155adantr 465 . . . . . . . . . . . . . . . . . 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 ) )
157 xrre 11133 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( b  e.  RR*  /\  ( S.1 `  f
)  e.  RR )  /\  ( -oo  <  b  /\  b  <_  ( S.1 `  f ) ) )  ->  b  e.  RR )
158141, 143, 149, 156, 157syl22anc 1219 . . . . . . . . . . . . . . . . 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 )
159128ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . 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
) ) )
160 simplrl 759 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
161 simplrl 759 . . . . . . . . . . . . . . . . . . . . . . . 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 )
162 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( f  e.  dom  S.1  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
f  e.  dom  S.1 )
163 cnvimass 5184 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( `' f " ( ran  f  \  { 0 } ) )  C_  dom  f
164 fdm 5558 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f : RR --> RR  ->  dom  f  =  RR )
16535, 164syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f  e.  dom  S.1  ->  dom  f  =  RR )
166163, 165syl5sseq 3399 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f  e.  dom  S.1  ->  ( `' f " ( ran  f  \  { 0 } ) )  C_  RR )
167166adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( f  e.  dom  S.1  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
( `' f "
( ran  f  \  { 0 } ) )  C_  RR )
168 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( f  e.  dom  S.1  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )
169164eqcomd 2443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( f : RR --> RR  ->  RR  =  dom  f )
170 ffun 5556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( f : RR --> RR  ->  Fun  f )
171 difpreima 5826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( Fun  f  ->  ( `' f " ( ran  f  \  { 0 } ) )  =  ( ( `' f " ran  f )  \  ( `' f " {
0 } ) ) )
172170, 171syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( f : RR --> RR  ->  ( `' f " ( ran  f  \  { 0 } ) )  =  ( ( `' f
" ran  f )  \  ( `' f
" { 0 } ) ) )
173 cnvimarndm 5185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( `' f " ran  f
)  =  dom  f
174173difeq1i 3465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( `' f " ran  f )  \  ( `' f " {
0 } ) )  =  ( dom  f  \  ( `' f
" { 0 } ) )
175172, 174syl6eq 2486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( f : RR --> RR  ->  ( `' f " ( ran  f  \  { 0 } ) )  =  ( dom  f  \ 
( `' f " { 0 } ) ) )
176169, 175difeq12d 3470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( f : RR --> RR  ->  ( RR  \  ( `' f " ( ran  f  \  { 0 } ) ) )  =  ( dom  f  \  ( dom  f  \  ( `' f
" { 0 } ) ) ) )
177 cnvimass 5184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( `' f " { 0 } )  C_  dom  f
178 dfss4 3579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( `' f " {
0 } )  C_  dom  f  <->  ( dom  f  \  ( dom  f  \  ( `' f
" { 0 } ) ) )  =  ( `' f " { 0 } ) )
179177, 178mpbi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( dom  f  \  ( dom  f  \  ( `' f " { 0 } ) ) )  =  ( `' f
" { 0 } )
180176, 179syl6eq 2486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( f : RR --> RR  ->  ( RR  \  ( `' f " ( ran  f  \  { 0 } ) ) )  =  ( `' f
" { 0 } ) )
181180eleq2d 2505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( f : RR --> RR  ->  ( z  e.  ( RR 
\  ( `' f
" ( ran  f  \  { 0 } ) ) )  <->  z  e.  ( `' f " {
0 } ) ) )
182 ffn 5554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( f : RR --> RR  ->  f  Fn  RR )
183 fniniseg 5819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( f  Fn  RR  ->  (
z  e.  ( `' f " { 0 } )  <->  ( z  e.  RR  /\  ( f `
 z )  =  0 ) ) )
184 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( z  e.  RR  /\  ( f `  z
)  =  0 )  ->  ( f `  z )  =  0 )
185183, 184syl6bi 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( f  Fn  RR  ->  (
z  e.  ( `' f " { 0 } )  ->  (
f `  z )  =  0 ) )
186182, 185syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( f : RR --> RR  ->  ( z  e.  ( `' f " { 0 } )  ->  (
f `  z )  =  0 ) )
187181, 186sylbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f : RR --> RR  ->  ( z  e.  ( RR 
\  ( `' f
" ( ran  f  \  { 0 } ) ) )  ->  (
f `  z )  =  0 ) )
18835, 187syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f  e.  dom  S.1  ->  ( z  e.  ( RR 
\  ( `' f
" ( ran  f  \  { 0 } ) ) )  ->  (
f `  z )  =  0 ) )
189188imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( f  e.  dom  S.1  /\  z  e.  ( RR 
\  ( `' f
" ( ran  f  \  { 0 } ) ) ) )  -> 
( f `  z
)  =  0 )
190189adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( f  e.  dom  S.1 
/\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =  0 )  /\  z  e.  ( RR  \  ( `' f " ( ran  f  \  { 0 } ) ) ) )  ->  ( f `  z )  =  0 )
191162, 167, 168, 190itg10a 21163 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( f  e.  dom  S.1  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
( S.1 `  f )  =  0 )
192161, 191sylan 471 . . . . . . . . . . . . . . . . . . . . . . 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 )
193160, 192breqtrd 4311 . . . . . . . . . . . . . . . . . . . . . 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 )
194159, 193, 138syl2anc 661 . . . . . . . . . . . . . . . . . . . . 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
) )
195 simprl 755 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F : RR --> ( 0 [,] +oo )  /\  ( f  e.  dom  S.1 
/\  ( f  oR  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  ->  f  e.  dom  S.1 )
196 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( b  <  ( S.1 `  f )  /\  b  e.  RR )  ->  b  e.  RR )
197195, 196anim12i 566 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
19863a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  RR  e.  _V )
199 fvex 5696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( f `
 u )  e. 
_V
200199a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( f  e. 
dom  S.1  /\  b  e.  RR )  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =/=  0 )  /\  u  e.  RR )  ->  ( f `  u
)  e.  _V )
201 ovex 6111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) )  e.  _V
202201, 106ifex 3853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 )  e. 
_V
203202a1i 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 )
20435feqmptd 5739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( f  e.  dom  S.1  ->  f  =  ( u  e.  RR  |->  ( f `  u ) ) )
205204ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  f  =  ( u  e.  RR  |->  ( f `  u
) ) )
206 eqidd 2439 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
207198, 200, 203, 205, 206offval2 6331 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
208 ovif2 6164 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
209173, 164syl5eq 2482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( f : RR --> RR  ->  ( `' f " ran  f )  =  RR )
210209difeq1d 3468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( f : RR --> RR  ->  ( ( `' f " ran  f )  \  ( `' f " {
0 } ) )  =  ( RR  \ 
( `' f " { 0 } ) ) )
211172, 210eqtrd 2470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( f : RR --> RR  ->  ( `' f " ( ran  f  \  { 0 } ) )  =  ( RR  \  ( `' f " {
0 } ) ) )
212211eleq2d 2505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( f : RR --> RR  ->  ( u  e.  ( `' f " ( ran  f  \  { 0 } ) )  <->  u  e.  ( RR  \  ( `' f " {
0 } ) ) ) )
21335, 212syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( f  e.  dom  S.1  ->  ( u  e.  ( `' f " ( ran  f  \  { 0 } ) )  <->  u  e.  ( RR  \  ( `' f " {
0 } ) ) ) )
214213ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) )
215 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( f  e. 
dom  S.1  /\  b  e.  RR )  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  =/=  0 )  /\  u  e.  RR )  ->  u  e.  RR )
216215biantrurd 508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) )
217 eldif 3333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( u  e.  ( RR  \ 
( `' f " { 0 } ) )  <->  ( u  e.  RR  /\  -.  u  e.  ( `' f " { 0 } ) ) )
218216, 217syl6bbr 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 } ) ) ) )
219214, 218bitr4d 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 } ) ) )
220219con2bid 329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) )
221 fniniseg 5819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( f  Fn  RR  ->  (
u  e.  ( `' f " { 0 } )  <->  ( u  e.  RR  /\  ( f `
 u )  =  0 ) ) )
22235, 182, 2213syl 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( f  e.  dom  S.1  ->  ( u  e.  ( `' f " { 0 } )  <->  ( u  e.  RR  /\  ( f `
 u )  =  0 ) ) )
223222ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
224220, 223bitr3d 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 ) ) )
225 oveq1 6093 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( f `  u )  =  0  ->  (
( f `  u
)  -  0 )  =  ( 0  -  0 ) )
226 0m0e0 10423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( 0  -  0 )  =  0
227225, 226syl6eq 2486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( f `  u )  =  0  ->  (
( f `  u
)  -  0 )  =  0 )
228227adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( u  e.  RR  /\  ( f `  u
)  =  0 )  ->  ( ( f `
 u )  - 
0 )  =  0 )
229224, 228syl6bi 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 ) )
230229imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
231230ifeq2da 3815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
232208, 231syl5eq 2482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
233232mpteq2dva 4373 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
234207, 233eqtrd 2470 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
235 simpll 753 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  f  e.  dom  S.1 )
236201a1i 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 )
237 1ex 9373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  1  e.  _V
238237, 106ifex 3853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  1 ,  0 )  e.  _V
239238a1i 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 )
240 fconstmpt 4877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) ) ) )
241240a1i 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 } ) ) ) ) ) ) )
242 eqidd 2439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
243198, 236, 239, 241, 242offval2 6331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
244 ovif2 6164 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
245 resubcl 9665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( S.1 `  f
)  e.  RR  /\  b  e.  RR )  ->  ( ( S.1 `  f
)  -  b )  e.  RR )
2468, 245sylan 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( f  e.  dom  S.1  /\  b  e.  RR )  ->  ( ( S.1 `  f )  -  b
)  e.  RR )
247246adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( ( S.1 `  f )  -  b )  e.  RR )
248 2re 10383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  2  e.  RR
249 i1fima 21131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( f  e.  dom  S.1  ->  ( `' f " ( ran  f  \  { 0 } ) )  e. 
dom  vol )
250 mblvol 20988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( `' f " ( ran  f  \  { 0 } ) )  e. 
dom  vol  ->  ( vol `  ( `' f "
( ran  f  \  { 0 } ) ) )  =  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) )
251249, 250syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( f  e.  dom  S.1  ->  ( vol `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) ) )
252 neldifsn 3997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  -.  0  e.  ( ran  f  \  { 0 } )
253 i1fima2 21132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( f  e.  dom  S.1  /\ 
-.  0  e.  ( ran  f  \  {
0 } ) )  ->  ( vol `  ( `' f " ( ran  f  \  { 0 } ) ) )  e.  RR )
254252, 253mpan2 671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( f  e.  dom  S.1  ->  ( vol `  ( `' f " ( ran  f  \  { 0 } ) ) )  e.  RR )
255251, 254eqeltrrd 2513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( f  e.  dom  S.1  ->  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  e.  RR )
256 remulcl 9359 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( 2  e.  RR  /\  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) )  e.  RR )  -> 
( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) )  e.  RR )
257248, 255, 256sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( f  e.  dom  S.1  ->  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) )  e.  RR )
258257ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( 2  x.  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) ) )  e.  RR )
259 2cnd 10386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  2  e.  CC )
260255ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( vol* `  ( `' f
" ( ran  f  \  { 0 } ) ) )  e.  RR )
261260recnd 9404 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( vol* `  ( `' f
" ( ran  f  \  { 0 } ) ) )  e.  CC )
262 2ne0 10406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  2  =/=  0
263262a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  2  =/=  0 )
264 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( vol* `  ( `' f
" ( ran  f  \  { 0 } ) ) )  =/=  0
)
265259, 261, 263, 264mulne0d 9980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( 2  x.  ( vol* `  ( `' f "
( ran  f  \  { 0 } ) ) ) )  =/=  0 )
266247, 258, 265redivcld 10151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
267266recnd 9404 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
268267mulid1d 9395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) ) ) )
269267mul01d 9560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
270268, 269ifeq12d 3804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
271244, 270syl5eq 2482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
272271mpteq2dv 4374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
273243, 272eqtrd 2470 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
274 eqid 2438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
275274i1f1 21143 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
276249, 254, 275syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( f  e.  dom  S.1  ->  ( u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  1 ,  0 ) )  e.  dom  S.1 )
277276ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
278277, 266i1fmulc 21156 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
279273, 278eqeltrrd 2513 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
280 i1fsub 21161 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
281235, 279, 280syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
282234, 281eqeltrrd 2513 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
283 eleq1 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( u  =  z  ->  (
u  e.  ( `' f " ( ran  f  \  { 0 } ) )  <->  z  e.  ( `' f " ( ran  f  \  { 0 } ) ) ) )
284 fveq2 5686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( u  =  z  ->  (
f `  u )  =  ( f `  z ) )
285284oveq1d 6101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) ) ) ) )
286283, 285ifbieq1d 3807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
287 eqid 2438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
288 ovex 6111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( f `  z )  -  ( ( ( S.1 `  f )  -  b )  / 
( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) )  e. 
_V
289288, 106ifex 3853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  if ( z  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( f `  z )  -  (
( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol* `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ) ,  0 )  e.  _V
290286, 287, 289fvmpt 5769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
291290breq2d 4299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
292291, 290ifbieq1d 3807 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
293 iftrue 3792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 0  <_  ( (
f `  z )  -  ( ( ( S.1 `  f )  -  b )  / 
( 2  x.  ( vol