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

Theorem ftc1anclem5 28380
Description: Lemma for ftc1anc 28384, the existence of a simple function the integral of whose pointwise difference from the function is less than a given positive real. (Contributed by Brendan Leahy, 17-Jun-2018.)
Hypotheses
Ref Expression
ftc1anc.g  |-  G  =  ( x  e.  ( A [,] B ) 
|->  S. ( A (,) x ) ( F `
 t )  _d t )
ftc1anc.a  |-  ( ph  ->  A  e.  RR )
ftc1anc.b  |-  ( ph  ->  B  e.  RR )
ftc1anc.le  |-  ( ph  ->  A  <_  B )
ftc1anc.s  |-  ( ph  ->  ( A (,) B
)  C_  D )
ftc1anc.d  |-  ( ph  ->  D  C_  RR )
ftc1anc.i  |-  ( ph  ->  F  e.  L^1 )
ftc1anc.f  |-  ( ph  ->  F : D --> CC )
Assertion
Ref Expression
ftc1anclem5  |-  ( (
ph  /\  Y  e.  RR+ )  ->  E. f  e.  dom  S.1 ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) ) ) )  < 
Y )
Distinct variable groups:    t, f, x, A    B, f, t, x    D, f, t, x   
f, F, t, x    ph, f, t, x    f, G    f, Y, t, x
Allowed substitution hints:    G( x, t)

Proof of Theorem ftc1anclem5
Dummy variable  g is distinct from all other variables.
StepHypRef Expression
1 iftrue 3794 . . . . . . . . 9  |-  ( t  e.  RR  ->  if ( t  e.  RR ,  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ,  0 )  =  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) )
21mpteq2ia 4371 . . . . . . . 8  |-  ( t  e.  RR  |->  if ( t  e.  RR , 
( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ,  0 ) )  =  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) )
32fveq2i 5691 . . . . . . 7  |-  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  RR ,  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ,  0 ) ) )  =  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )
4 ftc1anc.f . . . . . . . . . . . . . 14  |-  ( ph  ->  F : D --> CC )
54ffvelrnda 5840 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  D )  ->  ( F `  t )  e.  CC )
6 0cnd 9375 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  t  e.  D )  ->  0  e.  CC )
75, 6ifclda 3818 . . . . . . . . . . . 12  |-  ( ph  ->  if ( t  e.  D ,  ( F `
 t ) ,  0 )  e.  CC )
87recld 12679 . . . . . . . . . . 11  |-  ( ph  ->  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  RR )
98adantr 462 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  RR )  ->  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  RR )
10 ftc1anc.d . . . . . . . . . . 11  |-  ( ph  ->  D  C_  RR )
11 rembl 20922 . . . . . . . . . . . 12  |-  RR  e.  dom  vol
1211a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  RR  e.  dom  vol )
138adantr 462 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  D )  ->  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) )  e.  RR )
14 eldifn 3476 . . . . . . . . . . . . 13  |-  ( t  e.  ( RR  \  D )  ->  -.  t  e.  D )
1514adantl 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( RR  \  D ) )  ->  -.  t  e.  D )
16 iffalse 3796 . . . . . . . . . . . . . 14  |-  ( -.  t  e.  D  ->  if ( t  e.  D ,  ( F `  t ) ,  0 )  =  0 )
1716fveq2d 5692 . . . . . . . . . . . . 13  |-  ( -.  t  e.  D  -> 
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  =  ( Re `  0 ) )
18 re0 12637 . . . . . . . . . . . . 13  |-  ( Re
`  0 )  =  0
1917, 18syl6eq 2489 . . . . . . . . . . . 12  |-  ( -.  t  e.  D  -> 
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  =  0 )
2015, 19syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( RR  \  D ) )  ->  ( Re `  if ( t  e.  D ,  ( F `
 t ) ,  0 ) )  =  0 )
