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

Metamath Proof Explorer

Theorem bddiblnc

Description: Choice-free proof of bddibl . (Contributed by Brendan Leahy, 2-Nov-2017) (Revised by Brendan Leahy, 6-Nov-2017)

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

Proof

Step Hyp Ref Expression
1 mbff 
 |-  ( F e. MblFn -> F : dom F --> CC )
2 1 feqmptd 
 |-  ( F e. MblFn -> F = ( z e. dom F |-> ( F ` z ) ) )
3 2 3ad2ant1 
 |-  ( ( 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 
 |-  ( dom F = (/) -> A. z e. dom F ( F ` z ) = 0 )
5 mpteq12 
 |-  ( ( dom F = (/) /\ A. z e. dom F ( F ` z ) = 0 ) -> ( z e. dom F |-> ( F ` z ) ) = ( z e. (/) |-> 0 ) )
6 4 5 mpdan 
 |-  ( dom F = (/) -> ( z e. dom F |-> ( F ` z ) ) = ( z e. (/) |-> 0 ) )
7 fconstmpt 
 |-  ( (/) X. { 0 } ) = ( z e. (/) |-> 0 )
8 0mbl 
 |-  (/) e. dom vol
9 ibl0 
 |-  ( (/) e. dom vol -> ( (/) X. { 0 } ) e. L^1 )
10 8 9 ax-mp 
 |-  ( (/) X. { 0 } ) e. L^1
11 7 10 eqeltrri 
 |-  ( z e. (/) |-> 0 ) e. L^1
12 6 11 eqeltrdi 
 |-  ( dom F = (/) -> ( z e. dom F |-> ( F ` z ) ) e. L^1 )
13 12 adantl 
 |-  ( ( ( ( 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 
 |-  ( ( dom F =/= (/) /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) -> E. y e. dom F ( abs ` ( F ` y ) ) <_ x )
15 14 anim1i 
 |-  ( ( ( 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 ) )
16 15 an31s 
 |-  ( ( ( 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 ) )
17 1 ad2antrr 
 |-  ( ( ( F e. MblFn /\ ( vol ` dom F ) e. RR ) /\ x e. RR ) -> F : dom F --> CC )
18 17 ffvelcdmda 
 |-  ( ( ( ( F e. MblFn /\ ( vol ` dom F ) e. RR ) /\ x e. RR ) /\ y e. dom F ) -> ( F ` y ) e. CC )
19 18 absge0d 
 |-  ( ( ( ( F e. MblFn /\ ( vol ` dom F ) e. RR ) /\ x e. RR ) /\ y e. dom F ) -> 0 <_ ( abs ` ( F ` y ) ) )
20 0red 
 |-  ( ( ( ( F e. MblFn /\ ( vol ` dom F ) e. RR ) /\ x e. RR ) /\ y e. dom F ) -> 0 e. RR )
21 18 abscld 
 |-  ( ( ( ( F e. MblFn /\ ( vol ` dom F ) e. RR ) /\ x e. RR ) /\ y e. dom F ) -> ( abs ` ( F ` y ) ) e. RR )
