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

Theorem ftc1anclem5 28471
Description: Lemma for ftc1anc 28475, 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 3797 . . . . . . . . 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 4374 . . . . . . . 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 5694 . . . . . . 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 5843 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  D )  ->  ( F `  t )  e.  CC )
6 0cnd 9379 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  t  e.  D )  ->  0  e.  CC )
75, 6ifclda 3821 . . . . . . . . . . . 12  |-  ( ph  ->  if ( t  e.  D ,  ( F `
 t ) ,  0 )  e.  CC )
87recld 12683 . . . . . . . . . . 11  |-  ( ph  ->  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  RR )
98adantr 465 . . . . . . . . . 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 21022 . . . . . . . . . . . 12  |-  RR  e.  dom  vol
1211a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  RR  e.  dom  vol )
138adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  D )  ->  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) )  e.  RR )
14 eldifn 3479 . . . . . . . . . . . . 13  |-  ( t  e.  ( RR  \  D )  ->  -.  t  e.  D )
1514adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( RR  \  D ) )  ->  -.  t  e.  D )
16 iffalse 3799 . . . . . . . . . . . . . 14  |-  ( -.  t  e.  D  ->  if ( t  e.  D ,  ( F `  t ) ,  0 )  =  0 )
1716fveq2d 5695 . . . . . . . . . . . . 13  |-  ( -.  t  e.  D  -> 
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  =  ( Re `  0 ) )
18 re0 12641 . . . . . . . . . . . . 13  |-  ( Re
`  0 )  =  0
1917, 18syl6eq 2491 . . . . . . . . . . . 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 3797 . . . . . . . . . . . . . 14  |-  ( t  e.  D  ->  if ( t  e.  D ,  ( F `  t ) ,  0 )  =  ( F `
 t ) )
2221fveq2d 5695 . . . . . . . . . . . . 13  |-  ( t  e.  D  ->  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) )  =  ( Re
`  ( F `  t ) ) )
2322mpteq2ia 4374 . . . . . . . . . . . 12  |-  ( t  e.  D  |->  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  =  ( t  e.  D  |->  ( Re
`  ( F `  t ) ) )
244feqmptd 5744 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F  =  ( t  e.  D  |->  ( F `
 t ) ) )
