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

Theorem itg2cnlem2 19119
Description: Lemma for itgcn 19199. (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 10404 . . 3  |-  ( ph  ->  ( C  /  2
)  e.  RR+ )
3 itg2cn.5 . . . 4  |-  ( ph  ->  M  e.  NN )
43nnrpd 10391 . . 3  |-  ( ph  ->  M  e.  RR+ )
52, 4rpdivcld 10409 . 2  |-  ( ph  ->  ( ( C  / 
2 )  /  M
)  e.  RR+ )
6 simprl 732 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  u  e.  dom  vol )
7 itg2cn.2 . . . . . . . . . 10  |-  ( ph  ->  F  e. MblFn )
87adantr 451 . . . . . . . . 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 8840 . . . . . . . . . . . 12  |-  0  e.  RR
11 pnfxr 10457 . . . . . . . . . . . 12  |-  +oo  e.  RR*
12 icossre 10732 . . . . . . . . . . . 12  |-  ( ( 0  e.  RR  /\  +oo 
e.  RR* )  ->  (
0 [,)  +oo )  C_  RR )
1310, 11, 12mp2an 653 . . . . . . . . . . 11  |-  ( 0 [,)  +oo )  C_  RR
14 fss 5399 . . . . . . . . . . 11  |-  ( ( F : RR --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  RR )  ->  F : RR
--> RR )
159, 13, 14sylancl 643 . . . . . . . . . 10  |-  ( ph  ->  F : RR --> RR )
1615adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  F : RR --> RR )
17 mbfima 18989 . . . . . . . . 9  |-  ( ( F  e. MblFn  /\  F : RR
--> RR )  ->  ( `' F " ( M (,)  +oo ) )  e. 
dom  vol )
188, 16, 17syl2anc 642 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( `' F "
( M (,)  +oo ) )  e.  dom  vol )
19 inmbl 18901 . . . . . . . 8  |-  ( ( u  e.  dom  vol  /\  ( `' F "
( M (,)  +oo ) )  e.  dom  vol )  ->  ( u  i^i  ( `' F "
( M (,)  +oo ) ) )  e. 
dom  vol )
206, 18, 19syl2anc 642 . . . . . . 7  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( u  i^i  ( `' F " ( M (,)  +oo ) ) )  e.  dom  vol )
21 difmbl 18902 . . . . . . . 8  |-  ( ( u  e.  dom  vol  /\  ( `' F "
( M (,)  +oo ) )  e.  dom  vol )  ->  ( u  \  ( `' F "
( M (,)  +oo ) ) )  e. 
dom  vol )
226, 18, 21syl2anc 642 . . . . . . 7  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( u  \  ( `' F " ( M (,)  +oo ) ) )  e.  dom  vol )
23 inass 3381 . . . . . . . . . . 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 3528 . . . . . . . . . . . 12  |-  ( ( `' F " ( M (,)  +oo ) )  i^i  ( u  \  ( `' F " ( M (,)  +oo ) ) ) )  =  (/)
2524ineq2i 3369 . . . . . . . . . . 11  |-  ( u  i^i  ( ( `' F " ( M (,)  +oo ) )  i^i  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ) )  =  ( u  i^i  (/) )
26 in0 3482 . . . . . . . . . . 11  |-  ( u  i^i  (/) )  =  (/)
2723, 25, 263eqtri 2309 . . . . . . . . . 10  |-  ( ( u  i^i  ( `' F " ( M (,)  +oo ) ) )  i^i  ( u  \ 
( `' F "
( M (,)  +oo ) ) ) )  =  (/)
2827fveq2i 5530 . . . . . . . . 9  |-  ( vol
* `  ( (
u  i^i  ( `' F " ( M (,)  +oo ) ) )  i^i  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ) )  =  ( vol * `  (/) )
29 ovol0 18854 . . . . . . . . 9  |-  ( vol
* `  (/) )  =  0
3028, 29eqtri 2305 . . . . . . . 8  |-  ( vol
* `  ( (
u  i^i  ( `' F " ( M (,)  +oo ) ) )  i^i  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ) )  =  0
3130a1i 10 . . . . . . 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 3534 . . . . . . . . 9  |-  ( ( u  i^i  ( `' F " ( M (,)  +oo ) ) )  u.  ( u  \ 
( `' F "
( M (,)  +oo ) ) ) )  =  u
3332eqcomi 2289 . . . . . . . 8  |-  u  =  ( ( u  i^i  ( `' F "
( M (,)  +oo ) ) )  u.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) )
3433a1i 10 . . . . . . 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 18892 . . . . . . . . . 10  |-  ( u  e.  dom  vol  ->  u 
C_  RR )
366, 35syl 15 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  u  C_  RR )
3736sselda 3182 . . . . . . . 8  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  u
)  ->  x  e.  RR )
389adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  F : RR --> ( 0 [,)  +oo ) )
39 ffvelrn 5665 . . . . . . . . . . . . 13  |-  ( ( F : RR --> ( 0 [,)  +oo )  /\  x  e.  RR )  ->  ( F `  x )  e.  ( 0 [,)  +oo ) )
4038, 39sylan 457 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( F `  x )  e.  ( 0 [,)  +oo )
)
41 elrege0 10748 . . . . . . . . . . . 12  |-  ( ( F `  x )  e.  ( 0 [,) 
+oo )  <->  ( ( F `  x )  e.  RR  /\  0  <_ 
( F `  x
) ) )
4240, 41sylib 188 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( ( F `
 x )  e.  RR  /\  0  <_ 
( F `  x
) ) )
4342simpld 445 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( F `  x )  e.  RR )
4443rexrd 8883 . . . . . . . . 9  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( F `  x )  e.  RR* )
4542simprd 449 . . . . . . . . 9  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  0  <_  ( F `  x )
)
46 elxrge0 10749 . . . . . . . . 9  |-  ( ( F `  x )  e.  ( 0 [,] 
+oo )  <->  ( ( F `  x )  e.  RR*  /\  0  <_ 
( F `  x
) ) )
4744, 45, 46sylanbrc 645 . . . . . . . 8  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( F `  x )  e.  ( 0 [,]  +oo )
)
4837, 47syldan 456 . . . . . . 7  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  u
)  ->  ( F `  x )  e.  ( 0 [,]  +oo )
)
49 eqid 2285 . . . . . . 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 ) )
50 eqid 2285 . . . . . . 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 ) )
51 eqid 2285 . . . . . . 7  |-  ( x  e.  RR  |->  if ( x  e.  u ,  ( F `  x
) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  u ,  ( F `  x
) ,  0 ) )
52 0xr 8880 . . . . . . . . . . 11  |-  0  e.  RR*
53 0le0 9829 . . . . . . . . . . 11  |-  0  <_  0
54 elxrge0 10749 . . . . . . . . . . 11  |-  ( 0  e.  ( 0 [,] 
+oo )  <->  ( 0  e.  RR*  /\  0  <_  0 ) )
5552, 53, 54mpbir2an 886 . . . . . . . . . 10  |-  0  e.  ( 0 [,]  +oo )
56 ifcl 3603 . . . . . . . . . 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 ) )
5747, 55, 56sylancl 643 . . . . . . . . 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 ) )
5857, 49fmptd 5686 . . . . . . . 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 ) )
59 itg2cn.3 . . . . . . . . 9  |-  ( ph  ->  ( S.2 `  F
)  e.  RR )
6059adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  F )  e.  RR )
61 rexr 8879 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  x  e.  RR* )
6261anim1i 551 . . . . . . . . . . . 12  |-  ( ( x  e.  RR  /\  0  <_  x )  -> 
( x  e.  RR*  /\  0  <_  x )
)
63 elrege0 10748 . . . . . . . . . . . 12  |-  ( x  e.  ( 0 [,) 
+oo )  <->  ( x  e.  RR  /\  0  <_  x ) )
64 elxrge0 10749 . . . . . . . . . . . 12  |-  ( x  e.  ( 0 [,] 
+oo )  <->  ( x  e.  RR*  /\  0  <_  x ) )
6562, 63, 643imtr4i 257 . . . . . . . . . . 11  |-  ( x  e.  ( 0 [,) 
+oo )  ->  x  e.  ( 0 [,]  +oo ) )
6665ssriv 3186 . . . . . . . . . 10  |-  ( 0 [,)  +oo )  C_  (
0 [,]  +oo )
67 fss 5399 . . . . . . . . . 10  |-  ( ( F : RR --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  ( 0 [,]  +oo ) )  ->  F : RR --> ( 0 [,] 
+oo ) )
6838, 66, 67sylancl 643 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  F : RR --> ( 0 [,]  +oo ) )
6943leidd 9341 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( F `  x )  <_  ( F `  x )
)
70 breq1 4028 . . . . . . . . . . . . 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 ) ) )
71 breq1 4028 . . . . . . . . . . . . 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 ) ) )
7270, 71ifboth 3598 . . . . . . . . . . . 12  |-  ( ( ( F `  x
)  <_  ( F `  x )  /\  0  <_  ( F `  x
) )  ->  if ( x  e.  (
u  i^i  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  <_  ( F `  x ) )
7369, 45, 72syl2anc 642 . . . . . . . . . . 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 ) )
7473ralrimiva 2628 . . . . . . . . . 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 ) )
75 reex 8830 . . . . . . . . . . . 12  |-  RR  e.  _V
7675a1i 10 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  RR  e.  _V )
77 eqidd 2286 . . . . . . . . . . 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 ) ) )
7838feqmptd 5577 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  F  =  ( x  e.  RR  |->  ( F `  x ) ) )
7976, 57, 43, 77, 78ofrfval2 6098 . . . . . . . . . 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 ) ) )
8074, 79mpbird 223 . . . . . . . . 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 )
81 itg2le 19096 . . . . . . . . 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 ) )
8258, 68, 80, 81syl3anc 1182 . . . . . . . 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 ) )
83 itg2lecl 19095 . . . . . . . 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 )
8458, 60, 82, 83syl3anc 1182 . . . . . . 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 )
85 ifcl 3603 . . . . . . . . . 10  |-  ( ( ( F `  x
)  e.  ( 0 [,]  +oo )  /\  0  e.  ( 0 [,]  +oo ) )  ->  if ( x  e.  (
u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  e.  ( 0 [,] 
+oo ) )
8647, 55, 85sylancl 643 . . . . . . . . 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 ) )
8786, 50fmptd 5686 . . . . . . . 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 ) )
88 breq1 4028 . . . . . . . . . . . . 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 ) ) )
89 breq1 4028 . . . . . . . . . . . . 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 ) ) )
9088, 89ifboth 3598 . . . . . . . . . . . 12  |-  ( ( ( F `  x
)  <_  ( F `  x )  /\  0  <_  ( F `  x
) )  ->  if ( x  e.  (
u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  <_  ( F `  x ) )
9169, 45, 90syl2anc 642 . . . . . . . . . . 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 ) )
9291ralrimiva 2628 . . . . . . . . . 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 ) )
93 eqidd 2286 . . . . . . . . . . 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 ) ) )
9476, 86, 43, 93, 78ofrfval2 6098 . . . . . . . . . 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 ) ) )
9592, 94mpbird 223 . . . . . . . . 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 )
96 itg2le 19096 . . . . . . . . 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 ) )
9787, 68, 95, 96syl3anc 1182 . . . . . . . 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 ) )
98 itg2lecl 19095 . . . . . . . 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 )
9987, 60, 97, 98syl3anc 1182 . . . . . . 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 )
10020, 22, 31, 34, 48, 49, 50, 51, 84, 99itg2split 19106 . . . . . 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 ) ) ) ) )
1011adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  C  e.  RR+ )
102101rphalfcld 10404 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( C  /  2
)  e.  RR+ )
103102rpred 10392 . . . . . . 7  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( C  /  2
)  e.  RR )
104 ifcl 3603 . . . . . . . . . . 11  |-  ( ( ( F `  x
)  e.  ( 0 [,]  +oo )  /\  0  e.  ( 0 [,]  +oo ) )  ->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 )  e.  ( 0 [,] 
+oo ) )
10547, 55, 104sylancl 643 . . . . . . . . . 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 ) )
106 eqid 2285 . . . . . . . . . 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 ) )
107105, 106fmptd 5686 . . . . . . . . 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 ) )
108 breq1 4028 . . . . . . . . . . . . . 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 ) ) )
109 breq1 4028 . . . . . . . . . . . . . 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 ) ) )
110108, 109ifboth 3598 . . . . . . . . . . . . 13  |-  ( ( ( F `  x
)  <_  ( F `  x )  /\  0  <_  ( F `  x
) )  ->  if ( x  e.  ( `' F " ( M (,)  +oo ) ) ,  ( F `  x
) ,  0 )  <_  ( F `  x ) )
11169, 45, 110syl2anc 642 . . . . . . . . . . . 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
) )
112111ralrimiva 2628 . . . . . . . . . . 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 ) )
113 eqidd 2286 . . . . . . . . . . . 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 ) ) )
11476, 105, 47, 113, 78ofrfval2 6098 . . . . . . . . . . 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 ) ) )
115112, 114mpbird 223 . . . . . . . . . 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 )
116 itg2le 19096 . . . . . . . . . 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 ) )
117107, 68, 115, 116syl3anc 1182 . . . . . . . . 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 ) )
118 itg2lecl 19095 . . . . . . . . 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 )
119107, 60, 117, 118syl3anc 1182 . . . . . . . 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 )
12010a1i 10 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  0  e.  RR )
121 inss2 3392 . . . . . . . . . . . . . 14  |-  ( u  i^i  ( `' F " ( M (,)  +oo ) ) )  C_  ( `' F " ( M (,)  +oo ) )
122121sseli 3178 . . . . . . . . . . . . 13  |-  ( x  e.  ( u  i^i  ( `' F "
( M (,)  +oo ) ) )  ->  x  e.  ( `' F " ( M (,)  +oo ) ) )
123122a1i 10 . . . . . . . . . . . 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 ) ) ) )
124 ifle 10526 . . . . . . . . . . . 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 ) )
12543, 120, 45, 123, 124syl31anc 1185 . . . . . . . . . . 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 ) )
126125ralrimiva 2628 . . . . . . . . . 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 ) )
12776, 57, 105, 77, 113ofrfval2 6098 . . . . . . . . . 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 ) ) )
128126, 127mpbird 223 . . . . . . . . 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 ) ) )
129 itg2le 19096 . . . . . . . . 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 ) ) ) )
13058, 107, 128, 129syl3anc 1182 . . . . . . . 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 ) ) ) )
13178fveq2d 5531 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  F )  =  ( S.2 `  (
x  e.  RR  |->  ( F `  x ) ) ) )
132 cmmbl 18894 . . . . . . . . . . . . 13  |-  ( ( `' F " ( M (,)  +oo ) )  e. 
dom  vol  ->  ( RR  \  ( `' F "
( M (,)  +oo ) ) )  e. 
dom  vol )
13318, 132syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( RR  \  ( `' F " ( M (,)  +oo ) ) )  e.  dom  vol )
134 disjdif 3528 . . . . . . . . . . . . . . 15  |-  ( ( `' F " ( M (,)  +oo ) )  i^i  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) )  =  (/)
135134fveq2i 5530 . . . . . . . . . . . . . 14  |-  ( vol
* `  ( ( `' F " ( M (,)  +oo ) )  i^i  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ) )  =  ( vol * `  (/) )
136135, 29eqtri 2305 . . . . . . . . . . . . 13  |-  ( vol
* `  ( ( `' F " ( M (,)  +oo ) )  i^i  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ) )  =  0
137136a1i 10 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( vol * `  ( ( `' F " ( M (,)  +oo ) )  i^i  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ) )  =  0 )
138 undif2 3532 . . . . . . . . . . . . 13  |-  ( ( `' F " ( M (,)  +oo ) )  u.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) )  =  ( ( `' F " ( M (,)  +oo ) )  u.  RR )
139 mblss 18892 . . . . . . . . . . . . . . 15  |-  ( ( `' F " ( M (,)  +oo ) )  e. 
dom  vol  ->  ( `' F " ( M (,)  +oo ) )  C_  RR )
14018, 139syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( `' F "
( M (,)  +oo ) )  C_  RR )
141 ssequn1 3347 . . . . . . . . . . . . . 14  |-  ( ( `' F " ( M (,)  +oo ) )  C_  RR 
<->  ( ( `' F " ( M (,)  +oo ) )  u.  RR )  =  RR )
142140, 141sylib 188 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( `' F " ( M (,)  +oo ) )  u.  RR )  =  RR )
143138, 142syl5req 2330 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  RR  =  ( ( `' F " ( M (,)  +oo ) )  u.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ) )
144 eqid 2285 . . . . . . . . . . . 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 ) )
145 iftrue 3573 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  if ( x  e.  RR ,  ( F `  x ) ,  0 )  =  ( F `
 x ) )
146145mpteq2ia 4104 . . . . . . . . . . . . 13  |-  ( x  e.  RR  |->  if ( x  e.  RR , 
( F `  x
) ,  0 ) )  =  ( x  e.  RR  |->  ( F `
 x ) )
147146eqcomi 2289 . . . . . . . . . . . 12  |-  ( x  e.  RR  |->  ( F `
 x ) )  =  ( x  e.  RR  |->  if ( x  e.  RR ,  ( F `  x ) ,  0 ) )
148 ifcl 3603 . . . . . . . . . . . . . . 15  |-  ( ( ( F `  x
)  e.  ( 0 [,]  +oo )  /\  0  e.  ( 0 [,]  +oo ) )  ->  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  e.  ( 0 [,] 
+oo ) )
14947, 55, 148sylancl 643 . . . . . . . . . . . . . 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 ) )
150149, 144fmptd 5686 . . . . . . . . . . . . 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 ) )
151 breq1 4028 . . . . . . . . . . . . . . . . . 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 ) ) )
152 breq1 4028 . . . . . . . . . . . . . . . . . 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 ) ) )
153151, 152ifboth 3598 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  x
)  <_  ( F `  x )  /\  0  <_  ( F `  x
) )  ->  if ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x
) ,  0 )  <_  ( F `  x ) )
15469, 45, 153syl2anc 642 . . . . . . . . . . . . . . . 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 ) )
155154ralrimiva 2628 . . . . . . . . . . . . . . 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 ) )
156 eqidd 2286 . . . . . . . . . . . . . . . 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 ) ) )
15776, 149, 47, 156, 78ofrfval2 6098 . . . . . . . . . . . . . . 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 ) ) )
158155, 157mpbird 223 . . . . . . . . . . . . . 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 )
159 itg2le 19096 . . . . . . . . . . . . . 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 ) )
160150, 68, 158, 159syl3anc 1182 . . . . . . . . . . . . 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 ) )
161 itg2lecl 19095 . . . . . . . . . . . . 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 )
162150, 60, 160, 161syl3anc 1182 . . . . . . . . . . . 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 )
16318, 133, 137, 143, 47, 106, 144, 147, 119, 162itg2split 19106 . . . . . . . . . . 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 ) ) ) ) )
164131, 163eqtrd 2317 . . . . . . . . . 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 ) ) ) ) )
165 itg2cn.6 . . . . . . . . . . . . . 14  |-  ( ph  ->  -.  ( S.2 `  (
x  e.  RR  |->  if ( ( F `  x )  <_  M ,  ( F `  x ) ,  0 ) ) )  <_ 
( ( S.2 `  F
)  -  ( C  /  2 ) ) )
166165adantr 451 . . . . . . . . . . . . 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 ) ) )
167 eldif 3164 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( RR  \ 
( `' F "
( M (,)  +oo ) ) )  <->  ( x  e.  RR  /\  -.  x  e.  ( `' F "
( M (,)  +oo ) ) ) )
168167baib 871 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  RR  ->  (
x  e.  ( RR 
\  ( `' F " ( M (,)  +oo ) ) )  <->  -.  x  e.  ( `' F "
( M (,)  +oo ) ) ) )
169168adantl 452 . . . . . . . . . . . . . . . . . 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 ) ) ) )
170 ffn 5391 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F : RR --> ( 0 [,)  +oo )  ->  F  Fn  RR )
1719, 170syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  F  Fn  RR )
172171ad2antrr 706 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  F  Fn  RR )
173 elpreima 5647 . . . . . . . . . . . . . . . . . . . . 21  |-  ( F  Fn  RR  ->  (
x  e.  ( `' F " ( M (,)  +oo ) )  <->  ( x  e.  RR  /\  ( F `
 x )  e.  ( M (,)  +oo ) ) ) )