21 iftrue 3794 . . . . . . . . . . . . . 14  |-  ( t  e.  D  ->  if ( t  e.  D ,  ( F `  t ) ,  0 )  =  ( F `
 t ) )
2221fveq2d 5692 . . . . . . . . . . . . 13  |-  ( t  e.  D  ->  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) )  =  ( Re
`  ( F `  t ) ) )
2322mpteq2ia 4371 . . . . . . . . . . . 12  |-  ( t  e.  D  |->  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  =  ( t  e.  D  |->  ( Re
`  ( F `  t ) ) )
244feqmptd 5741 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F  =  ( t  e.  D  |->  ( F `
 t ) ) )
25 ftc1anc.i . . . . . . . . . . . . . . 15  |-  ( ph  ->  F  e.  L^1 )
2624, 25eqeltrrd 2516 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( t  e.  D  |->  ( F `  t
) )  e.  L^1 )
275iblcn 21176 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( t  e.  D  |->  ( F `  t ) )  e.  L^1  <->  ( (
t  e.  D  |->  ( Re `  ( F `
 t ) ) )  e.  L^1 
/\  ( t  e.  D  |->  ( Im `  ( F `  t ) ) )  e.  L^1 ) ) )
2826, 27mpbid 210 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( t  e.  D  |->  ( Re `  ( F `  t ) ) )  e.  L^1  /\  ( t  e.  D  |->  ( Im `  ( F `  t ) ) )  e.  L^1 ) )
2928simpld 456 . . . . . . . . . . . 12  |-  ( ph  ->  ( t  e.  D  |->  ( Re `  ( F `  t )
) )  e.  L^1 )
3023, 29syl5eqel 2525 . . . . . . . . . . 11  |-  ( ph  ->  ( t  e.  D  |->  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  e.  L^1 )
3110, 12, 13, 20, 30iblss2 21183 . . . . . . . . . 10  |-  ( ph  ->  ( t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) )  e.  L^1 )
328recnd 9408 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  CC )
3332adantr 462 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  RR )  ->  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  CC )
34 eqidd 2442 . . . . . . . . . . . 12  |-  ( ph  ->  ( t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) )  =  ( t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) ) )
35 absf 12821 . . . . . . . . . . . . . 14  |-  abs : CC
--> RR
3635a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  abs : CC --> RR )
3736feqmptd 5741 . . . . . . . . . . . 12  |-  ( ph  ->  abs  =  ( x  e.  CC  |->  ( abs `  x ) ) )
38 fveq2 5688 . . . . . . . . . . . 12  |-  ( x  =  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  ->  ( abs `  x )  =  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )
3933, 34, 37, 38fmptco 5873 . . . . . . . . . . 11  |-  ( ph  ->  ( abs  o.  (
t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) ) )  =  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )
40 eqid 2441 . . . . . . . . . . . . 13  |-  ( t  e.  RR  |->  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  =  ( t  e.  RR  |->  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )
419, 40fmptd 5864 . . . . . . . . . . . 12  |-  ( ph  ->  ( t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) ) : RR --> RR )
42 iblmbf 21145 . . . . . . . . . . . . . . . . . 18  |-  ( F  e.  L^1  ->  F  e. MblFn )
4325, 42syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  F  e. MblFn )
4424, 43eqeltrrd 2516 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( t  e.  D  |->  ( F `  t
) )  e. MblFn )
455ismbfcn2 21017 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( t  e.  D  |->  ( F `  t ) )  e. MblFn  <->  ( ( t  e.  D  |->  ( Re `  ( F `  t )
) )  e. MblFn  /\  (
t  e.  D  |->  ( Im `  ( F `
 t ) ) )  e. MblFn ) ) )
4644, 45mpbid 210 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( t  e.  D  |->  ( Re `  ( F `  t ) ) )  e. MblFn  /\  (
t  e.  D  |->  ( Im `  ( F `
 t ) ) )  e. MblFn ) )
4746simpld 456 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( t  e.  D  |->  ( Re `  ( F `  t )
) )  e. MblFn )
4823, 47syl5eqel 2525 . . . . . . . . . . . . 13  |-  ( ph  ->  ( t  e.  D  |->  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  e. MblFn
)
4910, 12, 13, 20, 48mbfss 21024 . . . . . . . . . . . 12  |-  ( ph  ->  ( t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) )  e. MblFn )
50 ftc1anclem1 28376 . . . . . . . . . . . 12  |-  ( ( ( t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) ) : RR --> RR  /\  ( t  e.  RR  |->  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  e. MblFn
)  ->  ( abs  o.  ( t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) ) )  e. MblFn
)
5141, 49, 50syl2anc 656 . . . . . . . . . . 11  |-  ( ph  ->  ( abs  o.  (
t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) ) )  e. MblFn
)
5239, 51eqeltrrd 2516 . . . . . . . . . 10  |-  ( ph  ->  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) )  e. MblFn )
539, 31, 52iblabsnc 28365 . . . . . . . . 9  |-  ( ph  ->  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) )  e.  L^1 )
5432abscld 12918 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) )  e.  RR )
5554adantr 462 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  RR )  ->  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  e.  RR )
5632absge0d 12926 . . . . . . . . . . 11  |-  ( ph  ->  0  <_  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) )
5756adantr 462 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  RR )  ->  0  <_ 
( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )
5855, 57iblpos 21170 . . . . . . . . 9  |-  ( ph  ->  ( ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )  e.  L^1  <->  ( (
t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) )  e. MblFn  /\  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  RR ,  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ,  0 ) ) )  e.  RR ) ) )
5953, 58mpbid 210 . . . . . . . 8  |-  ( ph  ->  ( ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )  e. MblFn  /\  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  RR ,  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ,  0 ) ) )  e.  RR ) )
6059simprd 460 . . . . . . 7  |-  ( ph  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  RR ,  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ,  0 ) ) )  e.  RR )
613, 60syl5eqelr 2526 . . . . . 6  |-  ( ph  ->  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  e.  RR )
62 ltsubrp 11018 . . . . . 6  |-  ( ( ( S.2 `  (
t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  e.  RR  /\  Y  e.  RR+ )  ->  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y )  <  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) ) )
6361, 62sylan 468 . . . . 5  |-  ( (
ph  /\  Y  e.  RR+ )  ->  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y )  < 
( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) ) )
64 rpre 10993 . . . . . . 7  |-  ( Y  e.  RR+  ->  Y  e.  RR )
65 resubcl 9669 . . . . . . 7  |-  ( ( ( S.2 `  (
t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  e.  RR  /\  Y  e.  RR )  ->  (
( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y )  e.  RR )
6661, 64, 65syl2an 474 . . . . . 6  |-  ( (
ph  /\  Y  e.  RR+ )  ->  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y )  e.  RR )
6761adantr 462 . . . . . 6  |-  ( (
ph  /\  Y  e.  RR+ )  ->  ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  e.  RR )
6866, 67ltnled 9517 . . . . 5  |-  ( (
ph  /\  Y  e.  RR+ )  ->  ( (
( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y )  <  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  <->  -.  ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y ) ) )
6963, 68mpbid 210 . . . 4  |-  ( (
ph  /\  Y  e.  RR+ )  ->  -.  ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y ) )
7054rexrd 9429 . . . . . . . . 9  |-  ( ph  ->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) )  e.  RR* )
71 elxrge0 11390 . . . . . . . . 9  |-  ( ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  e.  ( 0 [,] +oo )  <->  ( ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  e. 
RR*  /\  0  <_  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )
7270, 56, 71sylanbrc 659 . . . . . . . 8  |-  ( ph  ->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) )  e.  ( 0 [,] +oo )
)
7372adantr 462 . . . . . . 7  |-  ( (
ph  /\  t  e.  RR )  ->  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  e.  ( 0 [,] +oo ) )
74 eqid 2441 . . . . . . 7  |-  ( t  e.  RR  |->  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) )  =  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )
7573, 74fmptd 5864 . . . . . 6  |-  ( ph  ->  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) : RR --> ( 0 [,] +oo ) )
7675adantr 462 . . . . 5  |-  ( (
ph  /\  Y  e.  RR+ )  ->  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) : RR --> ( 0 [,] +oo ) )
7766rexrd 9429 . . . . 5  |-  ( (
ph  /\  Y  e.  RR+ )  ->  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y )  e. 
RR* )
78 itg2leub 21112 . . . . 5  |-  ( ( ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) : RR --> ( 0 [,] +oo )  /\  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y )  e.  RR* )  ->  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  <_ 
( ( S.2 `  (
t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y )  <->  A. g  e.  dom  S.1 ( g  oR  <_  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )  -> 
( S.1 `  g )  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y ) ) ) )
7976, 77, 78syl2anc 656 . . . 4  |-  ( (
ph  /\  Y  e.  RR+ )  ->  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y )  <->  A. g  e.  dom  S.1 ( g  oR  <_  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )  -> 
( S.1 `  g )  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y ) ) ) )
8069, 79mtbid 300 . . 3  |-  ( (
ph  /\  Y  e.  RR+ )  ->  -.  A. g  e.  dom  S.1 ( g  oR  <_  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )  -> 
( S.1 `  g )  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y ) ) )
81 rexanali 2759 . . 3  |-  ( E. g  e.  dom  S.1 ( g  oR  <_  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )  /\  -.  ( S.1 `  g
)  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y ) )  <->  -.  A. g  e.  dom  S.1 ( g  oR  <_  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )  -> 
( S.1 `  g )  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y ) ) )
8280, 81sylibr 212 . 2  |-  ( (
ph  /\  Y  e.  RR+ )  ->  E. g  e.  dom  S.1 ( g  oR  <_  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )  /\  -.  ( S.1 `  g
)  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y ) ) )
8366ad2antrr 720 . . . . . . . 8  |-  ( ( ( ( ph  /\  Y  e.  RR+ )  /\  g  e.  dom  S.1 )  /\  -.  ( S.1 `  g
)  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y ) )  ->  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y )  e.  RR )
84 itg1cl 21063 . . . . . . . . 9  |-  ( g  e.  dom  S.1  ->  ( S.1 `  g )  e.  RR )
8584ad2antlr 721 . . . . . . . 8  |-  ( ( ( ( ph  /\  Y  e.  RR+ )  /\  g  e.  dom  S.1 )  /\  -.  ( S.1 `  g
)  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y ) )  ->  ( S.1 `  g
)  e.  RR )
86 eqid 2441 . . . . . . . . . . . 12  |-  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) )  =  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) )
8786i1fpos 21084 . . . . . . . . . . 11  |-  ( g  e.  dom  S.1  ->  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  dom  S.1 )
88 0re 9382 . . . . . . . . . . . . . 14  |-  0  e.  RR
89 i1ff 21054 . . . . . . . . . . . . . . 15  |-  ( g  e.  dom  S.1  ->  g : RR --> RR )
9089ffvelrnda 5840 . . . . . . . . . . . . . 14  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  e.  RR )
91 max1 11153 . . . . . . . . . . . . . 14  |-  ( ( 0  e.  RR  /\  ( g `  t
)  e.  RR )  ->  0  <_  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )
9288, 90, 91sylancr 658 . . . . . . . . . . . . 13  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  0  <_  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )
9392ralrimiva 2797 . . . . . . . . . . . 12  |-  ( g  e.  dom  S.1  ->  A. t  e.  RR  0  <_  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) )
94 ax-resscn 9335 . . . . . . . . . . . . . . 15  |-  RR  C_  CC
9594a1i 11 . . . . . . . . . . . . . 14  |-  ( g  e.  dom  S.1  ->  RR  C_  CC )
96 fvex 5698 . . . . . . . . . . . . . . . . 17  |-  ( g `
 t )  e. 
_V
97 c0ex 9376 . . . . . . . . . . . . . . . . 17  |-  0  e.  _V
9896, 97ifex 3855 . . . . . . . . . . . . . . . 16  |-  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 )  e. 
_V
9998, 86fnmpti 5536 . . . . . . . . . . . . . . 15  |-  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) )  Fn  RR
10099a1i 11 . . . . . . . . . . . . . 14  |-  ( g  e.  dom  S.1  ->  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  Fn  RR )
10195, 1000pledm 21051 . . . . . . . . . . . . 13  |-  ( g  e.  dom  S.1  ->  ( 0p  oR  <_  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) )  <-> 
( RR  X.  {
0 } )  oR  <_  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) )
102 reex 9369 . . . . . . . . . . . . . . 15  |-  RR  e.  _V
103102a1i 11 . . . . . . . . . . . . . 14  |-  ( g  e.  dom  S.1  ->  RR  e.  _V )
10497a1i 11 . . . . . . . . . . . . . 14  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  0  e.  _V )
105 ifcl 3828 . . . . . . . . . . . . . . 15  |-  ( ( ( g `  t
)  e.  RR  /\  0  e.  RR )  ->  if ( 0  <_ 
( g `  t
) ,  ( g `
 t ) ,  0 )  e.  RR )
10690, 88, 105sylancl 657 . . . . . . . . . . . . . 14  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 )  e.  RR )
107 fconstmpt 4878 . . . . . . . . . . . . . . 15  |-  ( RR 
X.  { 0 } )  =  ( t  e.  RR  |->  0 )
108107a1i 11 . . . . . . . . . . . . . 14  |-  ( g  e.  dom  S.1  ->  ( RR  X.  { 0 } )  =  ( t  e.  RR  |->  0 ) )
109 eqidd 2442 . . . . . . . . . . . . . 14  |-  ( g  e.  dom  S.1  ->  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  =  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) )
110103, 104, 106, 108, 109ofrfval2 6336 . . . . . . . . . . . . 13  |-  ( g  e.  dom  S.1  ->  ( ( RR  X.  {
0 } )  oR  <_  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) )  <->  A. t  e.  RR  0  <_  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) )
111101, 110bitrd 253 . . . . . . . . . . . 12  |-  ( g  e.  dom  S.1  ->  ( 0p  oR  <_  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) )  <->  A. t  e.  RR  0  <_  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) )
11293, 111mpbird 232 . . . . . . . . . . 11  |-  ( g  e.  dom  S.1  ->  0p  oR  <_ 
( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) )
113 itg2itg1 21114 . . . . . . . . . . 11  |-  ( ( ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  dom  S.1 
/\  0p  oR  <_  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) )  ->  ( S.2 `  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) )  =  ( S.1 `  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) )
11487, 112, 113syl2anc 656 . . . . . . . . . 10  |-  ( g  e.  dom  S.1  ->  ( S.2 `  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) )  =  ( S.1 `  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) )
115 itg1cl 21063 . . . . . . . . . . 11  |-  ( ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  dom  S.1 
->  ( S.1 `  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) )  e.  RR )
11687, 115syl 16 . . . . . . . . . 10  |-  ( g  e.  dom  S.1  ->  ( S.1 `  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) )  e.  RR )
117114, 116eqeltrd 2515 . . . . . . . . 9  |-  ( g  e.  dom  S.1  ->  ( S.2 `  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) )  e.  RR )
118117ad2antlr 721 . . . . . . . 8  |-  ( ( ( ( ph  /\  Y  e.  RR+ )  /\  g  e.  dom  S.1 )  /\  -.  ( S.1 `  g
)  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y ) )  ->  ( S.2 `  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) )  e.  RR )
119 ltnle 9450 . . . . . . . . . 10  |-  ( ( ( ( S.2 `  (
t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y )  e.  RR  /\  ( S.1 `  g
)  e.  RR )  ->  ( ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y )  <  ( S.1 `  g
)  <->  -.  ( S.1 `  g )  <_  (
( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y ) ) )
12066, 84, 119syl2an 474 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  e.  RR+ )  /\  g  e.  dom  S.1 )  ->  (
( ( S.2 `  (
t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y )  <  ( S.1 `  g )  <->  -.  ( S.1 `  g )  <_ 
( ( S.2 `  (
t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y ) ) )
121120biimpar 482 . . . . . . . 8  |-  ( ( ( ( ph  /\  Y  e.  RR+ )  /\  g  e.  dom  S.1 )  /\  -.  ( S.1 `  g
)  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y ) )  ->  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y )  <  ( S.1 `  g ) )
122 max2 11155 . . . . . . . . . . . . . 14  |-  ( ( 0  e.  RR  /\  ( g `  t
)  e.  RR )  ->  ( g `  t )  <_  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )
12388, 90, 122sylancr 658 . . . . . . . . . . . . 13  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  <_  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )
124123ralrimiva 2797 . . . . . . . . . . . 12  |-  ( g  e.  dom  S.1  ->  A. t  e.  RR  (
g `  t )  <_  if ( 0  <_ 
( g `  t
) ,  ( g `
 t ) ,  0 ) )
12589feqmptd 5741 . . . . . . . . . . . . 13  |-  ( g  e.  dom  S.1  ->  g  =  ( t  e.  RR  |->  ( g `  t ) ) )
126103, 90, 106, 125, 109ofrfval2 6336 . . . . . . . . . . . 12  |-  ( g  e.  dom  S.1  ->  ( g  oR  <_ 
( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  <->  A. t  e.  RR  ( g `  t )  <_  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) )
127124, 126mpbird 232 . . . . . . . . . . 11  |-  ( g  e.  dom  S.1  ->  g  oR  <_  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) )
128 itg1le 21091 . . . . . . . . . . 11  |-  ( ( g  e.  dom  S.1  /\  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  dom  S.1 
/\  g  oR  <_  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) )  ->  ( S.1 `  g )  <_  ( S.1 `  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) )
12987, 127, 128mpd3an23 1311 . . . . . . . . . 10  |-  ( g  e.  dom  S.1  ->  ( S.1 `  g )  <_  ( S.1 `  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) )
130129, 114breqtrrd 4315 . . . . . . . . 9  |-  ( g  e.  dom  S.1  ->  ( S.1 `  g )  <_  ( S.2 `  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) )
131130ad2antlr 721 . . . . . . . 8  |-  ( ( ( ( ph  /\  Y  e.  RR+ )  /\  g  e.  dom  S.1 )  /\  -.  ( S.1 `  g
)  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y ) )  ->  ( S.1 `  g
)  <_  ( S.2 `  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) )
13283, 85, 118, 121, 131ltletrd 9527 . . . . . . 7  |-  ( ( ( ( ph  /\  Y  e.  RR+ )  /\  g  e.  dom  S.1 )  /\  -.  ( S.1 `  g
)  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y ) )  ->  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y )  <  ( S.2 `  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) )
133132adantrl 710 . . . . . 6  |-  ( ( ( ( ph  /\  Y  e.  RR+ )  /\  g  e.  dom  S.1 )  /\  ( g  oR  <_  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )  /\  -.  ( S.1 `  g
)  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y ) ) )  ->  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y )  < 
( S.2 `  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) )
134 i1fmbf 21053 . . . . . . . . . . . . . . . 16  |-  ( ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  dom  S.1 
->  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e. MblFn )
13587, 134syl 16 . . . . . . . . . . . . . . 15  |-  ( g  e.  dom  S.1  ->  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e. MblFn )
136135adantl 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  g  e.  dom  S.1 )  ->  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e. MblFn )
137 elrege0 11388 . . . . . . . . . . . . . . . . 17  |-  ( if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 )  e.  ( 0 [,) +oo )  <->  ( if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 )  e.  RR  /\  0  <_  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) )
138106, 92, 137sylanbrc 659 . . . . . . . . . . . . . . . 16  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 )  e.  ( 0 [,) +oo ) )
139138, 86fmptd 5864 . . . . . . . . . . . . . . 15  |-  ( g  e.  dom  S.1  ->  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) : RR --> ( 0 [,) +oo ) )
140139adantl 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  g  e.  dom  S.1 )  ->  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) : RR --> ( 0 [,) +oo ) )
141117adantl 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  g  e.  dom  S.1 )  ->  ( S.2 `  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) )  e.  RR )
142106recnd 9408 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 )  e.  CC )
143142negcld 9702 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  -u if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 )  e.  CC )
144 ifcl 3828 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( if ( 0  <_ 
( g `  t
) ,  ( g `
 t ) ,  0 )  e.  CC  /\  -u if ( 0  <_ 
( g `  t
) ,  ( g `
 t ) ,  0 )  e.  CC )  ->  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ,  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  CC )
145142, 143, 144syl2anc 656 . . . . . . . . . . . . . . . . . . 19  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ,  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  CC )
146 subcl 9605 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  CC  /\  if ( 0  <_ 
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ,  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  CC )  ->  ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ,  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) )  e.  CC )
14732, 145, 146syl2an 474 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( g  e.  dom  S.1  /\  t  e.  RR ) )  -> 
( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  if ( 0  <_  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ,  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) , 
-u if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) )  e.  CC )
148147anassrs 643 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  if ( 0  <_  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ,  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) , 
-u if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) )  e.  CC )
149148abscld 12918 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ,  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) )  e.  RR )
150148absge0d 12926 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  0  <_  ( abs `  (
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  if ( 0  <_  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ,  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) , 
-u if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) ) )
151 elrege0 11388 . . . . . . . . . . . . . . . 16  |-  ( ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `
 t ) ,  0 ) ) ,  if ( 0  <_ 
( g `  t
) ,  ( g `
 t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) )  e.  ( 0 [,) +oo )  <->  ( ( abs `  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  if ( 0  <_  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ,  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) , 
-u if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) )  e.  RR  /\  0  <_  ( abs `  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  if ( 0  <_  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ,  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) , 
-u if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) ) ) )
152149, 150, 151sylanbrc 659 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ,  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) )  e.  ( 0 [,) +oo ) )
153 eqid 2441 . . . . . . . . . . . . . . 15  |-  ( t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  if ( 0  <_  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ,  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) , 
-u if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) ) )  =  ( t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `
 t ) ,  0 ) ) ,  if ( 0  <_ 
( g `  t
) ,  ( g `
 t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) ) )
