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

Theorem itg2addnclem 25317
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.)
Hypothesis
Ref Expression
itg2addnclem.1  |-  L  =  { x  |  E. g  e.  dom  S.1 ( E. y  e.  RR+  (
g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  { 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, w, g, F
Allowed substitution hints:    L( x, y, z, w, g)

Proof of Theorem itg2addnclem
Dummy variables  t 
s  u  v  f  a  b are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2316 . . 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 19136 . 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+  (
g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  { y } ) )  o R  <_  F  /\  x  =  ( S.1 `  g ) ) }
43supeq1i 7245 . . 3  |-  sup ( L ,  RR* ,  <  )  =  sup ( { x  |  E. g  e.  dom  S.1 ( E. y  e.  RR+  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  o R  <_  F  /\  x  =  ( S.1 `  g ) ) } ,  RR* ,  <  )
5 xrltso 10522 . . . . 5  |-  <  Or  RR*
65a1i 10 . . . 4  |-  ( F : RR --> ( 0 [,]  +oo )  ->  <  Or 
RR* )
7 simprr 733 . . . . . . . 8  |-  ( ( f  e.  dom  S.1  /\  ( f  o R  <_  F  /\  x  =  ( S.1 `  f
) ) )  ->  x  =  ( S.1 `  f ) )
8 itg1cl 19093 . . . . . . . . . 10  |-  ( f  e.  dom  S.1  ->  ( S.1 `  f )  e.  RR )
98rexrd 8926 . . . . . . . . 9  |-  ( f  e.  dom  S.1  ->  ( S.1 `  f )  e.  RR* )
109adantr 451 . . . . . . . 8  |-  ( ( f  e.  dom  S.1  /\  ( f  o R  <_  F  /\  x  =  ( S.1 `  f
) ) )  -> 
( S.1 `  f )  e.  RR* )
117, 10eqeltrd 2390 . . . . . . 7  |-  ( ( f  e.  dom  S.1  /\  ( f  o R  <_  F  /\  x  =  ( S.1 `  f
) ) )  ->  x  e.  RR* )
1211rexlimiva 2696 . . . . . 6  |-  ( E. f  e.  dom  S.1 ( f  o R  <_  F  /\  x  =  ( S.1 `  f
) )  ->  x  e.  RR* )
1312abssi 3282 . . . . 5  |-  { x  |  E. f  e.  dom  S.1 ( f  o R  <_  F  /\  x  =  ( S.1 `  f
) ) }  C_  RR*
14 supxrcl 10680 . . . . 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 11 . . . 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 oveq1 5907 . . . . . . . . . . . . 13  |-  ( g  =  f  ->  (
g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  { y } ) )  =  ( f  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) ) )
1716breq1d 4070 . . . . . . . . . . . 12  |-  ( g  =  f  ->  (
( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR 
X.  { y } ) )  o R  <_  F  <->  ( f  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  o R  <_  F
) )
1817rexbidv 2598 . . . . . . . . . . 11  |-  ( g  =  f  ->  ( E. y  e.  RR+  (
g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  { y } ) )  o R  <_  F 
<->  E. y  e.  RR+  ( f  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR 
X.  { y } ) )  o R  <_  F ) )
19 fveq2 5563 . . . . . . . . . . . 12  |-  ( g  =  f  ->  ( S.1 `  g )  =  ( S.1 `  f
) )
2019eqeq2d 2327 . . . . . . . . . . 11  |-  ( g  =  f  ->  (
x  =  ( S.1 `  g )  <->  x  =  ( S.1 `  f ) ) )
2118, 20anbi12d 691 . . . . . . . . . 10  |-  ( g  =  f  ->  (
( E. y  e.  RR+  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR 
X.  { y } ) )  o R  <_  F  /\  x  =  ( S.1 `  g
) )  <->  ( E. y  e.  RR+  ( f  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  o R  <_  F  /\  x  =  ( S.1 `  f ) ) ) )
2221cbvrexv 2799 . . . . . . . . 9  |-  ( E. g  e.  dom  S.1 ( E. y  e.  RR+  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR 
X.  { y } ) )  o R  <_  F  /\  x  =  ( S.1 `  g
) )  <->  E. f  e.  dom  S.1 ( E. y  e.  RR+  ( f  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  o R  <_  F  /\  x  =  ( S.1 `  f ) ) )
23 i1ff 19084 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  e.  dom  S.1  ->  f : RR --> RR )
2423ad2antlr 707 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  f : RR --> RR )
2524ffvelrnda 5703 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  ->  (
f `  t )  e.  RR )
2625rexrd 8926 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  ->  (
f `  t )  e.  RR* )
2726adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  /\  if ( ( f `  t )  =  0 ,  0 ,  ( ( f `  t
)  +  y ) )  <_  ( F `  t ) )  -> 
( f `  t
)  e.  RR* )
28 0re 8883 . . . . . . . . . . . . . . . . . . 19  |-  0  e.  RR
29 simplr 731 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  ->  y  e.  RR+ )
3029rpred 10437 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  ->  y  e.  RR )
3125, 30readdcld 8907 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  ->  (
( f `  t
)  +  y )  e.  RR )
32 ifcl 3635 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 0  e.  RR  /\  ( ( f `  t )  +  y )  e.  RR )  ->  if ( ( f `  t )  =  0 ,  0 ,  ( ( f `
 t )  +  y ) )  e.  RR )
3328, 31, 32sylancr 644 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  ->  if ( ( f `  t )  =  0 ,  0 ,  ( ( f `  t
)  +  y ) )  e.  RR )
3433rexrd 8926 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  ->  if ( ( f `  t )  =  0 ,  0 ,  ( ( f `  t
)  +  y ) )  e.  RR* )
3534adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  /\  if ( ( f `  t )  =  0 ,  0 ,  ( ( f `  t
)  +  y ) )  <_  ( F `  t ) )  ->  if ( ( f `  t )  =  0 ,  0 ,  ( ( f `  t
)  +  y ) )  e.  RR* )
36 iccssxr 10779 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0 [,]  +oo )  C_  RR*
37 fss 5435 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  (
0 [,]  +oo )  C_  RR* )  ->  F : RR
--> RR* )
3836, 37mpan2 652 . . . . . . . . . . . . . . . . . . 19  |-  ( F : RR --> ( 0 [,]  +oo )  ->  F : RR --> RR* )
3938ad2antrr 706 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  F : RR
--> RR* )
4039ffvelrnda 5703 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  ->  ( F `  t )  e.  RR* )
4140adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  /\  if ( ( f `  t )  =  0 ,  0 ,  ( ( f `  t
)  +  y ) )  <_  ( F `  t ) )  -> 
( F `  t
)  e.  RR* )
42 id 19 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( f `  t )  =  0  ->  (
f `  t )  =  0 )
43 0le0 9872 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  <_  0
4442, 43syl6eqbr 4097 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( f `  t )  =  0  ->  (
f `  t )  <_  0 )
45 iftrue 3605 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( f `  t )  =  0  ->  if ( ( f `  t )  =  0 ,  0 ,  ( ( f `  t
)  +  y ) )  =  0 )
4644, 45breqtrrd 4086 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( f `  t )  =  0  ->  (
f `  t )  <_  if ( ( f `
 t )  =  0 ,  0 ,  ( ( f `  t )  +  y ) ) )
