MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  itg2cnlem2 Structured version   Unicode version

Theorem itg2cnlem2 19655
Description: Lemma for itgcn 19735. (Contributed by Mario Carneiro, 31-Aug-2014.)
Hypotheses
Ref Expression
itg2cn.1  |-  ( ph  ->  F : RR --> ( 0 [,)  +oo ) )
itg2cn.2  |-  ( ph  ->  F  e. MblFn )
itg2cn.3  |-  ( ph  ->  ( S.2 `  F
)  e.  RR )
itg2cn.4  |-  ( ph  ->  C  e.  RR+ )
itg2cn.5  |-  ( ph  ->  M  e.  NN )
itg2cn.6  |-  ( ph  ->  -.  ( S.2 `  (
x  e.  RR  |->  if ( ( F `  x )  <_  M ,  ( F `  x ) ,  0 ) ) )  <_ 
( ( S.2 `  F
)  -  ( C  /  2 ) ) )
Assertion
Ref Expression
itg2cnlem2  |-  ( ph  ->  E. d  e.  RR+  A. u  e.  dom  vol ( ( vol `  u
)  <  d  ->  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  u ,  ( F `  x
) ,  0 ) ) )  <  C
) )
Distinct variable groups:    u, d, x, C    F, d, u, x    ph, u, x    M, d, u, x
Allowed substitution hint:    ph( d)

Proof of Theorem itg2cnlem2
StepHypRef Expression
1 itg2cn.4 . . . 4  |-  ( ph  ->  C  e.  RR+ )
21rphalfcld 10661 . . 3  |-  ( ph  ->  ( C  /  2
)  e.  RR+ )
3 itg2cn.5 . . . 4  |-  ( ph  ->  M  e.  NN )
43nnrpd 10648 . . 3  |-  ( ph  ->  M  e.  RR+ )
52, 4rpdivcld 10666 . 2  |-  ( ph  ->  ( ( C  / 
2 )  /  M
)  e.  RR+ )
6 simprl 734 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  u  e.  dom  vol )
7 itg2cn.2 . . . . . . . . . 10  |-  ( ph  ->  F  e. MblFn )
87adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  F  e. MblFn )
9 itg2cn.1 . . . . . . . . . . 11  |-  ( ph  ->  F : RR --> ( 0 [,)  +oo ) )
10 0re 9092 . . . . . . . . . . . 12  |-  0  e.  RR
11 pnfxr 10714 . . . . . . . . . . . 12  |-  +oo  e.  RR*
12 icossre 10992 . . . . . . . . . . . 12  |-  ( ( 0  e.  RR  /\  +oo 
e.  RR* )  ->  (
0 [,)  +oo )  C_  RR )
1310, 11, 12mp2an 655 . . . . . . . . . . 11  |-  ( 0 [,)  +oo )  C_  RR
14 fss 5600 . . . . . . . . . . 11  |-  ( ( F : RR --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  RR )  ->  F : RR
--> RR )
159, 13, 14sylancl 645 . . . . . . . . . 10  |-  ( ph  ->  F : RR --> RR )
1615adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  F : RR --> RR )
17 mbfima 19525 . . . . . . . . 9  |-  ( ( F  e. MblFn  /\  F : RR
--> RR )  ->  ( `' F " ( M (,)  +oo ) )  e. 
dom  vol )
188, 16, 17syl2anc 644 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( `' F "
( M (,)  +oo ) )  e.  dom  vol )
19 inmbl 19437 . . . . . . . 8  |-  ( ( u  e.  dom  vol  /\  ( `' F "
( M (,)  +oo ) )  e.  dom  vol )  ->  ( u  i^i  ( `' F "
( M (,)  +oo ) ) )  e. 
dom  vol )
206, 18, 19syl2anc 644 . . . . . . 7  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( u  i^i  ( `' F " ( M (,)  +oo ) ) )  e.  dom  vol )
21 difmbl 19438 . . . . . . . 8  |-  ( ( u  e.  dom  vol  /\  ( `' F "
( M (,)  +oo ) )  e.  dom  vol )  ->  ( u  \  ( `' F "
( M (,)  +oo ) ) )  e. 
dom  vol )
226, 18, 21syl2anc 644 . . . . . . 7  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( u  \  ( `' F " ( M (,)  +oo ) ) )  e.  dom  vol )
23 inass 3552 . . . . . . . . . . 11  |-  ( ( u  i^i  ( `' F " ( M (,)  +oo ) ) )  i^i  ( u  \ 
( `' F "
( M (,)  +oo ) ) ) )  =  ( u  i^i  ( ( `' F " ( M (,)  +oo ) )  i^i  (
u  \  ( `' F " ( M (,)  +oo ) ) ) ) )
24 disjdif 3701 . . . . . . . . . . . 12  |-  ( ( `' F " ( M (,)  +oo ) )  i^i  ( u  \  ( `' F " ( M (,)  +oo ) ) ) )  =  (/)
2524ineq2i 3540 . . . . . . . . . . 11  |-  ( u  i^i  ( ( `' F " ( M (,)  +oo ) )  i^i  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ) )  =  ( u  i^i  (/) )
26 in0 3654 . . . . . . . . . . 11  |-  ( u  i^i  (/) )  =  (/)
2723, 25, 263eqtri 2461 . . . . . . . . . 10  |-  ( ( u  i^i  ( `' F " ( M (,)  +oo ) ) )  i^i  ( u  \ 
( `' F "
( M (,)  +oo ) ) ) )  =  (/)
2827fveq2i 5732 . . . . . . . . 9  |-  ( vol
* `  ( (
u  i^i  ( `' F " ( M (,)  +oo ) ) )  i^i  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ) )  =  ( vol * `  (/) )
29 ovol0 19390 . . . . . . . . 9  |-  ( vol
* `  (/) )  =  0
3028, 29eqtri 2457 . . . . . . . 8  |-  ( vol
* `  ( (
u  i^i  ( `' F " ( M (,)  +oo ) ) )  i^i  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ) )  =  0
3130a1i 11 . . . . . . 7  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( vol * `  ( ( u  i^i  ( `' F "
( M (,)  +oo ) ) )  i^i  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ) )  =  0 )
32 inundif 3707 . . . . . . . . 9  |-  ( ( u  i^i  ( `' F " ( M (,)  +oo ) ) )  u.  ( u  \ 
( `' F "
( M (,)  +oo ) ) ) )  =  u
3332eqcomi 2441 . . . . . . . 8  |-  u  =  ( ( u  i^i  ( `' F "
( M (,)  +oo ) ) )  u.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) )
3433a1i 11 . . . . . . 7  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  u  =  ( (
u  i^i  ( `' F " ( M (,)  +oo ) ) )  u.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ) )
35 mblss 19428 . . . . . . . . . 10  |-  ( u  e.  dom  vol  ->  u 
C_  RR )
366, 35syl 16 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  u  C_  RR )
3736sselda 3349 . . . . . . . 8  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  u
)  ->  x  e.  RR )
389adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  F : RR --> ( 0 [,)  +oo ) )
3938ffvelrnda 5871 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( F `  x )  e.  ( 0 [,)  +oo )
)
40 elrege0 11008 . . . . . . . . . . . 12  |-  ( ( F `  x )  e.  ( 0 [,) 
+oo )  <->  ( ( F `  x )  e.  RR  /\  0  <_ 
( F `  x
) ) )
4139, 40sylib 190 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( ( F `
 x )  e.  RR  /\  0  <_ 
( F `  x
) ) )
4241simpld 447 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( F `  x )  e.  RR )
4342rexrd 9135 . . . . . . . . 9  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( F `  x )  e.  RR* )
4441simprd 451 . . . . . . . . 9  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  0  <_  ( F `  x )
)
45 elxrge0 11009 . . . . . . . . 9  |-  ( ( F `  x )  e.  ( 0 [,] 
+oo )  <->  ( ( F `  x )  e.  RR*  /\  0  <_ 
( F `  x
) ) )
4643, 44, 45sylanbrc 647 . . . . . . . 8  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( F `  x )  e.  ( 0 [,]  +oo )
)
4737, 46syldan 458 . . . . . . 7  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  u
)  ->  ( F `  x )  e.  ( 0 [,]  +oo )
)
48 eqid 2437 . . . . . . 7  |-  ( x  e.  RR  |->  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) )
49 eqid 2437 . . . . . . 7  |-  ( x  e.  RR  |->  if ( x  e.  ( u 
\  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  ( u 
\  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) )
50 eqid 2437 . . . . . . 7  |-  ( x  e.  RR  |->  if ( x  e.  u ,  ( F `  x
) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  u ,  ( F `  x
) ,  0 ) )
51 0xr 9132 . . . . . . . . . . 11  |-  0  e.  RR*
52 0le0 10082 . . . . . . . . . . 11  |-  0  <_  0
53 elxrge0 11009 . . . . . . . . . . 11  |-  ( 0  e.  ( 0 [,] 
+oo )  <->  ( 0  e.  RR*  /\  0  <_  0 ) )
5451, 52, 53mpbir2an 888 . . . . . . . . . 10  |-  0  e.  ( 0 [,]  +oo )
55 ifcl 3776 . . . . . . . . . 10  |-  ( ( ( F `  x
)  e.  ( 0 [,]  +oo )  /\  0  e.  ( 0 [,]  +oo ) )  ->  if ( x  e.  (
u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  e.  ( 0 [,] 
+oo ) )
5646, 54, 55sylancl 645 . . . . . . . . 9  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  if ( x  e.  ( u  i^i  ( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  e.  ( 0 [,] 
+oo ) )
5756, 48fmptd 5894 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( x  e.  RR  |->  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) : RR --> ( 0 [,]  +oo ) )
58 itg2cn.3 . . . . . . . . 9  |-  ( ph  ->  ( S.2 `  F
)  e.  RR )
5958adantr 453 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  F )  e.  RR )
60 rexr 9131 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  x  e.  RR* )
6160anim1i 553 . . . . . . . . . . . 12  |-  ( ( x  e.  RR  /\  0  <_  x )  -> 
( x  e.  RR*  /\  0  <_  x )
)
62 elrege0 11008 . . . . . . . . . . . 12  |-  ( x  e.  ( 0 [,) 
+oo )  <->  ( x  e.  RR  /\  0  <_  x ) )
63 elxrge0 11009 . . . . . . . . . . . 12  |-  ( x  e.  ( 0 [,] 
+oo )  <->  ( x  e.  RR*  /\  0  <_  x ) )
6461, 62, 633imtr4i 259 . . . . . . . . . . 11  |-  ( x  e.  ( 0 [,) 
+oo )  ->  x  e.  ( 0 [,]  +oo ) )
6564ssriv 3353 . . . . . . . . . 10  |-  ( 0 [,)  +oo )  C_  (
0 [,]  +oo )
66 fss 5600 . . . . . . . . . 10  |-  ( ( F : RR --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  ( 0 [,]  +oo ) )  ->  F : RR --> ( 0 [,] 
+oo ) )
6738, 65, 66sylancl 645 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  F : RR --> ( 0 [,]  +oo ) )
6842leidd 9594 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( F `  x )  <_  ( F `  x )
)
69 breq1 4216 . . . . . . . . . . . . 13  |-  ( ( F `  x )  =  if ( x  e.  ( u  i^i  ( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  ->  ( ( F `
 x )  <_ 
( F `  x
)  <->  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 )  <_  ( F `  x ) ) )
70 breq1 4216 . . . . . . . . . . . . 13  |-  ( 0  =  if ( x  e.  ( u  i^i  ( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  ->  ( 0  <_ 
( F `  x
)  <->  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 )  <_  ( F `  x ) ) )
7169, 70ifboth 3771 . . . . . . . . . . . 12  |-  ( ( ( F `  x
)  <_  ( F `  x )  /\  0  <_  ( F `  x
) )  ->  if ( x  e.  (
u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  <_  ( F `  x ) )
7268, 44, 71syl2anc 644 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  if ( x  e.  ( u  i^i  ( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  <_  ( F `  x ) )
7372ralrimiva 2790 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  A. x  e.  RR  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 )  <_  ( F `  x ) )
74 reex 9082 . . . . . . . . . . . 12  |-  RR  e.  _V
7574a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  RR  e.  _V )
76 eqidd 2438 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( x  e.  RR  |->  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) )
7738feqmptd 5780 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  F  =  ( x  e.  RR  |->  ( F `  x ) ) )
7875, 56, 42, 76, 77ofrfval2 6324 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( x  e.  RR  |->  if ( x  e.  ( u  i^i  ( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) )  o R  <_  F 
<-> 
A. x  e.  RR  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 )  <_  ( F `  x ) ) )
7973, 78mpbird 225 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( x  e.  RR  |->  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) )  o R  <_  F )
80 itg2le 19632 . . . . . . . . 9  |-  ( ( ( x  e.  RR  |->  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) : RR --> ( 0 [,]  +oo )  /\  F : RR --> ( 0 [,]  +oo )  /\  ( x  e.  RR  |->  if ( x  e.  ( u  i^i  ( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) )  o R  <_  F )  ->  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( u  i^i  ( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) ) )  <_  ( S.2 `  F ) )
8157, 67, 79, 80syl3anc 1185 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) ) )  <_  ( S.2 `  F ) )
82 itg2lecl 19631 . . . . . . . 8  |-  ( ( ( x  e.  RR  |->  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) : RR --> ( 0 [,]  +oo )  /\  ( S.2 `  F
)  e.  RR  /\  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) ) )  <_  ( S.2 `  F ) )  ->  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) )  e.  RR )
8357, 59, 81, 82syl3anc 1185 . . . . . . 7  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) ) )  e.  RR )
84 ifcl 3776 . . . . . . . . . 10  |-  ( ( ( F `  x
)  e.  ( 0 [,]  +oo )  /\  0  e.  ( 0 [,]  +oo ) )  ->  if ( x  e.  (
u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  e.  ( 0 [,] 
+oo ) )
8546, 54, 84sylancl 645 . . . . . . . . 9  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  if ( x  e.  ( u  \ 
( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  e.  ( 0 [,] 
+oo ) )
8685, 49fmptd 5894 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( x  e.  RR  |->  if ( x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) : RR --> ( 0 [,]  +oo ) )
87 breq1 4216 . . . . . . . . . . . . 13  |-  ( ( F `  x )  =  if ( x  e.  ( u  \ 
( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  ->  ( ( F `
 x )  <_ 
( F `  x
)  <->  if ( x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 )  <_  ( F `  x ) ) )
88 breq1 4216 . . . . . . . . . . . . 13  |-  ( 0  =  if ( x  e.  ( u  \ 
( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  ->  ( 0  <_ 
( F `  x
)  <->  if ( x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 )  <_  ( F `  x ) ) )
8987, 88ifboth 3771 . . . . . . . . . . . 12  |-  ( ( ( F `  x
)  <_  ( F `  x )  /\  0  <_  ( F `  x
) )  ->  if ( x  e.  (
u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  <_  ( F `  x ) )
9068, 44, 89syl2anc 644 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  if ( x  e.  ( u  \ 
( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  <_  ( F `  x ) )
9190ralrimiva 2790 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  A. x  e.  RR  if ( x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 )  <_  ( F `  x ) )
92 eqidd 2438 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( x  e.  RR  |->  if ( x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) )
9375, 85, 42, 92, 77ofrfval2 6324 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( x  e.  RR  |->  if ( x  e.  ( u  \ 
( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) )  o R  <_  F 
<-> 
A. x  e.  RR  if ( x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 )  <_  ( F `  x ) ) )
9491, 93mpbird 225 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( x  e.  RR  |->  if ( x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) )  o R  <_  F )
95 itg2le 19632 . . . . . . . . 9  |-  ( ( ( x  e.  RR  |->  if ( x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) : RR --> ( 0 [,]  +oo )  /\  F : RR --> ( 0 [,]  +oo )  /\  ( x  e.  RR  |->  if ( x  e.  ( u  \ 
( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) )  o R  <_  F )  ->  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( u  \ 
( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) ) )  <_  ( S.2 `  F ) )
9686, 67, 94, 95syl3anc 1185 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( u 
\  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) ) )  <_  ( S.2 `  F ) )
97 itg2lecl 19631 . . . . . . . 8  |-  ( ( ( x  e.  RR  |->  if ( x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) : RR --> ( 0 [,]  +oo )  /\  ( S.2 `  F
)  e.  RR  /\  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( u 
\  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) ) )  <_  ( S.2 `  F ) )  ->  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) )  e.  RR )
9886, 59, 96, 97syl3anc 1185 . . . . . . 7  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( u 
\  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) ) )  e.  RR )
9920, 22, 31, 34, 47, 48, 49, 50, 83, 98itg2split 19642 . . . . . 6  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  u ,  ( F `  x
) ,  0 ) ) )  =  ( ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) )  +  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) ) ) )
1001adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  C  e.  RR+ )
101100rphalfcld 10661 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( C  /  2
)  e.  RR+ )
102101rpred 10649 . . . . . . 7  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( C  /  2
)  e.  RR )
103 ifcl 3776 . . . . . . . . . . 11  |-  ( ( ( F `  x
)  e.  ( 0 [,]  +oo )  /\  0  e.  ( 0 [,]  +oo ) )  ->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 )  e.  ( 0 [,] 
+oo ) )
10446, 54, 103sylancl 645 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x ) ,  0 )  e.  ( 0 [,]  +oo ) )
105 eqid 2437 . . . . . . . . . 10  |-  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 ) )
106104, 105fmptd 5894 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 ) ) : RR --> ( 0 [,]  +oo ) )
107 breq1 4216 . . . . . . . . . . . . . 14  |-  ( ( F `  x )  =  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x ) ,  0 )  -> 
( ( F `  x )  <_  ( F `  x )  <->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 )  <_  ( F `  x ) ) )
108 breq1 4216 . . . . . . . . . . . . . 14  |-  ( 0  =  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x ) ,  0 )  -> 
( 0  <_  ( F `  x )  <->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 )  <_  ( F `  x ) ) )
109107, 108ifboth 3771 . . . . . . . . . . . . 13  |-  ( ( ( F `  x
)  <_  ( F `  x )  /\  0  <_  ( F `  x
) )  ->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 )  <_  ( F `  x ) )
11068, 44, 109syl2anc 644 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x ) ,  0 )  <_ 
( F `  x
) )
111110ralrimiva 2790 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  A. x  e.  RR  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 )  <_  ( F `  x ) )
112 eqidd 2438 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 ) ) )
11375, 104, 46, 112, 77ofrfval2 6324 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x ) ,  0 ) )  o R  <_  F  <->  A. x  e.  RR  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 )  <_  ( F `  x ) ) )
114111, 113mpbird 225 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 ) )  o R  <_  F )
115 itg2le 19632 . . . . . . . . . 10  |-  ( ( ( x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 ) ) : RR --> ( 0 [,]  +oo )  /\  F : RR --> ( 0 [,] 
+oo )  /\  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 ) )  o R  <_  F )  ->  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x ) ,  0 ) ) )  <_  ( S.2 `  F ) )
116106, 67, 114, 115syl3anc 1185 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 ) ) )  <_  ( S.2 `  F ) )
117 itg2lecl 19631 . . . . . . . . 9  |-  ( ( ( x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 ) ) : RR --> ( 0 [,]  +oo )  /\  ( S.2 `  F )  e.  RR  /\  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 ) ) )  <_  ( S.2 `  F ) )  ->  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 ) ) )  e.  RR )
118106, 59, 116, 117syl3anc 1185 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 ) ) )  e.  RR )
11910a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  0  e.  RR )
120 inss2 3563 . . . . . . . . . . . . . 14  |-  ( u  i^i  ( `' F " ( M (,)  +oo ) ) )  C_  ( `' F " ( M (,)  +oo ) )
121120sseli 3345 . . . . . . . . . . . . 13  |-  ( x  e.  ( u  i^i  ( `' F "
( M (,)  +oo ) ) )  ->  x  e.  ( `' F " ( M (,)  +oo ) ) )
122121a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) )  ->  x  e.  ( `' F " ( M (,)  +oo ) ) ) )
123 ifle 10784 . . . . . . . . . . . 12  |-  ( ( ( ( F `  x )  e.  RR  /\  0  e.  RR  /\  0  <_  ( F `  x ) )  /\  ( x  e.  (
u  i^i  ( `' F " ( M (,)  +oo ) ) )  ->  x  e.  ( `' F " ( M (,)  +oo ) ) ) )  ->  if ( x  e.  ( u  i^i  ( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  <_  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x ) ,  0 ) )
12442, 119, 44, 122, 123syl31anc 1188 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  if ( x  e.  ( u  i^i  ( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  <_  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x ) ,  0 ) )
125124ralrimiva 2790 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  A. x  e.  RR  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 )  <_  if (
x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 ) )
12675, 56, 104, 76, 112ofrfval2 6324 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( x  e.  RR  |->  if ( x  e.  ( u  i^i  ( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) )  o R  <_ 
( x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 ) )  <->  A. x  e.  RR  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 )  <_  if (
x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 ) ) )
127125, 126mpbird 225 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( x  e.  RR  |->  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) )  o R  <_  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x ) ,  0 ) ) )
128 itg2le 19632 . . . . . . . . 9  |-  ( ( ( x  e.  RR  |->  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) : RR --> ( 0 [,]  +oo )  /\  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x ) ,  0 ) ) : RR --> ( 0 [,]  +oo )  /\  (
x  e.  RR  |->  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) )  o R  <_  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x ) ,  0 ) ) )  ->  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) )  <_ 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 ) ) ) )
12957, 106, 127, 128syl3anc 1185 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) ) )  <_  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x ) ,  0 ) ) ) )
13077fveq2d 5733 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  F )  =  ( S.2 `  (
x  e.  RR  |->  ( F `  x ) ) ) )
131 cmmbl 19430 . . . . . . . . . . . . 13  |-  ( ( `' F " ( M (,)  +oo ) )  e. 
dom  vol  ->  ( RR  \  ( `' F "
( M (,)  +oo ) ) )  e. 
dom  vol )
13218, 131syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( RR  \  ( `' F " ( M (,)  +oo ) ) )  e.  dom  vol )
133 disjdif 3701 . . . . . . . . . . . . . . 15  |-  ( ( `' F " ( M (,)  +oo ) )  i^i  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) )  =  (/)
134133fveq2i 5732 . . . . . . . . . . . . . 14  |-  ( vol
* `  ( ( `' F " ( M (,)  +oo ) )  i^i  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ) )  =  ( vol * `  (/) )
135134, 29eqtri 2457 . . . . . . . . . . . . 13  |-  ( vol
* `  ( ( `' F " ( M (,)  +oo ) )  i^i  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ) )  =  0
136135a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( vol * `  ( ( `' F " ( M (,)  +oo ) )  i^i  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ) )  =  0 )
137 undif2 3705 . . . . . . . . . . . . 13  |-  ( ( `' F " ( M (,)  +oo ) )  u.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) )  =  ( ( `' F " ( M (,)  +oo ) )  u.  RR )
138 mblss 19428 . . . . . . . . . . . . . . 15  |-  ( ( `' F " ( M (,)  +oo ) )  e. 
dom  vol  ->  ( `' F " ( M (,)  +oo ) )  C_  RR )
13918, 138syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( `' F "
( M (,)  +oo ) )  C_  RR )
140 ssequn1 3518 . . . . . . . . . . . . . 14  |-  ( ( `' F " ( M (,)  +oo ) )  C_  RR 
<->  ( ( `' F " ( M (,)  +oo ) )  u.  RR )  =  RR )
141139, 140sylib 190 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( `' F " ( M (,)  +oo ) )  u.  RR )  =  RR )
142137, 141syl5req 2482 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  RR  =  ( ( `' F " ( M (,)  +oo ) )  u.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ) )
143 eqid 2437 . . . . . . . . . . . 12  |-  ( x  e.  RR  |->  if ( x  e.  ( RR 
\  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  ( RR 
\  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) )
144 iftrue 3746 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  if ( x  e.  RR ,  ( F `  x ) ,  0 )  =  ( F `
 x ) )
145144mpteq2ia 4292 . . . . . . . . . . . . 13  |-  ( x  e.  RR  |->  if ( x  e.  RR , 
( F `  x
) ,  0 ) )  =  ( x  e.  RR  |->  ( F `
 x ) )
146145eqcomi 2441 . . . . . . . . . . . 12  |-  ( x  e.  RR  |->  ( F `
 x ) )  =  ( x  e.  RR  |->  if ( x  e.  RR ,  ( F `  x ) ,  0 ) )
147 ifcl 3776 . . . . . . . . . . . . . . 15  |-  ( ( ( F `  x
)  e.  ( 0 [,]  +oo )  /\  0  e.  ( 0 [,]  +oo ) )  ->  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  e.  ( 0 [,] 
+oo ) )
14846, 54, 147sylancl 645 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  if ( x  e.  ( RR  \ 
( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  e.  ( 0 [,] 
+oo ) )
149148, 143fmptd 5894 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( x  e.  RR  |->  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) : RR --> ( 0 [,]  +oo ) )
150 breq1 4216 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  x )  =  if ( x  e.  ( RR  \ 
( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  ->  ( ( F `
 x )  <_ 
( F `  x
)  <->  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 )  <_  ( F `  x ) ) )
151 breq1 4216 . . . . . . . . . . . . . . . . . 18  |-  ( 0  =  if ( x  e.  ( RR  \ 
( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  ->  ( 0  <_ 
( F `  x
)  <->  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 )  <_  ( F `  x ) ) )
152150, 151ifboth 3771 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  x
)  <_  ( F `  x )  /\  0  <_  ( F `  x
) )  ->  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  <_  ( F `  x ) )
15368, 44, 152syl2anc 644 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  if ( x  e.  ( RR  \ 
( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  <_  ( F `  x ) )
154153ralrimiva 2790 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  A. x  e.  RR  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 )  <_  ( F `  x ) )
155 eqidd 2438 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( x  e.  RR  |->  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) )
15675, 148, 46, 155, 77ofrfval2 6324 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( x  e.  RR  |->  if ( x  e.  ( RR  \ 
( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) )  o R  <_  F 
<-> 
A. x  e.  RR  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 )  <_  ( F `  x ) ) )
157154, 156mpbird 225 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( x  e.  RR  |->  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) )  o R  <_  F )
158 itg2le 19632 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  RR  |->  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) : RR --> ( 0 [,]  +oo )  /\  F : RR --> ( 0 [,]  +oo )  /\  ( x  e.  RR  |->  if ( x  e.  ( RR  \ 
( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) )  o R  <_  F )  ->  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( RR  \ 
( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) ) )  <_  ( S.2 `  F ) )
159149, 67, 157, 158syl3anc 1185 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( RR 
\  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) ) )  <_  ( S.2 `  F ) )
160 itg2lecl 19631 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  RR  |->  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) : RR --> ( 0 [,]  +oo )  /\  ( S.2 `  F
)  e.  RR  /\  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( RR 
\  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) ) )  <_  ( S.2 `  F ) )  ->  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) )  e.  RR )
161149, 59, 159, 160syl3anc 1185 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( RR 
\  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) ) )  e.  RR )
16218, 132, 136, 142, 46, 105, 143, 146, 118, 161itg2split 19642 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  ( x  e.  RR  |->  ( F `
 x ) ) )  =  ( ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 ) ) )  +  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( RR 
\  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) ) ) ) )
163130, 162eqtrd 2469 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  F )  =  ( ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 ) ) )  +  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( RR 
\  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) ) ) ) )
164 itg2cn.6 . . . . . . . . . . . . . 14  |-  ( ph  ->  -.  ( S.2 `  (
x  e.  RR  |->  if ( ( F `  x )  <_  M ,  ( F `  x ) ,  0 ) ) )  <_ 
( ( S.2 `  F
)  -  ( C  /  2 ) ) )
165164adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  -.  ( S.2 `  (
x  e.  RR  |->  if ( ( F `  x )  <_  M ,  ( F `  x ) ,  0 ) ) )  <_ 
( ( S.2 `  F
)  -  ( C  /  2 ) ) )
166 eldif 3331 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( RR  \ 
( `' F "
( M (,)  +oo ) ) )  <->  ( x  e.  RR  /\  -.  x  e.  ( `' F "
( M (,)  +oo ) ) ) )
167166baib 873 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  RR  ->  (
x  e.  ( RR 
\  ( `' F " ( M (,)  +oo ) ) )  <->  -.  x  e.  ( `' F "
( M (,)  +oo ) ) ) )
168167adantl 454 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) )  <->  -.  x  e.  ( `' F " ( M (,)  +oo ) ) ) )
169 ffn 5592 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F : RR --> ( 0 [,)  +oo )  ->  F  Fn  RR )
1709, 169syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  F  Fn  RR )
171170ad2antrr 708 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  F  Fn  RR )
172 elpreima 5851 . . . . . . . . . . . . . . . . . . . . 21  |-  ( F  Fn  RR  ->  (
x  e.  ( `' F " ( M (,)  +oo ) )  <->  ( x  e.  RR  /\  ( F `
 x )  e.  ( M (,)  +oo ) ) ) )
