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

Theorem bddiblnc 30061
Description: Choice-free proof of bddibl 22224. (Contributed by Brendan Leahy, 2-Nov-2017.) (Revised by Brendan Leahy, 6-Nov-2017.)
Assertion
Ref Expression
bddiblnc  |-  ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR  /\  E. x  e.  RR  A. y  e.  dom  F ( abs `  ( F `  y
) )  <_  x
)  ->  F  e.  L^1 )
Distinct variable group:    x, y, F

Proof of Theorem bddiblnc
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 mbff 22012 . . . 4  |-  ( F  e. MblFn  ->  F : dom  F --> CC )
21feqmptd 5911 . . 3  |-  ( F  e. MblFn  ->  F  =  ( z  e.  dom  F  |->  ( F `  z
) ) )
323ad2ant1 1018 . 2  |-  ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR  /\  E. x  e.  RR  A. y  e.  dom  F ( abs `  ( F `  y
) )  <_  x
)  ->  F  =  ( z  e.  dom  F 
|->  ( F `  z
) ) )
4 rzal 3916 . . . . . . . 8  |-  ( dom 
F  =  (/)  ->  A. z  e.  dom  F ( F `
 z )  =  0 )
5 mpteq12 4516 . . . . . . . 8  |-  ( ( dom  F  =  (/)  /\ 
A. z  e.  dom  F ( F `  z
)  =  0 )  ->  ( z  e. 
dom  F  |->  ( F `
 z ) )  =  ( z  e.  (/)  |->  0 ) )
64, 5mpdan 668 . . . . . . 7  |-  ( dom 
F  =  (/)  ->  (
z  e.  dom  F  |->  ( F `  z
) )  =  ( z  e.  (/)  |->  0 ) )
7 fconstmpt 5033 . . . . . . . 8  |-  ( (/)  X. 
{ 0 } )  =  ( z  e.  (/)  |->  0 )
8 0mbl 21928 . . . . . . . . 9  |-  (/)  e.  dom  vol
9 ibl0 22171 . . . . . . . . 9  |-  ( (/)  e.  dom  vol  ->  ( (/)  X. 
{ 0 } )  e.  L^1 )
108, 9ax-mp 5 . . . . . . . 8  |-  ( (/)  X. 
{ 0 } )  e.  L^1
117, 10eqeltrri 2528 . . . . . . 7  |-  ( z  e.  (/)  |->  0 )  e.  L^1
126, 11syl6eqel 2539 . . . . . 6  |-  ( dom 
F  =  (/)  ->  (
z  e.  dom  F  |->  ( F `  z
) )  e.  L^1 )
1312adantl 466 . . . . 5  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( x  e.  RR  /\  A. y  e.  dom  F ( abs `  ( F `  y
) )  <_  x
) )  /\  dom  F  =  (/) )  ->  (
z  e.  dom  F  |->  ( F `  z
) )  e.  L^1 )
14 r19.2z 3904 . . . . . . . . . 10  |-  ( ( dom  F  =/=  (/)  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x )  ->  E. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
1514anim1i 568 . . . . . . . . 9  |-  ( ( ( dom  F  =/=  (/)  /\  A. y  e. 
dom  F ( abs `  ( F `  y
) )  <_  x
)  /\  x  e.  RR )  ->  ( E. y  e.  dom  F
( abs `  ( F `  y )
)  <_  x  /\  x  e.  RR )
)
1615an31s 806 . . . . . . . 8  |-  ( ( ( x  e.  RR  /\ 
A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )  /\  dom  F  =/=  (/) )  -> 
( E. y  e. 
dom  F ( abs `  ( F `  y
) )  <_  x  /\  x  e.  RR ) )
171ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  x  e.  RR )  ->  F : dom  F --> CC )
1817ffvelrnda 6016 . . . . . . . . . . . . . 14  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  x  e.  RR )  /\  y  e.  dom  F )  ->  ( F `  y )  e.  CC )
1918absge0d 13257 . . . . . . . . . . . . 13  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  x  e.  RR )  /\  y  e.  dom  F )  ->  0  <_  ( abs `  ( F `
 y ) ) )
20 0red 9600 . . . . . . . . . . . . . 14  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  x  e.  RR )  /\  y  e.  dom  F )  ->  0  e.  RR )
2118abscld 13249 . . . . . . . . . . . . . 14  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  x  e.  RR )  /\  y  e.  dom  F )  ->  ( abs `  ( F `  y
) )  e.  RR )
22 simplr 755 . . . . . . . . . . . . . 14  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  x  e.  RR )  /\  y  e.  dom  F )  ->  x  e.  RR )
23 letr 9681 . . . . . . . . . . . . . 14  |-  ( ( 0  e.  RR  /\  ( abs `  ( F `
 y ) )  e.  RR  /\  x  e.  RR )  ->  (
( 0  <_  ( abs `  ( F `  y ) )  /\  ( abs `  ( F `
 y ) )  <_  x )  -> 
0  <_  x )
)
2420, 21, 22, 23syl3anc 1229 . . . . . . . . . . . . 13  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  x  e.  RR )  /\  y  e.  dom  F )  ->  ( (
0  <_  ( abs `  ( F `  y
) )  /\  ( abs `  ( F `  y ) )  <_  x )  ->  0  <_  x ) )
2519, 24mpand 675 . . . . . . . . . . . 12  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  x  e.  RR )  /\  y  e.  dom  F )  ->  ( ( abs `  ( F `  y ) )  <_  x  ->  0  <_  x
) )
2625rexlimdva 2935 . . . . . . . . . . 11  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  x  e.  RR )  ->  ( E. y  e. 
dom  F ( abs `  ( F `  y
) )  <_  x  ->  0  <_  x )
)
2726ex 434 . . . . . . . . . 10  |-  ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  -> 
( x  e.  RR  ->  ( E. y  e. 
dom  F ( abs `  ( F `  y
) )  <_  x  ->  0  <_  x )
) )
2827com23 78 . . . . . . . . 9  |-  ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  -> 
( E. y  e. 
dom  F ( abs `  ( F `  y
) )  <_  x  ->  ( x  e.  RR  ->  0  <_  x )
) )
2928imp32 433 . . . . . . . 8  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( E. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x  /\  x  e.  RR )
)  ->  0  <_  x )
3016, 29sylan2 474 . . . . . . 7  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  A. y  e.  dom  F ( abs `  ( F `  y
) )  <_  x
)  /\  dom  F  =/=  (/) ) )  ->  0  <_  x )
3130anassrs 648 . . . . . 6  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( x  e.  RR  /\  A. y  e.  dom  F ( abs `  ( F `  y
) )  <_  x
) )  /\  dom  F  =/=  (/) )  ->  0  <_  x )
32 an32 798 . . . . . . . 8  |-  ( ( ( x  e.  RR  /\ 
A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )  /\  0  <_  x )  <-> 
( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )
33 id 22 . . . . . . . . . . 11  |-  ( F  e. MblFn  ->  F  e. MblFn )
342, 33eqeltrrd 2532 . . . . . . . . . 10  |-  ( F  e. MblFn  ->  ( z  e. 
dom  F  |->  ( F `
 z ) )  e. MblFn )
3534ad2antrr 725 . . . . . . . . 9  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( z  e. 
dom  F  |->  ( F `
 z ) )  e. MblFn )
361ad3antrrr 729 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  RR )  ->  F : dom  F --> CC )
3736ffvelrnda 6016 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  z  e.  dom  F )  -> 
( F `  z
)  e.  CC )
3837recld 13009 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  z  e.  dom  F )  -> 
( Re `  ( F `  z )
)  e.  RR )
3938rexrd 9646 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  z  e.  dom  F )  -> 
( Re `  ( F `  z )
)  e.  RR* )
4039adantrr 716 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  (
z  e.  dom  F  /\  0  <_  ( Re
`  ( F `  z ) ) ) )  ->  ( Re `  ( F `  z
) )  e.  RR* )
41 simprr 757 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  (
z  e.  dom  F  /\  0  <_  ( Re
`  ( F `  z ) ) ) )  ->  0  <_  ( Re `  ( F `
 z ) ) )
