This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itg2cnlem2

Description: Lemma for itgcn . (Contributed by Mario Carneiro, 31-Aug-2014)

Ref Expression
Hypotheses 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 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 ) )

Proof

Step Hyp Ref Expression
1 itg2cn.1 
 |-  ( ph -> F : RR --> ( 0 [,) +oo ) )
2 itg2cn.2 
 |-  ( ph -> F e. MblFn )
3 itg2cn.3 
 |-  ( ph -> ( S.2 ` F ) e. RR )
4 itg2cn.4 
 |-  ( ph -> C e. RR+ )
5 itg2cn.5 
 |-  ( ph -> M e. NN )
6 itg2cn.6 
 |-  ( ph -> -. ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ M , ( F ` x ) , 0 ) ) ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) )
7 4 rphalfcld 
 |-  ( ph -> ( C / 2 ) e. RR+ )
8 5 nnrpd 
 |-  ( ph -> M e. RR+ )
9 7 8 rpdivcld 
 |-  ( ph -> ( ( C / 2 ) / M ) e. RR+ )
10 simprl 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> u e. dom vol )
11 2 adantr 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> F e. MblFn )
12 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
13 fss 
 |-  ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> F : RR --> RR )
14 1 12 13 sylancl 
 |-  ( ph -> F : RR --> RR )