4746adantl 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( f  e. 
dom  S.1  /\  y  e.  RR+ )  /\  t  e.  RR )  /\  (
f `  t )  =  0 )  -> 
( f `  t
)  <_  if (
( f `  t
)  =  0 ,  0 ,  ( ( f `  t )  +  y ) ) )
48 rpge0 10413 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  RR+  ->  0  <_ 
y )
4948ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( f  e.  dom  S.1 
/\  y  e.  RR+ )  /\  t  e.  RR )  ->  0  <_  y
)
5023ffvelrnda 5703 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( f `  t )  e.  RR )
5150adantlr 695 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( f  e.  dom  S.1 
/\  y  e.  RR+ )  /\  t  e.  RR )  ->  ( f `  t )  e.  RR )
52 simplr 731 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( f  e.  dom  S.1 
/\  y  e.  RR+ )  /\  t  e.  RR )  ->  y  e.  RR+ )
5352rpred 10437 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( f  e.  dom  S.1 
/\  y  e.  RR+ )  /\  t  e.  RR )  ->  y  e.  RR )
5451, 53addge01d 9405 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( f  e.  dom  S.1 
/\  y  e.  RR+ )  /\  t  e.  RR )  ->  ( 0  <_ 
y  <->  ( f `  t )  <_  (
( f `  t
)  +  y ) ) )
5549, 54mpbid 201 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( f  e.  dom  S.1 
/\  y  e.  RR+ )  /\  t  e.  RR )  ->  ( f `  t )  <_  (
( f `  t
)  +  y ) )
5655adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( f  e. 
dom  S.1  /\  y  e.  RR+ )  /\  t  e.  RR )  /\  (
f `  t )  =/=  0 )  ->  (
f `  t )  <_  ( ( f `  t )  +  y ) )
57 ifnefalse 3607 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( f `  t )  =/=  0  ->  if ( ( f `  t )  =  0 ,  0 ,  ( ( f `  t
)  +  y ) )  =  ( ( f `  t )  +  y ) )
5857adantl 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( f  e. 
dom  S.1  /\  y  e.  RR+ )  /\  t  e.  RR )  /\  (
f `  t )  =/=  0 )  ->  if ( ( f `  t )  =  0 ,  0 ,  ( ( f `  t
)  +  y ) )  =  ( ( f `  t )  +  y ) )
5956, 58breqtrrd 4086 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( f  e. 
dom  S.1  /\  y  e.  RR+ )  /\  t  e.  RR )  /\  (
f `  t )  =/=  0 )  ->  (
f `  t )  <_  if ( ( f `
 t )  =  0 ,  0 ,  ( ( f `  t )  +  y ) ) )
6047, 59pm2.61dane 2557 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( f  e.  dom  S.1 
/\  y  e.  RR+ )  /\  t  e.  RR )  ->  ( f `  t )  <_  if ( ( f `  t )  =  0 ,  0 ,  ( ( f `  t
)  +  y ) ) )
6160adantlll 698 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  ->  (
f `  t )  <_  if ( ( f `
 t )  =  0 ,  0 ,  ( ( f `  t )  +  y ) ) )
6261adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  /\  if ( ( f `  t )  =  0 ,  0 ,  ( ( f `  t
)  +  y ) )  <_  ( F `  t ) )  -> 
( f `  t
)  <_  if (
( f `  t
)  =  0 ,  0 ,  ( ( f `  t )  +  y ) ) )
63 simpr 447 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  /\  if ( ( f `  t )  =  0 ,  0 ,  ( ( f `  t
)  +  y ) )  <_  ( F `  t ) )  ->  if ( ( f `  t )  =  0 ,  0 ,  ( ( f `  t
)  +  y ) )  <_  ( F `  t ) )
6427, 35, 41, 62, 63xrletrd 10540 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  /\  if ( ( f `  t )  =  0 ,  0 ,  ( ( f `  t
)  +  y ) )  <_  ( F `  t ) )  -> 
( f `  t
)  <_  ( F `  t ) )
6564ex 423 . . . . . . . . . . . . . 14  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  ->  ( if ( ( f `  t )  =  0 ,  0 ,  ( ( f `  t
)  +  y ) )  <_  ( F `  t )  ->  (
f `  t )  <_  ( F `  t
) ) )
6665ralimdva 2655 . . . . . . . . . . . . 13  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  ( A. t  e.  RR  if ( ( f `  t )  =  0 ,  0 ,  ( ( f `  t
)  +  y ) )  <_  ( F `  t )  ->  A. t  e.  RR  ( f `  t )  <_  ( F `  t )
) )
67 ovex 5925 . . . . . . . . . . . . . . . . 17  |-  ( u ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) v )  e.  _V
6867a1i 10 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  (
u  e.  RR  /\  v  e.  { y } ) )  -> 
( u ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) v )  e.  _V )
69 vex 2825 . . . . . . . . . . . . . . . . . 18  |-  y  e. 
_V
7069fconst 5465 . . . . . . . . . . . . . . . . 17  |-  ( RR 
X.  { y } ) : RR --> { y }
7170a1i 10 . . . . . . . . . . . . . . . 16  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  ( RR 
X.  { y } ) : RR --> { y } )
72 reex 8873 . . . . . . . . . . . . . . . . 17  |-  RR  e.  _V
7372a1i 10 . . . . . . . . . . . . . . . 16  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  RR  e.  _V )
74 inidm 3412 . . . . . . . . . . . . . . . 16  |-  ( RR 
i^i  RR )  =  RR
7568, 24, 71, 73, 73, 74off 6135 . . . . . . . . . . . . . . 15  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  ( f  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) ) : RR --> _V )
76 ffn 5427 . . . . . . . . . . . . . . 15  |-  ( ( f  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  { y } ) ) : RR --> _V  ->  ( f  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  { y } ) )  Fn  RR )
7775, 76syl 15 . . . . . . . . . . . . . 14  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  ( f  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  Fn  RR )
78 ffn 5427 . . . . . . . . . . . . . . 15  |-  ( F : RR --> ( 0 [,]  +oo )  ->  F  Fn  RR )
7978ad2antrr 706 . . . . . . . . . . . . . 14  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  F  Fn  RR )
80 ffn 5427 . . . . . . . . . . . . . . . . . . 19  |-  ( f : RR --> RR  ->  f  Fn  RR )
8123, 80syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( f  e.  dom  S.1  ->  f  Fn  RR )
8281ad2antlr 707 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  f  Fn  RR )
8382adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  ->  f  Fn  RR )
84 ffn 5427 . . . . . . . . . . . . . . . . 17  |-  ( ( RR  X.  { y } ) : RR --> { y }  ->  ( RR  X.  { y } )  Fn  RR )
8570, 84mp1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  ->  ( RR  X.  { y } )  Fn  RR )
8672a1i 10 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  ->  RR  e.  _V )
87 eqidd 2317 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  /\  u  e.  RR )  ->  (
f `  u )  =  ( f `  u ) )
8869fvconst2 5768 . . . . . . . . . . . . . . . . 17  |-  ( u  e.  RR  ->  (
( RR  X.  {
y } ) `  u )  =  y )
8988adantl 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  /\  u  e.  RR )  ->  (
( RR  X.  {
y } ) `  u )  =  y )
9083, 85, 86, 86, 74, 87, 89offval 6127 . . . . . . . . . . . . . . 15  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  ->  (
f  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  { y } ) )  =  ( u  e.  RR  |->  ( ( f `  u ) ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) y ) ) )
91 fveq2 5563 . . . . . . . . . . . . . . . . 17  |-  ( u  =  t  ->  (
f `  u )  =  ( f `  t ) )
9291oveq1d 5915 . . . . . . . . . . . . . . . 16  |-  ( u  =  t  ->  (
( f `  u
) ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) y )  =  ( ( f `  t
) ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) y ) )
93 eqidd 2317 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  ->  (
z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) )  =  ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) )
94 eqeq1 2322 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  ( f `  t )  ->  (
z  =  0  <->  (
f `  t )  =  0 ) )
9594adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( z  =  ( f `
 t )  /\  w  =  y )  ->  ( z  =  0  <-> 
( f `  t
)  =  0 ) )
96 oveq12 5909 . . . . . . . . . . . . . . . . . . 19  |-  ( ( z  =  ( f `
 t )  /\  w  =  y )  ->  ( z  +  w
)  =  ( ( f `  t )  +  y ) )
9795, 96ifbieq2d 3619 . . . . . . . . . . . . . . . . . 18  |-  ( ( z  =  ( f `
 t )  /\  w  =  y )  ->  if ( z  =  0 ,  0 ,  ( z  +  w
) )  =  if ( ( f `  t )  =  0 ,  0 ,  ( ( f `  t
)  +  y ) ) )
9897adantl 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  /\  (
z  =  ( f `
 t )  /\  w  =  y )
)  ->  if (
z  =  0 ,  0 ,  ( z  +  w ) )  =  if ( ( f `  t )  =  0 ,  0 ,  ( ( f `
 t )  +  y ) ) )
99 c0ex 8877 . . . . . . . . . . . . . . . . . . 19  |-  0  e.  _V
100 ovex 5925 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f `  t )  +  y )  e. 
_V
10199, 100ifex 3657 . . . . . . . . . . . . . . . . . 18  |-  if ( ( f `  t
)  =  0 ,  0 ,  ( ( f `  t )  +  y ) )  e.  _V
102101a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  ->  if ( ( f `  t )  =  0 ,  0 ,  ( ( f `  t
)  +  y ) )  e.  _V )
10393, 98, 25, 30, 102ovmpt2d 6017 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  ->  (
( f `  t
) ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) y )  =  if ( ( f `  t )  =  0 ,  0 ,  ( ( f `  t
)  +  y ) ) )
10492, 103sylan9eqr 2370 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  /\  u  =  t )  -> 
( ( f `  u ) ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) y )  =  if ( ( f `  t )  =  0 ,  0 ,  ( ( f `  t
)  +  y ) ) )
105 simpr 447 . . . . . . . . . . . . . . 15  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  ->  t  e.  RR )
10690, 104, 105, 102fvmptd 5644 . . . . . . . . . . . . . 14  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  ->  (
( f  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR 
X.  { y } ) ) `  t
)  =  if ( ( f `  t
)  =  0 ,  0 ,  ( ( f `  t )  +  y ) ) )
107 eqidd 2317 . . . . . . . . . . . . . 14  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  ->  ( F `  t )  =  ( F `  t ) )
10877, 79, 73, 73, 74, 106, 107ofrfval 6128 . . . . . . . . . . . . 13  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  ( ( f  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  { y } ) )  o R  <_  F 
<-> 
A. t  e.  RR  if ( ( f `  t )  =  0 ,  0 ,  ( ( f `  t
)  +  y ) )  <_  ( F `  t ) ) )
109 eqidd 2317 . . . . . . . . . . . . . 14  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  t  e.  RR )  ->  (
f `  t )  =  ( f `  t ) )
11082, 79, 73, 73, 74, 109, 107ofrfval 6128 . . . . . . . . . . . . 13  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  ( f  o R  <_  F  <->  A. t  e.  RR  (
f `  t )  <_  ( F `  t
) ) )
11166, 108, 1103imtr4d 259 . . . . . . . . . . . 12  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  ( ( f  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  { y } ) )  o R  <_  F  ->  f  o R  <_  F ) )
112111rexlimdva 2701 . . . . . . . . . . 11  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  ->  ( E. y  e.  RR+  (
f  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  { y } ) )  o R  <_  F  ->  f  o R  <_  F ) )
113112anim1d 547 . . . . . . . . . 10  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1 )  ->  (
( E. y  e.  RR+  ( f  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR 
X.  { y } ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) )  ->  (
f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) ) )
114113reximdva 2689 . . . . . . . . 9  |-  ( F : RR --> ( 0 [,]  +oo )  ->  ( E. f  e.  dom  S.1 ( E. y  e.  RR+  ( f  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR 
X.  { y } ) )  o R  <_  F  /\  x  =  ( S.1 `  f
) )  ->  E. f  e.  dom  S.1 ( f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) ) )
11522, 114syl5bi 208 . . . . . . . 8  |-  ( F : RR --> ( 0 [,]  +oo )  ->  ( E. g  e.  dom  S.1 ( E. y  e.  RR+  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR 
X.  { y } ) )  o R  <_  F  /\  x  =  ( S.1 `  g
) )  ->  E. f  e.  dom  S.1 ( f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) ) )
116115ss2abdv 3280 . . . . . . 7  |-  ( F : RR --> ( 0 [,]  +oo )  ->  { x  |  E. g  e.  dom  S.1 ( E. y  e.  RR+  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR 
X.  { y } ) )  o R  <_  F  /\  x  =  ( S.1 `  g
) ) }  C_  { x  |  E. f  e.  dom  S.1 ( f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) } )
117116sseld 3213 . . . . . 6  |-  ( F : RR --> ( 0 [,]  +oo )  ->  (
b  e.  { x  |  E. g  e.  dom  S.1 ( E. y  e.  RR+  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR 
X.  { 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
) ) } ) )
118 simp3r 984 . . . . . . . . . . 11  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1  /\  (
f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) )  ->  x  =  ( S.1 `  f
) )
11993ad2ant2 977 . . . . . . . . . . 11  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1  /\  (
f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) )  ->  ( S.1 `  f )  e. 
RR* )
120118, 119eqeltrd 2390 . . . . . . . . . 10  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  f  e.  dom  S.1  /\  (
f  o R  <_  F  /\  x  =  ( S.1 `  f ) ) )  ->  x  e.  RR* )
121120rexlimdv3a 2703 . . . . . . . . 9  |-  ( F : RR --> ( 0 [,]  +oo )  ->  ( E. f  e.  dom  S.1 ( f  o R  <_  F  /\  x  =  ( S.1 `  f
) )  ->  x  e.  RR* ) )
122121abssdv 3281 . . . . . . . 8  |-  ( F : RR --> ( 0 [,]  +oo )  ->  { x  |  E. f  e.  dom  S.1 ( f  o R  <_  F  /\  x  =  ( S.1 `  f
) ) }  C_  RR* )
123 xrsupss 10674 . . . . . . . 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 ) ) )
124122, 123syl 15 . . . . . . 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 ) ) )
1256, 124supub 7255 . . . . . 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 ) )
126117, 125syld 40 . . . . 5  |-  ( F : RR --> ( 0 [,]  +oo )  ->  (
b  e.  { x  |  E. g  e.  dom  S.1 ( E. y  e.  RR+  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR 
X.  { 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 ) )
127126imp 418 . . . 4  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  b  e.  { x  |  E. g  e.  dom  S.1 ( E. y  e.  RR+  (
g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  { 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 )
128 simpr 447 . . . . . . 7  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  b  e.  RR* )  ->  b  e.  RR* )
129 supxrlub 10691 . . . . . . 7  |-  ( ( { 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 ) )
13013, 128, 129sylancr 644 . . . . . 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 ) )
131 simprrr 741 . . . . . . . . . . . . . . 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
) )
132131breq2d 4072 . . . . . . . . . . . . . 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 ) ) )
133 simplll 734 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  ( f  e. 
dom  S.1  /\  f  o R  <_  F )
)  /\  b  <  ( S.1 `  f ) )  ->  F : RR
--> ( 0 [,]  +oo ) )
134 i1f0 19095 . . . . . . . . . . . . . . . . . . . 20  |-  ( RR 
X.  { 0 } )  e.  dom  S.1
135 2rp 10406 . . . . . . . . . . . . . . . . . . . . 21  |-  2  e.  RR+
136 ffvelrn 5701 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  t  e.  RR )  ->  ( F `  t )  e.  ( 0 [,]  +oo ) )
137 0xr 8923 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  0  e.  RR*
138 pnfxr 10502 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  +oo  e.  RR*
139 elicc1 10747 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 0  e.  RR*  /\  +oo  e.  RR* )  ->  (
( F `  t
)  e.  ( 0 [,]  +oo )  <->  ( ( F `  t )  e.  RR*  /\  0  <_ 
( F `  t
)  /\  ( F `  t )  <_  +oo )
) )
140137, 138, 139mp2an 653 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F `  t )  e.  ( 0 [,] 
+oo )  <->  ( ( F `  t )  e.  RR*  /\  0  <_ 
( F `  t
)  /\  ( F `  t )  <_  +oo )
)
141140simp2bi 971 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( F `  t )  e.  ( 0 [,] 
+oo )  ->  0  <_  ( F `  t
) )
142136, 141syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  t  e.  RR )  ->  0  <_  ( F `  t
) )
143142ralrimiva 2660 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F : RR --> ( 0 [,]  +oo )  ->  A. t  e.  RR  0  <_  ( F `  t )
)
14467a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  (
u  e.  { 0 }  /\  v  e. 
{ 2 } ) )  ->  ( u
( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) v )  e.  _V )
14599fconst 5465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( RR 
X.  { 0 } ) : RR --> { 0 }
146145a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( F : RR --> ( 0 [,]  +oo )  ->  ( RR  X.  { 0 } ) : RR --> { 0 } )
147 fconstg 5466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 2  e.  RR+  ->  ( RR 
X.  { 2 } ) : RR --> { 2 } )
148135, 147mp1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( F : RR --> ( 0 [,]  +oo )  ->  ( RR  X.  { 2 } ) : RR --> { 2 } )
14972a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( F : RR --> ( 0 [,]  +oo )  ->  RR  e.  _V )
150144, 146, 148, 149, 149, 74off 6135 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( F : RR --> ( 0 [,]  +oo )  ->  (
( RR  X.  {
0 } )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
2 } ) ) : RR --> _V )
151 ffn 5427 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( RR  X.  {
0 } )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
2 } ) ) : RR --> _V  ->  ( ( RR  X.  {
0 } )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
2 } ) )  Fn  RR )
152150, 151syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F : RR --> ( 0 [,]  +oo )  ->  (
( RR  X.  {
0 } )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
2 } ) )  Fn  RR )
15372a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  e.  RR  ->  RR  e.  _V )
15499a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( t  e.  RR  /\  u  e.  RR )  ->  0  e.  _V )
155135a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( t  e.  RR  /\  u  e.  RR )  ->  2  e.  RR+ )
156 fconstmpt 4769 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( RR 
X.  { 0 } )  =  ( u  e.  RR  |->  0 )
157156a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  e.  RR  ->  ( RR  X.  { 0 } )  =  ( u  e.  RR  |->  0 ) )
158 fconstmpt 4769 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( RR 
X.  { 2 } )  =  ( u  e.  RR  |->  2 )
159158a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  e.  RR  ->  ( RR  X.  { 2 } )  =  ( u  e.  RR  |->  2 ) )
160153, 154, 155, 157, 159offval2 6137 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( t  e.  RR  ->  (
( RR  X.  {
0 } )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
2 } ) )  =  ( u  e.  RR  |->  ( 0 ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) 2 ) ) )
161160fveq1d 5565 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  e.  RR  ->  (
( ( RR  X.  { 0 } )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
2 } ) ) `
 t )  =  ( ( u  e.  RR  |->  ( 0 ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) 2 ) ) `
 t ) )