174172, 173syl 15 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
17543biantrurd 494 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( M  < 
( F `  x
)  <->  ( ( F `
 x )  e.  RR  /\  M  < 
( F `  x
) ) ) )
1763nnred 9763 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  M  e.  RR )
177176ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  M  e.  RR )
178177rexrd 8883 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  M  e.  RR* )
179 elioopnf 10739 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( M  e.  RR*  ->  ( ( F `  x )  e.  ( M (,)  +oo )  <->  ( ( F `
 x )  e.  RR  /\  M  < 
( F `  x
) ) ) )
180178, 179syl 15 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
181 simpr 447 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  x  e.  RR )
182181biantrurd 494 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
183175, 180, 1823bitr2d 272 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
184177, 43ltnled 8968 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( M  < 
( F `  x
)  <->  -.  ( F `  x )  <_  M
) )
185174, 183, 1843bitr2rd 273 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( -.  ( F `  x )  <_  M  <->  x  e.  ( `' F " ( M (,)  +oo ) ) ) )
186185con1bid 320 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( -.  x  e.  ( `' F "
( M (,)  +oo ) )  <->  ( F `  x )  <_  M
) )
187169, 186bitrd 244 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  ( x  e.  ( RR  \  ( `' F " ( M (,)  +oo ) ) )  <-> 
( F `  x
)  <_  M )
)
188187ifbid 3585 . . . . . . . . . . . . . . . 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 ) )
189188mpteq2dva 4108 . . . . . . . . . . . . . . 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 ) ) )
190189fveq2d 5531 . . . . . . . . . . . . . 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 ) ) ) )
191190breq1d 4035 . . . . . . . . . . . . 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 ) ) ) )
192166, 191mtbird 292 . . . . . . . . . . . 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 ) ) )
19360, 103resubcld 9213 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( S.2 `  F
)  -  ( C  /  2 ) )  e.  RR )
194193, 162ltnled 8968 . . . . . . . . . . . 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 ) ) ) )
195192, 194mpbird 223 . . . . . . . . . . 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 ) ) ) )
19660, 103, 162ltsubadd2d 9372 . . . . . . . . . . 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 ) ) ) ) ) )
197195, 196mpbid 201 . . . . . . . . . 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 ) ) ) ) )
198164, 197eqbrtrrd 4047 . . . . . . . . 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 ) ) ) ) )
199119, 103, 162ltadd1d 9367 . . . . . . . . 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 ) ) ) ) ) )
200198, 199mpbird 223 . . . . . . . 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 ) )
20184, 119, 103, 130, 200lelttrd 8976 . . . . . . 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 ) )
202176adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  M  e.  RR )
203 mblvol 18891 . . . . . . . . . . 11  |-  ( u  e.  dom  vol  ->  ( vol `  u )  =  ( vol * `  u ) )
2046, 203syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( vol `  u
)  =  ( vol
* `  u )
)
2055rpred 10392 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( C  / 
2 )  /  M
)  e.  RR )
206205adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( C  / 
2 )  /  M
)  e.  RR )
207 simprr 733 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( vol `  u
)  <  ( ( C  /  2 )  /  M ) )
208204, 207eqbrtrrd 4047 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( vol * `  u )  <  (
( C  /  2
)  /  M ) )
209 ovolcl 18839 . . . . . . . . . . . . . 14  |-  ( u 
C_  RR  ->  ( vol
* `  u )  e.  RR* )
21036, 209syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( vol * `  u )  e.  RR* )
211206rexrd 8883 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( C  / 
2 )  /  M
)  e.  RR* )
212 xrltle 10485 . . . . . . . . . . . . 13  |-  ( ( ( vol * `  u )  e.  RR*  /\  ( ( C  / 
2 )  /  M
)  e.  RR* )  ->  ( ( vol * `  u )  <  (
( C  /  2
)  /  M )  ->  ( vol * `  u )  <_  (
( C  /  2
)  /  M ) ) )
213210, 211, 212syl2anc 642 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( vol * `  u )  <  (
( C  /  2
)  /  M )  ->  ( vol * `  u )  <_  (
( C  /  2
)  /  M ) ) )
214208, 213mpd 14 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( vol * `  u )  <_  (
( C  /  2
)  /  M ) )
215 ovollecl 18844 . . . . . . . . . . 11  |-  ( ( u  C_  RR  /\  (
( C  /  2
)  /  M )  e.  RR  /\  ( vol * `  u )  <_  ( ( C  /  2 )  /  M ) )  -> 
( vol * `  u )  e.  RR )
21636, 206, 214, 215syl3anc 1182 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( vol * `  u )  e.  RR )
217204, 216eqeltrd 2359 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( vol `  u
)  e.  RR )
218202, 217remulcld 8865 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( M  x.  ( vol `  u ) )  e.  RR )
219202rexrd 8883 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  M  e.  RR* )
2203adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  M  e.  NN )
221220nnnn0d 10020 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  M  e.  NN0 )
222221nn0ge0d 10023 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
0  <_  M )
223 elxrge0 10749 . . . . . . . . . . . . . 14  |-  ( M  e.  ( 0 [,] 
+oo )  <->  ( M  e.  RR*  /\  0  <_  M ) )
224219, 222, 223sylanbrc 645 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  M  e.  ( 0 [,]  +oo ) )
225 ifcl 3603 . . . . . . . . . . . . 13  |-  ( ( M  e.  ( 0 [,]  +oo )  /\  0  e.  ( 0 [,]  +oo ) )  ->  if ( x  e.  u ,  M ,  0 )  e.  ( 0 [,] 
+oo ) )
226224, 55, 225sylancl 643 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  if ( x  e.  u ,  M ,  0 )  e.  ( 0 [,] 
+oo ) )
227226adantr 451 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  RR )  ->  if ( x  e.  u ,  M ,  0 )  e.  ( 0 [,]  +oo ) )
228 eqid 2285 . . . . . . . . . . 11  |-  ( x  e.  RR  |->  if ( x  e.  u ,  M ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  u ,  M ,  0 ) )
229227, 228fmptd 5686 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( x  e.  RR  |->  if ( x  e.  u ,  M ,  0 ) ) : RR --> ( 0 [,]  +oo ) )
230 eldifn 3301 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( u  \ 
( `' F "
( M (,)  +oo ) ) )  ->  -.  x  e.  ( `' F " ( M (,)  +oo ) ) )
231230adantl 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) )  ->  -.  x  e.  ( `' F "
( M (,)  +oo ) ) )
232 difss 3305 . . . . . . . . . . . . . . . . . . 19  |-  ( u 
\  ( `' F " ( M (,)  +oo ) ) )  C_  u
233232a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( u  \  ( `' F " ( M (,)  +oo ) ) ) 
C_  u )
234233sselda 3182 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) )  ->  x  e.  u )
23537, 185syldan 456 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  u
)  ->  ( -.  ( F `  x )  <_  M  <->  x  e.  ( `' F " ( M (,)  +oo ) ) ) )
236234, 235syldan 456 . . . . . . . . . . . . . . . 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 ) ) ) )
237236con1bid 320 . . . . . . . . . . . . . . 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
) )
238231, 237mpbid 201 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) )  ->  ( F `  x )  <_  M
)
239 iftrue 3573 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( u  \ 
( `' F "
( M (,)  +oo ) ) )  ->  if ( x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 )  =  ( F `
 x ) )
240239adantl 452 . . . . . . . . . . . . . 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 ) )
241 iftrue 3573 . . . . . . . . . . . . . . 15  |-  ( x  e.  u  ->  if ( x  e.  u ,  M ,  0 )  =  M )
242234, 241syl 15 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) )  ->  if (
x  e.  u ,  M ,  0 )  =  M )
243238, 240, 2423brtr4d 4055 . . . . . . . . . . . . 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 ) )
244 iffalse 3574 . . . . . . . . . . . . . . 15  |-  ( -.  x  e.  ( u 
\  ( `' F " ( M (,)  +oo ) ) )  ->  if ( x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) ,  ( F `  x ) ,  0 )  =  0 )
245244adantl 452 . . . . . . . . . . . . . 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 )
246 breq2 4029 . . . . . . . . . . . . . . . . 17  |-  ( M  =  if ( x  e.  u ,  M ,  0 )  -> 
( 0  <_  M  <->  0  <_  if ( x  e.  u ,  M ,  0 ) ) )
247 breq2 4029 . . . . . . . . . . . . . . . . 17  |-  ( 0  =  if ( x  e.  u ,  M ,  0 )  -> 
( 0  <_  0  <->  0  <_  if ( x  e.  u ,  M ,  0 ) ) )
248246, 247ifboth 3598 . . . . . . . . . . . . . . . 16  |-  ( ( 0  <_  M  /\  0  <_  0 )  -> 
0  <_  if (
x  e.  u ,  M ,  0 ) )
249222, 53, 248sylancl 643 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
0  <_  if (
x  e.  u ,  M ,  0 ) )
250249adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
u  e.  dom  vol  /\  ( vol `  u
)  <  ( ( C  /  2 )  /  M ) ) )  /\  -.  x  e.  ( u  \  ( `' F " ( M (,)  +oo ) ) ) )  ->  0  <_  if ( x  e.  u ,  M ,  0 ) )
251245, 250eqbrtrd 4045 . . . . . . . . . . . . 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 ) )
252243, 251pm2.61dan 766 . . . . . . . . . . . 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 ) )
253252ralrimivw 2629 . . . . . . . . . . 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 ) )
254 eqidd 2286 . . . . . . . . . . . 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 ) ) )
25576, 86, 227, 93, 254ofrfval2 6098 . . . . . . . . . . 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 ) ) )
256253, 255mpbird 223 . . . . . . . . . 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 ) ) )
257 itg2le 19096 . . . . . . . . . 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 ) ) ) )
25887, 229, 256, 257syl3anc 1182 . . . . . . . . 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 ) ) ) )
259 elrege0 10748 . . . . . . . . . . 11  |-  ( M  e.  ( 0 [,) 
+oo )  <->  ( M  e.  RR  /\  0  <_  M ) )
260202, 222, 259sylanbrc 645 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  M  e.  ( 0 [,)  +oo ) )
261 itg2const 19097 . . . . . . . . . 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 ) ) )
2626, 217, 260, 261syl3anc 1182 . . . . . . . . 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 ) ) )
263258, 262breqtrd 4049 . . . . . . . 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 ) ) )
264220nngt0d 9791 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
0  <  M )
265 ltmuldiv2 9629 . . . . . . . . . 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 ) ) )
266217, 103, 202, 264, 265syl112anc 1186 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( M  x.  ( vol `  u ) )  <  ( C  /  2 )  <->  ( vol `  u )  <  (
( C  /  2
)  /  M ) ) )
267207, 266mpbird 223 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( M  x.  ( vol `  u ) )  <  ( C  / 
2 ) )
26899, 218, 103, 263, 267lelttrd 8976 . . . . . . 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 ) )
26984, 99, 103, 103, 201, 268lt2addd 9396 . . . . . 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
) ) )
270100, 269eqbrtrd 4045 . . . . 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 ) ) )
271101rpcnd 10394 . . . . . 6  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  ->  C  e.  CC )
2722712halvesd 9959 . . . . 5  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( ( C  / 
2 )  +  ( C  /  2 ) )  =  C )
273270, 272breqtrd 4049 . . . 4  |-  ( (
ph  /\  ( u  e.  dom  vol  /\  ( vol `  u )  < 
( ( C  / 
2 )  /  M
) ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  u ,  ( F `  x
) ,  0 ) ) )  <  C
)
274273expr 598 . . 3  |-  ( (
ph  /\  u  e.  dom  vol )  ->  (
( vol `  u
)  <  ( ( C  /  2 )  /  M )  ->  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  u ,  ( F `  x ) ,  0 ) ) )  <  C ) )
275274ralrimiva 2628 . 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 ) )
276 breq2 4029 . . . . 5  |-  ( d  =  ( ( C  /  2 )  /  M )  ->  (
( vol `  u
)  <  d  <->  ( vol `  u )  <  (
( C  /  2
)  /  M ) ) )
277276imbi1d 308 . . . 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 ) ) )
278277ralbidv 2565 . . 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 ) ) )
279278rspcev 2886 . 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 ) )
2805, 275, 279syl2anc 642 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 176    /\ wa 358    = wceq 1625    e. wcel 1686   A.wral 2545   E.wrex 2546   _Vcvv 2790    \ cdif 3151    u. cun 3152    i^i cin 3153    C_ wss 3154   (/)c0 3457   ifcif 3567   class class class wbr 4025    e. cmpt 4079   `'ccnv 4690   dom cdm 4691   "cima 4694    Fn wfn 5252   -->wf 5253   ` cfv 5257  (class class class)co 5860    o Rcofr 6079