42 elxrge0 11640 . . . . . . . . . . . . . 14  |-  ( ( Re `  ( F `
 z ) )  e.  ( 0 [,] +oo )  <->  ( ( Re
`  ( F `  z ) )  e. 
RR*  /\  0  <_  ( Re `  ( F `
 z ) ) ) )
4340, 41, 42sylanbrc 664 . . . . . . . . . . . . 13  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  (
z  e.  dom  F  /\  0  <_  ( Re
`  ( F `  z ) ) ) )  ->  ( Re `  ( F `  z
) )  e.  ( 0 [,] +oo )
)
44 0e0iccpnf 11642 . . . . . . . . . . . . . 14  |-  0  e.  ( 0 [,] +oo )
4544a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  -.  (
z  e.  dom  F  /\  0  <_  ( Re
`  ( F `  z ) ) ) )  ->  0  e.  ( 0 [,] +oo ) )
4643, 45ifclda 3958 . . . . . . . . . . . 12  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  RR )  ->  if ( ( z  e.  dom  F  /\  0  <_  ( Re
`  ( F `  z ) ) ) ,  ( Re `  ( F `  z ) ) ,  0 )  e.  ( 0 [,] +oo ) )
47 eqid 2443 . . . . . . . . . . . 12  |-  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  (
Re `  ( F `  z ) ) ) ,  ( Re `  ( F `  z ) ) ,  0 ) )  =  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  (
Re `  ( F `  z ) ) ) ,  ( Re `  ( F `  z ) ) ,  0 ) )
4846, 47fmptd 6040 . . . . . . . . . . 11  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  ( Re
`  ( F `  z ) ) ) ,  ( Re `  ( F `  z ) ) ,  0 ) ) : RR --> ( 0 [,] +oo ) )
49 mbfdm 22013 . . . . . . . . . . . . . 14  |-  ( F  e. MblFn  ->  dom  F  e.  dom  vol )
5049ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  dom  F  e.  dom  vol )
51 simplr 755 . . . . . . . . . . . . 13  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( vol `  dom  F )  e.  RR )
52 elrege0 11638 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( 0 [,) +oo )  <->  ( x  e.  RR  /\  0  <_  x ) )
5352biimpri 206 . . . . . . . . . . . . . 14  |-  ( ( x  e.  RR  /\  0  <_  x )  ->  x  e.  ( 0 [,) +oo ) )
5453ad2antrl 727 . . . . . . . . . . . . 13  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  x  e.  ( 0 [,) +oo )
)
55 itg2const 22125 . . . . . . . . . . . . 13  |-  ( ( dom  F  e.  dom  vol 
/\  ( vol `  dom  F )  e.  RR  /\  x  e.  ( 0 [,) +oo ) )  ->  ( S.2 `  (
z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) )  =  ( x  x.  ( vol `  dom  F ) ) )
5650, 51, 54, 55syl3anc 1229 . . . . . . . . . . . 12  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( S.2 `  (
z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) )  =  ( x  x.  ( vol `  dom  F ) ) )
57 simprll 763 . . . . . . . . . . . . 13  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  x  e.  RR )
5857, 51remulcld 9627 . . . . . . . . . . . 12  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( x  x.  ( vol `  dom  F ) )  e.  RR )
5956, 58eqeltrd 2531 . . . . . . . . . . 11  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( S.2 `  (
z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) )  e.  RR )
60 rexr 9642 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  RR  ->  x  e.  RR* )
61 elxrge0 11640 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( 0 [,] +oo )  <->  ( x  e. 
RR*  /\  0  <_  x ) )
6261biimpri 206 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  RR*  /\  0  <_  x )  ->  x  e.  ( 0 [,] +oo ) )
6360, 62sylan 471 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  RR  /\  0  <_  x )  ->  x  e.  ( 0 [,] +oo ) )
6463ad2antrl 727 . . . . . . . . . . . . . . 15  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  x  e.  ( 0 [,] +oo )
)
6564adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  RR )  ->  x  e.  ( 0 [,] +oo )
)
66 ifcl 3968 . . . . . . . . . . . . . 14  |-  ( ( x  e.  ( 0 [,] +oo )  /\  0  e.  ( 0 [,] +oo ) )  ->  if ( z  e.  dom  F ,  x ,  0 )  e.  ( 0 [,] +oo ) )
6765, 44, 66sylancl 662 . . . . . . . . . . . . 13  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  RR )  ->  if ( z  e.  dom  F ,  x ,  0 )  e.  ( 0 [,] +oo ) )
68 eqid 2443 . . . . . . . . . . . . 13  |-  ( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) )  =  ( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) )
6967, 68fmptd 6040 . . . . . . . . . . . 12  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) : RR --> ( 0 [,] +oo ) )
70 ifan 3972 . . . . . . . . . . . . . . 15  |-  if ( ( z  e.  dom  F  /\  0  <_  (
Re `  ( F `  z ) ) ) ,  ( Re `  ( F `  z ) ) ,  0 )  =  if ( z  e.  dom  F ,  if ( 0  <_  (
Re `  ( F `  z ) ) ,  ( Re `  ( F `  z )
) ,  0 ) ,  0 )
711ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  F : dom  F --> CC )
7271ffvelrnda 6016 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  ( F `  z )  e.  CC )
7372recld 13009 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  ( Re `  ( F `  z
) )  e.  RR )
7472abscld 13249 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  ( abs `  ( F `  z
) )  e.  RR )
7557adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  x  e.  RR )
7672releabsd 13264 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  ( Re `  ( F `  z
) )  <_  ( abs `  ( F `  z ) ) )
77 fveq2 5856 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  z  ->  ( F `  y )  =  ( F `  z ) )
7877fveq2d 5860 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  z  ->  ( abs `  ( F `  y ) )  =  ( abs `  ( F `  z )
) )
7978breq1d 4447 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  z  ->  (
( abs `  ( F `  y )
)  <_  x  <->  ( abs `  ( F `  z
) )  <_  x
) )
8079rspccva 3195 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x  /\  z  e.  dom  F )  ->  ( abs `  ( F `  z )
)  <_  x )
8180adantll 713 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x )  /\  z  e.  dom  F )  ->  ( abs `  ( F `  z )
)  <_  x )
8281adantll 713 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  ( abs `  ( F `  z
) )  <_  x
)
8373, 74, 75, 76, 82letrd 9742 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  ( Re `  ( F `  z
) )  <_  x
)
84 simprlr 764 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  0  <_  x
)
8584adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  0  <_  x )
86 breq1 4440 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( Re `  ( F `
 z ) )  =  if ( 0  <_  ( Re `  ( F `  z ) ) ,  ( Re
`  ( F `  z ) ) ,  0 )  ->  (
( Re `  ( F `  z )
)  <_  x  <->  if (
0  <_  ( Re `  ( F `  z
) ) ,  ( Re `  ( F `
 z ) ) ,  0 )  <_  x ) )
87 breq1 4440 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  =  if ( 0  <_  ( Re `  ( F `  z ) ) ,  ( Re
`  ( F `  z ) ) ,  0 )  ->  (
0  <_  x  <->  if (
0  <_  ( Re `  ( F `  z
) ) ,  ( Re `  ( F `
 z ) ) ,  0 )  <_  x ) )
8886, 87ifboth 3962 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( Re `  ( F `  z )
)  <_  x  /\  0  <_  x )  ->  if ( 0  <_  (
Re `  ( F `  z ) ) ,  ( Re `  ( F `  z )
) ,  0 )  <_  x )
8983, 85, 88syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  if (
0  <_  ( Re `  ( F `  z
) ) ,  ( Re `  ( F `
 z ) ) ,  0 )  <_  x )
90 iftrue 3932 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  dom  F  ->  if ( z  e.  dom  F ,  if ( 0  <_  ( Re `  ( F `  z ) ) ,  ( Re
`  ( F `  z ) ) ,  0 ) ,  0 )  =  if ( 0  <_  ( Re `  ( F `  z
) ) ,  ( Re `  ( F `
 z ) ) ,  0 ) )
9190adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  if (
z  e.  dom  F ,  if ( 0  <_ 
( Re `  ( F `  z )
) ,  ( Re
`  ( F `  z ) ) ,  0 ) ,  0 )  =  if ( 0  <_  ( Re `  ( F `  z
) ) ,  ( Re `  ( F `
 z ) ) ,  0 ) )
92 iftrue 3932 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  dom  F  ->  if ( z  e.  dom  F ,  x ,  0 )  =  x )
9392adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  if (
z  e.  dom  F ,  x ,  0 )  =  x )
9489, 91, 933brtr4d 4467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  if (
z  e.  dom  F ,  if ( 0  <_ 
( Re `  ( F `  z )
) ,  ( Re
`  ( F `  z ) ) ,  0 ) ,  0 )  <_  if (
z  e.  dom  F ,  x ,  0 ) )
9594ex 434 . . . . . . . . . . . . . . . 16  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( z  e. 
dom  F  ->  if ( z  e.  dom  F ,  if ( 0  <_ 
( Re `  ( F `  z )
) ,  ( Re
`  ( F `  z ) ) ,  0 ) ,  0 )  <_  if (
z  e.  dom  F ,  x ,  0 ) ) )
96 0le0 10632 . . . . . . . . . . . . . . . . . 18  |-  0  <_  0
9796a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( -.  z  e.  dom  F  ->  0  <_  0 )
98 iffalse 3935 . . . . . . . . . . . . . . . . 17  |-  ( -.  z  e.  dom  F  ->  if ( z  e. 
dom  F ,  if ( 0  <_  (
Re `  ( F `  z ) ) ,  ( Re `  ( F `  z )
) ,  0 ) ,  0 )  =  0 )
99 iffalse 3935 . . . . . . . . . . . . . . . . 17  |-  ( -.  z  e.  dom  F  ->  if ( z  e. 
dom  F ,  x ,  0 )  =  0 )
10097, 98, 993brtr4d 4467 . . . . . . . . . . . . . . . 16  |-  ( -.  z  e.  dom  F  ->  if ( z  e. 
dom  F ,  if ( 0  <_  (
Re `  ( F `  z ) ) ,  ( Re `  ( F `  z )
) ,  0 ) ,  0 )  <_  if ( z  e.  dom  F ,  x ,  0 ) )
10195, 100pm2.61d1 159 . . . . . . . . . . . . . . 15  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  if ( z  e.  dom  F ,  if ( 0  <_  (
Re `  ( F `  z ) ) ,  ( Re `  ( F `  z )
) ,  0 ) ,  0 )  <_  if ( z  e.  dom  F ,  x ,  0 ) )
10270, 101syl5eqbr 4470 . . . . . . . . . . . . . 14  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  if ( ( z  e.  dom  F  /\  0  <_  ( Re
`  ( F `  z ) ) ) ,  ( Re `  ( F `  z ) ) ,  0 )  <_  if ( z  e.  dom  F ,  x ,  0 ) )
103102ralrimivw 2858 . . . . . . . . . . . . 13  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  A. z  e.  RR  if ( ( z  e. 
dom  F  /\  0  <_  ( Re `  ( F `  z )
) ) ,  ( Re `  ( F `
 z ) ) ,  0 )  <_  if ( z  e.  dom  F ,  x ,  0 ) )
104 reex 9586 . . . . . . . . . . . . . . 15  |-  RR  e.  _V
105104a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  RR  e.  _V )
106 eqidd 2444 . . . . . . . . . . . . . 14  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  ( Re
`  ( F `  z ) ) ) ,  ( Re `  ( F `  z ) ) ,  0 ) )  =  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  (
Re `  ( F `  z ) ) ) ,  ( Re `  ( F `  z ) ) ,  0 ) ) )
107 eqidd 2444 . . . . . . . . . . . . . 14  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) )  =  ( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) )
108105, 46, 67, 106, 107ofrfval2 6542 . . . . . . . . . . . . 13  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  (
Re `  ( F `  z ) ) ) ,  ( Re `  ( F `  z ) ) ,  0 ) )  oR  <_ 
( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) )  <->  A. z  e.  RR  if ( ( z  e.  dom  F  /\  0  <_  ( Re
`  ( F `  z ) ) ) ,  ( Re `  ( F `  z ) ) ,  0 )  <_  if ( z  e.  dom  F ,  x ,  0 ) ) )
109103, 108mpbird 232 . . . . . . . . . . . 12  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  ( Re
`  ( F `  z ) ) ) ,  ( Re `  ( F `  z ) ) ,  0 ) )  oR  <_ 
( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) )
110 itg2le 22124 . . . . . . . . . . . 12  |-  ( ( ( z  e.  RR  |->  if ( ( z  e. 
dom  F  /\  0  <_  ( Re `  ( F `  z )
) ) ,  ( Re `  ( F `
 z ) ) ,  0 ) ) : RR --> ( 0 [,] +oo )  /\  ( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) : RR --> ( 0 [,] +oo )  /\  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  ( Re
`  ( F `  z ) ) ) ,  ( Re `  ( F `  z ) ) ,  0 ) )  oR  <_ 
( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) )  -> 
( S.2 `  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  (
Re `  ( F `  z ) ) ) ,  ( Re `  ( F `  z ) ) ,  0 ) ) )  <_  ( S.2 `  ( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) ) )
11148, 69, 109, 110syl3anc 1229 . . . . . . . . . . 11  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( S.2 `  (
z  e.  RR  |->  if ( ( z  e. 
dom  F  /\  0  <_  ( Re `  ( F `  z )
) ) ,  ( Re `  ( F `
 z ) ) ,  0 ) ) )  <_  ( S.2 `  ( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) ) )
112 itg2lecl 22123 . . . . . . . . . . 11  |-  ( ( ( z  e.  RR  |->  if ( ( z  e. 
dom  F  /\  0  <_  ( Re `  ( F `  z )
) ) ,  ( Re `  ( F `
 z ) ) ,  0 ) ) : RR --> ( 0 [,] +oo )  /\  ( S.2 `  ( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) )  e.  RR  /\  ( S.2 `  (
z  e.  RR  |->  if ( ( z  e. 
dom  F  /\  0  <_  ( Re `  ( F `  z )
) ) ,  ( Re `  ( F `
 z ) ) ,  0 ) ) )  <_  ( S.2 `  ( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) ) )  ->  ( S.2 `  (
z  e.  RR  |->  if ( ( z  e. 
dom  F  /\  0  <_  ( Re `  ( F `  z )
) ) ,  ( Re `  ( F `
 z ) ) ,  0 ) ) )  e.  RR )
11348, 59, 111, 112syl3anc 1229 . . . . . . . . . 10  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( S.2 `  (
z  e.  RR  |->  if ( ( z  e. 
dom  F  /\  0  <_  ( Re `  ( F `  z )
) ) ,  ( Re `  ( F `
 z ) ) ,  0 ) ) )  e.  RR )
11438renegcld 9993 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  z  e.  dom  F )  ->  -u ( Re `  ( F `  z )
)  e.  RR )
115114rexrd 9646 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  z  e.  dom  F )  ->  -u ( Re `  ( F `  z )
)  e.  RR* )
116115adantrr 716 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  (
z  e.  dom  F  /\  0  <_  -u (
Re `  ( F `  z ) ) ) )  ->  -u ( Re
`  ( F `  z ) )  e. 
RR* )
117 simprr 757 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  (
z  e.  dom  F  /\  0  <_  -u (
Re `  ( F `  z ) ) ) )  ->  0  <_  -u ( Re `  ( F `
 z ) ) )
118 elxrge0 11640 . . . . . . . . . . . . . 14  |-  ( -u ( Re `  ( F `
 z ) )  e.  ( 0 [,] +oo )  <->  ( -u (
Re `  ( F `  z ) )  e. 
RR*  /\  0  <_  -u ( Re `  ( F `
 z ) ) ) )
119116, 117, 118sylanbrc 664 . . . . . . . . . . . . 13  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  (
z  e.  dom  F  /\  0  <_  -u (
Re `  ( F `  z ) ) ) )  ->  -u ( Re
`  ( F `  z ) )  e.  ( 0 [,] +oo ) )
12044a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  -.  (
z  e.  dom  F  /\  0  <_  -u (
Re `  ( F `  z ) ) ) )  ->  0  e.  ( 0 [,] +oo ) )
121119, 120ifclda 3958 . . . . . . . . . . . 12  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  RR )  ->  if ( ( z  e.  dom  F  /\  0  <_  -u (
Re `  ( F `  z ) ) ) ,  -u ( Re `  ( F `  z ) ) ,  0 )  e.  ( 0 [,] +oo ) )
122 eqid 2443 . . . . . . . . . . . 12  |-  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  -u (
Re `  ( F `  z ) ) ) ,  -u ( Re `  ( F `  z ) ) ,  0 ) )  =  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  -u (
Re `  ( F `  z ) ) ) ,  -u ( Re `  ( F `  z ) ) ,  0 ) )
123121, 122fmptd 6040 . . . . . . . . . . 11  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  -u (
Re `  ( F `  z ) ) ) ,  -u ( Re `  ( F `  z ) ) ,  0 ) ) : RR --> ( 0 [,] +oo ) )
124 ifan 3972 . . . . . . . . . . . . . . 15  |-  if ( ( z  e.  dom  F  /\  0  <_  -u (
Re `  ( F `  z ) ) ) ,  -u ( Re `  ( F `  z ) ) ,  0 )  =  if ( z  e.  dom  F ,  if ( 0  <_  -u (
Re `  ( F `  z ) ) , 
-u ( Re `  ( F `  z ) ) ,  0 ) ,  0 )
12573renegcld 9993 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  -u ( Re
`  ( F `  z ) )  e.  RR )
12673recnd 9625 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  ( Re `  ( F `  z
) )  e.  CC )
127126abscld 13249 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  ( abs `  ( Re `  ( F `  z )
) )  e.  RR )
128125leabsd 13228 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  -u ( Re
`  ( F `  z ) )  <_ 
( abs `  -u (
Re `  ( F `  z ) ) ) )
129126absnegd 13262 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  ( abs `  -u ( Re `  ( F `  z )
) )  =  ( abs `  ( Re
`  ( F `  z ) ) ) )
130128, 129breqtrd 4461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  -u ( Re
`  ( F `  z ) )  <_ 
( abs `  (
Re `  ( F `  z ) ) ) )
131 absrele 13123 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F `  z )  e.  CC  ->  ( abs `  ( Re `  ( F `  z ) ) )  <_  ( abs `  ( F `  z ) ) )
13272, 131syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  ( abs `  ( Re `  ( F `  z )
) )  <_  ( abs `  ( F `  z ) ) )
133125, 127, 74, 130, 132letrd 9742 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  -u ( Re
`  ( F `  z ) )  <_ 
( abs `  ( F `  z )
) )
134125, 74, 75, 133, 82letrd 9742 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  -u ( Re
`  ( F `  z ) )  <_  x )
135 breq1 4440 . . . . . . . . . . . . . . . . . . . 20  |-  ( -u ( Re `  ( F `
 z ) )  =  if ( 0  <_  -u ( Re `  ( F `  z ) ) ,  -u (
Re `  ( F `  z ) ) ,  0 )  ->  ( -u ( Re `  ( F `  z )
)  <_  x  <->  if (
0  <_  -u ( Re
`  ( F `  z ) ) , 
-u ( Re `  ( F `  z ) ) ,  0 )  <_  x ) )
136 breq1 4440 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  =  if ( 0  <_  -u ( Re `  ( F `  z ) ) ,  -u (
Re `  ( F `  z ) ) ,  0 )  ->  (
0  <_  x  <->  if (
0  <_  -u ( Re
`  ( F `  z ) ) , 
-u ( Re `  ( F `  z ) ) ,  0 )  <_  x ) )
137135, 136ifboth 3962 . . . . . . . . . . . . . . . . . . 19  |-  ( (
-u ( Re `  ( F `  z ) )  <_  x  /\  0  <_  x )  ->  if ( 0  <_  -u (
Re `  ( F `  z ) ) , 
-u ( Re `  ( F `  z ) ) ,  0 )  <_  x )
138134, 85, 137syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  if (
0  <_  -u ( Re
`  ( F `  z ) ) , 
-u ( Re `  ( F `  z ) ) ,  0 )  <_  x )
139 iftrue 3932 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  dom  F  ->  if ( z  e.  dom  F ,  if ( 0  <_  -u ( Re `  ( F `  z ) ) ,  -u (
Re `  ( F `  z ) ) ,  0 ) ,  0 )  =  if ( 0  <_  -u ( Re
`  ( F `  z ) ) , 
-u ( Re `  ( F `  z ) ) ,  0 ) )
140139adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  if (
z  e.  dom  F ,  if ( 0  <_  -u ( Re `  ( F `  z )
) ,  -u (
Re `  ( F `  z ) ) ,  0 ) ,  0 )  =  if ( 0  <_  -u ( Re
`  ( F `  z ) ) , 
-u ( Re `  ( F `  z ) ) ,  0 ) )
141138, 140, 933brtr4d 4467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  if (
z  e.  dom  F ,  if ( 0  <_  -u ( Re `  ( F `  z )
) ,  -u (
Re `  ( F `  z ) ) ,  0 ) ,  0 )  <_  if (
z  e.  dom  F ,  x ,  0 ) )
142141ex 434 . . . . . . . . . . . . . . . 16  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( z  e. 
dom  F  ->  if ( z  e.  dom  F ,  if ( 0  <_  -u ( Re `  ( F `  z )
) ,  -u (
Re `  ( F `  z ) ) ,  0 ) ,  0 )  <_  if (
z  e.  dom  F ,  x ,  0 ) ) )
143 iffalse 3935 . . . . . . . . . . . . . . . . 17  |-  ( -.  z  e.  dom  F  ->  if ( z  e. 
dom  F ,  if ( 0  <_  -u (
Re `  ( F `  z ) ) , 
-u ( Re `  ( F `  z ) ) ,  0 ) ,  0 )  =  0 )
14497, 143, 993brtr4d 4467 . . . . . . . . . . . . . . . 16  |-  ( -.  z  e.  dom  F  ->  if ( z  e. 
dom  F ,  if ( 0  <_  -u (
Re `  ( F `  z ) ) , 
-u ( Re `  ( F `  z ) ) ,  0 ) ,  0 )  <_  if ( z  e.  dom  F ,  x ,  0 ) )
145142, 144pm2.61d1 159 . . . . . . . . . . . . . . 15  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  if ( z  e.  dom  F ,  if ( 0  <_  -u (
Re `  ( F `  z ) ) , 
-u ( Re `  ( F `  z ) ) ,  0 ) ,  0 )  <_  if ( z  e.  dom  F ,  x ,  0 ) )
146124, 145syl5eqbr 4470 . . . . . . . . . . . . . 14  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  if ( ( z  e.  dom  F  /\  0  <_  -u (
Re `  ( F `  z ) ) ) ,  -u ( Re `  ( F `  z ) ) ,  0 )  <_  if ( z  e.  dom  F ,  x ,  0 ) )
147146ralrimivw 2858 . . . . . . . . . . . . 13  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  A. z  e.  RR  if ( ( z  e. 
dom  F  /\  0  <_ 
-u ( Re `  ( F `  z ) ) ) ,  -u ( Re `  ( F `
 z ) ) ,  0 )  <_  if ( z  e.  dom  F ,  x ,  0 ) )