22 simplr 
 |-  ( ( ( ( F e. MblFn /\ ( vol ` dom F ) e. RR ) /\ x e. RR ) /\ y e. dom F ) -> x e. RR )
23 letr 
 |-  ( ( 0 e. RR /\ ( abs ` ( F ` y ) ) e. RR /\ x e. RR ) -> ( ( 0 <_ ( abs ` ( F ` y ) ) /\ ( abs ` ( F ` y ) ) <_ x ) -> 0 <_ x ) )
24 20 21 22 23 syl3anc 
 |-  ( ( ( ( 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 ) )
25 19 24 mpand 
 |-  ( ( ( ( F e. MblFn /\ ( vol ` dom F ) e. RR ) /\ x e. RR ) /\ y e. dom F ) -> ( ( abs ` ( F ` y ) ) <_ x -> 0 <_ x ) )
26 25 rexlimdva 
 |-  ( ( ( F e. MblFn /\ ( vol ` dom F ) e. RR ) /\ x e. RR ) -> ( E. y e. dom F ( abs ` ( F ` y ) ) <_ x -> 0 <_ x ) )
27 26 ex 
 |-  ( ( F e. MblFn /\ ( vol ` dom F ) e. RR ) -> ( x e. RR -> ( E. y e. dom F ( abs ` ( F ` y ) ) <_ x -> 0 <_ x ) ) )
28 27 com23 
 |-  ( ( F e. MblFn /\ ( vol ` dom F ) e. RR ) -> ( E. y e. dom F ( abs ` ( F ` y ) ) <_ x -> ( x e. RR -> 0 <_ x ) ) )
29 28 imp32 
 |-  ( ( ( F e. MblFn /\ ( vol ` dom F ) e. RR ) /\ ( E. y e. dom F ( abs ` ( F ` y ) ) <_ x /\ x e. RR ) ) -> 0 <_ x )
30 16 29 sylan2 
 |-  ( ( ( F e. MblFn /\ ( vol ` dom F ) e. RR ) /\ ( ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) /\ dom F =/= (/) ) ) -> 0 <_ x )
31 30 anassrs 
 |-  ( ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( F e. MblFn -> F e. MblFn )
34 2 33 eqeltrrd 
 |-  ( F e. MblFn -> ( z e. dom F |-> ( F ` z ) ) e. MblFn )
35 34 ad2antrr 
 |-  ( ( ( 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 )
36 1 ad3antrrr 
 |-  ( ( ( ( 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 )
37 36 ffvelcdmda 
 |-  ( ( ( ( ( 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 )
38 37 recld 
 |-  ( ( ( ( ( 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 )
39 38 rexrd 
 |-  ( ( ( ( ( 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* )
40 39 adantrr 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( Re ` ( F ` z ) ) e. ( 0 [,] +oo ) <-> ( ( Re ` ( F ` z ) ) e. RR* /\ 0 <_ ( Re ` ( F ` z ) ) ) )
43 40 41 42 sylanbrc 
 |-  ( ( ( ( ( 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 
 |-  0 e. ( 0 [,] +oo )
45 44 a1i 
 |-  ( ( ( ( ( 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 ) )
46 43 45 ifclda 
 |-  ( ( ( ( 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 46 fmpttd 
 |-  ( ( ( 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 ) )
48 mbfdm 
 |-  ( F e. MblFn -> dom F e. dom vol )
49 48 ad2antrr 
 |-  ( ( ( 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 )
50 simplr 
 |-  ( ( ( 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 )
51 elrege0 
 |-  ( x e. ( 0 [,) +oo ) <-> ( x e. RR /\ 0 <_ x ) )
52 51 biimpri 
 |-  ( ( x e. RR /\ 0 <_ x ) -> x e. ( 0 [,) +oo ) )
53 52 ad2antrl 
 |-  ( ( ( 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 ) )
54 itg2const 
 |-  ( ( 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 ) ) )
55 49 50 53 54 syl3anc 
 |-  ( ( ( 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 ) ) )
56 simprll 
 |-  ( ( ( 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 )
57 56 50 remulcld 
 |-  ( ( ( 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 )
58 55 57 eqeltrd 
 |-  ( ( ( 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 )
59 rexr 
 |-  ( x e. RR -> x e. RR* )
60 elxrge0 
 |-  ( x e. ( 0 [,] +oo ) <-> ( x e. RR* /\ 0 <_ x ) )
61 60 biimpri 
 |-  ( ( x e. RR* /\ 0 <_ x ) -> x e. ( 0 [,] +oo ) )
62 59 61 sylan 
 |-  ( ( x e. RR /\ 0 <_ x ) -> x e. ( 0 [,] +oo ) )
63 62 ad2antrl 
 |-  ( ( ( 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 ) )
64 63 adantr 
 |-  ( ( ( ( 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 ) )
65 ifcl 
 |-  ( ( x e. ( 0 [,] +oo ) /\ 0 e. ( 0 [,] +oo ) ) -> if ( z e. dom F , x , 0 ) e. ( 0 [,] +oo ) )
66 64 44 65 sylancl 
 |-  ( ( ( ( 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 ) )
67 66 fmpttd 
 |-  ( ( ( 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 ) )
68 ifan 
 |-  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 )
69 1 ad2antrr 
 |-  ( ( ( 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 )
70 69 ffvelcdmda 
 |-  ( ( ( ( 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 )
71 70 recld 
 |-  ( ( ( ( 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 )
72 70 abscld 
 |-  ( ( ( ( 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 )
73 56 adantr 
 |-  ( ( ( ( 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 )
74 70 releabsd 
 |-  ( ( ( ( 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 ) ) )
75 2fveq3 
 |-  ( y = z -> ( abs ` ( F ` y ) ) = ( abs ` ( F ` z ) ) )
76 75 breq1d 
 |-  ( y = z -> ( ( abs ` ( F ` y ) ) <_ x <-> ( abs ` ( F ` z ) ) <_ x ) )
77 76 rspccva 
 |-  ( ( A. y e. dom F ( abs ` ( F ` y ) ) <_ x /\ z e. dom F ) -> ( abs ` ( F ` z ) ) <_ x )
78 77 adantll 
 |-  ( ( ( ( x e. RR /\ 0 <_ x ) /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) /\ z e. dom F ) -> ( abs ` ( F ` z ) ) <_ x )
79 78 adantll 
 |-  ( ( ( ( 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 )
80 71 72 73 74 79 letrd 
 |-  ( ( ( ( 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 )
81 simprlr 
 |-  ( ( ( F e. MblFn /\ ( vol ` dom F ) e. RR ) /\ ( ( x e. RR /\ 0 <_ x ) /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> 0 <_ x )
82 81 adantr 
 |-  ( ( ( ( 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 )
83 breq1 
 |-  ( ( 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 ) )
84 breq1 
 |-  ( 0 = if ( 0 <_ ( Re ` ( F ` z ) ) , ( Re ` ( F ` z ) ) , 0 ) -> ( 0 <_ x <-> if ( 0 <_ ( Re ` ( F ` z ) ) , ( Re ` ( F ` z ) ) , 0 ) <_ x ) )
85 83 84 ifboth 
 |-  ( ( ( Re ` ( F ` z ) ) <_ x /\ 0 <_ x ) -> if ( 0 <_ ( Re ` ( F ` z ) ) , ( Re ` ( F ` z ) ) , 0 ) <_ x )
86 80 82 85 syl2anc 
 |-  ( ( ( ( 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 )
87 iftrue 
 |-  ( 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 ) )
88 87 adantl 
 |-  ( ( ( ( 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 ) )
89 iftrue 
 |-  ( z e. dom F -> if ( z e. dom F , x , 0 ) = x )
90 89 adantl 
 |-  ( ( ( ( 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 )
91 86 88 90 3brtr4d 
 |-  ( ( ( ( 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 ) )
92 91 ex 
 |-  ( ( ( 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 ) ) )
93 0le0 
 |-  0 <_ 0
94 93 a1i 
 |-  ( -. z e. dom F -> 0 <_ 0 )
95 iffalse 
 |-  ( -. z e. dom F -> if ( z e. dom F , if ( 0 <_ ( Re ` ( F ` z ) ) , ( Re ` ( F ` z ) ) , 0 ) , 0 ) = 0 )
96 iffalse 
 |-  ( -. z e. dom F -> if ( z e. dom F , x , 0 ) = 0 )
97 94 95 96 3brtr4d 
 |-  ( -. 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 ) )
98 92 97 pm2.61d1 
 |-  ( ( ( 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 ) )
99 68 98 eqbrtrid 
 |-  ( ( ( 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 ) )
100 99 ralrimivw 
 |-  ( ( ( 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 ) )
101 reex 
 |-  RR e. _V
102 101 a1i 
 |-  ( ( ( 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 )
103 eqidd 
 |-  ( ( ( 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 ) ) )
104 eqidd 
 |-  ( ( ( 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 ) ) )
105 102 46 66 103 104 ofrfval2 
 |-  ( ( ( 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 ) ) )
106 100 105 mpbird 
 |-  ( ( ( 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 ) ) )
107 itg2le 
 |-  ( ( ( 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 ) ) ) )
108 47 67 106 107 syl3anc 
 |-  ( ( ( 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 ) ) ) )
109 itg2lecl 
 |-  ( ( ( 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 )
110 47 58 108 109 syl3anc 
 |-  ( ( ( 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 )
111 38 renegcld 
 |-  ( ( ( ( ( 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 )
112 111 rexrd 
 |-  ( ( ( ( ( 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* )
113 112 adantrr 
 |-  ( ( ( ( ( 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* )
114 simprr 
 |-  ( ( ( ( ( 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 ) ) )
115 elxrge0 
 |-  ( -u ( Re ` ( F ` z ) ) e. ( 0 [,] +oo ) <-> ( -u ( Re ` ( F ` z ) ) e. RR* /\ 0 <_ -u ( Re ` ( F ` z ) ) ) )
116 113 114 115 sylanbrc 
 |-  ( ( ( ( ( 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 ) )
117 44 a1i 
 |-  ( ( ( ( ( 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 ) )
118 116 117 ifclda 
 |-  ( ( ( ( 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 ) )
119 118 fmpttd 
 |-  ( ( ( 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 ) )
120 ifan 
 |-  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 )
121 71 renegcld 
 |-  ( ( ( ( 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 )
122 71 recnd 
 |-  ( ( ( ( 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 )
123 122 abscld 
 |-  ( ( ( ( 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 )
124 121 leabsd 
 |-  ( ( ( ( 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 ) ) ) )
125 122 absnegd 
 |-  ( ( ( ( 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 ) ) ) )
126 124 125 breqtrd 
 |-  ( ( ( ( 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 ) ) ) )
127 absrele 
 |-  ( ( F ` z ) e. CC -> ( abs ` ( Re ` ( F ` z ) ) ) <_ ( abs ` ( F ` z ) ) )
128 70 127 syl 
 |-  ( ( ( ( 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 ) ) )
129 121 123 72 126 128 letrd 
 |-  ( ( ( ( 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 ) ) )
130 121 72 73 129 79 letrd 
 |-  ( ( ( ( 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 )
131 breq1 
 |-  ( -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 ) )
132 breq1 
 |-  ( 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 ) )
133 131 132 ifboth 
 |-  ( ( -u ( Re ` ( F ` z ) ) <_ x /\ 0 <_ x ) -> if ( 0 <_ -u ( Re ` ( F ` z ) ) , -u ( Re ` ( F ` z ) ) , 0 ) <_ x )
134 130 82 133 syl2anc 
 |-  ( ( ( ( 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 )
135 iftrue 
 |-  ( 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 ) )
136 135 adantl 
 |-  ( ( ( ( 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 ) )
137 134 136 90 3brtr4d 
 |-  ( ( ( ( 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 ) )
138 137 ex 
 |-  ( ( ( 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 ) ) )
139 iffalse 
 |-  ( -. z e. dom F -> if ( z e. dom F , if ( 0 <_ -u ( Re ` ( F ` z ) ) , -u ( Re ` ( F ` z ) ) , 0 ) , 0 ) = 0 )
140 94 139 96 3brtr4d 
 |-  ( -. 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 ) )
141 138 140 pm2.61d1 
 |-  ( ( ( 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 ) )
142 120 141 eqbrtrid 
 |-  ( ( ( 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 ) )
143 142 ralrimivw 
 |-  ( ( ( 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 ) )
144 eqidd 
 |-  ( ( ( 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 ) ) )
145 102 118 66 144 104 ofrfval2 
 |-  ( ( ( 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 ) ) )
146 143 145 mpbird 
 |-  ( ( ( 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 ) ) )
147 itg2le 
 |-  ( ( ( 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 ) ) ) )
148 119 67 146 147 syl3anc 
 |-  ( ( ( 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 ) ) ) )
149 itg2lecl 
 |-  ( ( ( 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 )
150 119 58 148 149 syl3anc 
 |-  ( ( ( 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 )
151 110 150 jca 
 |-  ( ( ( 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 ) )
152 37 imcld 
 |-  ( ( ( ( ( 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 )
153 152 rexrd 
 |-  ( ( ( ( ( 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* )
154 153 adantrr 
 |-  ( ( ( ( ( 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* )
155 simprr 
 |-  ( ( ( ( ( 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 ) ) )
156 elxrge0 
 |-  ( ( Im ` ( F ` z ) ) e. ( 0 [,] +oo ) <-> ( ( Im ` ( F ` z ) ) e. RR* /\ 0 <_ ( Im ` ( F ` z ) ) ) )
157 154 155 156 sylanbrc 
 |-  ( ( ( ( ( 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 ) )
158 44 a1i 
 |-  ( ( ( ( ( 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 ) )
159 157 158 ifclda 
 |-  ( ( ( ( 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 ) )
160 159 fmpttd 
 |-  ( ( ( 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 ) )
161 ifan 
 |-  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 )
162 70 imcld 
 |-  ( ( ( ( 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 )
163 162 recnd 
 |-  ( ( ( ( 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 )
164 163 abscld 
 |-  ( ( ( ( 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 )
165 162 leabsd 
 |-  ( ( ( ( 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 ) ) ) )
166 absimle 
 |-  ( ( F ` z ) e. CC -> ( abs ` ( Im ` ( F ` z ) ) ) <_ ( abs ` ( F ` z ) ) )
167 70 166 syl 
 |-  ( ( ( ( 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 ) ) )
168 162 164 72 165 167 letrd 
 |-  ( ( ( ( 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 ) ) )
169 162 72 73 168 79 letrd 
 |-  ( ( ( ( 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 )
170 breq1 
 |-  ( ( 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 ) )
171 breq1 
 |-  ( 0 = if ( 0 <_ ( Im ` ( F ` z ) ) , ( Im ` ( F ` z ) ) , 0 ) -> ( 0 <_ x <-> if ( 0 <_ ( Im ` ( F ` z ) ) , ( Im ` ( F ` z ) ) , 0 ) <_ x ) )
172 170 171 ifboth 
 |-  ( ( ( Im ` ( F ` z ) ) <_ x /\ 0 <_ x ) -> if ( 0 <_ ( Im ` ( F ` z ) ) , ( Im ` ( F ` z ) ) , 0 ) <_ x )
173 169 82 172 syl2anc 
 |-  ( ( ( ( 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 )
174 iftrue 
 |-  ( 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 ) )
175 174 adantl 
 |-  ( ( ( ( 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 ) )
176 173 175 90 3brtr4d 
 |-  ( ( ( ( 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 ) )
177 176 ex 
 |-  ( ( ( 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 ) ) )
178 iffalse 
 |-  ( -. z e. dom F -> if ( z e. dom F , if ( 0 <_ ( Im ` ( F ` z ) ) , ( Im ` ( F ` z ) ) , 0 ) , 0 ) = 0 )
179 94 178 96 3brtr4d 
 |-  ( -. 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 ) )
180 177 179 pm2.61d1 
 |-  ( ( ( 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 ) )
181 161 180 eqbrtrid 
 |-  ( ( ( 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 ) )
182 181 ralrimivw 
 |-  ( ( ( 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 ) )
183 eqidd 
 |-  ( ( ( 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 ) ) )
184 102 159 66 183 104 ofrfval2 
 |-  ( ( ( 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 ) ) )
185 182 184 mpbird 
 |-  ( ( ( 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 ) ) )
186 itg2le 
 |-  ( ( ( 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 ) ) ) )
187 160 67 185 186 syl3anc 
 |-  ( ( ( 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 ) ) ) )
188 itg2lecl 
 |-  ( ( ( 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 )
189 160 58 187 188 syl3anc 
 |-  ( ( ( 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 )
190 152 renegcld 
 |-  ( ( ( ( ( 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 )
191 190 rexrd 
 |-  ( ( ( ( ( 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* )
192 191 adantrr 
 |-  ( ( ( ( ( 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* )
193 simprr 
 |-  ( ( ( ( ( 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 ) ) )
194 elxrge0 
 |-  ( -u ( Im ` ( F ` z ) ) e. ( 0 [,] +oo ) <-> ( -u ( Im ` ( F ` z ) ) e. RR* /\ 0 <_ -u ( Im ` ( F ` z ) ) ) )
195 192 193 194 sylanbrc 
 |-  ( ( ( ( ( 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 ) )
196 44 a1i 
 |-  ( ( ( ( ( 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 ) )
197 195 196 ifclda 
 |-  ( ( ( ( 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 ) )
198 197 fmpttd 
 |-  ( ( ( 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 ) )
199 ifan 
 |-  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 )
200 162 renegcld 
 |-  ( ( ( ( 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 )
201 200 leabsd 
 |-  ( ( ( ( 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 ) ) ) )
202 163 absnegd 
 |-  ( ( ( ( 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 ) ) ) )
203 201 202 breqtrd 
 |-  ( ( ( ( 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 ) ) ) )
204 200 164 72 203 167 letrd 
 |-  ( ( ( ( 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 ) ) )
205 200 72 73 204 79 letrd 
 |-  ( ( ( ( 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 )
206 breq1 
 |-  ( -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 ) )
207 breq1 
 |-  ( 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 ) )
208 206 207 ifboth 
 |-  ( ( -u ( Im ` ( F ` z ) ) <_ x /\ 0 <_ x ) -> if ( 0 <_ -u ( Im ` ( F ` z ) ) , -u ( Im ` ( F ` z ) ) , 0 ) <_ x )
209 205 82 208 syl2anc 
 |-  ( ( ( ( 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 )
210 iftrue 
 |-  ( 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 ) )
211 210 adantl 
 |-  ( ( ( ( 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 ) )
212 209 211 90 3brtr4d 
 |-  ( ( ( ( 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 ) )
213 212 ex 
 |-  ( ( ( 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 ) ) )
214 iffalse 
 |-  ( -. z e. dom F -> if ( z e. dom F , if ( 0 <_ -u ( Im ` ( F ` z ) ) , -u ( Im ` ( F ` z ) ) , 0 ) , 0 ) = 0 )
215 94 214 96 3brtr4d 
 |-  ( -. 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 ) )
216 213 215 pm2.61d1 
 |-  ( ( ( 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 ) )
217 199 216 eqbrtrid 
 |-  ( ( ( 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 ) )
218 217 ralrimivw 
 |-  ( ( ( 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 ) )
219 eqidd 
 |-  ( ( ( 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 ) ) )
220 102 197 66 219 104 ofrfval2 
 |-  ( ( ( 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 ) ) )
221 218 220 mpbird 
 |-  ( ( ( 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 ) ) )
222 itg2le 
 |-  ( ( ( z e. RR |-> if ( ( z e. dom F /\ 0 <_ -u ( Im ` ( F ` z ) ) ) , -u ( 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 <_ -u ( Im ` ( F ` z ) ) ) , -u ( 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 <_ -u ( Im ` ( F ` z ) ) ) , -u ( Im ` ( F ` z ) ) , 0 ) ) ) <_ ( S.2 ` ( z e. RR |-> if ( z e. dom F , x , 0 ) ) ) )
223 198 67 221 222 syl3anc 
 |-  ( ( ( 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 ( Im ` ( F ` z ) ) ) , -u ( Im ` ( F ` z ) ) , 0 ) ) ) <_ ( S.2 ` ( z e. RR |-> if ( z e. dom F , x , 0 ) ) ) )
224 itg2lecl 
 |-  ( ( ( z e. RR |-> if ( ( z e. dom F /\ 0 <_ -u ( Im ` ( F ` z ) ) ) , -u ( 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 <_ -u ( Im ` ( F ` z ) ) ) , -u ( 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 <_ -u ( Im ` ( F ` z ) ) ) , -u ( Im ` ( F ` z ) ) , 0 ) ) ) e. RR )
225 198 58 223 224 syl3anc 
 |-  ( ( ( 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 ( Im ` ( F ` z ) ) ) , -u ( Im ` ( F ` z ) ) , 0 ) ) ) e. RR )
226 189 225 jca 
 |-  ( ( ( 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 /\ ( S.2 ` ( z e. RR |-> if ( ( z e. dom F /\ 0 <_ -u ( Im ` ( F ` z ) ) ) , -u ( Im ` ( F ` z ) ) , 0 ) ) ) e. RR ) )
227 eqid 
 |-  ( 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 /\ 0 <_ ( Re ` ( F ` z ) ) ) , ( Re ` ( F ` z ) ) , 0 ) ) )
228 eqid 
 |-  ( 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 /\ 0 <_ -u ( Re ` ( F ` z ) ) ) , -u ( Re ` ( F ` z ) ) , 0 ) ) )
229 eqid 
 |-  ( 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 /\ 0 <_ ( Im ` ( F ` z ) ) ) , ( Im ` ( F ` z ) ) , 0 ) ) )
230 eqid 
 |-  ( S.2 ` ( z e. RR |-> if ( ( z e. dom F /\ 0 <_ -u ( Im ` ( F ` z ) ) ) , -u ( Im ` ( F ` z ) ) , 0 ) ) ) = ( S.2 ` ( z e. RR |-> if ( ( z e. dom F /\ 0 <_ -u ( Im ` ( F ` z ) ) ) , -u ( Im ` ( F ` z ) ) , 0 ) ) )
231 227 228 229 230 70 iblcnlem1 
 |-  ( ( ( 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. L^1 <-> ( ( z e. dom F |-> ( F ` z ) ) e. MblFn /\ ( ( 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 ) /\ ( ( S.2 ` ( z e. RR |-> if ( ( z e. dom F /\ 0 <_ ( Im ` ( F ` z ) ) ) , ( Im ` ( F ` z ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( z e. RR |-> if ( ( z e. dom F /\ 0 <_ -u ( Im ` ( F ` z ) ) ) , -u ( Im ` ( F ` z ) ) , 0 ) ) ) e. RR ) ) ) )
232 35 151 226 231 mpbir3and 
 |-  ( ( ( 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. L^1 )
233 32 232 sylan2b 
 |-  ( ( ( F e. MblFn /\ ( vol ` dom F ) e. RR ) /\ ( ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) /\ 0 <_ x ) ) -> ( z e. dom F |-> ( F ` z ) ) e. L^1 )
234 233 anassrs 
 |-  ( ( ( ( F e. MblFn /\ ( vol ` dom F ) e. RR ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ 0 <_ x ) -> ( z e. dom F |-> ( F ` z ) ) e. L^1 )
235 31 234 syldan 
 |-  ( ( ( ( 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 )
236 13 235 pm2.61dane 
 |-  ( ( ( F e. MblFn /\ ( vol ` dom F ) e. RR ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( z e. dom F |-> ( F ` z ) ) e. L^1 )
237 236 rexlimdvaa 
 |-  ( ( F e. MblFn /\ ( vol ` dom F ) e. RR ) -> ( E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x -> ( z e. dom F |-> ( F ` z ) ) e. L^1 ) )
238 237 3impia 
 |-  ( ( F e. MblFn /\ ( vol ` dom F ) e. RR /\ E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) -> ( z e. dom F |-> ( F ` z ) ) e. L^1 )
239 3 238 eqeltrd 
 |-  ( ( 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 )