154152, 153fmptd 5864 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  g  e.  dom  S.1 )  ->  (
t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `
 t ) ,  0 ) ) ,  if ( 0  <_ 
( g `  t
) ,  ( g `
 t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) ) ) : RR --> ( 0 [,) +oo ) )
155 eleq1 2501 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  t  ->  (
x  e.  D  <->  t  e.  D ) )
156 fveq2 5688 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  t  ->  ( F `  x )  =  ( F `  t ) )
157 eqidd 2442 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  t  ->  0  =  0 )
158155, 156, 157ifbieq12d 3813 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  t  ->  if ( x  e.  D ,  ( F `  x ) ,  0 )  =  if ( t  e.  D , 
( F `  t
) ,  0 ) )
159158fveq2d 5692 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  t  ->  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) )  =  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )
160 eqid 2441 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR  |->  ( Re
`  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) )  =  ( x  e.  RR  |->  ( Re
`  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) )
161 fvex 5698 . . . . . . . . . . . . . . . . . . . 20  |-  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  _V
162159, 160, 161fvmpt 5771 . . . . . . . . . . . . . . . . . . 19  |-  ( t  e.  RR  ->  (
( x  e.  RR  |->  ( Re `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) `  t
)  =  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )
163159breq2d 4301 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  t  ->  (
0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) )  <->  0  <_  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) ) )
164 fveq2 5688 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  t  ->  (
g `  x )  =  ( g `  t ) )
165164breq2d 4301 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  t  ->  (
0  <_  ( g `  x )  <->  0  <_  ( g `  t ) ) )
166165, 164, 157ifbieq12d 3813 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  t  ->  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 )  =  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) )
167166negeqd 9600 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  t  ->  -u if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 )  =  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )
168163, 166, 167ifbieq12d 3813 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  t  ->  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) , 
-u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )  =  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ,  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) )
169 eqid 2441 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR  |->  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ,  -u if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ) )  =  ( x  e.  RR  |->  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) , 
-u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) )
170 negex 9604 . . . . . . . . . . . . . . . . . . . . 21  |-  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 )  e.  _V
17198, 170ifex 3855 . . . . . . . . . . . . . . . . . . . 20  |-  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `
 t ) ,  0 ) ) ,  if ( 0  <_ 
( g `  t
) ,  ( g `
 t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  _V
172168, 169, 171fvmpt 5771 . . . . . . . . . . . . . . . . . . 19  |-  ( t  e.  RR  ->  (
( x  e.  RR  |->  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) , 
-u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) ) `  t )  =  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ,  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) )
173162, 172oveq12d 6108 . . . . . . . . . . . . . . . . . 18  |-  ( t  e.  RR  ->  (
( ( x  e.  RR  |->  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ) `  t )  -  (
( x  e.  RR  |->  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) , 
-u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) ) `  t ) )  =  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `
 t ) ,  0 ) ) ,  if ( 0  <_ 
( g `  t
) ,  ( g `
 t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) )
