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

Theorem itg2addnclem 26246
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 ) ) )  o R  <_  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 2435 . . 3  |-  { x  |  E. f  e.  dom  S.1 ( f  o R  <_  F  /\  x  =  ( S.1 `  f
) ) }  =  { x  |  E. f  e.  dom  S.1 (
f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) }
21itg2val 19612 . 2  |-  ( F : RR --> ( 0 [,]  +oo )  ->  ( S.2 `  F )  =  sup ( { x  |  E. f  e.  dom  S.1 ( f  o R  <_  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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  g
) ) }
43supeq1i 7444 . . 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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  g ) ) } ,  RR* ,  <  )
5 xrltso 10726 . . . . 5  |-  <  Or  RR*
65a1i 11 . . . 4  |-  ( F : RR --> ( 0 [,]  +oo )  ->  <  Or 
RR* )
7 simprr 734 . . . . . . . 8  |-  ( ( f  e.  dom  S.1  /\  ( f  o R  <_  F  /\  x  =  ( S.1 `  f
) ) )  ->  x  =  ( S.1 `  f ) )
8 itg1cl 19569 . . . . . . . . . 10  |-  ( f  e.  dom  S.1  ->  ( S.1 `  f )  e.  RR )
98rexrd 9126 . . . . . . . . 9  |-  ( f  e.  dom  S.1  ->  ( S.1 `  f )  e.  RR* )
109adantr 452 . . . . . . . 8  |-  ( ( f  e.  dom  S.1  /\  ( f  o R  <_  F  /\  x  =  ( S.1 `  f
) ) )  -> 
( S.1 `  f )  e.  RR* )
117, 10eqeltrd 2509 . . . . . . 7  |-  ( ( f  e.  dom  S.1  /\  ( f  o R  <_  F  /\  x  =  ( S.1 `  f
) ) )  ->  x  e.  RR* )
1211rexlimiva 2817 . . . . . 6  |-  ( E. f  e.  dom  S.1 ( f  o R  <_  F  /\  x  =  ( S.1 `  f
) )  ->  x  e.  RR* )
1312abssi 3410 . . . . 5  |-  { x  |  E. f  e.  dom  S.1 ( f  o R  <_  F  /\  x  =  ( S.1 `  f
) ) }  C_  RR*
14 supxrcl 10885 . . . . 5  |-  ( { x  |  E. f  e.  dom  S.1 ( f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) } 
C_  RR*  ->  sup ( { x  |  E. f  e.  dom  S.1 (
f  o R  <_  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  o R  <_  F  /\  x  =  ( S.1 `  f ) ) } ,  RR* ,  <  )  e.  RR* )
16 fveq1 5719 . . . . . . . . . . . . . . . 16  |-  ( g  =  f  ->  (
g `  z )  =  ( f `  z ) )
1716eqeq1d 2443 . . . . . . . . . . . . . . 15  |-  ( g  =  f  ->  (
( g `  z
)  =  0  <->  (
f `  z )  =  0 ) )
1816oveq1d 6088 . . . . . . . . . . . . . . 15  |-  ( g  =  f  ->  (
( g `  z
)  +  y )  =  ( ( f `
 z )  +  y ) )
1917, 18ifbieq2d 3751 . . . . . . . . . . . . . 14  |-  ( g  =  f  ->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) )  =  if ( ( f `  z
)  =  0 ,  0 ,  ( ( f `  z )  +  y ) ) )
2019mpteq2dv 4288 . . . . . . . . . . . . 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 4214 . . . . . . . . . . . 12  |-  ( g  =  f  ->  (
( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  o R  <_  F  <->  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  y ) ) )  o R  <_  F
) )
2221rexbidv 2718 . . . . . . . . . . 11  |-  ( g  =  f  ->  ( E. y  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  o R  <_  F  <->  E. y  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  y ) ) )  o R  <_  F
) )
23 fveq2 5720 . . . . . . . . . . . 12  |-  ( g  =  f  ->  ( S.1 `  g )  =  ( S.1 `  f
) )
2423eqeq2d 2446 . . . . . . . . . . 11  |-  ( g  =  f  ->  (
x  =  ( S.1 `  g )  <->  x  =  ( S.1 `  f ) ) )
2522, 24anbi12d 692 . . . . . . . . . 10  |-  ( g  =  f  ->  (
( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  o R  <_  F  /\  x  =  ( S.1 `  g
) )  <->  ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( f `  z
)  =  0 ,  0 ,  ( ( f `  z )  +  y ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f ) ) ) )
2625cbvrexv 2925 . . . . . . . . 9  |-  ( E. g  e.  dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  o R  <_  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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f ) ) )
27 breq2 4208 . . . . . . . . . . . . . . . . 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 4208 . . . . . . . . . . . . . . . . 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 20 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f `  z )  =  0  ->  (
f `  z )  =  0 )
30 0le0 10073 . . . . . . . . . . . . . . . . . . 19  |-  0  <_  0
3129, 30syl6eqbr 4241 . . . . . . . . . . . . . . . . . 18  |-  ( ( f `  z )  =  0  ->  (
f `  z )  <_  0 )
3231adantl 453 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( f  e. 
dom  S.1  /\  y  e.  RR+ )  /\  z  e.  RR )  /\  (
f `  z )  =  0 )  -> 
( f `  z
)  <_  0 )
33 rpge0 10616 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  RR+  ->  0  <_ 
y )
3433ad2antlr 708 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( f  e.  dom  S.1 
/\  y  e.  RR+ )  /\  z  e.  RR )  ->  0  <_  y
)
35 i1ff 19560 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  e.  dom  S.1  ->  f : RR --> RR )
3635ffvelrnda 5862 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( f  e.  dom  S.1  /\  z  e.  RR )  ->  ( f `  z )  e.  RR )
3736adantlr 696 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( f  e.  dom  S.1 
/\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( f `  z )  e.  RR )
38 rpre 10610 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  RR+  ->  y  e.  RR )
3938ad2antlr 708 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( f  e.  dom  S.1 
/\  y  e.  RR+ )  /\  z  e.  RR )  ->  y  e.  RR )
4037, 39addge01d 9606 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( f  e.  dom  S.1 
/\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( 0  <_ 
y  <->  ( f `  z )  <_  (
( f `  z
)  +  y ) ) )
4134, 40mpbid 202 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( f  e.  dom  S.1 
/\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( f `  z )  <_  (
( f `  z
)  +  y ) )
4241adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( f  e. 
dom  S.1  /\  y  e.  RR+ )  /\  z  e.  RR )  /\  -.  ( f `  z
)  =  0 )  ->  ( f `  z )  <_  (
( f `  z
)  +  y ) )
4327, 28, 32, 42ifbothda 3761 . . . . . . . . . . . . . . . 16  |-  ( ( ( f  e.  dom  S.1 
/\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( f `  z )  <_  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  y ) ) )
4443adantlll 699 . . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  f : RR --> RR )
4645ffvelrnda 5862 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  (
f `  z )  e.  RR )
4746rexrd 9126 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  (
f `  z )  e.  RR* )
48 0re 9083 . . . . . . . . . . . . . . . . . 18  |-  0  e.  RR
4938ad2antlr 708 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  y  e.  RR )
5046, 49readdcld 9107 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  (
( f `  z
)  +  y )  e.  RR )
51 ifcl 3767 . . . . . . . . . . . . . . . . . 18  |-  ( ( 0  e.  RR  /\  ( ( f `  z )  +  y )  e.  RR )  ->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  y ) )  e.  RR )
5248, 50, 51sylancr 645 . . . . . . . . . . . . . . . . 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 9126 . . . . . . . . . . . . . . . 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 10985 . . . . . . . . . . . . . . . . . . 19  |-  ( 0 [,]  +oo )  C_  RR*
55 fss 5591 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  (
0 [,]  +oo )  C_  RR* )  ->  F : RR
--> RR* )
5654, 55mpan2 653 . . . . . . . . . . . . . . . . . 18  |-  ( F : RR --> ( 0 [,]  +oo )  ->  F : RR --> RR* )
5756ad2antrr 707 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  F : RR
--> RR* )
5857ffvelrnda 5862 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( F `  z )  e.  RR* )
59 xrletr 10740 . . . . . . . . . . . . . . . 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 1184 . . . . . . . . . . . . . . 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 657 . . . . . . . . . . . . . 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 2776 . . . . . . . . . . . . 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 9073 . . . . . . . . . . . . . . 15  |-  RR  e.  _V
6463a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  RR  e.  _V )
65 eqidd 2436 . . . . . . . . . . . . . 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 20 . . . . . . . . . . . . . . . 16  |-  ( F : RR --> ( 0 [,]  +oo )  ->  F : RR --> ( 0 [,] 
+oo ) )
6766feqmptd 5771 . . . . . . . . . . . . . . 15  |-  ( F : RR --> ( 0 [,]  +oo )  ->  F  =  ( z  e.  RR  |->  ( F `  z ) ) )
6867ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  F  =  ( z  e.  RR  |->  ( F `  z ) ) )
6964, 52, 58, 65, 68ofrfval2 6315 . . . . . . . . . . . . 13  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  ( ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  y ) ) )  o R  <_  F  <->  A. z  e.  RR  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `
 z )  +  y ) )  <_ 
( F `  z
) ) )
7035feqmptd 5771 . . . . . . . . . . . . . . 15  |-  ( f  e.  dom  S.1  ->  f  =  ( z  e.  RR  |->  ( f `  z ) ) )
7170ad2antlr 708 . . . . . . . . . . . . . 14  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  f  =  ( z  e.  RR  |->  ( f `  z
) ) )
7264, 46, 58, 71, 68ofrfval2 6315 . . . . . . . . . . . . 13  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  ( f  o R  <_  F  <->  A. z  e.  RR  (
f `  z )  <_  ( F `  z
) ) )
7362, 69, 723imtr4d 260 . . . . . . . . . . . 12  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  ( ( z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  y ) ) )  o R  <_  F  ->  f  o R  <_  F ) )
7473rexlimdva 2822 . . . . . . . . . . 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 ) ) )  o R  <_  F  ->  f  o R  <_  F ) )
7574anim1d 548 . . . . . . . . . 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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) )  ->  (
f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) ) )
7675reximdva 2810 . . . . . . . . 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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) )  ->  E. f  e.  dom  S.1 ( f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) ) )
7726, 76syl5bi 209 . . . . . . . 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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  g
) )  ->  E. f  e.  dom  S.1 ( f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) ) )
7877ss2abdv 3408 . . . . . . 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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  g
) ) }  C_  { x  |  E. f  e.  dom  S.1 ( f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) } )
7978sseld 3339 . . . . . 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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  g
) ) }  ->  b  e.  { x  |  E. f  e.  dom  S.1 ( f  o R  <_  F  /\  x  =  ( S.1 `  f
) ) } ) )
80 simp3r 986 . . . . . . . . . . 11  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1  /\  (
f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) )  ->  x  =  ( S.1 `  f
) )
8193ad2ant2 979 . . . . . . . . . . 11  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1  /\  (
f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) )  ->  ( S.1 `  f )  e. 
RR* )
8280, 81eqeltrd 2509 . . . . . . . . . 10  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1  /\  (
f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) )  ->  x  e.  RR* )
8382rexlimdv3a 2824 . . . . . . . . 9  |-  ( F : RR --> ( 0 [,]  +oo )  ->  ( E. f  e.  dom  S.1 ( f  o R  <_  F  /\  x  =  ( S.1 `  f
) )  ->  x  e.  RR* ) )
8483abssdv 3409 . . . . . . . 8  |-  ( F : RR --> ( 0 [,]  +oo )  ->  { x  |  E. f  e.  dom  S.1 ( f  o R  <_  F  /\  x  =  ( S.1 `  f
) ) }  C_  RR* )
85 xrsupss 10879 . . . . . . . 8  |-  ( { x  |  E. f  e.  dom  S.1 ( f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) } 
C_  RR*  ->  E. a  e.  RR*  ( A. b  e.  { x  |  E. f  e.  dom  S.1 (
f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) }  -.  a  <  b  /\  A. b  e.  RR*  ( b  < 
a  ->  E. s  e.  { x  |  E. f  e.  dom  S.1 (
f  o R  <_  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  o R  <_  F  /\  x  =  ( S.1 `  f ) ) }  -.  a  <  b  /\  A. b  e.  RR*  ( b  < 
a  ->  E. s  e.  { x  |  E. f  e.  dom  S.1 (
f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) } b  < 
s ) ) )
876, 86supub 7456 . . . . . 6  |-  ( F : RR --> ( 0 [,]  +oo )  ->  (
b  e.  { x  |  E. f  e.  dom  S.1 ( f  o R  <_  F  /\  x  =  ( S.1 `  f
) ) }  ->  -. 
sup ( { x  |  E. f  e.  dom  S.1 ( f  o R  <_  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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  g
) ) }  ->  -. 
sup ( { x  |  E. f  e.  dom  S.1 ( f  o R  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  )  < 
b ) )
8988imp 419 . . . 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 ) ) )  o R  <_  F  /\  x  =  ( S.1 `  g
) ) } )  ->  -.  sup ( { x  |  E. f  e.  dom  S.1 (
f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) } ,  RR* ,  <  )  <  b
)
90 supxrlub 10896 . . . . . . . 8  |-  ( ( { x  |  E. f  e.  dom  S.1 (
f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) }  C_  RR*  /\  b  e.  RR* )  ->  (
b  <  sup ( { x  |  E. f  e.  dom  S.1 (
f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) } ,  RR* ,  <  )  <->  E. s  e.  { x  |  E. f  e.  dom  S.1 (
f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) } b  < 
s ) )
9113, 90mpan 652 . . . . . . 7  |-  ( b  e.  RR*  ->  ( b  <  sup ( { x  |  E. f  e.  dom  S.1 ( f  o R  <_  F  /\  x  =  ( S.1 `  f
) ) } ,  RR* ,  <  )  <->  E. s  e.  { x  |  E. f  e.  dom  S.1 (
f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) } b  < 
s ) )
9291adantl 453 . . . . . 6  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  b  e.  RR* )  ->  (
b  <  sup ( { x  |  E. f  e.  dom  S.1 (
f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) } ,  RR* ,  <  )  <->  E. s  e.  { x  |  E. f  e.  dom  S.1 (
f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) } b  < 
s ) )
93 simprrr 742 . . . . . . . . . . . . . . 15  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  ( f  e. 
dom  S.1  /\  ( f  o R  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  ->  s  =  ( S.1 `  f
) )
9493breq2d 4216 . . . . . . . . . . . . . 14  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  ( f  e. 
dom  S.1  /\  ( f  o R  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  ->  (
b  <  s  <->  b  <  ( S.1 `  f ) ) )
95 simplll 735 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  ( f  e. 
dom  S.1  /\  ( f  o R  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  /\  b  <  ( S.1 `  f
) )  ->  F : RR --> ( 0 [,] 
+oo ) )
96 i1f0 19571 . . . . . . . . . . . . . . . . . . 19  |-  ( RR 
X.  { 0 } )  e.  dom  S.1
97 2rp 10609 . . . . . . . . . . . . . . . . . . . . 21  |-  2  e.  RR+
98 ne0i 3626 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 2  e.  RR+  ->  RR+  =/=  (/) )
9997, 98ax-mp 8 . . . . . . . . . . . . . . . . . . . 20  |-  RR+  =/=  (/)
100 ffvelrn 5860 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  z  e.  RR )  ->  ( F `  z )  e.  ( 0 [,]  +oo ) )
101 elxrge0 11000 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F `  z )  e.  ( 0 [,] 
+oo )  <->  ( ( F `  z )  e.  RR*  /\  0  <_ 
( F `  z
) ) )
102100, 101sylib 189 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  z  e.  RR )  ->  (
( F `  z
)  e.  RR*  /\  0  <_  ( F `  z
) ) )
103102simprd 450 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  z  e.  RR )  ->  0  <_  ( F `  z
) )
104103ralrimiva 2781 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F : RR --> ( 0 [,]  +oo )  ->  A. z  e.  RR  0  <_  ( F `  z )
)
10563a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F : RR --> ( 0 [,]  +oo )  ->  RR  e.  _V )
106 c0ex 9077 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  0  e.  _V
107106a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  z  e.  RR )  ->  0  e.  _V )
108 eqidd 2436 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F : RR --> ( 0 [,]  +oo )  ->  (
z  e.  RR  |->  0 )  =  ( z  e.  RR  |->  0 ) )
109105, 107, 100, 108, 67ofrfval2 6315 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F : RR --> ( 0 [,]  +oo )  ->  (
( z  e.  RR  |->  0 )  o R  <_  F  <->  A. z  e.  RR  0  <_  ( F `  z )
) )
110104, 109mpbird 224 . . . . . . . . . . . . . . . . . . . . 21  |-  ( F : RR --> ( 0 [,]  +oo )  ->  (
z  e.  RR  |->  0 )  o R  <_  F )
111110ralrimivw 2782 . . . . . . . . . . . . . . . . . . . 20  |-  ( F : RR --> ( 0 [,]  +oo )  ->  A. y  e.  RR+  ( z  e.  RR  |->  0 )  o R  <_  F )
112 r19.2z 3709 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
RR+  =/=  (/)  /\  A. y  e.  RR+  ( z  e.  RR  |->  0 )  o R  <_  F
)  ->  E. y  e.  RR+  ( z  e.  RR  |->  0 )  o R  <_  F )
11399, 111, 112sylancr 645 . . . . . . . . . . . . . . . . . . 19  |-  ( F : RR --> ( 0 [,]  +oo )  ->  E. y  e.  RR+  ( z  e.  RR  |->  0 )  o R  <_  F )
114 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( S.1 `  g
)  =  ( S.1 `  ( RR  X.  {
0 } ) ) )
115 itg10 19572 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( S.1 `  ( RR  X.  {
0 } ) )  =  0
116114, 115syl6req 2484 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( g  =  ( RR  X.  { 0 } )  ->  0  =  ( S.1 `  g ) )
117116biantrud 494 . . . . . . . . . . . . . . . . . . . . 21  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  y ) ) )  o R  <_  F  <->  ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  o R  <_  F  /\  0  =  ( S.1 `  g
) ) ) )
118 fveq1 5719 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( g `  z )  =  ( ( RR  X.  {
0 } ) `  z ) )
119106fvconst2 5939 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  e.  RR  ->  (
( RR  X.  {
0 } ) `  z )  =  0 )
120118, 119sylan9eq 2487 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( g  =  ( RR 
X.  { 0 } )  /\  z  e.  RR )  ->  (
g `  z )  =  0 )
121 iftrue 3737 . . . . . . . . . . . . . . . . . . . . . . . . 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 4287 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  y ) ) )  =  ( z  e.  RR  |->  0 ) )
124123breq1d 4214 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( ( z  e.  RR  |->  if ( ( g `  z
)  =  0 ,  0 ,  ( ( g `  z )  +  y ) ) )  o R  <_  F 
<->  ( z  e.  RR  |->  0 )  o R  <_  F ) )
125124rexbidv 2718 . . . . . . . . . . . . . . . . . . . . 21  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  y ) ) )  o R  <_  F  <->  E. y  e.  RR+  (
z  e.  RR  |->  0 )  o R  <_  F ) )
126117, 125bitr3d 247 . . . . . . . . . . . . . . . . . . . 20  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( ( E. y  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  o R  <_  F  /\  0  =  ( S.1 `  g
) )  <->  E. y  e.  RR+  ( z  e.  RR  |->  0 )  o R  <_  F )
)
127126rspcev 3044 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( RR  X.  {
0 } )  e. 
dom  S.1  /\  E. y  e.  RR+  ( z  e.  RR  |->  0 )  o R  <_  F )  ->  E. g  e.  dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  o R  <_  F  /\  0  =  ( S.1 `  g
) ) )
12896, 113, 127sylancr 645 . . . . . . . . . . . . . . . . . 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 ) ) )  o R  <_  F  /\  0  =  ( S.1 `  g ) ) )
129 id 20 . . . . . . . . . . . . . . . . . . 19  |-  ( b  =  -oo  ->  b  =  -oo )
130 mnflt 10714 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  e.  RR  ->  -oo  <  0 )
13148, 130mp1i 12 . . . . . . . . . . . . . . . . . . 19  |-  ( b  =  -oo  ->  -oo  <  0 )
132129, 131eqbrtrd 4224 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  -oo  ->  b  <  0 )
133 eqeq1 2441 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  0  ->  (
a  =  ( S.1 `  g )  <->  0  =  ( S.1 `  g ) ) )
134133anbi2d 685 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  0  ->  (
( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  o R  <_  F  /\  a  =  ( S.1 `  g
) )  <->  ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z
)  =  0 ,  0 ,  ( ( g `  z )  +  y ) ) )  o R  <_  F  /\  0  =  ( S.1 `  g ) ) ) )
135134rexbidv 2718 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  0  ->  ( E. g  e.  dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  o R  <_  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 ) ) )  o R  <_  F  /\  0  =  ( S.1 `  g ) ) ) )
136 breq2 4208 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  0  ->  (
b  <  a  <->  b  <  0 ) )
137135, 136anbi12d 692 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  0  ->  (
( E. g  e. 
dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `
 z )  +  y ) ) )  o R  <_  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 ) ) )  o R  <_  F  /\  0  =  ( S.1 `  g ) )  /\  b  <  0
) ) )
138106, 137spcev 3035 . . . . . . . . . . . . . . . . . 18  |-  ( ( E. g  e.  dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  y ) ) )  o R  <_  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 ) ) )  o R  <_  F  /\  a  =  ( S.1 `  g ) )  /\  b  <  a
) )
139128, 132, 138syl2an 464 . . . . . . . . . . . . . . . . 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 ) ) )  o R  <_  F  /\  a  =  ( S.1 `  g ) )  /\  b  <  a
) )
14095, 139sylan 458 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( F : RR --> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  (
f  e.  dom  S.1  /\  ( f  o R  <_  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 ) ) )  o R  <_  F  /\  a  =  ( S.1 `  g
) )  /\  b  <  a ) )
141 simp-4r 744 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( F : RR --> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  (
f  e.  dom  S.1  /\  ( f  o R  <_  F  /\  s  =  ( S.1 `  f
) ) ) )  /\  b  <  ( S.1 `  f ) )  /\  b  =/=  -oo )  ->  b  e.  RR* )
1428adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f  e.  dom  S.1  /\  ( f  o R  <_  F  /\  s  =  ( S.1 `  f
) ) )  -> 
( S.1 `  f )  e.  RR )
143142ad3antlr 712 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( F : RR --> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  (
f  e.  dom  S.1  /\  ( f  o R  <_  F  /\  s  =  ( S.1 `  f
) ) ) )  /\  b  <  ( S.1 `  f ) )  /\  b  =/=  -oo )  ->  ( S.1 `  f
)  e.  RR )
144 simpllr 736 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  ( f  e. 
dom  S.1  /\  ( f  o R  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  /\  b  <  ( S.1 `  f
) )  ->  b  e.  RR* )
145 ngtmnft 10747 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( b  e.  RR*  ->  ( b  =  -oo  <->  -.  -oo  <  b ) )
146145biimprd 215 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  e.  RR*  ->  ( -. 
-oo  <  b  ->  b  =  -oo ) )
147146necon1ad 2665 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  e.  RR*  ->  ( b  =/=  -oo  ->  -oo  <  b ) )
148147imp 419 . . . . . . . . . . . . . . . . . . 19  |-  ( ( b  e.  RR*  /\  b  =/=  -oo )  ->  -oo  <  b )
149144, 148sylan 458 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( F : RR --> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  (
f  e.  dom  S.1  /\  ( f  o R  <_  F  /\  s  =  ( S.1 `  f
) ) ) )  /\  b  <  ( S.1 `  f ) )  /\  b  =/=  -oo )  ->  -oo  <  b )
150 simpr 448 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  b  e.  RR* )  ->  b  e.  RR* )
1519adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( f  e.  dom  S.1  /\  ( f  o R  <_  F  /\  s  =  ( S.1 `  f
) ) )  -> 
( S.1 `  f )  e.  RR* )
152150, 151anim12i 550 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  ( f  e. 
dom  S.1  /\  ( f  o R  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  ->  (
b  e.  RR*  /\  ( S.1 `  f )  e. 
RR* ) )
153 xrltle 10734 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( b  e.  RR*  /\  ( S.1 `  f )  e. 
RR* )  ->  (
b  <  ( S.1 `  f )  ->  b  <_  ( S.1 `  f
) ) )
154153imp 419 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( b  e.  RR*  /\  ( S.1 `  f
)  e.  RR* )  /\  b  <  ( S.1 `  f ) )  -> 
b  <_  ( S.1 `  f ) )
155152, 154sylan 458 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  ( f  e. 
dom  S.1  /\  ( f  o R  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  /\  b  <  ( S.1 `  f
) )  ->  b  <_  ( S.1 `  f
) )
156155adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( F : RR --> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  (
f  e.  dom  S.1  /\  ( f  o R  <_  F  /\  s  =  ( S.1 `  f
) ) ) )  /\  b  <  ( S.1 `  f ) )  /\  b  =/=  -oo )  ->  b  <_  ( S.1 `  f ) )
157 xrre 10749 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( b  e.  RR*  /\  ( S.1 `  f
)  e.  RR )  /\  (  -oo  <  b  /\  b  <_  ( S.1 `  f ) ) )  ->  b  e.  RR )
158141, 143, 149, 156, 157syl22anc 1185 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( F : RR --> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  (
f  e.  dom  S.1  /\  ( f  o R  <_  F  /\  s  =  ( S.1 `  f
) ) ) )  /\  b  <  ( S.1 `  f ) )  /\  b  =/=  -oo )  ->  b  e.  RR )
159128ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  ( f  e. 
dom  S.1  /\  ( f  o R  <_  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 ) ) )  o R  <_  F  /\  0  =  ( S.1 `  g
) ) )
160 simplrl 737 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  ( f  e. 
dom  S.1  /\  ( f  o R  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  /\  (
b  <  ( S.1 `  f )  /\  b  e.  RR ) )  /\  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
b  <  ( S.1 `  f ) )
161 simplrl 737 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  ( f  e. 
dom  S.1  /\  ( f  o R  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  /\  (
b  <  ( S.1 `  f )  /\  b  e.  RR ) )  -> 
f  e.  dom  S.1 )
162 simpl 444 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( f  e.  dom  S.1  /\  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
f  e.  dom  S.1 )
163 cnvimass 5216 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( `' f " ( ran  f  \  { 0 } ) )  C_  dom  f
164 fdm 5587 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f : RR --> RR  ->  dom  f  =  RR )
16535, 164syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f  e.  dom  S.1  ->  dom  f  =  RR )
166163, 165syl5sseq 3388 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f  e.  dom  S.1  ->  ( `' f " ( ran  f  \  { 0 } ) )  C_  RR )
167166adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( f  e.  dom  S.1  /\  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
( `' f "
( ran  f  \  { 0 } ) )  C_  RR )
168 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( f  e.  dom  S.1  /\  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )
169164eqcomd 2440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( f : RR --> RR  ->  RR  =  dom  f )
170 ffun 5585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( f : RR --> RR  ->  Fun  f )
171 difpreima 5850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( `' f " ran  f
)  =  dom  f
174173difeq1i 3453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( `' f " ran  f )  \  ( `' f " {
0 } ) )  =  ( dom  f  \  ( `' f
" { 0 } ) )
175172, 174syl6eq 2483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( f : RR --> RR  ->  ( `' f " ( ran  f  \  { 0 } ) )  =  ( dom  f  \ 
( `' f " { 0 } ) ) )
176169, 175difeq12d 3458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( f : RR --> RR  ->  ( RR  \  ( `' f " ( ran  f  \  { 0 } ) ) )  =  ( dom  f  \  ( dom  f  \  ( `' f
" { 0 } ) ) ) )
177 cnvimass 5216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( `' f " { 0 } )  C_  dom  f
178 dfss4 3567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( `' f " {
0 } )  C_  dom  f  <->  ( dom  f  \  ( dom  f  \  ( `' f
" { 0 } ) ) )  =  ( `' f " { 0 } ) )
179177, 178mpbi 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( dom  f  \  ( dom  f  \  ( `' f " { 0 } ) ) )  =  ( `' f
" { 0 } )
180176, 179syl6eq 2483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( f : RR --> RR  ->  ( RR  \  ( `' f " ( ran  f  \  { 0 } ) ) )  =  ( `' f
" { 0 } ) )
181180eleq2d 2502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( f : RR --> RR  ->  ( z  e.  ( RR 
\  ( `' f
" ( ran  f  \  { 0 } ) ) )  <->  z  e.  ( `' f " {
0 } ) ) )
182 ffn 5583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( f : RR --> RR  ->  f  Fn  RR )
183 fniniseg 5843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( f  Fn  RR  ->  (
z  e.  ( `' f " { 0 } )  <->  ( z  e.  RR  /\  ( f `
 z )  =  0 ) ) )
184 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( z  e.  RR  /\  ( f `  z
)  =  0 )  ->  ( f `  z )  =  0 )
185183, 184syl6bi 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 419 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( f  e.  dom  S.1  /\  z  e.  ( RR 
\  ( `' f
" ( ran  f  \  { 0 } ) ) ) )  -> 
( f `  z
)  =  0 )
190189adantlr 696 . . . . . . . . . . . . . . . . . . . . . . . . 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 19594 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( f  e.  dom  S.1  /\  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
( S.1 `  f )  =  0 )
192161, 191sylan 458 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  ( f  e. 
dom  S.1  /\  ( f  o R  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  /\  (
b  <  ( S.1 `  f )  /\  b  e.  RR ) )  /\  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
( S.1 `  f )  =  0 )
193160, 192breqtrd 4228 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  ( f  e. 
dom  S.1  /\  ( f  o R  <_  F  /\  s  =  ( S.1 `  f ) ) ) )  /\  (
b  <  ( S.1 `  f )  /\  b  e.  RR ) )  /\  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
b  <  0 )
194159, 193, 138syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  ( f  e. 
dom  S.1  /\  ( f  o R  <_  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 ) ) )  o R  <_  F  /\  a  =  ( S.1 `  g ) )  /\  b  <  a
) )
195 simprl 733 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  (
f  e.  dom  S.1  /\  ( f  o R  <_  F  /\  s  =  ( S.1 `  f
) ) ) )  ->  f  e.  dom  S.1 )
196 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( b  <  ( S.1 `  f )  /\  b  e.  RR )  ->  b  e.  RR )
197195, 196anim12i 550 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  ( f  e. 
dom  S.1  /\  ( f  o R  <_  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 5734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) )  e.  _V
202201, 106ifex 3789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( f  e.  dom  S.1  ->  f  =  ( u  e.  RR  |->  ( f `  u ) ) )
205204ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  f  =  ( u  e.  RR  |->  ( f `  u
) ) )
206 eqidd 2436 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6314 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( f  o F  -  (
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 oveq2 6081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 )  =  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) )  ->  ( ( f `
 u )  -  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) )  =  ( ( f `
 u )  -  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ) )
209 oveq2 6081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 )  =  0  ->  ( (
f `  u )  -  if ( u  e.  ( `' f "
( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) )  =  ( ( f `  u
)  -  0 ) )
210208, 209ifsb 3740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
211173, 164syl5eq 2479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( f : RR --> RR  ->  ( `' f " ran  f )  =  RR )
212211difeq1d 3456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( f : RR --> RR  ->  ( ( `' f " ran  f )  \  ( `' f " {
0 } ) )  =  ( RR  \ 
( `' f " { 0 } ) ) )
213172, 212eqtrd 2467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( f : RR --> RR  ->  ( `' f " ( ran  f  \  { 0 } ) )  =  ( RR  \  ( `' f " {
0 } ) ) )
214213eleq2d 2502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( f : RR --> RR  ->  ( u  e.  ( `' f " ( ran  f  \  { 0 } ) )  <->  u  e.  ( RR  \  ( `' f " {
0 } ) ) ) )
21535, 214syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( f  e.  dom  S.1  ->  ( u  e.  ( `' f " ( ran  f  \  { 0 } ) )  <->  u  e.  ( RR  \  ( `' f " {
0 } ) ) ) )
216215ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) )
217 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( f  e. 
dom  S.1  /\  b  e.  RR )  /\  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) )  =/=  0 )  /\  u  e.  RR )  ->  u  e.  RR )
218217biantrurd 495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) )
219 eldif 3322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( u  e.  ( RR  \ 
( `' f " { 0 } ) )  <->  ( u  e.  RR  /\  -.  u  e.  ( `' f " { 0 } ) ) )
220218, 219syl6bbr 255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) )
221216, 220bitr4d 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) )
222221con2bid 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) )
223 fniniseg 5843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( f  Fn  RR  ->  (
u  e.  ( `' f " { 0 } )  <->  ( u  e.  RR  /\  ( f `
 u )  =  0 ) ) )