148 eqidd 2444 . . . . . . . . . . . . . 14  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  -u (
Re `  ( F `  z ) ) ) ,  -u ( Re `  ( F `  z ) ) ,  0 ) )  =  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  -u (
Re `  ( F `  z ) ) ) ,  -u ( Re `  ( F `  z ) ) ,  0 ) ) )
149105, 121, 67, 148, 107ofrfval2 6542 . . . . . . . . . . . . 13  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  -u (
Re `  ( F `  z ) ) ) ,  -u ( Re `  ( F `  z ) ) ,  0 ) )  oR  <_ 
( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) )  <->  A. z  e.  RR  if ( ( z  e.  dom  F  /\  0  <_  -u (
Re `  ( F `  z ) ) ) ,  -u ( Re `  ( F `  z ) ) ,  0 )  <_  if ( z  e.  dom  F ,  x ,  0 ) ) )
150147, 149mpbird 232 . . . . . . . . . . . 12  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  -u (
Re `  ( F `  z ) ) ) ,  -u ( Re `  ( F `  z ) ) ,  0 ) )  oR  <_ 
( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) )
151 itg2le 22124 . . . . . . . . . . . 12  |-  ( ( ( z  e.  RR  |->  if ( ( z  e. 
dom  F  /\  0  <_ 
-u ( Re `  ( F `  z ) ) ) ,  -u ( Re `  ( F `
 z ) ) ,  0 ) ) : RR --> ( 0 [,] +oo )  /\  ( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) : RR --> ( 0 [,] +oo )  /\  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  -u (
Re `  ( F `  z ) ) ) ,  -u ( Re `  ( F `  z ) ) ,  0 ) )  oR  <_ 
( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) )  -> 
( S.2 `  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  -u (
Re `  ( F `  z ) ) ) ,  -u ( Re `  ( F `  z ) ) ,  0 ) ) )  <_  ( S.2 `  ( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) ) )
152123, 69, 150, 151syl3anc 1229 . . . . . . . . . . 11  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( S.2 `  (
z  e.  RR  |->  if ( ( z  e. 
dom  F  /\  0  <_ 
-u ( Re `  ( F `  z ) ) ) ,  -u ( Re `  ( F `
 z ) ) ,  0 ) ) )  <_  ( S.2 `  ( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) ) )
153 itg2lecl 22123 . . . . . . . . . . 11  |-  ( ( ( z  e.  RR  |->  if ( ( z  e. 
dom  F  /\  0  <_ 
-u ( Re `  ( F `  z ) ) ) ,  -u ( Re `  ( F `
 z ) ) ,  0 ) ) : RR --> ( 0 [,] +oo )  /\  ( S.2 `  ( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) )  e.  RR  /\  ( S.2 `  (
z  e.  RR  |->  if ( ( z  e. 
dom  F  /\  0  <_ 
-u ( Re `  ( F `  z ) ) ) ,  -u ( Re `  ( F `
 z ) ) ,  0 ) ) )  <_  ( S.2 `  ( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) ) )  ->  ( S.2 `  (
z  e.  RR  |->  if ( ( z  e. 
dom  F  /\  0  <_ 
-u ( Re `  ( F `  z ) ) ) ,  -u ( Re `  ( F `
 z ) ) ,  0 ) ) )  e.  RR )