174173fveq2d 5692 . . . . . . . . . . . . . . . . 17  |-  ( t  e.  RR  ->  ( abs `  ( ( ( x  e.  RR  |->  ( Re `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) `  t
)  -  ( ( x  e.  RR  |->  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) , 
-u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) ) `  t ) ) )  =  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `
 t ) ,  0 ) ) ,  if ( 0  <_ 
( g `  t
) ,  ( g `
 t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) ) )
175174mpteq2ia 4371 . . . . . . . . . . . . . . . 16  |-  ( t  e.  RR  |->  ( abs `  ( ( ( x  e.  RR  |->  ( Re
`  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ) `  t )  -  ( ( x  e.  RR  |->  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ,  -u if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ) ) `  t ) ) ) )  =  ( t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  if ( 0  <_  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ,  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) , 
-u if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) ) )
176175fveq2i 5691 . . . . . . . . . . . . . . 15  |-  ( S.2 `  ( t  e.  RR  |->  ( abs `  ( ( ( x  e.  RR  |->  ( Re `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) `  t
)  -  ( ( x  e.  RR  |->  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) , 
-u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) ) `  t ) ) ) ) )  =  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `
 t ) ,  0 ) ) ,  if ( 0  <_ 
( g `  t
) ,  ( g `
 t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) ) ) )
177102a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  RR  e.  _V )
178 fvex 5698 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( g `
 x )  e. 