162 eqidd 2317 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( u  =  t  ->  0  =  0 )
163 2re 9860 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  2  e.  RR
164 iftrue 3605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  0  ->  if ( z  =  0 ,  0 ,  ( z  +  w ) )  =  0 )
165 eqidd 2317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( w  =  2  ->  0  =  0 )
166 eqid 2316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) )  =  ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) )
167164, 165, 166, 99ovmpt2 6025 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 0  e.  RR  /\  2  e.  RR )  ->  ( 0 ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) 2 )  =  0 )
16828, 163, 167mp2an 653 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 0 ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) 2 )  =  0
169168mpteq2i 4140 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( u  e.  RR  |->  ( 0 ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) 2 ) )  =  ( u  e.  RR  |->  0 )
170162, 169, 99fvmpt 5640 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  e.  RR  ->  (
( u  e.  RR  |->  ( 0 ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) 2 ) ) `  t )  =  0 )
171161, 170eqtrd 2348 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  e.  RR  ->  (
( ( RR  X.  { 0 } )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
2 } ) ) `
 t )  =  0 )
172171adantl 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  t  e.  RR )  ->  (
( ( RR  X.  { 0 } )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
2 } ) ) `
 t )  =  0 )
173 eqidd 2317 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  t  e.  RR )  ->  ( F `  t )  =  ( F `  t ) )
174152, 78, 149, 149, 74, 172, 173ofrfval 6128 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F : RR --> ( 0 [,]  +oo )  ->  (
( ( RR  X.  { 0 } )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
2 } ) )  o R  <_  F  <->  A. t  e.  RR  0  <_  ( F `  t ) ) )
175143, 174mpbird 223 . . . . . . . . . . . . . . . . . . . . 21  |-  ( F : RR --> ( 0 [,]  +oo )  ->  (
( RR  X.  {
0 } )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
2 } ) )  o R  <_  F
)
176 sneq 3685 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  2  ->  { y }  =  { 2 } )
177176xpeq2d 4750 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  2  ->  ( RR  X.  { y } )  =  ( RR 
X.  { 2 } ) )
178177oveq2d 5916 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  2  ->  (
( RR  X.  {
0 } )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  =  ( ( RR 
X.  { 0 } )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  { 2 } ) ) )
179178breq1d 4070 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  2  ->  (
( ( RR  X.  { 0 } )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  o R  <_  F  <->  ( ( RR  X.  {
0 } )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
2 } ) )  o R  <_  F
) )
180179rspcev 2918 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2  e.  RR+  /\  (
( RR  X.  {
0 } )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
2 } ) )  o R  <_  F
)  ->  E. y  e.  RR+  ( ( RR 
X.  { 0 } )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  { y } ) )  o R  <_  F )
181135, 175, 180sylancr 644 . . . . . . . . . . . . . . . . . . . 20  |-  ( F : RR --> ( 0 [,]  +oo )  ->  E. y  e.  RR+  ( ( RR 
X.  { 0 } )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  { y } ) )  o R  <_  F )
182 fveq2 5563 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( S.1 `  g
)  =  ( S.1 `  ( RR  X.  {
0 } ) ) )
183 itg10 19096 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( S.1 `  ( RR  X.  {
0 } ) )  =  0
184182, 183syl6req 2365 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g  =  ( RR  X.  { 0 } )  ->  0  =  ( S.1 `  g ) )
185184biantrud 493 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( E. y  e.  RR+  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  o R  <_  F  <->  ( E. y  e.  RR+  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR 
X.  { y } ) )  o R  <_  F  /\  0  =  ( S.1 `  g
) ) ) )
186 oveq1 5907 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  =  ( ( RR 
X.  { 0 } )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  { y } ) ) )
187186breq1d 4070 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  o R  <_  F  <->  ( ( RR  X.  {
0 } )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  o R  <_  F
) )
188187rexbidv 2598 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( E. y  e.  RR+  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  o R  <_  F  <->  E. y  e.  RR+  (
( RR  X.  {
0 } )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  o R  <_  F
) )
189185, 188bitr3d 246 . . . . . . . . . . . . . . . . . . . . 21  |-  ( g  =  ( RR  X.  { 0 } )  ->  ( ( E. y  e.  RR+  (
g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  { y } ) )  o R  <_  F  /\  0  =  ( S.1 `  g ) )  <->  E. y  e.  RR+  ( ( RR  X.  { 0 } )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  o R  <_  F
) )
190189rspcev 2918 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( RR  X.  {
0 } )  e. 
dom  S.1  /\  E. y  e.  RR+  ( ( RR 
X.  { 0 } )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  { y } ) )  o R  <_  F )  ->  E. g  e.  dom  S.1 ( E. y  e.  RR+  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  o R  <_  F  /\  0  =  ( S.1 `  g ) ) )
191134, 181, 190sylancr 644 . . . . . . . . . . . . . . . . . . 19  |-  ( F : RR --> ( 0 [,]  +oo )  ->  E. g  e.  dom  S.1 ( E. y  e.  RR+  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  o R  <_  F  /\  0  =  ( S.1 `  g ) ) )
192 id 19 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  -oo  ->  b  =  -oo )
193 mnflt 10511 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 0  e.  RR  ->  -oo  <  0 )
19428, 193mp1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  -oo  ->  -oo  <  0 )
195192, 194eqbrtrd 4080 . . . . . . . . . . . . . . . . . . 19  |-  ( b  =  -oo  ->  b  <  0 )
196 eqeq1 2322 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  0  ->  (
a  =  ( S.1 `  g )  <->  0  =  ( S.1 `  g ) ) )
197196anbi2d 684 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  0  ->  (
( E. y  e.  RR+  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR 
X.  { y } ) )  o R  <_  F  /\  a  =  ( S.1 `  g
) )  <->  ( E. y  e.  RR+  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  o R  <_  F  /\  0  =  ( S.1 `  g ) ) ) )
198197rexbidv 2598 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  0  ->  ( E. g  e.  dom  S.1 ( E. y  e.  RR+  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR 
X.  { y } ) )  o R  <_  F  /\  a  =  ( S.1 `  g
) )  <->  E. g  e.  dom  S.1 ( E. y  e.  RR+  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  o R  <_  F  /\  0  =  ( S.1 `  g ) ) ) )
199 breq2 4064 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  0  ->  (
b  <  a  <->  b  <  0 ) )
200198, 199anbi12d 691 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  0  ->  (
( E. g  e. 
dom  S.1 ( E. y  e.  RR+  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  o R  <_  F  /\  a  =  ( S.1 `  g ) )  /\  b  <  a
)  <->  ( E. g  e.  dom  S.1 ( E. y  e.  RR+  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  o R  <_  F  /\  0  =  ( S.1 `  g ) )  /\  b  <  0
) ) )
20199, 200spcev 2909 . . . . . . . . . . . . . . . . . . 19  |-  ( ( E. g  e.  dom  S.1 ( E. y  e.  RR+  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR 
X.  { y } ) )  o R  <_  F  /\  0  =  ( S.1 `  g
) )  /\  b  <  0 )  ->  E. a
( E. g  e. 
dom  S.1 ( E. y  e.  RR+  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  o R  <_  F  /\  a  =  ( S.1 `  g ) )  /\  b  <  a
) )
202191, 195, 201syl2an 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  b  =  -oo )  ->  E. a
( E. g  e. 
dom  S.1 ( E. y  e.  RR+  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  o R  <_  F  /\  a  =  ( S.1 `  g ) )  /\  b  <  a
) )
203133, 202sylan 457 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( F : RR --> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  (
f  e.  dom  S.1  /\  f  o R  <_  F ) )  /\  b  <  ( S.1 `  f
) )  /\  b  =  -oo )  ->  E. a
( E. g  e. 
dom  S.1 ( E. y  e.  RR+  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  o R  <_  F  /\  a  =  ( S.1 `  g ) )  /\  b  <  a
) )
204 simpllr 735 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  ( f  e. 
dom  S.1  /\  f  o R  <_  F )
)  /\  b  <  ( S.1 `  f ) )  ->  b  e.  RR* )
205204adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( F : RR --> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  (
f  e.  dom  S.1  /\  f  o R  <_  F ) )  /\  b  <  ( S.1 `  f
) )  /\  b  =/=  -oo )  ->  b  e.  RR* )
206 simplrl 736 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  ( f  e. 
dom  S.1  /\  f  o R  <_  F )
)  /\  b  <  ( S.1 `  f ) )  ->  f  e.  dom  S.1 )
207206, 8syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  ( f  e. 
dom  S.1  /\  f  o R  <_  F )
)  /\  b  <  ( S.1 `  f ) )  ->  ( S.1 `  f )  e.  RR )
208207adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( F : RR --> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  (
f  e.  dom  S.1  /\  f  o R  <_  F ) )  /\  b  <  ( S.1 `  f
) )  /\  b  =/=  -oo )  ->  ( S.1 `  f )  e.  RR )
209 ngtmnft 10543 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( b  e.  RR*  ->  ( b  =  -oo  <->  -.  -oo  <  b ) )
210209biimprd 214 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( b  e.  RR*  ->  ( -. 
-oo  <  b  ->  b  =  -oo ) )
211210necon1ad 2546 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  e.  RR*  ->  ( b  =/=  -oo  ->  -oo  <  b ) )
212211imp 418 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( b  e.  RR*  /\  b  =/=  -oo )  ->  -oo  <  b )
213204, 212sylan 457 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( F : RR --> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  (
f  e.  dom  S.1  /\  f  o R  <_  F ) )  /\  b  <  ( S.1 `  f
) )  /\  b  =/=  -oo )  ->  -oo  <  b )
214 simplr 731 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  ( f  e. 
dom  S.1  /\  f  o R  <_  F )
)  ->  b  e.  RR* )
2159ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  ( f  e. 
dom  S.1  /\  f  o R  <_  F )
)  ->  ( S.1 `  f )  e.  RR* )
216 xrltle 10530 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( b  e.  RR*  /\  ( S.1 `  f )  e. 
RR* )  ->  (
b  <  ( S.1 `  f )  ->  b  <_  ( S.1 `  f
) ) )
217214, 215, 216syl2anc 642 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  ( f  e. 
dom  S.1  /\  f  o R  <_  F )
)  ->  ( b  <  ( S.1 `  f
)  ->  b  <_  ( S.1 `  f ) ) )
218217imp 418 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  ( f  e. 
dom  S.1  /\  f  o R  <_  F )
)  /\  b  <  ( S.1 `  f ) )  ->  b  <_  ( S.1 `  f ) )
219218adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( F : RR --> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  (
f  e.  dom  S.1  /\  f  o R  <_  F ) )  /\  b  <  ( S.1 `  f
) )  /\  b  =/=  -oo )  ->  b  <_  ( S.1 `  f
) )
220 xrre 10545 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( b  e.  RR*  /\  ( S.1 `  f
)  e.  RR )  /\  (  -oo  <  b  /\  b  <_  ( S.1 `  f ) ) )  ->  b  e.  RR )
221205, 208, 213, 219, 220syl22anc 1183 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( F : RR --> ( 0 [,]  +oo )  /\  b  e.  RR* )  /\  (
f  e.  dom  S.1  /\  f  o R  <_  F ) )  /\  b  <  ( S.1 `  f
) )  /\  b  =/=  -oo )  ->  b  e.  RR )
222191ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  ( f  e. 
dom  S.1  /\  f  o R  <_  F )
)  /\  ( b  <  ( S.1 `  f
)  /\  b  e.  RR ) )  /\  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  ->  E. g  e.  dom  S.1 ( E. y  e.  RR+  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR 
X.  { y } ) )  o R  <_  F  /\  0  =  ( S.1 `  g
) ) )
223 simplrl 736 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  ( f  e. 
dom  S.1  /\  f  o R  <_  F )
)  /\  ( b  <  ( S.1 `  f
)  /\  b  e.  RR ) )  /\  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
b  <  ( S.1 `  f ) )
224 simplrl 736 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  ( f  e. 
dom  S.1  /\  f  o R  <_  F )
)  /\  ( b  <  ( S.1 `  f
)  /\  b  e.  RR ) )  ->  f  e.  dom  S.1 )
225 simpl 443 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( f  e.  dom  S.1  /\  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
f  e.  dom  S.1 )
226 cnvimass 5070 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( `' f " ( ran  f  \  { 0 } ) )  C_  dom  f
227 fdm 5431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( f : RR --> RR  ->  dom  f  =  RR )
22823, 227syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f  e.  dom  S.1  ->  dom  f  =  RR )
229226, 228syl5sseq 3260 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f  e.  dom  S.1  ->  ( `' f " ( ran  f  \  { 0 } ) )  C_  RR )
230229adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( f  e.  dom  S.1  /\  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
( `' f "
( ran  f  \  { 0 } ) )  C_  RR )
231 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( f  e.  dom  S.1  /\  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )
232227eqcomd 2321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( f : RR --> RR  ->  RR  =  dom  f )
233 ffun 5429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( f : RR --> RR  ->  Fun  f )
234 difpreima 5691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( Fun  f  ->  ( `' f " ( ran  f  \  { 0 } ) )  =  ( ( `' f " ran  f )  \  ( `' f " {
0 } ) ) )
235233, 234syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( f : RR --> RR  ->  ( `' f " ( ran  f  \  { 0 } ) )  =  ( ( `' f
" ran  f )  \  ( `' f
" { 0 } ) ) )
236 cnvimarndm 5071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( `' f " ran  f
)  =  dom  f
237236difeq1i 3324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( `' f " ran  f )  \  ( `' f " {
0 } ) )  =  ( dom  f  \  ( `' f
" { 0 } ) )
238235, 237syl6eq 2364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( f : RR --> RR  ->  ( `' f " ( ran  f  \  { 0 } ) )  =  ( dom  f  \ 
( `' f " { 0 } ) ) )
239232, 238difeq12d 3329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( f : RR --> RR  ->  ( RR  \  ( `' f " ( ran  f  \  { 0 } ) ) )  =  ( dom  f  \  ( dom  f  \  ( `' f
" { 0 } ) ) ) )
240 cnvimass 5070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( `' f " { 0 } )  C_  dom  f
241 dfss4 3437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( `' f " {
0 } )  C_  dom  f  <->  ( dom  f  \  ( dom  f  \  ( `' f
" { 0 } ) ) )  =  ( `' f " { 0 } ) )
242240, 241mpbi 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( dom  f  \  ( dom  f  \  ( `' f " { 0 } ) ) )  =  ( `' f
" { 0 } )
243239, 242syl6eq 2364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( f : RR --> RR  ->  ( RR  \  ( `' f " ( ran  f  \  { 0 } ) ) )  =  ( `' f
" { 0 } ) )
244243eleq2d 2383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( f : RR --> RR  ->  ( t  e.  ( RR 
\  ( `' f
" ( ran  f  \  { 0 } ) ) )  <->  t  e.  ( `' f " {
0 } ) ) )
245 fniniseg 5684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( f  Fn  RR  ->  (
t  e.  ( `' f " { 0 } )  <->  ( t  e.  RR  /\  ( f `
 t )  =  0 ) ) )
246 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( t  e.  RR  /\  ( f `  t
)  =  0 )  ->  ( f `  t )  =  0 )
247245, 246syl6bi 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( f  Fn  RR  ->  (
t  e.  ( `' f " { 0 } )  ->  (
f `  t )  =  0 ) )
24880, 247syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( f : RR --> RR  ->  ( t  e.  ( `' f " { 0 } )  ->  (
f `  t )  =  0 ) )
249244, 248sylbid 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( f : RR --> RR  ->  ( t  e.  ( RR 
\  ( `' f
" ( ran  f  \  { 0 } ) ) )  ->  (
f `  t )  =  0 ) )
25023, 249syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f  e.  dom  S.1  ->  ( t  e.  ( RR 
\  ( `' f
" ( ran  f  \  { 0 } ) ) )  ->  (
f `  t )  =  0 ) )
251250imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( f  e.  dom  S.1  /\  t  e.  ( RR 
\  ( `' f
" ( ran  f  \  { 0 } ) ) ) )  -> 
( f `  t
)  =  0 )
252251adantlr 695 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( f  e.  dom  S.1 
/\  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) )  =  0 )  /\  t  e.  ( RR  \  ( `' f " ( ran  f  \  { 0 } ) ) ) )  ->  ( f `  t )  =  0 )
253225, 230, 231, 252itg10a 19118 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( f  e.  dom  S.1  /\  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
( S.1 `  f )  =  0 )
254224, 253sylan 457 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  ( f  e. 
dom  S.1  /\  f  o R  <_  F )
)  /\  ( b  <  ( S.1 `  f
)  /\  b  e.  RR ) )  /\  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
( S.1 `  f )  =  0 )
255223, 254breqtrd 4084 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  ( f  e. 
dom  S.1  /\  f  o R  <_  F )
)  /\  ( b  <  ( S.1 `  f
)  /\  b  e.  RR ) )  /\  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) )  =  0 )  -> 
b  <  0 )
256222, 255, 201syl2anc 642 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( F : RR
--> ( 0 [,]  +oo )  /\  ( f  e. 
dom  S.1  /\  f  o R  <_  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+  ( g  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  o R  <_  F  /\  a  =  ( S.1 `  g ) )  /\  b  <  a
) )
257 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( F : RR --> ( 0 [,]  +oo )  /\  (
f  e.  dom  S.1  /\  f  o R  <_  F ) )  -> 
f  e.  dom  S.1 )
258 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( b  <  ( S.1 `  f )  /\  b  e.  RR )  ->  b  e.  RR )
259257, 258anim12i 549 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( F : RR --> ( 0 [,]  +oo )  /\  ( f  e. 
dom  S.1  /\  f  o R  <_  F )
)  /\  ( b  <  ( S.1 `  f
)  /\  b  e.  RR ) )  ->  (
f  e.  dom  S.1  /\  b  e.  RR ) )
26081ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  f  Fn  RR )
261 eqid 2316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( v  e.  RR  |->  if ( v  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) )  =  ( v  e.  RR  |->  if ( v  e.  ( `' f
" ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) )
262 ovex 5925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) )  e.  _V
263262, 99ifex 3657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  if ( v  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 )  e. 
_V
264263a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( v  e.  RR  ->  if ( v  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 )  e. 
_V )
265261, 264fmpti 5721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( v  e.  RR  |->  if ( v  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) ) : RR --> _V
266 ffn 5427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( v  e.  RR  |->  if ( v  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) ) : RR --> _V  ->  ( v  e.  RR  |->  if ( v  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) )  Fn  RR )
267265, 266mp1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( v  e.  RR  |->  if ( v  e.  ( `' f
" ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) )  Fn  RR )
26872a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  RR  e.  _V )
269 eqidd 2317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( f  e. 
dom  S.1  /\  b  e.  RR )  /\  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) )  =/=  0 )  /\  u  e.  RR )  ->  ( f `  u
)  =  ( f `
 u ) )
270 eleq1 2376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( v  =  u  ->  (
v  e.  ( `' f " ( ran  f  \  { 0 } ) )  <->  u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ) )
271270ifbid 3617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( v  =  u  ->  if ( v  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 )  =  if ( u  e.  ( `' f "
( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) )
272262, 99ifex 3657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 )  e. 
_V
273271, 261, 272fvmpt 5640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( u  e.  RR  ->  (
( v  e.  RR  |->  if ( v  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) ) `
 u )  =  if ( u  e.  ( `' f "
( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) )
274273adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( f  e. 
dom  S.1  /\  b  e.  RR )  /\  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) )  =/=  0 )  /\  u  e.  RR )  ->  ( ( v  e.  RR  |->  if ( v  e.  ( `' f
" ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) ) `  u
)  =  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( ( S.1 `  f )  -  b
)  /  ( 2  x.  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) ) ) ) ,  0 ) )
275260, 267, 268, 268, 74, 269, 274offval 6127 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( f  o F  -  (
v  e.  RR  |->  if ( v  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 ) ) ) )
276 oveq2 5908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 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 } ) ) ) ) ) ) )
277 oveq2 5908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 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 ) )
278276, 277ifsb 3608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 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 ) )
279236, 227syl5eq 2360 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( f : RR --> RR  ->  ( `' f " ran  f )  =  RR )
280279difeq1d 3327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( f : RR --> RR  ->  ( ( `' f " ran  f )  \  ( `' f " {
0 } ) )  =  ( RR  \ 
( `' f " { 0 } ) ) )
281235, 280eqtrd 2348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( f : RR --> RR  ->  ( `' f " ( ran  f  \  { 0 } ) )  =  ( RR  \  ( `' f " {
0 } ) ) )
282281eleq2d 2383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( f : RR --> RR  ->  ( u  e.  ( `' f " ( ran  f  \  { 0 } ) )  <->  u  e.  ( RR  \  ( `' f " {
0 } ) ) ) )
28323, 282syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( f  e.  dom  S.1  ->  ( u  e.  ( `' f " ( ran  f  \  { 0 } ) )  <->  u  e.  ( RR  \  ( `' f " {
0 } ) ) ) )
284283ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( 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 } ) ) ) )
285 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ( f  e. 
dom  S.1  /\  b  e.  RR )  /\  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) )  =/=  0 )  /\  u  e.  RR )  ->  u  e.  RR )
286285biantrurd 494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( 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 } ) ) ) )
287 eldif 3196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( u  e.  ( RR  \ 
( `' f " { 0 } ) )  <->  ( u  e.  RR  /\  -.  u  e.  ( `' f " { 0 } ) ) )
288286, 287syl6bbr 254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( 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 } ) ) ) )
289284, 288bitr4d 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( 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 } ) ) )
290289notbid 285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  ( `' f " { 0 } ) ) )
291 notnot 282 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( u  e.  ( `' f
" { 0 } )  <->  -.  -.  u  e.  ( `' f " { 0 } ) )
292290, 291syl6bbr 254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) )
293 fniniseg 5684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( f  Fn  RR  ->  (
u  e.  ( `' f " { 0 } )  <->  ( u  e.  RR  /\  ( f `
 u )  =  0 ) ) )