154123, 59, 152, 153syl3anc 1229 . . . . . . . . . 10  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( S.2 `  (
z  e.  RR  |->  if ( ( z  e. 
dom  F  /\  0  <_ 
-u ( Re `  ( F `  z ) ) ) ,  -u ( Re `  ( F `
 z ) ) ,  0 ) ) )  e.  RR )
155113, 154jca 532 . . . . . . . . 9  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( ( S.2 `  ( z  e.  RR  |->  if ( ( z  e. 
dom  F  /\  0  <_  ( Re `  ( F `  z )
) ) ,  ( Re `  ( F `
 z ) ) ,  0 ) ) )  e.  RR  /\  ( S.2 `  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  -u (
Re `  ( F `  z ) ) ) ,  -u ( Re `  ( F `  z ) ) ,  0 ) ) )  e.  RR ) )
15637imcld 13010 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  z  e.  dom  F )  -> 
( Im `  ( F `  z )
)  e.  RR )
157156rexrd 9646 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  z  e.  dom  F )  -> 
( Im `  ( F `  z )
)  e.  RR* )
158157adantrr 716 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  (
z  e.  dom  F  /\  0  <_  ( Im
`  ( F `  z ) ) ) )  ->  ( Im `  ( F `  z
) )  e.  RR* )
159 simprr 757 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  (
z  e.  dom  F  /\  0  <_  ( Im
`  ( F `  z ) ) ) )  ->  0  <_  ( Im `  ( F `
 z ) ) )
160 elxrge0 11640 . . . . . . . . . . . . . 14  |-  ( ( Im `  ( F `
 z ) )  e.  ( 0 [,] +oo )  <->  ( ( Im
`  ( F `  z ) )  e. 
RR*  /\  0  <_  ( Im `  ( F `
 z ) ) ) )
161158, 159, 160sylanbrc 664 . . . . . . . . . . . . 13  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  (
z  e.  dom  F  /\  0  <_  ( Im
`  ( F `  z ) ) ) )  ->  ( Im `  ( F `  z
) )  e.  ( 0 [,] +oo )
)
16244a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  -.  (
z  e.  dom  F  /\  0  <_  ( Im
`  ( F `  z ) ) ) )  ->  0  e.  ( 0 [,] +oo ) )
163161, 162ifclda 3958 . . . . . . . . . . . 12  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  RR )  ->  if ( ( z  e.  dom  F  /\  0  <_  ( Im
`  ( F `  z ) ) ) ,  ( Im `  ( F `  z ) ) ,  0 )  e.  ( 0 [,] +oo ) )
164 eqid 2443 . . . . . . . . . . . 12  |-  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  (
Im `  ( F `  z ) ) ) ,  ( Im `  ( F `  z ) ) ,  0 ) )  =  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  (
Im `  ( F `  z ) ) ) ,  ( Im `  ( F `  z ) ) ,  0 ) )
165163, 164fmptd 6040 . . . . . . . . . . 11  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  ( Im
`  ( F `  z ) ) ) ,  ( Im `  ( F `  z ) ) ,  0 ) ) : RR --> ( 0 [,] +oo ) )
166 ifan 3972 . . . . . . . . . . . . . . 15  |-  if ( ( z  e.  dom  F  /\  0  <_  (
Im `  ( F `  z ) ) ) ,  ( Im `  ( F `  z ) ) ,  0 )  =  if ( z  e.  dom  F ,  if ( 0  <_  (
Im `  ( F `  z ) ) ,  ( Im `  ( F `  z )
) ,  0 ) ,  0 )
16772imcld 13010 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  ( Im `  ( F `  z
) )  e.  RR )
168167recnd 9625 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  ( Im `  ( F `  z
) )  e.  CC )
169168abscld 13249 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  ( abs `  ( Im `  ( F `  z )
) )  e.  RR )
170167leabsd 13228 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  ( Im `  ( F `  z
) )  <_  ( abs `  ( Im `  ( F `  z ) ) ) )
171 absimle 13124 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F `  z )  e.  CC  ->  ( abs `  ( Im `  ( F `  z ) ) )  <_  ( abs `  ( F `  z ) ) )
17272, 171syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  ( abs `  ( Im `  ( F `  z )
) )  <_  ( abs `  ( F `  z ) ) )
173167, 169, 74, 170, 172letrd 9742 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  ( Im `  ( F `  z
) )  <_  ( abs `  ( F `  z ) ) )
174167, 74, 75, 173, 82letrd 9742 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  ( Im `  ( F `  z
) )  <_  x
)
175 breq1 4440 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( Im `  ( F `
 z ) )  =  if ( 0  <_  ( Im `  ( F `  z ) ) ,  ( Im
`  ( F `  z ) ) ,  0 )  ->  (
( Im `  ( F `  z )
)  <_  x  <->  if (
0  <_  ( Im `  ( F `  z
) ) ,  ( Im `  ( F `
 z ) ) ,  0 )  <_  x ) )
176 breq1 4440 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  =  if ( 0  <_  ( Im `  ( F `  z ) ) ,  ( Im
`  ( F `  z ) ) ,  0 )  ->  (
0  <_  x  <->  if (
0  <_  ( Im `  ( F `  z
) ) ,  ( Im `  ( F `
 z ) ) ,  0 )  <_  x ) )
177175, 176ifboth 3962 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( Im `  ( F `  z )
)  <_  x  /\  0  <_  x )  ->  if ( 0  <_  (
Im `  ( F `  z ) ) ,  ( Im `  ( F `  z )
) ,  0 )  <_  x )
178174, 85, 177syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  if (
0  <_  ( Im `  ( F `  z
) ) ,  ( Im `  ( F `
 z ) ) ,  0 )  <_  x )