22435, 182, 2233syl 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( f  e.  dom  S.1  ->  ( u  e.  ( `' f " { 0 } )  <->  ( u  e.  RR  /\  ( f `
 u )  =  0 ) ) )
225224ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
226222, 225bitr3d 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
227 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( f `  u )  =  0  ->  (
( f `  u
)  -  0 )  =  ( 0  -  0 ) )
228 0cn 9076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  0  e.  CC
229228subidi 9363 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( 0  -  0 )  =  0
230227, 229syl6eq 2483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( f `  u )  =  0  ->  (
( f `  u
)  -  0 )  =  0 )
231230adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( u  e.  RR  /\  ( f `  u
)  =  0 )  ->  ( ( f `
 u )  - 
0 )  =  0 )
232226, 231syl6bi 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
233232imp 419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
234233ifeq2da 3757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
235210, 234syl5eq 2479 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
236235mpteq2dva 4287 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
237207, 236eqtrd 2467 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( f  o F  -  (
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 ) ) )
238 simpll 731 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  f  e.  dom  S.1 )
239201a1i 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 )
240 1ex 9078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  1  e.  _V
241240, 106ifex 3789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  1 ,  0 )  e.  _V
242241a1i 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 )
243 fconstmpt 4913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) ) ) )
244243a1i 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 } ) ) ) ) ) ) )
245 eqidd 2436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
246198, 239, 242, 244, 245offval2 6314 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) ) ) } )  o F  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 ) ) ) )
247 oveq2 6081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  1 ,  0 )  =  1  ->  (
( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) )  x.  if ( u  e.  ( `' f
" ( ran  f  \  { 0 } ) ) ,  1 ,  0 ) )  =  ( ( ( ( S.1 `  f )  -  b )  / 
( 2  x.  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) )  x.  1 ) )
248 oveq2 6081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  1 ,  0 )  =  0  ->  (
( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) )  x.  if ( u  e.  ( `' f
" ( ran  f  \  { 0 } ) ) ,  1 ,  0 ) )  =  ( ( ( ( S.1 `  f )  -  b )  / 
( 2  x.  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) )  x.  0 ) )
249247, 248ifsb 3740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
250 resubcl 9357 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( S.1 `  f
)  e.  RR  /\  b  e.  RR )  ->  ( ( S.1 `  f
)  -  b )  e.  RR )
2518, 250sylan 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( f  e.  dom  S.1  /\  b  e.  RR )  ->  ( ( S.1 `  f )  -  b
)  e.  RR )
252251adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( ( S.1 `  f )  -  b )  e.  RR )
253 2re 10061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  2  e.  RR
254 i1fima 19562 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( f  e.  dom  S.1  ->  ( `' f " ( ran  f  \  { 0 } ) )  e. 
dom  vol )
255 mblvol 19418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( `' f " ( ran  f  \  { 0 } ) )  e. 
dom  vol  ->  ( vol `  ( `' f "
( ran  f  \  { 0 } ) ) )  =  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) ) )
256254, 255syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( f  e.  dom  S.1  ->  ( vol `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) ) )
257 neldifsn 3921 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  -.  0  e.  ( ran  f  \  { 0 } )
258 i1fima2 19563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( f  e.  dom  S.1  /\ 
-.  0  e.  ( ran  f  \  {
0 } ) )  ->  ( vol `  ( `' f " ( ran  f  \  { 0 } ) ) )  e.  RR )
259257, 258mpan2 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( f  e.  dom  S.1  ->  ( vol `  ( `' f " ( ran  f  \  { 0 } ) ) )  e.  RR )
260256, 259eqeltrrd 2510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( f  e.  dom  S.1  ->  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) )  e.  RR )
261 remulcl 9067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( 2  e.  RR  /\  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) )  e.  RR )  -> 
( 2  x.  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) ) )  e.  RR )
262253, 260, 261sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( f  e.  dom  S.1  ->  ( 2  x.  ( vol
* `  ( `' f " ( ran  f  \  { 0 } ) ) ) )  e.  RR )
263262ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( 2  x.  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) ) )  e.  RR )
264 2cn 10062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  2  e.  CC
265264a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  2  e.  CC )
266260ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( vol * `
 ( `' f
" ( ran  f  \  { 0 } ) ) )  e.  RR )
267266recnd 9106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( vol * `
 ( `' f
" ( ran  f  \  { 0 } ) ) )  e.  CC )
268 2ne0 10075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  2  =/=  0
269268a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  2  =/=  0 )
270 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( vol * `
 ( `' f
" ( ran  f  \  { 0 } ) ) )  =/=  0
)
271265, 267, 269, 270mulne0d 9666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( 2  x.  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) ) )  =/=  0 )
272252, 263, 271redivcld 9834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
273272recnd 9106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
274273mulid1d 9097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) ) ) )
275273mul01d 9257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
276274, 275ifeq12d 3747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
277249, 276syl5eq 2479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
278277mpteq2dv 4288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
279246, 278eqtrd 2467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) ) ) } )  o F  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 ) ) )
280 eqid 2435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
281280i1f1 19574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
282254, 259, 281syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( f  e.  dom  S.1  ->  ( u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  1 ,  0 ) )  e.  dom  S.1 )
283282ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
284283, 272i1fmulc 19587 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) ) ) } )  o F  x.  (
u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  1 ,  0 ) ) )  e.  dom  S.1 )
285279, 284eqeltrrd 2510 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
286 i1fsub 19592 . . . . . . . . . . . . . . . . . . . . . . . . . . 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  o F  -  ( 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 )
287238, 285, 286syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( f  o F  -  (
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 )
288237, 287eqeltrrd 2510 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
289 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( u  =  z  ->  (
u  e.  ( `' f " ( ran  f  \  { 0 } ) )  <->  z  e.  ( `' f " ( ran  f  \  { 0 } ) ) ) )
290 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( u  =  z  ->  (
f `  u )  =  ( f `  z ) )
291290oveq1d 6088 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) ) ) ) )
292 eqidd 2436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( u  =  z  ->  0  =  0 )
293289, 291, 292ifbieq12d 3753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
294 eqid 2435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
295 ovex 6098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( f `  z )  -  ( ( ( S.1 `  f )  -  b )  / 
( 2  x.  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) )  e. 
_V
296295, 106ifex 3789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  if ( z  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( f `  z )  -  (
( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) ) )