_V
179178, 97ifex 3855 . . . . . . . . . . . . . . . . . . . . 21  |-  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 )  e. 
_V
180179, 97ifex 3855 . . . . . . . . . . . . . . . . . . . 20  |-  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ,  0 )  e.  _V
181180a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR )  ->  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ,  0 )  e.  _V )
182 ovex 6115 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -u
1  x.  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )  e.  _V
18397, 182ifex 3855 . . . . . . . . . . . . . . . . . . . 20  |-  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  0 ,  ( -u
1  x.  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) )  e.  _V
184183a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR )  ->  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  0 ,  ( -u
1  x.  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) )  e.  _V )
185 ffn 5556 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( F : D --> CC  ->  F  Fn  D )
186 frn 5562 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( F : D --> CC  ->  ran 
F  C_  CC )
187 ref 12597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  Re : CC
--> RR
188 ffn 5556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( Re : CC --> RR  ->  Re  Fn  CC )
189187, 188ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  Re  Fn  CC
190 fnco 5516 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( Re  Fn  CC  /\  F  Fn  D  /\  ran  F  C_  CC )  ->  ( Re  o.  F
)  Fn  D )
191189, 190mp3an1 1296 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( F  Fn  D  /\  ran  F  C_  CC )  ->  ( Re  o.  F
)  Fn  D )
192185, 186, 191syl2anc 656 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( F : D --> CC  ->  ( Re  o.  F )  Fn  D )
193 elpreima 5820 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( Re  o.  F )  Fn  D  ->  (
x  e.  ( `' ( Re  o.  F
) " ( 0 [,) +oo ) )  <-> 
( x  e.  D  /\  ( ( Re  o.  F ) `  x
)  e.  ( 0 [,) +oo ) ) ) )
1944, 192, 1933syl 20 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( x  e.  ( `' ( Re  o.  F ) " (
0 [,) +oo )
)  <->  ( x  e.  D  /\  ( ( Re  o.  F ) `
 x )  e.  ( 0 [,) +oo ) ) ) )