179 iftrue 3932 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  dom  F  ->  if ( z  e.  dom  F ,  if ( 0  <_  ( Im `  ( F `  z ) ) ,  ( Im
`  ( F `  z ) ) ,  0 ) ,  0 )  =  if ( 0  <_  ( Im `  ( F `  z
) ) ,  ( Im `  ( F `
 z ) ) ,  0 ) )
180179adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  if (
z  e.  dom  F ,  if ( 0  <_ 
( Im `  ( F `  z )
) ,  ( Im
`  ( F `  z ) ) ,  0 ) ,  0 )  =  if ( 0  <_  ( Im `  ( F `  z
) ) ,  ( Im `  ( F `
 z ) ) ,  0 ) )
181178, 180, 933brtr4d 4467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  if (
z  e.  dom  F ,  if ( 0  <_ 
( Im `  ( F `  z )
) ,  ( Im
`  ( F `  z ) ) ,  0 ) ,  0 )  <_  if (
z  e.  dom  F ,  x ,  0 ) )
182181ex 434 . . . . . . . . . . . . . . . 16  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( z  e. 
dom  F  ->  if ( z  e.  dom  F ,  if ( 0  <_ 
( Im `  ( F `  z )
) ,  ( Im
`  ( F `  z ) ) ,  0 ) ,  0 )  <_  if (
z  e.  dom  F ,  x ,  0 ) ) )
183 iffalse 3935 . . . . . . . . . . . . . . . . 17  |-  ( -.  z  e.  dom  F  ->  if ( z  e. 
dom  F ,  if ( 0  <_  (
Im `  ( F `  z ) ) ,  ( Im `  ( F `  z )
) ,  0 ) ,  0 )  =  0 )
18497, 183, 993brtr4d 4467 . . . . . . . . . . . . . . . 16  |-  ( -.  z  e.  dom  F  ->  if ( z  e. 
dom  F ,  if ( 0  <_  (
Im `  ( F `  z ) ) ,  ( Im `  ( F `  z )
) ,  0 ) ,  0 )  <_  if ( z  e.  dom  F ,  x ,  0 ) )
185182, 184pm2.61d1 159 . . . . . . . . . . . . . . 15  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  if ( z  e.  dom  F ,  if ( 0  <_  (
Im `  ( F `  z ) ) ,  ( Im `  ( F `  z )
) ,  0 ) ,  0 )  <_  if ( z  e.  dom  F ,  x ,  0 ) )
186166, 185syl5eqbr 4470 . . . . . . . . . . . . . 14  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  if ( ( z  e.  dom  F  /\  0  <_  ( Im
`  ( F `  z ) ) ) ,  ( Im `  ( F `  z ) ) ,  0 )  <_  if ( z  e.  dom  F ,  x ,  0 ) )
187186ralrimivw 2858 . . . . . . . . . . . . 13  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  A. z  e.  RR  if ( ( z  e. 
dom  F  /\  0  <_  ( Im `  ( F `  z )
) ) ,  ( Im `  ( F `
 z ) ) ,  0 )  <_  if ( z  e.  dom  F ,  x ,  0 ) )