15 14 adantr 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> F : RR --> RR )
16 mbfima 
 |-  ( ( F e. MblFn /\ F : RR --> RR ) -> ( `' F " ( M (,) +oo ) ) e. dom vol )
17 11 15 16 syl2anc 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( `' F " ( M (,) +oo ) ) e. dom vol )
18 inmbl 
 |-  ( ( u e. dom vol /\ ( `' F " ( M (,) +oo ) ) e. dom vol ) -> ( u i^i ( `' F " ( M (,) +oo ) ) ) e. dom vol )
19 10 17 18 syl2anc 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( u i^i ( `' F " ( M (,) +oo ) ) ) e. dom vol )
20 difmbl 
 |-  ( ( u e. dom vol /\ ( `' F " ( M (,) +oo ) ) e. dom vol ) -> ( u \ ( `' F " ( M (,) +oo ) ) ) e. dom vol )
21 10 17 20 syl2anc 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( u \ ( `' F " ( M (,) +oo ) ) ) e. dom vol )
22 inass 
 |-  ( ( u i^i ( `' F " ( M (,) +oo ) ) ) i^i ( u \ ( `' F " ( M (,) +oo ) ) ) ) = ( u i^i ( ( `' F " ( M (,) +oo ) ) i^i ( u \ ( `' F " ( M (,) +oo ) ) ) ) )
23 disjdif 
 |-  ( ( `' F " ( M (,) +oo ) ) i^i ( u \ ( `' F " ( M (,) +oo ) ) ) ) = (/)
24 23 ineq2i 
 |-  ( u i^i ( ( `' F " ( M (,) +oo ) ) i^i ( u \ ( `' F " ( M (,) +oo ) ) ) ) ) = ( u i^i (/) )
25 in0 
 |-  ( u i^i (/) ) = (/)
26 22 24 25 3eqtri 
 |-  ( ( u i^i ( `' F " ( M (,) +oo ) ) ) i^i ( u \ ( `' F " ( M (,) +oo ) ) ) ) = (/)
27 26 fveq2i 
 |-  ( vol* ` ( ( u i^i ( `' F " ( M (,) +oo ) ) ) i^i ( u \ ( `' F " ( M (,) +oo ) ) ) ) ) = ( vol* ` (/) )
28 ovol0 
 |-  ( vol* ` (/) ) = 0
29 27 28 eqtri 
 |-  ( vol* ` ( ( u i^i ( `' F " ( M (,) +oo ) ) ) i^i ( u \ ( `' F " ( M (,) +oo ) ) ) ) ) = 0
30 29 a1i 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( vol* ` ( ( u i^i ( `' F " ( M (,) +oo ) ) ) i^i ( u \ ( `' F " ( M (,) +oo ) ) ) ) ) = 0 )
31 inundif 
 |-  ( ( u i^i ( `' F " ( M (,) +oo ) ) ) u. ( u \ ( `' F " ( M (,) +oo ) ) ) ) = u
32 31 eqcomi 
 |-  u = ( ( u i^i ( `' F " ( M (,) +oo ) ) ) u. ( u \ ( `' F " ( M (,) +oo ) ) ) )
33 32 a1i 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> u = ( ( u i^i ( `' F " ( M (,) +oo ) ) ) u. ( u \ ( `' F " ( M (,) +oo ) ) ) ) )
34 mblss 
 |-  ( u e. dom vol -> u C_ RR )
35 10 34 syl 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> u C_ RR )
36 35 sselda 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. u ) -> x e. RR )
37 1 adantr 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> F : RR --> ( 0 [,) +oo ) )
38 37 ffvelcdmda 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. RR ) -> ( F ` x ) e. ( 0 [,) +oo ) )
39 elrege0 
 |-  ( ( F ` x ) e. ( 0 [,) +oo ) <-> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
40 38 39 sylib 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. RR ) -> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
41 40 simpld 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. RR ) -> ( F ` x ) e. RR )
42 41 rexrd 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. RR ) -> ( F ` x ) e. RR* )
43 40 simprd 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. RR ) -> 0 <_ ( F ` x ) )
44 elxrge0 
 |-  ( ( F ` x ) e. ( 0 [,] +oo ) <-> ( ( F ` x ) e. RR* /\ 0 <_ ( F ` x ) ) )
45 42 43 44 sylanbrc 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. RR ) -> ( F ` x ) e. ( 0 [,] +oo ) )
46 36 45 syldan 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. u ) -> ( F ` x ) e. ( 0 [,] +oo ) )
47 eqid 
 |-  ( 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 ) )
48 eqid 
 |-  ( 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 ) )
49 eqid 
 |-  ( x e. RR |-> if ( x e. u , ( F ` x ) , 0 ) ) = ( x e. RR |-> if ( x e. u , ( F ` x ) , 0 ) )
50 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
51 ifcl 
 |-  ( ( ( F ` x ) e. ( 0 [,] +oo ) /\ 0 e. ( 0 [,] +oo ) ) -> if ( x e. ( u i^i ( `' F " ( M (,) +oo ) ) ) , ( F ` x ) , 0 ) e. ( 0 [,] +oo ) )
52 45 50 51 sylancl 
 |-  ( ( ( 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 ) )
53 52 fmpttd 
 |-  ( ( 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 ) )
54 3 adantr 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( S.2 ` F ) e. RR )
55 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
56 fss 
 |-  ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> F : RR --> ( 0 [,] +oo ) )
57 37 55 56 sylancl 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> F : RR --> ( 0 [,] +oo ) )
58 41 leidd 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. RR ) -> ( F ` x ) <_ ( F ` x ) )
59 breq1 
 |-  ( ( 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 ) ) )
60 breq1 
 |-  ( 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 ) ) )
61 59 60 ifboth 
 |-  ( ( ( F ` x ) <_ ( F ` x ) /\ 0 <_ ( F ` x ) ) -> if ( x e. ( u i^i ( `' F " ( M (,) +oo ) ) ) , ( F ` x ) , 0 ) <_ ( F ` x ) )
62 58 43 61 syl2anc 
 |-  ( ( ( 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 ) )
63 62 ralrimiva 
 |-  ( ( 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 ) )
64 reex 
 |-  RR e. _V
65 64 a1i 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> RR e. _V )
66 eqidd 
 |-  ( ( 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 ) ) )
67 37 feqmptd 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> F = ( x e. RR |-> ( F ` x ) ) )
68 65 52 41 66 67 ofrfval2 
 |-  ( ( 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 ) ) oR <_ F <-> A. x e. RR if ( x e. ( u i^i ( `' F " ( M (,) +oo ) ) ) , ( F ` x ) , 0 ) <_ ( F ` x ) ) )
69 63 68 mpbird 
 |-  ( ( 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 ) ) oR <_ F )
70 itg2le 
 |-  ( ( ( 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 ) ) oR <_ F ) -> ( S.2 ` ( x e. RR |-> if ( x e. ( u i^i ( `' F " ( M (,) +oo ) ) ) , ( F ` x ) , 0 ) ) ) <_ ( S.2 ` F ) )
71 53 57 69 70 syl3anc 
 |-  ( ( 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 ) )
72 itg2lecl 
 |-  ( ( ( 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 )
73 53 54 71 72 syl3anc 
 |-  ( ( 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 )
74 ifcl 
 |-  ( ( ( F ` x ) e. ( 0 [,] +oo ) /\ 0 e. ( 0 [,] +oo ) ) -> if ( x e. ( u \ ( `' F " ( M (,) +oo ) ) ) , ( F ` x ) , 0 ) e. ( 0 [,] +oo ) )
75 45 50 74 sylancl 
 |-  ( ( ( 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 ) )
76 75 fmpttd 
 |-  ( ( 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 ) )
77 breq1 
 |-  ( ( 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 ) ) )
78 breq1 
 |-  ( 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 ) ) )
79 77 78 ifboth 
 |-  ( ( ( F ` x ) <_ ( F ` x ) /\ 0 <_ ( F ` x ) ) -> if ( x e. ( u \ ( `' F " ( M (,) +oo ) ) ) , ( F ` x ) , 0 ) <_ ( F ` x ) )
80 58 43 79 syl2anc 
 |-  ( ( ( 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 ) )
81 80 ralrimiva 
 |-  ( ( 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 ) )
82 eqidd 
 |-  ( ( 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 ) ) )
83 65 75 41 82 67 ofrfval2 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( ( x e. RR |-> if ( x e. ( u \ ( `' F " ( M (,) +oo ) ) ) , ( F ` x ) , 0 ) ) oR <_ F <-> A. x e. RR if ( x e. ( u \ ( `' F " ( M (,) +oo ) ) ) , ( F ` x ) , 0 ) <_ ( F ` x ) ) )
84 81 83 mpbird 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( x e. RR |-> if ( x e. ( u \ ( `' F " ( M (,) +oo ) ) ) , ( F ` x ) , 0 ) ) oR <_ F )
85 itg2le 
 |-  ( ( ( 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 ) ) oR <_ F ) -> ( S.2 ` ( x e. RR |-> if ( x e. ( u \ ( `' F " ( M (,) +oo ) ) ) , ( F ` x ) , 0 ) ) ) <_ ( S.2 ` F ) )
86 76 57 84 85 syl3anc 
 |-  ( ( 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 ) )
87 itg2lecl 
 |-  ( ( ( 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 )
88 76 54 86 87 syl3anc 
 |-  ( ( 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 )
89 19 21 30 33 46 47 48 49 73 88 itg2split 
 |-  ( ( 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 ) ) ) ) )
90 4 adantr 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> C e. RR+ )
91 90 rphalfcld 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( C / 2 ) e. RR+ )
92 91 rpred 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( C / 2 ) e. RR )
93 ifcl 
 |-  ( ( ( F ` x ) e. ( 0 [,] +oo ) /\ 0 e. ( 0 [,] +oo ) ) -> if ( x e. ( `' F " ( M (,) +oo ) ) , ( F ` x ) , 0 ) e. ( 0 [,] +oo ) )
94 45 50 93 sylancl 
 |-  ( ( ( 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 ) )
95 94 fmpttd 
 |-  ( ( 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 ) )
96 breq1 
 |-  ( ( 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 ) ) )
97 breq1 
 |-  ( 0 = if ( x e. ( `' F " ( M (,) +oo ) ) , ( F ` x ) , 0 ) -> ( 0 <_ ( F ` x ) <-> if ( x e. ( `' F " ( M (,) +oo ) ) , ( F ` x ) , 0 ) <_ ( F ` x ) ) )
98 96 97 ifboth 
 |-  ( ( ( F ` x ) <_ ( F ` x ) /\ 0 <_ ( F ` x ) ) -> if ( x e. ( `' F " ( M (,) +oo ) ) , ( F ` x ) , 0 ) <_ ( F ` x ) )
99 58 43 98 syl2anc 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. RR ) -> if ( x e. ( `' F " ( M (,) +oo ) ) , ( F ` x ) , 0 ) <_ ( F ` x ) )
100 99 ralrimiva 
 |-  ( ( 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 ) )
101 eqidd 
 |-  ( ( 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 ) ) )
102 65 94 45 101 67 ofrfval2 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( ( x e. RR |-> if ( x e. ( `' F " ( M (,) +oo ) ) , ( F ` x ) , 0 ) ) oR <_ F <-> A. x e. RR if ( x e. ( `' F " ( M (,) +oo ) ) , ( F ` x ) , 0 ) <_ ( F ` x ) ) )
103 100 102 mpbird 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( x e. RR |-> if ( x e. ( `' F " ( M (,) +oo ) ) , ( F ` x ) , 0 ) ) oR <_ F )
104 itg2le 
 |-  ( ( ( 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 ) ) oR <_ F ) -> ( S.2 ` ( x e. RR |-> if ( x e. ( `' F " ( M (,) +oo ) ) , ( F ` x ) , 0 ) ) ) <_ ( S.2 ` F ) )
105 95 57 103 104 syl3anc 
 |-  ( ( 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 ) )
106 itg2lecl 
 |-  ( ( ( 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 )
107 95 54 105 106 syl3anc 
 |-  ( ( 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 )
108 0red 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. RR ) -> 0 e. RR )
109 elinel2 
 |-  ( x e. ( u i^i ( `' F " ( M (,) +oo ) ) ) -> x e. ( `' F " ( M (,) +oo ) ) )
110 109 a1i 
 |-  ( ( ( 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 ) ) ) )
111 ifle 
 |-  ( ( ( ( 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 ) )
112 41 108 43 110 111 syl31anc 
 |-  ( ( ( 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 ) )
113 112 ralrimiva 
 |-  ( ( 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 ) )
114 65 52 94 66 101 ofrfval2 
 |-  ( ( 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 ) ) oR <_ ( 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 ) ) )
115 113 114 mpbird 
 |-  ( ( 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 ) ) oR <_ ( x e. RR |-> if ( x e. ( `' F " ( M (,) +oo ) ) , ( F ` x ) , 0 ) ) )
116 itg2le 
 |-  ( ( ( 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 ) ) oR <_ ( 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 ) ) ) )
117 53 95 115 116 syl3anc 
 |-  ( ( 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 ) ) ) )
118 67 fveq2d 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( S.2 ` F ) = ( S.2 ` ( x e. RR |-> ( F ` x ) ) ) )
119 cmmbl 
 |-  ( ( `' F " ( M (,) +oo ) ) e. dom vol -> ( RR \ ( `' F " ( M (,) +oo ) ) ) e. dom vol )
120 17 119 syl 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( RR \ ( `' F " ( M (,) +oo ) ) ) e. dom vol )
121 disjdif 
 |-  ( ( `' F " ( M (,) +oo ) ) i^i ( RR \ ( `' F " ( M (,) +oo ) ) ) ) = (/)
122 121 fveq2i 
 |-  ( vol* ` ( ( `' F " ( M (,) +oo ) ) i^i ( RR \ ( `' F " ( M (,) +oo ) ) ) ) ) = ( vol* ` (/) )
123 122 28 eqtri 
 |-  ( vol* ` ( ( `' F " ( M (,) +oo ) ) i^i ( RR \ ( `' F " ( M (,) +oo ) ) ) ) ) = 0
124 123 a1i 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( vol* ` ( ( `' F " ( M (,) +oo ) ) i^i ( RR \ ( `' F " ( M (,) +oo ) ) ) ) ) = 0 )
125 undif2 
 |-  ( ( `' F " ( M (,) +oo ) ) u. ( RR \ ( `' F " ( M (,) +oo ) ) ) ) = ( ( `' F " ( M (,) +oo ) ) u. RR )
126 mblss 
 |-  ( ( `' F " ( M (,) +oo ) ) e. dom vol -> ( `' F " ( M (,) +oo ) ) C_ RR )
127 17 126 syl 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( `' F " ( M (,) +oo ) ) C_ RR )
128 ssequn1 
 |-  ( ( `' F " ( M (,) +oo ) ) C_ RR <-> ( ( `' F " ( M (,) +oo ) ) u. RR ) = RR )
129 127 128 sylib 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( ( `' F " ( M (,) +oo ) ) u. RR ) = RR )
130 125 129 eqtr2id 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> RR = ( ( `' F " ( M (,) +oo ) ) u. ( RR \ ( `' F " ( M (,) +oo ) ) ) ) )
131 eqid 
 |-  ( x e. RR |-> if ( x e. ( `' F " ( M (,) +oo ) ) , ( F ` x ) , 0 ) ) = ( x e. RR |-> if ( x e. ( `' F " ( M (,) +oo ) ) , ( F ` x ) , 0 ) )
132 eqid 
 |-  ( 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 ) )
133 iftrue 
 |-  ( x e. RR -> if ( x e. RR , ( F ` x ) , 0 ) = ( F ` x ) )
134 133 mpteq2ia 
 |-  ( x e. RR |-> if ( x e. RR , ( F ` x ) , 0 ) ) = ( x e. RR |-> ( F ` x ) )
135 134 eqcomi 
 |-  ( x e. RR |-> ( F ` x ) ) = ( x e. RR |-> if ( x e. RR , ( F ` x ) , 0 ) )
136 ifcl 
 |-  ( ( ( F ` x ) e. ( 0 [,] +oo ) /\ 0 e. ( 0 [,] +oo ) ) -> if ( x e. ( RR \ ( `' F " ( M (,) +oo ) ) ) , ( F ` x ) , 0 ) e. ( 0 [,] +oo ) )
137 45 50 136 sylancl 
 |-  ( ( ( 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 ) )
138 137 fmpttd 
 |-  ( ( 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 ) )
139 breq1 
 |-  ( ( 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 ) ) )
140 breq1 
 |-  ( 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 ) ) )
141 139 140 ifboth 
 |-  ( ( ( F ` x ) <_ ( F ` x ) /\ 0 <_ ( F ` x ) ) -> if ( x e. ( RR \ ( `' F " ( M (,) +oo ) ) ) , ( F ` x ) , 0 ) <_ ( F ` x ) )
142 58 43 141 syl2anc 
 |-  ( ( ( 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 ) )
143 142 ralrimiva 
 |-  ( ( 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 ) )
144 eqidd 
 |-  ( ( 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 ) ) )
145 65 137 45 144 67 ofrfval2 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( ( x e. RR |-> if ( x e. ( RR \ ( `' F " ( M (,) +oo ) ) ) , ( F ` x ) , 0 ) ) oR <_ F <-> A. x e. RR if ( x e. ( RR \ ( `' F " ( M (,) +oo ) ) ) , ( F ` x ) , 0 ) <_ ( F ` x ) ) )
146 143 145 mpbird 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( x e. RR |-> if ( x e. ( RR \ ( `' F " ( M (,) +oo ) ) ) , ( F ` x ) , 0 ) ) oR <_ F )
147 itg2le 
 |-  ( ( ( 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 ) ) oR <_ F ) -> ( S.2 ` ( x e. RR |-> if ( x e. ( RR \ ( `' F " ( M (,) +oo ) ) ) , ( F ` x ) , 0 ) ) ) <_ ( S.2 ` F ) )
148 138 57 146 147 syl3anc 
 |-  ( ( 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 ) )
149 itg2lecl 
 |-  ( ( ( 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 )
150 138 54 148 149 syl3anc 
 |-  ( ( 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 )
151 17 120 124 130 45 131 132 135 107 150 itg2split 
 |-  ( ( 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 ) ) ) ) )
152 118 151 eqtrd 
 |-  ( ( 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 ) ) ) ) )
153 eldif 
 |-  ( x e. ( RR \ ( `' F " ( M (,) +oo ) ) ) <-> ( x e. RR /\ -. x e. ( `' F " ( M (,) +oo ) ) ) )
154 153 baib 
 |-  ( x e. RR -> ( x e. ( RR \ ( `' F " ( M (,) +oo ) ) ) <-> -. x e. ( `' F " ( M (,) +oo ) ) ) )
155 154 adantl 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. RR ) -> ( x e. ( RR \ ( `' F " ( M (,) +oo ) ) ) <-> -. x e. ( `' F " ( M (,) +oo ) ) ) )
156 1 ffnd 
 |-  ( ph -> F Fn RR )
157 156 ad2antrr 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. RR ) -> F Fn RR )
158 elpreima 
 |-  ( F Fn RR -> ( x e. ( `' F " ( M (,) +oo ) ) <-> ( x e. RR /\ ( F ` x ) e. ( M (,) +oo ) ) ) )
159 157 158 syl 
 |-  ( ( ( 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 ) ) ) )
160 41 biantrurd 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. RR ) -> ( M < ( F ` x ) <-> ( ( F ` x ) e. RR /\ M < ( F ` x ) ) ) )
161 5 nnred 
 |-  ( ph -> M e. RR )
162 161 ad2antrr 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. RR ) -> M e. RR )
163 162 rexrd 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. RR ) -> M e. RR* )
164 elioopnf 
 |-  ( M e. RR* -> ( ( F ` x ) e. ( M (,) +oo ) <-> ( ( F ` x ) e. RR /\ M < ( F ` x ) ) ) )
165 163 164 syl 
 |-  ( ( ( 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 ) ) ) )
166 simpr 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. RR ) -> x e. RR )
167 166 biantrurd 
 |-  ( ( ( 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 ) ) ) )
168 160 165 167 3bitr2d 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. RR ) -> ( M < ( F ` x ) <-> ( x e. RR /\ ( F ` x ) e. ( M (,) +oo ) ) ) )
169 162 41 ltnled 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. RR ) -> ( M < ( F ` x ) <-> -. ( F ` x ) <_ M ) )
170 159 168 169 3bitr2rd 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. RR ) -> ( -. ( F ` x ) <_ M <-> x e. ( `' F " ( M (,) +oo ) ) ) )
171 170 con1bid 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. RR ) -> ( -. x e. ( `' F " ( M (,) +oo ) ) <-> ( F ` x ) <_ M ) )
172 155 171 bitrd 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. RR ) -> ( x e. ( RR \ ( `' F " ( M (,) +oo ) ) ) <-> ( F ` x ) <_ M ) )
173 172 ifbid 
 |-  ( ( ( 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 ) )
174 173 mpteq2dva 
 |-  ( ( 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 ) ) )
175 174 fveq2d 
 |-  ( ( 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 ) ) ) )
176 6 adantr 
 |-  ( ( 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 ) ) )
177 175 176 eqnbrtrd 
 |-  ( ( 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 ) ) )
178 54 92 resubcld 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( ( S.2 ` F ) - ( C / 2 ) ) e. RR )
179 178 150 ltnled 
 |-  ( ( 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 ) ) ) )
180 177 179 mpbird 
 |-  ( ( 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 ) ) ) )
181 54 92 150 ltsubadd2d 
 |-  ( ( 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 ) ) ) ) ) )
182 180 181 mpbid 
 |-  ( ( 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 ) ) ) ) )
183 152 182 eqbrtrrd 
 |-  ( ( 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 ) ) ) ) )
184 107 92 150 ltadd1d 
 |-  ( ( 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 ) ) ) ) ) )
185 183 184 mpbird 
 |-  ( ( 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 ) )
186 73 107 92 117 185 lelttrd 
 |-  ( ( 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 ) )
187 161 adantr 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> M e. RR )
188 mblvol 
 |-  ( u e. dom vol -> ( vol ` u ) = ( vol* ` u ) )
189 10 188 syl 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( vol ` u ) = ( vol* ` u ) )
190 9 rpred 
 |-  ( ph -> ( ( C / 2 ) / M ) e. RR )
191 190 adantr 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( ( C / 2 ) / M ) e. RR )
192 ovolcl 
 |-  ( u C_ RR -> ( vol* ` u ) e. RR* )
193 35 192 syl 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( vol* ` u ) e. RR* )
194 191 rexrd 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( ( C / 2 ) / M ) e. RR* )
195 simprr 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( vol ` u ) < ( ( C / 2 ) / M ) )
196 189 195 eqbrtrrd 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( vol* ` u ) < ( ( C / 2 ) / M ) )
197 193 194 196 xrltled 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( vol* ` u ) <_ ( ( C / 2 ) / M ) )
198 ovollecl 
 |-  ( ( u C_ RR /\ ( ( C / 2 ) / M ) e. RR /\ ( vol* ` u ) <_ ( ( C / 2 ) / M ) ) -> ( vol* ` u ) e. RR )
199 35 191 197 198 syl3anc 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( vol* ` u ) e. RR )
200 189 199 eqeltrd 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( vol ` u ) e. RR )
201 187 200 remulcld 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( M x. ( vol ` u ) ) e. RR )
202 187 rexrd 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> M e. RR* )
203 5 adantr 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> M e. NN )
204 203 nnnn0d 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> M e. NN0 )
205 204 nn0ge0d 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> 0 <_ M )
206 elxrge0 
 |-  ( M e. ( 0 [,] +oo ) <-> ( M e. RR* /\ 0 <_ M ) )
207 202 205 206 sylanbrc 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> M e. ( 0 [,] +oo ) )
208 ifcl 
 |-  ( ( M e. ( 0 [,] +oo ) /\ 0 e. ( 0 [,] +oo ) ) -> if ( x e. u , M , 0 ) e. ( 0 [,] +oo ) )
209 207 50 208 sylancl 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> if ( x e. u , M , 0 ) e. ( 0 [,] +oo ) )
210 209 adantr 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. RR ) -> if ( x e. u , M , 0 ) e. ( 0 [,] +oo ) )
211 210 fmpttd 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( x e. RR |-> if ( x e. u , M , 0 ) ) : RR --> ( 0 [,] +oo ) )
212 eldifn 
 |-  ( x e. ( u \ ( `' F " ( M (,) +oo ) ) ) -> -. x e. ( `' F " ( M (,) +oo ) ) )
213 212 adantl 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. ( u \ ( `' F " ( M (,) +oo ) ) ) ) -> -. x e. ( `' F " ( M (,) +oo ) ) )
214 difssd 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( u \ ( `' F " ( M (,) +oo ) ) ) C_ u )
215 214 sselda 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. ( u \ ( `' F " ( M (,) +oo ) ) ) ) -> x e. u )
216 36 170 syldan 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. u ) -> ( -. ( F ` x ) <_ M <-> x e. ( `' F " ( M (,) +oo ) ) ) )
217 215 216 syldan 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. ( u \ ( `' F " ( M (,) +oo ) ) ) ) -> ( -. ( F ` x ) <_ M <-> x e. ( `' F " ( M (,) +oo ) ) ) )
218 217 con1bid 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. ( u \ ( `' F " ( M (,) +oo ) ) ) ) -> ( -. x e. ( `' F " ( M (,) +oo ) ) <-> ( F ` x ) <_ M ) )
219 213 218 mpbid 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. ( u \ ( `' F " ( M (,) +oo ) ) ) ) -> ( F ` x ) <_ M )
220 iftrue 
 |-  ( x e. ( u \ ( `' F " ( M (,) +oo ) ) ) -> if ( x e. ( u \ ( `' F " ( M (,) +oo ) ) ) , ( F ` x ) , 0 ) = ( F ` x ) )
221 220 adantl 
 |-  ( ( ( 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 ) )
222 215 iftrued 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ x e. ( u \ ( `' F " ( M (,) +oo ) ) ) ) -> if ( x e. u , M , 0 ) = M )
223 219 221 222 3brtr4d 
 |-  ( ( ( 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 ) )
224 iffalse 
 |-  ( -. x e. ( u \ ( `' F " ( M (,) +oo ) ) ) -> if ( x e. ( u \ ( `' F " ( M (,) +oo ) ) ) , ( F ` x ) , 0 ) = 0 )
225 224 adantl 
 |-  ( ( ( 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 )
226 0le0 
 |-  0 <_ 0
227 breq2 
 |-  ( M = if ( x e. u , M , 0 ) -> ( 0 <_ M <-> 0 <_ if ( x e. u , M , 0 ) ) )
228 breq2 
 |-  ( 0 = if ( x e. u , M , 0 ) -> ( 0 <_ 0 <-> 0 <_ if ( x e. u , M , 0 ) ) )
229 227 228 ifboth 
 |-  ( ( 0 <_ M /\ 0 <_ 0 ) -> 0 <_ if ( x e. u , M , 0 ) )
230 205 226 229 sylancl 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> 0 <_ if ( x e. u , M , 0 ) )
231 230 adantr 
 |-  ( ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) /\ -. x e. ( u \ ( `' F " ( M (,) +oo ) ) ) ) -> 0 <_ if ( x e. u , M , 0 ) )
232 225 231 eqbrtrd 
 |-  ( ( ( 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 ) )
233 223 232 pm2.61dan 
 |-  ( ( 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 ) )
234 233 ralrimivw 
 |-  ( ( 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 ) )
235 eqidd 
 |-  ( ( 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 ) ) )
236 65 75 210 82 235 ofrfval2 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( ( x e. RR |-> if ( x e. ( u \ ( `' F " ( M (,) +oo ) ) ) , ( F ` x ) , 0 ) ) oR <_ ( 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 ) ) )
237 234 236 mpbird 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( x e. RR |-> if ( x e. ( u \ ( `' F " ( M (,) +oo ) ) ) , ( F ` x ) , 0 ) ) oR <_ ( x e. RR |-> if ( x e. u , M , 0 ) ) )
238 itg2le 
 |-  ( ( ( 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 ) ) oR <_ ( 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 ) ) ) )
239 76 211 237 238 syl3anc 
 |-  ( ( 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 ) ) ) )
240 elrege0 
 |-  ( M e. ( 0 [,) +oo ) <-> ( M e. RR /\ 0 <_ M ) )
241 187 205 240 sylanbrc 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> M e. ( 0 [,) +oo ) )
242 itg2const 
 |-  ( ( 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 ) ) )
243 10 200 241 242 syl3anc 
 |-  ( ( 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 ) ) )
244 239 243 breqtrd 
 |-  ( ( 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 ) ) )
245 203 nngt0d 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> 0 < M )
246 ltmuldiv2 
 |-  ( ( ( vol ` u ) e. RR /\ ( C / 2 ) e. RR /\ ( M e. RR /\ 0 < M ) ) -> ( ( M x. ( vol ` u ) ) < ( C / 2 ) <-> ( vol ` u ) < ( ( C / 2 ) / M ) ) )
247 200 92 187 245 246 syl112anc 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( ( M x. ( vol ` u ) ) < ( C / 2 ) <-> ( vol ` u ) < ( ( C / 2 ) / M ) ) )
248 195 247 mpbird 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( M x. ( vol ` u ) ) < ( C / 2 ) )
249 88 201 92 244 248 lelttrd 
 |-  ( ( 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 ) )
250 73 88 92 92 186 249 lt2addd 
 |-  ( ( 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 ) ) )
251 89 250 eqbrtrd 
 |-  ( ( 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 ) ) )
252 90 rpcnd 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> C e. CC )
253 252 2halvesd 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( ( C / 2 ) + ( C / 2 ) ) = C )
254 251 253 breqtrd 
 |-  ( ( ph /\ ( u e. dom vol /\ ( vol ` u ) < ( ( C / 2 ) / M ) ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. u , ( F ` x ) , 0 ) ) ) < C )
255 254 expr 
 |-  ( ( ph /\ u e. dom vol ) -> ( ( vol ` u ) < ( ( C / 2 ) / M ) -> ( S.2 ` ( x e. RR |-> if ( x e. u , ( F ` x ) , 0 ) ) ) < C ) )
256 255 ralrimiva 
 |-  ( ph -> A. u e. dom vol ( ( vol ` u ) < ( ( C / 2 ) / M ) -> ( S.2 ` ( x e. RR |-> if ( x e. u , ( F ` x ) , 0 ) ) ) < C ) )
257 breq2 
 |-  ( d = ( ( C / 2 ) / M ) -> ( ( vol ` u ) < d <-> ( vol ` u ) < ( ( C / 2 ) / M ) ) )
258 257 rspceaimv 
 |-  ( ( ( ( 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 ) )
259 9 256 258 syl2anc 
 |-  ( 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 ) )