195 fco 5565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( Re : CC --> RR  /\  F : D --> CC )  ->  ( Re  o.  F ) : D --> RR )
196187, 4, 195sylancr 658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ( Re  o.  F
) : D --> RR )
197196ffvelrnda 5840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  x  e.  D )  ->  (
( Re  o.  F
) `  x )  e.  RR )
198197biantrurd 505 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  D )  ->  (
0  <_  ( (
Re  o.  F ) `  x )  <->  ( (
( Re  o.  F
) `  x )  e.  RR  /\  0  <_ 
( ( Re  o.  F ) `  x
) ) ) )
199 elrege0 11388 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( Re  o.  F
) `  x )  e.  ( 0 [,) +oo ) 
<->  ( ( ( Re  o.  F ) `  x )  e.  RR  /\  0  <_  ( (
Re  o.  F ) `  x ) ) )
200198, 199syl6bbr 263 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  D )  ->  (
0  <_  ( (
Re  o.  F ) `  x )  <->  ( (
Re  o.  F ) `  x )  e.  ( 0 [,) +oo )
) )
201 fvco3 5765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F : D --> CC  /\  x  e.  D )  ->  ( ( Re  o.  F ) `  x
)  =  ( Re
`  ( F `  x ) ) )
2024, 201sylan 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  D )  ->  (
( Re  o.  F
) `  x )  =  ( Re `  ( F `  x ) ) )
203202breq2d 4301 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  D )  ->  (
0  <_  ( (
Re  o.  F ) `  x )  <->  0  <_  ( Re `  ( F `
 x ) ) ) )