188 eqidd 2444 . . . . . . . . . . . . . 14  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  ( Im
`  ( F `  z ) ) ) ,  ( Im `  ( F `  z ) ) ,  0 ) )  =  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  (
Im `  ( F `  z ) ) ) ,  ( Im `  ( F `  z ) ) ,  0 ) ) )
189105, 163, 67, 188, 107ofrfval2 6542 . . . . . . . . . . . . 13  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  (
Im `  ( F `  z ) ) ) ,  ( Im `  ( F `  z ) ) ,  0 ) )  oR  <_ 
( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) )  <->  A. z  e.  RR  if ( ( z  e.  dom  F  /\  0  <_  ( Im
`  ( F `  z ) ) ) ,  ( Im `  ( F `  z ) ) ,  0 )  <_  if ( z  e.  dom  F ,  x ,  0 ) ) )
190187, 189mpbird 232 . . . . . . . . . . . 12  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  ( Im
`  ( F `  z ) ) ) ,  ( Im `  ( F `  z ) ) ,  0 ) )  oR  <_ 
( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) )
191 itg2le 22124 . . . . . . . . . . . 12  |-  ( ( ( z  e.  RR  |->  if ( ( z  e. 
dom  F  /\  0  <_  ( Im `  ( F `  z )
) ) ,  ( Im `  ( F `
 z ) ) ,  0 ) ) : RR --> ( 0 [,] +oo )  /\  ( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) : RR --> ( 0 [,] +oo )  /\  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  ( Im
`  ( F `  z ) ) ) ,  ( Im `  ( F `  z ) ) ,  0 ) )  oR  <_ 
( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) )  -> 
( S.2 `  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  (
Im `  ( F `  z ) ) ) ,  ( Im `  ( F `  z ) ) ,  0 ) ) )  <_  ( S.2 `  ( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) ) )
192165, 69, 190, 191syl3anc 1229 . . . . . . . . . . 11  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( S.2 `  (
z  e.  RR  |->  if ( ( z  e. 
dom  F  /\  0  <_  ( Im `  ( F `  z )
) ) ,  ( Im `  ( F `
 z ) ) ,  0 ) ) )  <_  ( S.2 `  ( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) ) )
193 itg2lecl 22123 . . . . . . . . . . 11  |-  ( ( ( z  e.  RR  |->  if ( ( z  e. 
dom  F  /\  0  <_  ( Im `  ( F `  z )
) ) ,  ( Im `  ( F `
 z ) ) ,  0 ) ) : RR --> ( 0 [,] +oo )  /\  ( S.2 `  ( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) )  e.  RR  /\  ( S.2 `  (
z  e.  RR  |->  if ( ( z  e. 
dom  F  /\  0  <_  ( Im `  ( F `  z )
) ) ,  ( Im `  ( F `
 z ) ) ,  0 ) ) )  <_  ( S.2 `  ( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) ) )  ->  ( S.2 `  (
z  e.  RR  |->  if ( ( z  e. 
dom  F  /\  0  <_  ( Im `  ( F `  z )
) ) ,  ( Im `  ( F `
 z ) ) ,  0 ) ) )  e.  RR )