25 ftc1anc.i . . . . . . . . . . . . . . 15  |-  ( ph  ->  F  e.  L^1 )
2624, 25eqeltrrd 2518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( t  e.  D  |->  ( F `  t
) )  e.  L^1 )
275iblcn 21276 . . . . . . . . . . . . . 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 459 . . . . . . . . . . . 12  |-  ( ph  ->  ( t  e.  D  |->  ( Re `  ( F `  t )
) )  e.  L^1 )
3023, 29syl5eqel 2527 . . . . . . . . . . 11  |-  ( ph  ->  ( t  e.  D  |->  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  e.  L^1 )
3110, 12, 13, 20, 30iblss2 21283 . . . . . . . . . 10  |-  ( ph  ->  ( t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) )  e.  L^1 )
328recnd 9412 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  CC )
3332adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  RR )  ->  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  CC )
34 eqidd 2444 . . . . . . . . . . . 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 12825 . . . . . . . . . . . . . 14  |-  abs : CC
--> RR
3635a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  abs : CC --> RR )
3736feqmptd 5744 . . . . . . . . . . . 12  |-  ( ph  ->  abs  =  ( x  e.  CC  |->  ( abs `  x ) ) )
38 fveq2 5691 . . . . . . . . . . . 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 5876 . . . . . . . . . . 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 2443 . . . . . . . . . . . . 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 5867 . . . . . . . . . . . 12  |-  ( ph  ->  ( t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) ) : RR --> RR )
42 iblmbf 21245 . . . . . . . . . . . . . . . . . 18  |-  ( F  e.  L^1  ->  F  e. MblFn )
4325, 42syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  F  e. MblFn )
4424, 43eqeltrrd 2518 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( t  e.  D  |->  ( F `  t
) )  e. MblFn )
455ismbfcn2 21117 . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( t  e.  D  |->  ( Re `  ( F `  t )
) )  e. MblFn )
4823, 47syl5eqel 2527 . . . . . . . . . . . . 13  |-  ( ph  ->  ( t  e.  D  |->  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  e. MblFn
)
4910, 12, 13, 20, 48mbfss 21124 . . . . . . . . . . . 12  |-  ( ph  ->  ( t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) )  e. MblFn )
50 ftc1anclem1 28467 . . . . . . . . . . . 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 661 . . . . . . . . . . 11  |-  ( ph  ->  ( abs  o.  (
t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) ) )  e. MblFn
)
5239, 51eqeltrrd 2518 . . . . . . . . . 10  |-  ( ph  ->  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) )  e. MblFn )
539, 31, 52iblabsnc 28456 . . . . . . . . 9  |-  ( ph  ->  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) )  e.  L^1 )
5432abscld 12922 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) )  e.  RR )
5554adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  RR )  ->  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  e.  RR )
5632absge0d 12930 . . . . . . . . . . 11  |-  ( ph  ->  0  <_  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) )
5756adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  RR )  ->  0  <_ 
( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )
5855, 57iblpos 21270 . . . . . . . . 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 463 . . . . . . 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 2528 . . . . . 6  |-  ( ph  ->  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  e.  RR )
62 ltsubrp 11022 . . . . . 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 471 . . . . 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 10997 . . . . . . 7  |-  ( Y  e.  RR+  ->  Y  e.  RR )
65 resubcl 9673 . . . . . . 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 477 . . . . . 6  |-  ( (
ph  /\  Y  e.  RR+ )  ->  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y )  e.  RR )
6761adantr 465 . . . . . 6  |-  ( (
ph  /\  Y  e.  RR+ )  ->  ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  e.  RR )
6866, 67ltnled 9521 . . . . 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 9433 . . . . . . . . 9  |-  ( ph  ->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) )  e.  RR* )
71 elxrge0 11394 . . . . . . . . 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 664 . . . . . . . 8  |-  ( ph  ->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) )  e.  ( 0 [,] +oo )
)
7372adantr 465 . . . . . . 7  |-  ( (
ph  /\  t  e.  RR )  ->  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  e.  ( 0 [,] +oo ) )
74 eqid 2443 . . . . . . 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 5867 . . . . . 6  |-  ( ph  ->  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) : RR --> ( 0 [,] +oo ) )
7675adantr 465 . . . . 5  |-  ( (
ph  /\  Y  e.  RR+ )  ->  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) : RR --> ( 0 [,] +oo ) )
7766rexrd 9433 . . . . 5  |-  ( (
ph  /\  Y  e.  RR+ )  ->  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y )  e. 
RR* )
78 itg2leub 21212 . . . . 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 661 . . . 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 2761 . . 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 725 . . . . . . . 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 21163 . . . . . . . . 9  |-  ( g  e.  dom  S.1  ->  ( S.1 `  g )  e.  RR )
8584ad2antlr 726 . . . . . . . 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 2443 . . . . . . . . . . . 12  |-  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) )  =  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) )
8786i1fpos 21184 . . . . . . . . . . 11  |-  ( g  e.  dom  S.1  ->  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  dom  S.1 )
88 0re 9386 . . . . . . . . . . . . . 14  |-  0  e.  RR
89 i1ff 21154 . . . . . . . . . . . . . . 15  |-  ( g  e.  dom  S.1  ->  g : RR --> RR )
9089ffvelrnda 5843 . . . . . . . . . . . . . 14  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  e.  RR )
91 max1 11157 . . . . . . . . . . . . . 14  |-  ( ( 0  e.  RR  /\  ( g `  t
)  e.  RR )  ->  0  <_  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )
9288, 90, 91sylancr 663 . . . . . . . . . . . . 13  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  0  <_  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )
9392ralrimiva 2799 . . . . . . . . . . . 12  |-  ( g  e.  dom  S.1  ->  A. t  e.  RR  0  <_  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) )
94 ax-resscn 9339 . . . . . . . . . . . . . . 15  |-  RR  C_  CC
9594a1i 11 . . . . . . . . . . . . . 14  |-  ( g  e.  dom  S.1  ->  RR  C_  CC )
96 fvex 5701 . . . . . . . . . . . . . . . . 17  |-  ( g `
 t )  e. 
_V
97 c0ex 9380 . . . . . . . . . . . . . . . . 17  |-  0  e.  _V
9896, 97ifex 3858 . . . . . . . . . . . . . . . 16  |-  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 )  e. 
_V
9998, 86fnmpti 5539 . . . . . . . . . . . . . . 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 21151 . . . . . . . . . . . . 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 9373 . . . . . . . . . . . . . . 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 3831 . . . . . . . . . . . . . . 15  |-  ( ( ( g `  t
)  e.  RR  /\  0  e.  RR )  ->  if ( 0  <_ 
( g `  t
) ,  ( g `
 t ) ,  0 )  e.  RR )
10690, 88, 105sylancl 662 . . . . . . . . . . . . . 14  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 )  e.  RR )
107 fconstmpt 4882 . . . . . . . . . . . . . . 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 2444 . . . . . . . . . . . . . 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 6337 . . . . . . . . . . . . 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 21214 . . . . . . . . . . 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 661 . . . . . . . . . 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 21163 . . . . . . . . . . 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 2517 . . . . . . . . 9  |-  ( g  e.  dom  S.1  ->  ( S.2 `  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) )  e.  RR )
118117ad2antlr 726 . . . . . . . 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 9454 . . . . . . . . . 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 477 . . . . . . . . 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 485 . . . . . . . 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 11159 . . . . . . . . . . . . . 14  |-  ( ( 0  e.  RR  /\  ( g `  t
)  e.  RR )  ->  ( g `  t )  <_  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )
12388, 90, 122sylancr 663 . . . . . . . . . . . . 13  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  <_  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )
124123ralrimiva 2799 . . . . . . . . . . . 12  |-  ( g  e.  dom  S.1  ->  A. t  e.  RR  (
g `  t )  <_  if ( 0  <_ 
( g `  t
) ,  ( g `
 t ) ,  0 ) )
12589feqmptd 5744 . . . . . . . . . . . . 13  |-  ( g  e.  dom  S.1  ->  g  =  ( t  e.  RR  |->  ( g `  t ) ) )
126103, 90, 106, 125, 109ofrfval2 6337 . . . . . . . . . . . 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 21191 . . . . . . . . . . 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 1316 . . . . . . . . . 10  |-  ( g  e.  dom  S.1  ->  ( S.1 `  g )  <_  ( S.1 `  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) )
130129, 114breqtrrd 4318 . . . . . . . . 9  |-  ( g  e.  dom  S.1  ->  ( S.1 `  g )  <_  ( S.2 `  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) )
131130ad2antlr 726 . . . . . . . 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 9531 . . . . . . 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 715 . . . . . 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 21153 . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  g  e.  dom  S.1 )  ->  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e. MblFn )
137 elrege0 11392 . . . . . . . . . . . . . . . . 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 664 . . . . . . . . . . . . . . . 16  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 )  e.  ( 0 [,) +oo ) )
139138, 86fmptd 5867 . . . . . . . . . . . . . . 15  |-  ( g  e.  dom  S.1  ->  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) : RR --> ( 0 [,) +oo ) )
140139adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  g  e.  dom  S.1 )  ->  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) : RR --> ( 0 [,) +oo ) )
141117adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  g  e.  dom  S.1 )  ->  ( S.2 `  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) )  e.  RR )
142106recnd 9412 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 )  e.  CC )
143142negcld 9706 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  -u if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 )  e.  CC )
144 ifcl 3831 . . . . . . . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . . . . . . . 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 9609 . . . . . . . . . . . . . . . . . . 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 477 . . . . . . . . . . . . . . . . . 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 648 . . . . . . . . . . . . . . . . 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 12922 . . . . . . . . . . . . . . . 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 12930 . . . . . . . . . . . . . . . 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 11392 . . . . . . . . . . . . . . . 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 664 . . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . . 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 5867 . . . . . . . . . . . . . 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 2503 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  t  ->  (
x  e.  D  <->  t  e.  D ) )
156 fveq2 5691 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  t  ->  ( F `  x )  =  ( F `  t ) )
157 eqidd 2444 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  t  ->  0  =  0 )
158155, 156, 157ifbieq12d 3816 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  t  ->  if ( x  e.  D ,  ( F `  x ) ,  0 )  =  if ( t  e.  D , 
( F `  t
) ,  0 ) )
159158fveq2d 5695 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  t  ->  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) )  =  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )
160 eqid 2443 . . . . . . . . . . . . . . . . . . . 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 5701 . . . . . . . . . . . . . . . . . . . 20  |-  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  _V
162159, 160, 161fvmpt 5774 . . . . . . . . . . . . . . . . . . 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 4304 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  t  ->  (
0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) )  <->  0  <_  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) ) )
164 fveq2 5691 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  t  ->  (
g `  x )  =  ( g `  t ) )
165164breq2d 4304 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  t  ->  (
0  <_  ( g `  x )  <->  0  <_  ( g `  t ) ) )
166165, 164, 157ifbieq12d 3816 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  t  ->  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 )  =  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) )
167166negeqd 9604 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  t  ->  -u if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 )  =  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )
168163, 166, 167ifbieq12d 3816 . . . . . . . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . . . . . . . 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 9608 . . . . . . . . . . . . . . . . . . . . 21  |-  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 )  e.  _V
17198, 170ifex 3858 . . . . . . . . . . . . . . . . . . . 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 5774 . . . . . . . . . . . . . . . . . . 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 6109 . . . . . . . . . . . . . . . . . 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 5695 . . . . . . . . . . . . . . . . 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 4374 . . . . . . . . . . . . . . . 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 5694 . . . . . . . . . . . . . . 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 5701 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( g `
 x )  e. 
_V
179178, 97ifex 3858 . . . . . . . . . . . . . . . . . . . . 21  |-  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 )  e. 
_V
180179, 97ifex 3858 . . . . . . . . . . . . . . . . . . . 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 6116 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -u
1  x.  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )  e.  _V
18397, 182ifex 3858 . . . . . . . . . . . . . . . . . . . 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 5559 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( F : D --> CC  ->  F  Fn  D )
186 frn 5565 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( F : D --> CC  ->  ran 
F  C_  CC )
187 ref 12601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  Re : CC
--> RR
188 ffn 5559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( Re : CC --> RR  ->  Re  Fn  CC )
189187, 188ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  Re  Fn  CC
190 fnco 5519 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( Re  Fn  CC  /\  F  Fn  D  /\  ran  F  C_  CC )  ->  ( Re  o.  F
)  Fn  D )
191189, 190mp3an1 1301 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( F  Fn  D  /\  ran  F  C_  CC )  ->  ( Re  o.  F
)  Fn  D )
192185, 186, 191syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( F : D --> CC  ->  ( Re  o.  F )  Fn  D )
193 elpreima 5823 . . . . . . . . . . . . . . . . . . . . . . . . . 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 5568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( Re : CC --> RR  /\  F : D --> CC )  ->  ( Re  o.  F ) : D --> RR )
196187, 4, 195sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ( Re  o.  F
) : D --> RR )
197196ffvelrnda 5843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  x  e.  D )  ->  (
( Re  o.  F
) `  x )  e.  RR )
198197biantrurd 508 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  D )  ->  (
0  <_  ( (
Re  o.  F ) `  x )  <->  ( (
( Re  o.  F
) `  x )  e.  RR  /\  0  <_ 
( ( Re  o.  F ) `  x
) ) ) )
199 elrege0 11392 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F : D --> CC  /\  x  e.  D )  ->  ( ( Re  o.  F ) `  x
)  =  ( Re
`  ( F `  x ) ) )
2024, 201sylan 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  D )  ->  (
( Re  o.  F
) `  x )  =  ( Re `  ( F `  x ) ) )
203202breq2d 4304 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 641 . . . . . . . . . . . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  e.  ( `' ( Re  o.  F )
" ( 0 [,) +oo ) )  <->  ( x  e.  D  /\  0  <_  ( Re `  ( F `  x )
) ) ) )
208 0le0 10411 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  0  <_  0
209208, 18breqtrri 4317 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  0  <_  ( Re `  0
)
210209biantru 505 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( -.  x  e.  D  <->  ( -.  x  e.  D  /\  0  <_  ( Re ` 
0 ) ) )
211 eldif 3338 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( RR  \  D )  <->  ( x  e.  RR  /\  -.  x  e.  D ) )
212211baibr 897 . . . . . . . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  e.  ( RR  \  D )  <->  ( -.  x  e.  D  /\  0  <_  ( Re ` 
0 ) ) ) )
215207, 214orbi12d 709 . . . . . . . . . . . . . . . . . . . . . 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 3497 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( ( `' ( Re  o.  F
) " ( 0 [,) +oo ) )  u.  ( RR  \  D ) )  <->  ( x  e.  ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  \/  x  e.  ( RR  \  D
) ) )
217 fveq2 5691 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( if ( x  e.  D ,  ( F `  x ) ,  0 )  =  ( F `
 x )  -> 
( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  =  ( Re `  ( F `
 x ) ) )
218217breq2d 4304 . . . . . . . . . . . . . . . . . . . . . . 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 5691 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( if ( x  e.  D ,  ( F `  x ) ,  0 )  =  0  -> 
( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  =  ( Re `  0 ) )
220219breq2d 4304 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( if ( x  e.  D ,  ( F `  x ) ,  0 )  =  0  -> 
( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) )  <->  0  <_  (
Re `  0 )
) )
221218, 220elimif 3823 . . . . . . . . . . . . . . . . . . . . . 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 3811 . . . . . . . . . . . . . . . . . . . 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 4378 . . . . . . . . . . . . . . . . . . 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 3811 . . . . . . . . . . . . . . . . . . . 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 4378 . . . . . . . . . . . . . . . . . . 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 6336 . . . . . . . . . . . . . . . . . 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 3797 . . . . . . . . . . . . . . . . . . . . . . 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 3797 . . . . . . . . . . . . . . . . . . . . . . 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 6109 . . . . . . . . . . . . . . . . . . . . . 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 3797 . . . . . . . . . . . . . . . . . . . . . 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 2478 . . . . . . . . . . . . . . . . . . . . 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 3799 . . . . . . . . . . . . . . . . . . . . . . 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 3799 . . . . . . . . . . . . . . . . . . . . . . 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 6109 . . . . . . . . . . . . . . . . . . . . . 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 3799 . . . . . . . . . . . . . . . . . . . . . 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 2478 . . . . . . . . . . . . . . . . . . . . 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 5843 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  ( g `  x )  e.  RR )
240239recnd 9412 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  ( g `  x )  e.  CC )
241 0cn 9378 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  CC
242 ifcl 3831 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( g `  x
)  e.  CC  /\  0  e.  CC )  ->  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 )  e.  CC )
243240, 241, 242sylancl 662 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 )  e.  CC )
244243addid1d 9569 . . . . . . . . . . . . . . . . . . . . 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 9796 . . . . . . . . . . . . . . . . . . . . . . 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 6107 . . . . . . . . . . . . . . . . . . . . . 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 9706 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  -u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 )  e.  CC )
248247addid2d 9570 . . . . . . . . . . . . . . . . . . . . . 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 2475 . . . . . . . . . . . . . . . . . . . . 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 3809 . . . . . . . . . . . . . . . . . . . 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 2487 . . . . . . . . . . . . . . . . . . 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 4378 . . . . . . . . . . . . . . . . . 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 2495 . . . . . . . . . . . . . . . . 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 9430 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  RR*
255 pnfxr 11092 . . . . . . . . . . . . . . . . . . . . . . 23  |- +oo  e.  RR*
256 0ltpnf 11103 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  < +oo
257 snunioo 11411 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 0  e.  RR*  /\ +oo  e.  RR*  /\  0  < +oo )  ->  ( { 0 }  u.  (
0 (,) +oo )
)  =  ( 0 [,) +oo ) )
258254, 255, 256, 257mp3an 1314 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( { 0 }  u.  (
0 (,) +oo )
)  =  ( 0 [,) +oo )
259258imaeq2i 5167 . . . . . . . . . . . . . . . . . . . . 21  |-  ( `' ( Re  o.  F
) " ( { 0 }  u.  (
0 (,) +oo )
) )  =  ( `' ( Re  o.  F ) " (
0 [,) +oo )
)
260 imaundi 5249 . . . . . . . . . . . . . . . . . . . . 21  |-  ( `' ( Re  o.  F
) " ( { 0 }  u.  (
0 (,) +oo )
) )  =  ( ( `' ( Re  o.  F ) " { 0 } )  u.  ( `' ( Re  o.  F )
" ( 0 (,) +oo ) ) )
261259, 260eqtr3i 2465 . . . . . . . . . . . . . . . . . . . 20  |-  ( `' ( Re  o.  F
) " ( 0 [,) +oo ) )  =  ( ( `' ( Re  o.  F
) " { 0 } )  u.  ( `' ( Re  o.  F ) " (
0 (,) +oo )
) )
262 ismbfcn 21109 . . . . . . . . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( Re  o.  F
)  e. MblFn )
266 mbfimasn 21112 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( Re  o.  F
)  e. MblFn  /\  (
Re  o.  F ) : D --> RR  /\  0  e.  RR )  ->  ( `' ( Re  o.  F ) " {
0 } )  e. 
dom  vol )
26788, 266mp3an3 1303 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( Re  o.  F
)  e. MblFn  /\  (
Re  o.  F ) : D --> RR )  -> 
( `' ( Re  o.  F ) " { 0 } )  e.  dom  vol )
268 mbfima 21110 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( Re  o.  F
)  e. MblFn  /\  (
Re  o.  F ) : D --> RR )  -> 
( `' ( Re  o.  F ) "
( 0 (,) +oo ) )  e.  dom  vol )
269 unmbl 21019 . . . . . . . . . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( `' ( Re  o.  F )
" { 0 } )  u.  ( `' ( Re  o.  F
) " ( 0 (,) +oo ) ) )  e.  dom  vol )
272261, 271syl5eqel 2527 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  e.  dom  vol )
273 fdm 5563 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F : D --> CC  ->  dom 
F  =  D )
2744, 273syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  dom  F  =  D )
275 mbfdm 21106 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F  e. MblFn  ->  dom  F  e.  dom  vol )
27643, 275syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  dom  F  e.  dom  vol )
277274, 276eqeltrrd 2518 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  D  e.  dom  vol )
278 difmbl 21024 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( RR  e.  dom  vol  /\  D  e.  dom  vol )  ->  ( RR  \  D )  e.  dom  vol )
27911, 277, 278sylancr 663 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( RR  \  D
)  e.  dom  vol )
280 unmbl 21019 . . . . . . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( `' ( Re  o.  F )
" ( 0 [,) +oo ) )  u.  ( RR  \  D ) )  e.  dom  vol )
282 fveq2 5691 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( t  =  x  ->  (
g `  t )  =  ( g `  x ) )
283282breq2d 4304 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  =  x  ->  (
0  <_  ( g `  t )  <->  0  <_  ( g `  x ) ) )
284 eqidd 2444 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  =  x  ->  0  =  0 )
285283, 282, 284ifbieq12d 3816 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  =  x  ->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 )  =  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )
286285, 86, 179fvmpt 5774 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  RR  ->  (
( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) `  x
)  =  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )
287286eqcomd 2448 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 )  =  ( ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) `  x
) )
288287ifeq1d 3807 . . . . . . . . . . . . . . . . . . . . 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 4374 . . . . . . . . . . . . . . . . . . . 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 21183 . . . . . . . . . . . . . . . . . . 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 ) ,  (