204200, 203bitr3d 255 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  D )  ->  (
( ( Re  o.  F ) `  x
)  e.  ( 0 [,) +oo )  <->  0  <_  ( Re `  ( F `
 x ) ) ) )
205204pm5.32da 636 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( x  e.  D  /\  ( ( Re  o.  F ) `
 x )  e.  ( 0 [,) +oo ) )  <->  ( x  e.  D  /\  0  <_  ( Re `  ( F `  x )
) ) ) )
206194, 205bitrd 253 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( x  e.  ( `' ( Re  o.  F ) " (
0 [,) +oo )
)  <->  ( x  e.  D  /\  0  <_ 
( Re `  ( F `  x )
) ) ) )
207206adantr 462 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  e.  ( `' ( Re  o.  F )
" ( 0 [,) +oo ) )  <->  ( x  e.  D  /\  0  <_  ( Re `  ( F `  x )
) ) ) )
208 0le0 10407 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  0  <_  0
209208, 18breqtrri 4314 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  0  <_  ( Re `  0
)
210209biantru 502 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( -.  x  e.  D  <->  ( -.  x  e.  D  /\  0  <_  ( Re ` 
0 ) ) )
211 eldif 3335 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( RR  \  D )  <->  ( x  e.  RR  /\  -.  x  e.  D ) )
212211baibr 892 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  RR  ->  ( -.  x  e.  D  <->  x  e.  ( RR  \  D ) ) )
213210, 212syl5rbbr 260 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  RR  ->  (
x  e.  ( RR 
\  D )  <->  ( -.  x  e.  D  /\  0  <_  ( Re ` 
0 ) ) ) )
214213adantl 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  e.  ( RR  \  D )  <->  ( -.  x  e.  D  /\  0  <_  ( Re ` 
0 ) ) ) )
215207, 214orbi12d 704 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( x  e.  ( `' ( Re  o.  F
) " ( 0 [,) +oo ) )  \/  x  e.  ( RR  \  D ) )  <->  ( ( x  e.  D  /\  0  <_  ( Re `  ( F `  x )
) )  \/  ( -.  x  e.  D  /\  0  <_  ( Re
`  0 ) ) ) ) )
216 elun 3494 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( ( `' ( Re  o.  F
) " ( 0 [,) +oo ) )  u.  ( RR  \  D ) )  <->  ( x  e.  ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  \/  x  e.  ( RR  \  D
) ) )
217 fveq2 5688 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( if ( x  e.  D ,  ( F `  x ) ,  0 )  =  ( F `
 x )  -> 
( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  =  ( Re `  ( F `
 x ) ) )
218217breq2d 4301 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( if ( x  e.  D ,  ( F `  x ) ,  0 )  =  ( F `
 x )  -> 
( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) )  <->  0  <_  (
Re `  ( F `  x ) ) ) )
219 fveq2 5688 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( if ( x  e.  D ,  ( F `  x ) ,  0 )  =  0  -> 
( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  =  ( Re `  0 ) )
220219breq2d 4301 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( if ( x  e.  D ,  ( F `  x ) ,  0 )  =  0  -> 
( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) )  <->  0  <_  (
Re `  0 )
) )
221218, 220elimif 3820 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  <->  ( (
x  e.  D  /\  0  <_  ( Re `  ( F `  x ) ) )  \/  ( -.  x  e.  D  /\  0  <_  ( Re
`  0 ) ) ) )
222215, 216, 2213bitr4g 288 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  e.  ( ( `' ( Re  o.  F
) " ( 0 [,) +oo ) )  u.  ( RR  \  D ) )  <->  0  <_  ( Re `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) )
223222ifbid 3808 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  RR )  ->  if ( x  e.  ( ( `' ( Re  o.  F ) " (
0 [,) +oo )
)  u.  ( RR 
\  D ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ,  0 )  =  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ,  0 ) )
224223mpteq2dva 4375 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( x  e.  RR  |->  if ( x  e.  ( ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ,  0 ) )  =  ( x  e.  RR  |->  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ,  0 ) ) )
225222ifbid 3808 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  RR )  ->  if ( x  e.  ( ( `' ( Re  o.  F ) " (
0 [,) +oo )
)  u.  ( RR 
\  D ) ) ,  0 ,  (
-u 1  x.  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ) )  =  if ( 0  <_ 
( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ,  0 ,  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) ) )
226225mpteq2dva 4375 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( x  e.  RR  |->  if ( x  e.  ( ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  0 ,  (
-u 1  x.  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ) ) )  =  ( x  e.  RR  |->  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ,  0 ,  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) ) ) )
227177, 181, 184, 224, 226offval2 6335 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( x  e.  RR  |->  if ( x  e.  ( ( `' ( Re  o.  F
) " ( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ,  0 ) )  oF  +  ( x  e.  RR  |->  if ( x  e.  ( ( `' ( Re  o.  F
) " ( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  0 ,  ( -u
1  x.  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) ) ) )  =  ( x  e.  RR  |->  ( if ( 0  <_ 
( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ,  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ,  0 )  +  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ,  0 ,  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) ) ) ) )
228 iftrue 3794 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  ->  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ,  0 )  =  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) )
229 iftrue 3794 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  ->  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  0 ,  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) )  =  0 )
230228, 229oveq12d 6108 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  ->  ( if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ,  0 )  +  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  0 ,  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) ) )  =  ( if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 )  +  0 ) )
231 iftrue 3794 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  ->  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  ( if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 )  +  0 ) ,  ( 0  +  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) ) )  =  ( if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 )  +  0 ) )
232230, 231eqtr4d 2476 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  ->  ( if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ,  0 )  +  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  0 ,  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) ) )  =  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  ( if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 )  +  0 ) ,  ( 0  +  ( -u
1  x.  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) ) ) )
233 iffalse 3796 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) )  ->  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ,  0 )  =  0 )
234 iffalse 3796 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) )  ->  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  0 ,  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) )  =  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) )
235233, 234oveq12d 6108 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( -.  0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) )  -> 
( if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ,  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ,  0 )  +  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ,  0 ,  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) ) )  =  ( 0  +  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) ) )
236 iffalse 3796 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( -.  0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) )  ->  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  ( if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 )  +  0 ) ,  ( 0  +  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) ) )  =  ( 0  +  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) ) )
237235, 236eqtr4d 2476 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -.  0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) )  -> 
( if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ,  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ,  0 )  +  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ,  0 ,  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) ) )  =  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  ( if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 )  +  0 ) ,  ( 0  +  ( -u
1  x.  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) ) ) )
238232, 237pm2.61i 164 . . . . . . . . . . . . . . . . . . . 20  |-  ( if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ,  0 )  +  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  0 ,  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) ) )  =  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  ( if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 )  +  0 ) ,  ( 0  +  ( -u
1  x.  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) ) )
23989ffvelrnda 5840 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  ( g `  x )  e.  RR )
240239recnd 9408 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  ( g `  x )  e.  CC )
241 0cn 9374 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  CC
242 ifcl 3828 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( g `  x
)  e.  CC  /\  0  e.  CC )  ->  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 )  e.  CC )
243240, 241, 242sylancl 657 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 )  e.  CC )
244243addid1d 9565 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  ( if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 )  +  0 )  =  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) )
245243mulm1d 9792 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) )  = 
-u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )
246245oveq2d 6106 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  ( 0  +  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) )  =  ( 0  + 
-u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) )
247243negcld 9702 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  -u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 )  e.  CC )
248247addid2d 9566 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  ( 0  + 
-u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )  =  -u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )
249246, 248eqtrd 2473 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  ( 0  +  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) )  =  -u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )
250244, 249ifeq12d 3806 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ,  ( if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 )  +  0 ) ,  ( 0  +  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) ) )  =  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ,  -u if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ) )
251238, 250syl5eq 2485 . . . . . . . . . . . . . . . . . . 19  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  ( if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ,  0 )  +  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  0 ,  ( -u
1  x.  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) ) )  =  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) , 
-u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) )
252251mpteq2dva 4375 . . . . . . . . . . . . . . . . . 18  |-  ( g  e.  dom  S.1  ->  ( x  e.  RR  |->  ( if ( 0  <_ 
( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ,  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ,  0 )  +  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ,  0 ,  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) ) ) )  =  ( x  e.  RR  |->  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) , 
-u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) ) )
253227, 252sylan9eq 2493 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  g  e.  dom  S.1 )  ->  (
( x  e.  RR  |->  if ( x  e.  ( ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ,  0 ) )  oF  +  ( x  e.  RR  |->  if ( x  e.  ( ( `' ( Re  o.  F ) " (
0 [,) +oo )
)  u.  ( RR 
\  D ) ) ,  0 ,  (
-u 1  x.  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ) ) ) )  =  ( x  e.  RR  |->  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ,  -u if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ) ) )
254 0xr 9426 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  RR*
255 pnfxr 11088 . . . . . . . . . . . . . . . . . . . . . . 23  |- +oo  e.  RR*
256 0ltpnf 11099 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  < +oo
257 snunioo 11407 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 0  e.  RR*  /\ +oo  e.  RR*  /\  0  < +oo )  ->  ( { 0 }  u.  (
0 (,) +oo )
)  =  ( 0 [,) +oo ) )
258254, 255, 256, 257mp3an 1309 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( { 0 }  u.  (
0 (,) +oo )
)  =  ( 0 [,) +oo )
259258imaeq2i 5164 . . . . . . . . . . . . . . . . . . . . 21  |-  ( `' ( Re  o.  F
) " ( { 0 }  u.  (
0 (,) +oo )
) )  =  ( `' ( Re  o.  F ) " (
0 [,) +oo )
)
260 imaundi 5246 . . . . . . . . . . . . . . . . . . . . 21  |-  ( `' ( Re  o.  F
) " ( { 0 }  u.  (
0 (,) +oo )
) )  =  ( ( `' ( Re  o.  F ) " { 0 } )  u.  ( `' ( Re  o.  F )
" ( 0 (,) +oo ) ) )
261259, 260eqtr3i 2463 . . . . . . . . . . . . . . . . . . . 20  |-  ( `' ( Re  o.  F
) " ( 0 [,) +oo ) )  =  ( ( `' ( Re  o.  F
) " { 0 } )  u.  ( `' ( Re  o.  F ) " (
0 (,) +oo )
) )
262 ismbfcn 21009 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( F : D --> CC  ->  ( F  e. MblFn  <->  ( ( Re  o.  F )  e. MblFn  /\  ( Im  o.  F
)  e. MblFn ) )
)
2634, 262syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( F  e. MblFn  <->  ( (
Re  o.  F )  e. MblFn  /\  ( Im  o.  F )  e. MblFn )
) )
26443, 263mpbid 210 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( Re  o.  F )  e. MblFn  /\  (
Im  o.  F )  e. MblFn ) )
265264simpld 456 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( Re  o.  F
)  e. MblFn )
266 mbfimasn 21012 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( Re  o.  F
)  e. MblFn  /\  (
Re  o.  F ) : D --> RR  /\  0  e.  RR )  ->  ( `' ( Re  o.  F ) " {
0 } )  e. 
dom  vol )
26788, 266mp3an3 1298 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( Re  o.  F
)  e. MblFn  /\  (
Re  o.  F ) : D --> RR )  -> 
( `' ( Re  o.  F ) " { 0 } )  e.  dom  vol )
268 mbfima 21010 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( Re  o.  F
)  e. MblFn  /\  (
Re  o.  F ) : D --> RR )  -> 
( `' ( Re  o.  F ) "
( 0 (,) +oo ) )  e.  dom  vol )
269 unmbl 20919 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( `' ( Re  o.  F ) " { 0 } )  e.  dom  vol  /\  ( `' ( Re  o.  F ) " (
0 (,) +oo )
)  e.  dom  vol )  ->  ( ( `' ( Re  o.  F
) " { 0 } )  u.  ( `' ( Re  o.  F ) " (
0 (,) +oo )
) )  e.  dom  vol )
270267, 268, 269syl2anc 656 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( Re  o.  F
)  e. MblFn  /\  (
Re  o.  F ) : D --> RR )  -> 
( ( `' ( Re  o.  F )
" { 0 } )  u.  ( `' ( Re  o.  F
) " ( 0 (,) +oo ) ) )  e.  dom  vol )
271265, 196, 270syl2anc 656 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( `' ( Re  o.  F )
" { 0 } )  u.  ( `' ( Re  o.  F
) " ( 0 (,) +oo ) ) )  e.  dom  vol )
272261, 271syl5eqel 2525 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  e.  dom  vol )
273 fdm 5560 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F : D --> CC  ->  dom 
F  =  D )
2744, 273syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  dom  F  =  D )
275 mbfdm 21006 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F  e. MblFn  ->  dom  F  e.  dom  vol )
27643, 275syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  dom  F  e.  dom  vol )
277274, 276eqeltrrd 2516 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  D  e.  dom  vol )
278 difmbl 20924 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( RR  e.  dom  vol  /\  D  e.  dom  vol )  ->  ( RR  \  D )  e.  dom  vol )
27911, 277, 278sylancr 658 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( RR  \  D
)  e.  dom  vol )
280 unmbl 20919 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  e.  dom  vol 
/\  ( RR  \  D )  e.  dom  vol )  ->  ( ( `' ( Re  o.  F ) " (
0 [,) +oo )
)  u.  ( RR 
\  D ) )  e.  dom  vol )
281272, 279, 280syl2anc 656 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( `' ( Re  o.  F )
" ( 0 [,) +oo ) )  u.  ( RR  \  D ) )  e.  dom  vol )
282 fveq2 5688 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( t  =  x  ->  (
g `  t )  =  ( g `  x ) )
283282breq2d 4301 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  =  x  ->  (
0  <_  ( g `  t )  <->  0  <_  ( g `  x ) ) )
284 eqidd 2442 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  =  x  ->  0  =  0 )
285283, 282, 284ifbieq12d 3813 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  =  x  ->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 )  =  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )
286285, 86, 179fvmpt 5771 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  RR  ->  (
( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) `  x
)  =  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )
287286eqcomd 2446 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 )  =  ( ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) `  x
) )
288287ifeq1d 3804 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  RR  ->  if ( x  e.  (
( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ,  0 )  =  if ( x  e.  ( ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  ( ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) `
 x ) ,  0 ) )
289288mpteq2ia 4371 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR  |->  if ( x  e.  ( ( `' ( Re  o.  F ) " (
0 [,) +oo )
)  u.  ( RR 
\  D ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  ( ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  ( ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) `
 x ) ,  0 ) )
290289i1fres 21083 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  dom  S.1 
/\  ( ( `' ( Re  o.  F
) " ( 0 [,) +oo ) )  u.  ( RR  \  D ) )  e. 
dom  vol )  ->  (
x  e.  RR  |->  if ( x  e.  ( ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ,  0 ) )  e. 
dom  S.1 )
291 id 22 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  dom  S.1 
->  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  (