194165, 59, 192, 193syl3anc 1229 . . . . . . . . . 10  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( S.2 `  (
z  e.  RR  |->  if ( ( z  e. 
dom  F  /\  0  <_  ( Im `  ( F `  z )
) ) ,  ( Im `  ( F `
 z ) ) ,  0 ) ) )  e.  RR )
195156renegcld 9993 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  z  e.  dom  F )  ->  -u ( Im `  ( F `  z )
)  e.  RR )
196195rexrd 9646 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  z  e.  dom  F )  ->  -u ( Im `  ( F `  z )
)  e.  RR* )
197196adantrr 716 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  (
z  e.  dom  F  /\  0  <_  -u (
Im `  ( F `  z ) ) ) )  ->  -u ( Im
`  ( F `  z ) )  e. 
RR* )
198 simprr 757 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  (
z  e.  dom  F  /\  0  <_  -u (
Im `  ( F `  z ) ) ) )  ->  0  <_  -u ( Im `  ( F `
 z ) ) )
199 elxrge0 11640 . . . . . . . . . . . . . 14  |-  ( -u ( Im `  ( F `
 z ) )  e.  ( 0 [,] +oo )  <->  ( -u (
Im `  ( F `  z ) )  e. 
RR*  /\  0  <_  -u ( Im `  ( F `
 z ) ) ) )
200197, 198, 199sylanbrc 664 . . . . . . . . . . . . 13  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  (
z  e.  dom  F  /\  0  <_  -u (
Im `  ( F `  z ) ) ) )  ->  -u ( Im
`  ( F `  z ) )  e.  ( 0 [,] +oo ) )
20144a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ( ( F  e. MblFn  /\  ( vol ` 
dom  F )  e.  RR )  /\  (
( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `  y )
)  <_  x )
)  /\  z  e.  RR )  /\  -.  (
z  e.  dom  F  /\  0  <_  -u (
Im `  ( F `  z ) ) ) )  ->  0  e.  ( 0 [,] +oo ) )
202200, 201ifclda 3958 . . . . . . . . . . . 12  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  RR )  ->  if ( ( z  e.  dom  F  /\  0  <_  -u (
Im `  ( F `  z ) ) ) ,  -u ( Im `  ( F `  z ) ) ,  0 )  e.  ( 0 [,] +oo ) )
203 eqid 2443 . . . . . . . . . . . 12  |-  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  -u (
Im `  ( F `  z ) ) ) ,  -u ( Im `  ( F `  z ) ) ,  0 ) )  =  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  -u (
Im `  ( F `  z ) ) ) ,  -u ( Im `  ( F `  z ) ) ,  0 ) )
204202, 203fmptd 6040 . . . . . . . . . . 11  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  -u (
Im `  ( F `  z ) ) ) ,  -u ( Im `  ( F `  z ) ) ,  0 ) ) : RR --> ( 0 [,] +oo ) )
205 ifan 3972 . . . . . . . . . . . . . . 15  |-  if ( ( z  e.  dom  F  /\  0  <_  -u (
Im `  ( F `  z ) ) ) ,  -u ( Im `  ( F `  z ) ) ,  0 )  =  if ( z  e.  dom  F ,  if ( 0  <_  -u (
Im `  ( F `  z ) ) , 
-u ( Im `  ( F `  z ) ) ,  0 ) ,  0 )
206167renegcld 9993 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  -u ( Im
`  ( F `  z ) )  e.  RR )
207206leabsd 13228 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  -u ( Im
`  ( F `  z ) )  <_ 
( abs `  -u (
Im `  ( F `  z ) ) ) )
208168absnegd 13262 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  ( abs `  -u ( Im `  ( F `  z )
) )  =  ( abs `  ( Im
`  ( F `  z ) ) ) )
209207, 208breqtrd 4461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  -u ( Im
`  ( F `  z ) )  <_ 
( abs `  (
Im `  ( F `  z ) ) ) )
210206, 169, 74, 209, 172letrd 9742 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  -u ( Im
`  ( F `  z ) )  <_ 
( abs `  ( F `  z )
) )
211206, 74, 75, 210, 82letrd 9742 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  -u ( Im
`  ( F `  z ) )  <_  x )
212 breq1 4440 . . . . . . . . . . . . . . . . . . . 20  |-  ( -u ( Im `  ( F `
 z ) )  =  if ( 0  <_  -u ( Im `  ( F `  z ) ) ,  -u (
Im `  ( F `  z ) ) ,  0 )  ->  ( -u ( Im `  ( F `  z )
)  <_  x  <->  if (
0  <_  -u ( Im
`  ( F `  z ) ) , 
-u ( Im `  ( F `  z ) ) ,  0 )  <_  x ) )
213 breq1 4440 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  =  if ( 0  <_  -u ( Im `  ( F `  z ) ) ,  -u (
Im `  ( F `  z ) ) ,  0 )  ->  (
0  <_  x  <->  if (
0  <_  -u ( Im
`  ( F `  z ) ) , 
-u ( Im `  ( F `  z ) ) ,  0 )  <_  x ) )
214212, 213ifboth 3962 . . . . . . . . . . . . . . . . . . 19  |-  ( (
-u ( Im `  ( F `  z ) )  <_  x  /\  0  <_  x )  ->  if ( 0  <_  -u (
Im `  ( F `  z ) ) , 
-u ( Im `  ( F `  z ) ) ,  0 )  <_  x )
215211, 85, 214syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  if (
0  <_  -u ( Im
`  ( F `  z ) ) , 
-u ( Im `  ( F `  z ) ) ,  0 )  <_  x )
216 iftrue 3932 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  dom  F  ->  if ( z  e.  dom  F ,  if ( 0  <_  -u ( Im `  ( F `  z ) ) ,  -u (
Im `  ( F `  z ) ) ,  0 ) ,  0 )  =  if ( 0  <_  -u ( Im
`  ( F `  z ) ) , 
-u ( Im `  ( F `  z ) ) ,  0 ) )
217216adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  if (
z  e.  dom  F ,  if ( 0  <_  -u ( Im `  ( F `  z )
) ,  -u (
Im `  ( F `  z ) ) ,  0 ) ,  0 )  =  if ( 0  <_  -u ( Im
`  ( F `  z ) ) , 
-u ( Im `  ( F `  z ) ) ,  0 ) )
218215, 217, 933brtr4d 4467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  /\  z  e.  dom  F )  ->  if (
z  e.  dom  F ,  if ( 0  <_  -u ( Im `  ( F `  z )
) ,  -u (
Im `  ( F `  z ) ) ,  0 ) ,  0 )  <_  if (
z  e.  dom  F ,  x ,  0 ) )
219218ex 434 . . . . . . . . . . . . . . . 16  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( z  e. 
dom  F  ->  if ( z  e.  dom  F ,  if ( 0  <_  -u ( Im `  ( F `  z )
) ,  -u (
Im `  ( F `  z ) ) ,  0 ) ,  0 )  <_  if (
z  e.  dom  F ,  x ,  0 ) ) )
220 iffalse 3935 . . . . . . . . . . . . . . . . 17  |-  ( -.  z  e.  dom  F  ->  if ( z  e. 
dom  F ,  if ( 0  <_  -u (
Im `  ( F `  z ) ) , 
-u ( Im `  ( F `  z ) ) ,  0 ) ,  0 )  =  0 )
22197, 220, 993brtr4d 4467 . . . . . . . . . . . . . . . 16  |-  ( -.  z  e.  dom  F  ->  if ( z  e. 
dom  F ,  if ( 0  <_  -u (
Im `  ( F `  z ) ) , 
-u ( Im `  ( F `  z ) ) ,  0 ) ,  0 )  <_  if ( z  e.  dom  F ,  x ,  0 ) )
222219, 221pm2.61d1 159 . . . . . . . . . . . . . . 15  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  if ( z  e.  dom  F ,  if ( 0  <_  -u (
Im `  ( F `  z ) ) , 
-u ( Im `  ( F `  z ) ) ,  0 ) ,  0 )  <_  if ( z  e.  dom  F ,  x ,  0 ) )
223205, 222syl5eqbr 4470 . . . . . . . . . . . . . 14  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  if ( ( z  e.  dom  F  /\  0  <_  -u (
Im `  ( F `  z ) ) ) ,  -u ( Im `  ( F `  z ) ) ,  0 )  <_  if ( z  e.  dom  F ,  x ,  0 ) )
224223ralrimivw 2858 . . . . . . . . . . . . 13  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  A. z  e.  RR  if ( ( z  e. 
dom  F  /\  0  <_ 
-u ( Im `  ( F `  z ) ) ) ,  -u ( Im `  ( F `
 z ) ) ,  0 )  <_  if ( z  e.  dom  F ,  x ,  0 ) )
225 eqidd 2444 . . . . . . . . . . . . . 14  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  -u (
Im `  ( F `  z ) ) ) ,  -u ( Im `  ( F `  z ) ) ,  0 ) )  =  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  -u (
Im `  ( F `  z ) ) ) ,  -u ( Im `  ( F `  z ) ) ,  0 ) ) )
226105, 202, 67, 225, 107ofrfval2 6542 . . . . . . . . . . . . 13  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  -u (
Im `  ( F `  z ) ) ) ,  -u ( Im `  ( F `  z ) ) ,  0 ) )  oR  <_ 
( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) )  <->  A. z  e.  RR  if ( ( z  e.  dom  F  /\  0  <_  -u (
Im `  ( F `  z ) ) ) ,  -u ( Im `  ( F `  z ) ) ,  0 )  <_  if ( z  e.  dom  F ,  x ,  0 ) ) )
227224, 226mpbird 232 . . . . . . . . . . . 12  |-  ( ( ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR )  /\  ( ( x  e.  RR  /\  0  <_  x )  /\  A. y  e.  dom  F ( abs `  ( F `
 y ) )  <_  x ) )  ->  ( z  e.  RR  |->  if ( ( z  e.  dom  F  /\  0  <_  -u (
Im `  ( F `  z ) ) ) ,  -u ( Im `  ( F `  z ) ) ,  0 ) )  oR  <_ 
( z  e.  RR  |->  if ( z  e.  dom  F ,  x ,  0 ) ) )
228 itg2le 22124 . . . . . . . . . . . 12  |-  ( ( ( z  e.  RR  |->  if ( ( z  e. 
dom  F  /\  0  <_ 
-u ( Im `  ( F `  z