29423, 80, 2933syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( f  e.  dom  S.1  ->  ( u  e.  ( `' f " { 0 } )  <->  ( u  e.  RR  /\  ( f `
 u )  =  0 ) ) )
295294ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( 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 ) ) )
296292, 295bitrd 244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( 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 ) ) )
297 oveq1 5907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( f `  u )  =  0  ->  (
( f `  u
)  -  0 )  =  ( 0  -  0 ) )
298 0cn 8876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  0  e.  CC
299298subidi 9162 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( 0  -  0 )  =  0
300297, 299syl6eq 2364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( f `  u )  =  0  ->  (
( f `  u
)  -  0 )  =  0 )
301300adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( u  e.  RR  /\  ( f `  u
)  =  0 )  ->  ( ( f `
 u )  - 
0 )  =  0 )
302296, 301syl6bi 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( 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 ) )
303302imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
304303ifeq2da 3625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ,  ( ( 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 ) )
305278, 304syl5eq 2360 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( 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 ) )
306305mpteq2dva 4143 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )  =  ( u  e.  RR  |->  if ( u  e.  ( `' f " ( ran  f  \  { 0 } ) ) ,  ( ( f `  u )  -  (
( ( S.1 `  f
)  -  b )  /  ( 2  x.  ( vol * `  ( `' f " ( ran  f  \  { 0 } ) ) ) ) ) ) ,  0 ) ) )
307275, 306eqtrd 2348 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( f  e.  dom  S.1 
/\  b  e.  RR )  /\  ( vol * `  ( `' f "
( ran  f  \  { 0 } ) ) )  =/=  0
)  ->  ( f  o F  -  (
v  e.  RR  |->  if ( v  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 "