173171, 172syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( x  e.  ( `' F "
( M (,)  +oo ) )  <->  ( x  e.  RR  /\  ( F `
 x )  e.  ( M (,)  +oo ) ) ) )
17442biantrurd 496 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( M  < 
( F `  x
)  <->  ( ( F `
 x )  e.  RR  /\  M  < 
( F `  x
) ) ) )
1753nnred 10016 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  M  e.  RR )
176175ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  M  e.  RR )
177176rexrd 9135 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  M  e.  RR* )
178 elioopnf 10999 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( M  e.  RR*  ->  ( ( F `  x )  e.  ( M (,)  +oo )  <->  ( ( F `
 x )  e.  RR  /\  M  < 
( F `  x
) ) ) )
179177, 178syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( ( F `
 x )  e.  ( M (,)  +oo ) 
<->  ( ( F `  x )  e.  RR  /\  M  <  ( F `
 x ) ) ) )
180 simpr 449 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  x  e.  RR )
181180biantrurd 496 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( ( F `
 x )  e.  ( M (,)  +oo ) 
<->  ( x  e.  RR  /\  ( F `  x
)  e.  ( M (,)  +oo ) ) ) )
182174, 179, 1813bitr2d 274 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( M  < 
( F `  x
)  <->  ( x  e.  RR  /\  ( F `
 x )  e.  ( M (,)  +oo ) ) ) )
183176, 42ltnled 9221 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( M  < 
( F `  x
)  <->  -.  ( F `  x )  <_  M
) )
184173, 182, 1833bitr2rd 275 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( -.  ( F `  x )  <_  M  <->  x  e.  ( `' F " ( M (,)  +oo ) ) ) )
185184con1bid 322 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( -.  x  e.  ( `' F "
( M (,)  +oo ) )  <->  ( F `  x )  <_  M
) )
186168, 185bitrd 246 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) )  <-> 
( F `  x
)  <_  M )
)
187186ifbid 3758 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  if ( x  e.  ( RR  \ 
( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  =  if ( ( F `  x )  <_  M ,  ( F `  x ) ,  0 ) )
188187mpteq2dva 4296 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( x  e.  RR  |->  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) )  =  ( x  e.  RR  |->  if ( ( F `  x )  <_  M ,  ( F `  x ) ,  0 ) ) )
189188fveq2d 5733 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( RR 
\  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) ) )  =  ( S.2 `  ( x  e.  RR  |->  if ( ( F `  x
)  <_  M , 
( F `  x
) ,  0 ) ) ) )
190189breq1d 4223 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) )  <_ 
( ( S.2 `  F
)  -  ( C  /  2 ) )  <-> 
( S.2 `  ( x  e.  RR  |->  if ( ( F `  x
)  <_  M , 
( F `  x
) ,  0 ) ) )  <_  (
( S.2 `  F )  -  ( C  / 
2 ) ) ) )
191165, 190mtbird 294 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  -.  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) )  <_ 
( ( S.2 `  F
)  -  ( C  /  2 ) ) )
19259, 102resubcld 9466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( S.2 `  F
)  -  ( C  /  2 ) )  e.  RR )
193192, 161ltnled 9221 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( ( S.2 `  F )  -  ( C  /  2 ) )  <  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) )  <->  -.  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( RR  \ 
( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) ) )  <_  (
( S.2 `  F )  -  ( C  / 
2 ) ) ) )
194191, 193mpbird 225 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( S.2 `  F
)  -  ( C  /  2 ) )  <  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) ) )
19559, 102, 161ltsubadd2d 9625 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( ( S.2 `  F )  -  ( C  /  2 ) )  <  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) )  <->  ( S.2 `  F )  <  (
( C  /  2
)  +  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) ) ) ) )
196194, 195mpbid 203 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  F )  <  ( ( C  /  2 )  +  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) ) ) )
197163, 196eqbrtrrd 4235 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 ) ) )  +  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( RR 
\  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) ) ) )  < 
( ( C  / 
2 )  +  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( RR 
\  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) ) ) ) )
198118, 102, 161ltadd1d 9620 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 ) ) )  <  ( C  /  2 )  <->  ( ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x ) ,  0 ) ) )  +  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) ) )  <  ( ( C  /  2 )  +  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) ) ) ) )
199197, 198mpbird 225 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 ) ) )  <  ( C  /  2 ) )
20083, 118, 102, 129, 199lelttrd 9229 . . . . . . 7  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) ) )  <  ( C  /  2 ) )
201175adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  M  e.  RR )
202 mblvol 19427 . . . . . . . . . . 11  |-  ( u  e.  dom  vol  ->  ( vol `  u )  =  ( vol * `  u ) )
2036, 202syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( vol `  u
)  =  ( vol
* `  u )
)
2045rpred 10649 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( C  / 
2 )  /  M
)  e.  RR )
205204adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( C  / 
2 )  /  M
)  e.  RR )
206 simprr 735 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( vol `  u
)  <  ( ( C  /  2 )  /  M ) )
207203, 206eqbrtrrd 4235 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( vol * `  u )  <  (
( C  /  2
)  /  M ) )
208 ovolcl 19375 . . . . . . . . . . . . . 14  |-  ( u 
C_  RR  ->  ( vol
* `  u )  e.  RR* )
20936, 208syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( vol * `  u )  e.  RR* )
210205rexrd 9135 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( C  / 
2 )  /  M
)  e.  RR* )
211 xrltle 10743 . . . . . . . . . . . . 13  |-  ( ( ( vol * `  u )  e.  RR*  /\  ( ( C  / 
2 )  /  M
)  e.  RR* )  ->  ( ( vol * `  u )  <  (
( C  /  2
)  /  M )  ->  ( vol * `  u )  <_  (
( C  /  2
)  /  M ) ) )
212209, 210, 211syl2anc 644 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( vol * `  u )  <  (
( C  /  2
)  /  M )  ->  ( vol * `  u )  <_  (
( C  /  2
)  /  M ) ) )
213207, 212mpd 15 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( vol * `  u )  <_  (
( C  /  2
)  /  M ) )
214 ovollecl 19380 . . . . . . . . . . 11  |-  ( ( u  C_  RR  /\  (
( C  /  2
)  /  M )  e.  RR  /\  ( vol * `  u )  <_  ( ( C  /  2 )  /  M ) )  -> 
( vol * `  u )  e.  RR )
21536, 205, 213, 214syl3anc 1185 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( vol * `  u )  e.  RR )
216203, 215eqeltrd 2511 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( vol `  u
)  e.  RR )
217201, 216remulcld 9117 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( M  x.  ( vol `  u ) )  e.  RR )
218201rexrd 9135 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  M  e.  RR* )
2193adantr 453 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  M  e.  NN )
220219nnnn0d 10275 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  M  e.  NN0 )
221220nn0ge0d 10278 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
0  <_  M )
222 elxrge0 11009 . . . . . . . . . . . . . 14  |-  ( M  e.  ( 0 [,] 
+oo )  <->  ( M  e.  RR*  /\  0  <_  M ) )
223218, 221, 222sylanbrc 647 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  M  e.  ( 0 [,]  +oo ) )
224 ifcl 3776 . . . . . . . . . . . . 13  |-  ( ( M  e.  ( 0 [,]  +oo )  /\  0  e.  ( 0 [,]  +oo ) )  ->  if ( x  e.  u ,  M ,  0 )  e.  ( 0 [,] 
+oo ) )
225223, 54, 224sylancl 645 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  if ( x  e.  u ,  M ,  0 )  e.  ( 0 [,] 
+oo ) )
226225adantr 453 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  if ( x  e.  u ,  M ,  0 )  e.  ( 0 [,]  +oo ) )
227 eqid 2437 . . . . . . . . . . 11  |-  ( x  e.  RR  |->  if ( x  e.  u ,  M ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  u ,  M ,  0 ) )
228226, 227fmptd 5894 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( x  e.  RR  |->  if ( x  e.  u ,  M ,  0 ) ) : RR --> ( 0 [,]  +oo ) )
229 eldifn 3471 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( u  \ 
( `' F "
( M (,)  +oo ) ) )  ->  -.  x  e.  ( `' F " ( M (,)  +oo ) ) )
230229adantl 454 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) )  ->  -.  x  e.  ( `' F "
( M (,)  +oo ) ) )
231 difssd 3476 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( u  \  ( `' F " ( M (,)  +oo ) ) ) 
C_  u )
232231sselda 3349 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) )  ->  x  e.  u )
23337, 184syldan 458 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  u
)  ->  ( -.  ( F `  x )  <_  M  <->  x  e.  ( `' F " ( M (,)  +oo ) ) ) )
234232, 233syldan 458 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) )  ->  ( -.  ( F `  x )  <_  M  <->  x  e.  ( `' F " ( M (,)  +oo ) ) ) )
235234con1bid 322 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) )  ->  ( -.  x  e.  ( `' F " ( M (,)  +oo ) )  <->  ( F `  x )  <_  M
) )
236230, 235mpbid 203 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) )  ->  ( F `  x )  <_  M
)
237 iftrue 3746 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( u  \ 
( `' F "
( M (,)  +oo ) ) )  ->  if ( x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 )  =  ( F `
 x ) )
238237adantl 454 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) )  ->  if (
x  e.  ( u 
\  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  =  ( F `  x ) )
239 iftrue 3746 . . . . . . . . . . . . . . 15  |-  ( x  e.  u  ->  if ( x  e.  u ,  M ,  0 )  =  M )
240232, 239syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) )  ->  if (
x  e.  u ,  M ,  0 )  =  M )
241236, 238, 2403brtr4d 4243 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) )  ->  if (
x  e.  ( u 
\  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  <_  if ( x  e.  u ,  M ,  0 ) )
242 iffalse 3747 . . . . . . . . . . . . . . 15  |-  ( -.  x  e.  ( u 
\  ( `' F " ( M (,)  +oo ) ) )  ->  if ( x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 )  =  0 )
243242adantl 454 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  -.  x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) )  ->  if (
x  e.  ( u 
\  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  =  0 )
244 breq2 4217 . . . . . . . . . . . . . . . . 17  |-  ( M  =  if ( x  e.  u ,  M ,  0 )  -> 
( 0  <_  M  <->  0  <_  if ( x  e.  u ,  M ,  0 ) ) )
245 breq2 4217 . . . . . . . . . . . . . . . . 17  |-  ( 0  =  if ( x  e.  u ,  M ,  0 )  -> 
( 0  <_  0  <->  0  <_  if ( x  e.  u ,  M ,  0 ) ) )
246244, 245ifboth 3771 . . . . . . . . . . . . . . . 16  |-  ( ( 0  <_  M  /\  0  <_  0 )  -> 
0  <_  if (
x  e.  u ,  M ,  0 ) )
247221, 52, 246sylancl 645 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
0  <_  if (
x  e.  u ,  M ,  0 ) )
248247adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  -.  x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) )  ->  0  <_  if ( x  e.  u ,  M ,  0 ) )
249243, 248eqbrtrd 4233 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  -.  x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) )  ->  if (
x  e.  ( u 
\  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  <_  if ( x  e.  u ,  M ,  0 ) )
250241, 249pm2.61dan 768 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  if ( x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 )  <_  if (
x  e.  u ,  M ,  0 ) )
251250ralrimivw 2791 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  A. x  e.  RR  if ( x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 )  <_  if (
x  e.  u ,  M ,  0 ) )
252 eqidd 2438 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( x  e.  RR  |->  if ( x  e.  u ,  M ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  u ,  M ,  0 ) ) )
25375, 85, 226, 92, 252ofrfval2 6324 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( x  e.  RR  |->  if ( x  e.  ( u  \ 
( `' F "
( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) )  o R  <_ 
( x  e.  RR  |->  if ( x  e.  u ,  M ,  0 ) )  <->  A. x  e.  RR  if ( x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 )  <_  if (
x  e.  u ,  M ,  0 ) ) )
254251, 253mpbird 225 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( x  e.  RR  |->  if ( x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) )  o R  <_  ( x  e.  RR  |->  if ( x  e.  u ,  M ,  0 ) ) )
255 itg2le 19632 . . . . . . . . . 10  |-  ( ( ( x  e.  RR  |->  if ( x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) : RR --> ( 0 [,]  +oo )  /\  ( x  e.  RR  |->  if ( x  e.  u ,  M ,  0 ) ) : RR --> ( 0 [,]  +oo )  /\  (
x  e.  RR  |->  if ( x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) )  o R  <_  ( x  e.  RR  |->  if ( x  e.  u ,  M ,  0 ) ) )  ->  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) )  <_ 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  u ,  M ,  0 ) ) ) )
25686, 228, 254, 255syl3anc 1185 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( u 
\  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) ) )  <_  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  u ,  M ,  0 ) ) ) )
257 elrege0 11008 . . . . . . . . . . 11  |-  ( M  e.  ( 0 [,) 
+oo )  <->  ( M  e.  RR  /\  0  <_  M ) )
258201, 221, 257sylanbrc 647 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  M  e.  ( 0 [,)  +oo ) )
259 itg2const 19633 . . . . . . . . . 10  |-  ( ( u  e.  dom  vol  /\  ( vol `  u
)  e.  RR  /\  M  e.  ( 0 [,)  +oo ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  u ,  M ,  0 ) ) )  =  ( M  x.  ( vol `  u ) ) )
2606, 216, 258, 259syl3anc 1185 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  u ,  M ,  0 ) ) )  =  ( M  x.  ( vol `  u ) ) )
261256, 260breqtrd 4237 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( u 
\  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) ) )  <_  ( M  x.  ( vol `  u ) ) )
262219nngt0d 10044 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
0  <  M )
263 ltmuldiv2 9882 . . . . . . . . . 10  |-  ( ( ( vol `  u
)  e.  RR  /\  ( C  /  2
)  e.  RR  /\  ( M  e.  RR  /\  0  <  M ) )  ->  ( ( M  x.  ( vol `  u ) )  < 
( C  /  2
)  <->  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )
264216, 102, 201, 262, 263syl112anc 1189 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( M  x.  ( vol `  u ) )  <  ( C  /  2 )  <->  ( vol `  u )  <  (
( C  /  2
)  /  M ) ) )
265206, 264mpbird 225 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( M  x.  ( vol `  u ) )  <  ( C  / 
2 ) )
26698, 217, 102, 261, 265lelttrd 9229 . . . . . . 7  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  ( u 
\  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 ) ) )  <  ( C  /  2 ) )
26783, 98, 102, 102, 200, 266lt2addd 9649 . . . . . 6  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) )  +  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 ) ) ) )  <  ( ( C  /  2 )  +  ( C  /  2
) ) )
26899, 267eqbrtrd 4233 . . . . 5  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  u ,  ( F `  x
) ,  0 ) ) )  <  (
( C  /  2
)  +  ( C  /  2 ) ) )
269100rpcnd 10651 . . . . . 6  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  C  e.  CC )
2702692halvesd 10214 . . . . 5  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( C  / 
2 )  +  ( C  /  2 ) )  =  C )
271268, 270breqtrd 4237 . . . 4  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  u ,  ( F `  x
) ,  0 ) ) )  <  C
)
272271expr 600 . . 3  |-  ( (
ph  /\  u  e.  dom  vol )  ->  (
( vol `  u
)  <  ( ( C  /  2 )  /  M )  ->  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  u ,  ( F `  x ) ,  0 ) ) )  <  C ) )
273272ralrimiva 2790 . 2  |-  ( ph  ->  A. u  e.  dom  vol ( ( vol `  u
)  <  ( ( C  /  2 )  /  M )  ->  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  u ,  ( F `  x ) ,  0 ) ) )  <  C ) )
274 breq2 4217 . . . . 5  |-  ( d  =  ( ( C  /  2 )  /  M )  ->  (
( vol `  u
)  <  d  <->  ( vol `  u )  <  (
( C  /  2
)  /  M ) ) )
275274imbi1d 310 . . . 4  |-  ( d  =  ( ( C  /  2 )  /  M )  ->  (
( ( vol `  u
)  <  d  ->  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  u ,  ( F `  x
) ,  0 ) ) )  <  C
)  <->  ( ( vol `  u )  <  (
( C  /  2
)  /  M )  ->  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  u ,  ( F `  x ) ,  0 ) ) )  < 
C ) ) )
276275ralbidv 2726 . . 3  |-  ( d  =  ( ( C  /  2 )  /  M )  ->  ( A. u  e.  dom  vol ( ( vol `  u
)  <  d  ->  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  u ,  ( F `  x
) ,  0 ) ) )  <  C
)  <->  A. u  e.  dom  vol ( ( vol `  u
)  <  ( ( C  /  2 )  /  M )  ->  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  u ,  ( F `  x ) ,  0 ) ) )  <  C ) ) )
277276rspcev 3053 . 2  |-  ( ( ( ( C  / 
2 )  /  M
)  e.  RR+  /\  A. u  e.  dom  vol (
( vol `  u
)  <  ( ( C  /  2 )  /  M )  ->  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  u ,  ( F `  x ) ,  0 ) ) )  <  C ) )  ->  E. d  e.  RR+  A. u  e. 
dom  vol ( ( vol `  u )  <  d  ->  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  u ,  ( F `  x ) ,  0 ) ) )  < 
C ) )
2785, 273, 277syl2anc 644 1  |-  ( ph  ->  E. d  e.  RR+  A. u  e.  dom  vol ( ( vol `  u
)  <  d  ->  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  u ,  ( F `  x
) ,  0 ) ) )  <  C
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653    e. wcel 1726   A.wral 2706   E.wrex 2707   _Vcvv 2957    \ cdif 3318    u. cun 3319    i^i cin 3320    C_ wss 3321   (/)c0 3629   ifcif 3740   class class class wbr 4213    e. cmpt 4267   `'ccnv 4878   dom cdm 4879   "cima 4882    Fn wfn 5450   -->wf 5451   ` cfv 5455  (class class class)co 6082    o Rcofr 6305   RRcr 8990   0cc0 8991    + caddc 8994    x. cmul 8996    +oocpnf 9118   RR*cxr 9120    < clt 9121    <_ cle 9122    - cmin 9292    / cdiv 9678   NNcn 10001   2c2 10050   RR+crp 10613   (,)cioo 10917   [,)cico 10919   [,]cicc 10920   vol *covol 19360   volcvol 19361  MblFncmbf 19507   S.2citg2 19509
This theorem is referenced by:  itg2cn  19656
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-rep 4321  ax-sep 4331  ax-nul 4339  ax-pow 4378  ax-pr 4404  ax-un 4702  ax-inf2 7597  ax-cnex 9047  ax-resscn 9048  ax-1cn 9049  ax-icn 9050  ax-addcl 9051  ax-addrcl 9052  ax-mulcl 9053  ax-mulrcl 9054  ax-mulcom 9055  ax-addass 9056  ax-mulass 9057  ax-distr 9058  ax-i2m1 9059  ax-1ne0 9060