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

Theorem ftc1anclem5 30062
Description: Lemma for ftc1anc 30066, 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 3928 . . . . . . . . 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 4515 . . . . . . . 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 5855 . . . . . . 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 6012 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  D )  ->  ( F `  t )  e.  CC )
6 0cnd 9587 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  t  e.  D )  ->  0  e.  CC )
75, 6ifclda 3954 . . . . . . . . . . . 12  |-  ( ph  ->  if ( t  e.  D ,  ( F `
 t ) ,  0 )  e.  CC )
87recld 13001 . . . . . . . . . . 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 21817 . . . . . . . . . . . 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 3609 . . . . . . . . . . . . 13  |-  ( t  e.  ( RR  \  D )  ->  -.  t  e.  D )
1514adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( RR  \  D ) )  ->  -.  t  e.  D )
16 iffalse 3931 . . . . . . . . . . . . . 14  |-  ( -.  t  e.  D  ->  if ( t  e.  D ,  ( F `  t ) ,  0 )  =  0 )
1716fveq2d 5856 . . . . . . . . . . . . 13  |-  ( -.  t  e.  D  -> 
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  =  ( Re `  0 ) )
18 re0 12959 . . . . . . . . . . . . 13  |-  ( Re
`  0 )  =  0
1917, 18syl6eq 2498 . . . . . . . . . . . 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 3928 . . . . . . . . . . . . . 14  |-  ( t  e.  D  ->  if ( t  e.  D ,  ( F `  t ) ,  0 )  =  ( F `
 t ) )
2221fveq2d 5856 . . . . . . . . . . . . 13  |-  ( t  e.  D  ->  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) )  =  ( Re
`  ( F `  t ) ) )
2322mpteq2ia 4515 . . . . . . . . . . . 12  |-  ( t  e.  D  |->  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  =  ( t  e.  D  |->  ( Re
`  ( F `  t ) ) )
244feqmptd 5907 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F  =  ( t  e.  D  |->  ( F `
 t ) ) )
25 ftc1anc.i . . . . . . . . . . . . . . 15  |-  ( ph  ->  F  e.  L^1 )
2624, 25eqeltrrd 2530 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( t  e.  D  |->  ( F `  t
) )  e.  L^1 )
275iblcn 22071 . . . . . . . . . . . . . 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 2533 . . . . . . . . . . 11  |-  ( ph  ->  ( t  e.  D  |->  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  e.  L^1 )
3110, 12, 13, 20, 30iblss2 22078 . . . . . . . . . 10  |-  ( ph  ->  ( t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) )  e.  L^1 )
328recnd 9620 . . . . . . . . . . . . 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 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 13144 . . . . . . . . . . . . . 14  |-  abs : CC
--> RR
3635a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  abs : CC --> RR )
3736feqmptd 5907 . . . . . . . . . . . 12  |-  ( ph  ->  abs  =  ( x  e.  CC  |->  ( abs `  x ) ) )
38 fveq2 5852 . . . . . . . . . . . 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 6045 . . . . . . . . . . 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 6036 . . . . . . . . . . . 12  |-  ( ph  ->  ( t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) ) : RR --> RR )
42 iblmbf 22040 . . . . . . . . . . . . . . . . . 18  |-  ( F  e.  L^1  ->  F  e. MblFn )
4325, 42syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  F  e. MblFn )
4424, 43eqeltrrd 2530 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( t  e.  D  |->  ( F `  t
) )  e. MblFn )
455ismbfcn2 21912 . . . . . . . . . . . . . . . 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 2533 . . . . . . . . . . . . 13  |-  ( ph  ->  ( t  e.  D  |->  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  e. MblFn
)
4910, 12, 13, 20, 48mbfss 21919 . . . . . . . . . . . 12  |-  ( ph  ->  ( t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) )  e. MblFn )
50 ftc1anclem1 30058 . . . . . . . . . . . 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 2530 . . . . . . . . . 10  |-  ( ph  ->  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) )  e. MblFn )
539, 31, 52iblabsnc 30047 . . . . . . . . 9  |-  ( ph  ->  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) )  e.  L^1 )
5432abscld 13241 . . . . . . . . . . 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 13249 . . . . . . . . . . 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 22065 . . . . . . . . 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 2534 . . . . . 6  |-  ( ph  ->  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  e.  RR )
62 ltsubrp 11255 . . . . . 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 11230 . . . . . . 7  |-  ( Y  e.  RR+  ->  Y  e.  RR )
65 resubcl 9883 . . . . . . 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 9730 . . . . 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 9641 . . . . . . . . 9  |-  ( ph  ->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) )  e.  RR* )
71 elxrge0 11633 . . . . . . . . 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 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 6036 . . . . . 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 9641 . . . . 5  |-  ( (
ph  /\  Y  e.  RR+ )  ->  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y )  e. 
RR* )
78 itg2leub 22007 . . . . 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 2894 . . 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 21958 . . . . . . . . 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 2441 . . . . . . . . . . . 12  |-  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) )  =  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) )
8786i1fpos 21979 . . . . . . . . . . 11  |-  ( g  e.  dom  S.1  ->  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  dom  S.1 )
88 0re 9594 . . . . . . . . . . . . . 14  |-  0  e.  RR
89 i1ff 21949 . . . . . . . . . . . . . . 15  |-  ( g  e.  dom  S.1  ->  g : RR --> RR )
9089ffvelrnda 6012 . . . . . . . . . . . . . 14  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  e.  RR )
91 max1 11390 . . . . . . . . . . . . . 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 2855 . . . . . . . . . . . 12  |-  ( g  e.  dom  S.1  ->  A. t  e.  RR  0  <_  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) )
94 ax-resscn 9547 . . . . . . . . . . . . . . 15  |-  RR  C_  CC
9594a1i 11 . . . . . . . . . . . . . 14  |-  ( g  e.  dom  S.1  ->  RR  C_  CC )
96 fvex 5862 . . . . . . . . . . . . . . . . 17  |-  ( g `
 t )  e. 
_V
97 c0ex 9588 . . . . . . . . . . . . . . . . 17  |-  0  e.  _V
9896, 97ifex 3991 . . . . . . . . . . . . . . . 16  |-  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 )  e. 
_V
9998, 86fnmpti 5695 . . . . . . . . . . . . . . 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 21946 . . . . . . . . . . . . 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 9581 . . . . . . . . . . . . . . 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 3964 . . . . . . . . . . . . . . 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 5029 . . . . . . . . . . . . . . 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 6538 . . . . . . . . . . . . 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 22009 . . . . . . . . . . 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 21958 . . . . . . . . . . 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 2529 . . . . . . . . 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 9662 . . . . . . . . . 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 11392 . . . . . . . . . . . . . 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 2855 . . . . . . . . . . . 12  |-  ( g  e.  dom  S.1  ->  A. t  e.  RR  (
g `  t )  <_  if ( 0  <_ 
( g `  t
) ,  ( g `
 t ) ,  0 ) )
12589feqmptd 5907 . . . . . . . . . . . . 13  |-  ( g  e.  dom  S.1  ->  g  =  ( t  e.  RR  |->  ( g `  t ) ) )
126103, 90, 106, 125, 109ofrfval2 6538 . . . . . . . . . . . 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 21986 . . . . . . . . . . 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 1325 . . . . . . . . . 10  |-  ( g  e.  dom  S.1  ->  ( S.1 `  g )  <_  ( S.1 `  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) )
130129, 114breqtrrd 4459 . . . . . . . . 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 9740 . . . . . . 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 21948 . . . . . . . . . . . . . . . 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 11631 . . . . . . . . . . . . . . . . 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 6036 . . . . . . . . . . . . . . 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 9620 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 )  e.  CC )
143142negcld 9918 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  -u if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 )  e.  CC )
144142, 143ifcld 3965 . . . . . . . . . . . . . . . . . . 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 )
145 subcl 9819 . . . . . . . . . . . . . . . . . . 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 )
14632, 144, 145syl2an 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 )
147146anassrs 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 )
148147abscld 13241 . . . . . . . . . . . . . . . 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 )
149147absge0d 13249 . . . . . . . . . . . . . . . 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 ) ) ) ) )
150 elrege0 11631 . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
151148, 149, 150sylanbrc 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 ) )
152 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 ) ) ) ) )
153151, 152fmptd 6036 . . . . . . . . . . . . . 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 ) )
154 eleq1 2513 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  t  ->  (
x  e.  D  <->  t  e.  D ) )
155 fveq2 5852 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  t  ->  ( F `  x )  =  ( F `  t ) )
156154, 155ifbieq1d 3945 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  t  ->  if ( x  e.  D ,  ( F `  x ) ,  0 )  =  if ( t  e.  D , 
( F `  t
) ,  0 ) )
157156fveq2d 5856 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  t  ->  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) )  =  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )
158 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 ) ) )
159 fvex 5862 . . . . . . . . . . . . . . . . . . . 20  |-  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  _V
160157, 158, 159fvmpt 5937 . . . . . . . . . . . . . . . . . . 19  |-  ( t  e.  RR  ->  (
( x  e.  RR  |->  ( Re `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) `  t
)  =  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )
161157breq2d 4445 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  t  ->  (
0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) )  <->  0  <_  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) ) )
162 fveq2 5852 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  t  ->  (
g `  x )  =  ( g `  t ) )
163162breq2d 4445 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  t  ->  (
0  <_  ( g `  x )  <->  0  <_  ( g `  t ) ) )
164163, 162ifbieq1d 3945 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  t  ->  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 )  =  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) )
165164negeqd 9814 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  t  ->  -u if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 )  =  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )
166161, 164, 165ifbieq12d 3949 . . . . . . . . . . . . . . . . . . . 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 ) ) )
167 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 ) ) )
168 negex 9818 . . . . . . . . . . . . . . . . . . . . 21  |-  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 )  e.  _V
16998, 168ifex 3991 . . . . . . . . . . . . . . . . . . . 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
170166, 167, 169fvmpt 5937 . . . . . . . . . . . . . . . . . . 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 ) ) )
171160, 170oveq12d 6295 . . . . . . . . . . . . . . . . . 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 ) ) ) )
172171fveq2d 5856 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
173172mpteq2ia 4515 . . . . . . . . . . . . . . . 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 ) ) ) ) )
174173fveq2i 5855 . . . . . . . . . . . . . . 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 ) ) ) ) ) )
175102a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  RR  e.  _V )
176 fvex 5862 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( g `
 x )  e. 
_V
177176, 97ifex 3991 . . . . . . . . . . . . . . . . . . . . 21  |-  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 )  e. 
_V
178177, 97ifex 3991 . . . . . . . . . . . . . . . . . . . 20  |-  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ,  0 )  e.  _V
179178a1i 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 )
180 ovex 6305 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -u
1  x.  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )  e.  _V
18197, 180ifex 3991 . . . . . . . . . . . . . . . . . . . 20  |-  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  0 ,  ( -u
1  x.  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) )  e.  _V
182181a1i 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 )
183 ffn 5717 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( F : D --> CC  ->  F  Fn  D )
184 frn 5723 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( F : D --> CC  ->  ran 
F  C_  CC )
185 ref 12919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  Re : CC
--> RR
186 ffn 5717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( Re : CC --> RR  ->  Re  Fn  CC )
187185, 186ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  Re  Fn  CC
188 fnco 5675 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( Re  Fn  CC  /\  F  Fn  D  /\  ran  F  C_  CC )  ->  ( Re  o.  F
)  Fn  D )
189187, 188mp3an1 1310 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( F  Fn  D  /\  ran  F  C_  CC )  ->  ( Re  o.  F
)  Fn  D )
190183, 184, 189syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( F : D --> CC  ->  ( Re  o.  F )  Fn  D )
191 elpreima 5988 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( Re  o.  F )  Fn  D  ->  (
x  e.  ( `' ( Re  o.  F
) " ( 0 [,) +oo ) )  <-> 
( x  e.  D  /\  ( ( Re  o.  F ) `  x
)  e.  ( 0 [,) +oo ) ) ) )
1924, 190, 1913syl 20 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( x  e.  ( `' ( Re  o.  F ) " (
0 [,) +oo )
)  <->  ( x  e.  D  /\  ( ( Re  o.  F ) `
 x )  e.  ( 0 [,) +oo ) ) ) )
193 fco 5727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( Re : CC --> RR  /\  F : D --> CC )  ->  ( Re  o.  F ) : D --> RR )
194185, 4, 193sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ( Re  o.  F
) : D --> RR )
195194ffvelrnda 6012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  x  e.  D )  ->  (
( Re  o.  F
) `  x )  e.  RR )
196195biantrurd 508 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  D )  ->  (
0  <_  ( (
Re  o.  F ) `  x )  <->  ( (
( Re  o.  F
) `  x )  e.  RR  /\  0  <_ 
( ( Re  o.  F ) `  x
) ) ) )
197 elrege0 11631 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( Re  o.  F
) `  x )  e.  ( 0 [,) +oo ) 
<->  ( ( ( Re  o.  F ) `  x )  e.  RR  /\  0  <_  ( (
Re  o.  F ) `  x ) ) )
198196, 197syl6bbr 263 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  D )  ->  (
0  <_  ( (
Re  o.  F ) `  x )  <->  ( (
Re  o.  F ) `  x )  e.  ( 0 [,) +oo )
) )
199 fvco3 5931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F : D --> CC  /\  x  e.  D )  ->  ( ( Re  o.  F ) `  x
)  =  ( Re
`  ( F `  x ) ) )
2004, 199sylan 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  D )  ->  (
( Re  o.  F
) `  x )  =  ( Re `  ( F `  x ) ) )
201200breq2d 4445 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  D )  ->  (
0  <_  ( (
Re  o.  F ) `  x )  <->  0  <_  ( Re `  ( F `
 x ) ) ) )
202198, 201bitr3d 255 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  D )  ->  (
( ( Re  o.  F ) `  x
)  e.  ( 0 [,) +oo )  <->  0  <_  ( Re `  ( F `
 x ) ) ) )
203202pm5.32da 641 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( x  e.  D  /\  ( ( Re  o.  F ) `
 x )  e.  ( 0 [,) +oo ) )  <->  ( x  e.  D  /\  0  <_  ( Re `  ( F `  x )
) ) ) )
204192, 203bitrd 253 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( x  e.  ( `' ( Re  o.  F ) " (
0 [,) +oo )
)  <->  ( x  e.  D  /\  0  <_ 
( Re `  ( F `  x )
) ) ) )
205204adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  e.  ( `' ( Re  o.  F )
" ( 0 [,) +oo ) )  <->  ( x  e.  D  /\  0  <_  ( Re `  ( F `  x )
) ) ) )
206 0le0 10626 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  0  <_  0
207206, 18breqtrri 4458 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  0  <_  ( Re `  0
)
208207biantru 505 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( -.  x  e.  D  <->  ( -.  x  e.  D  /\  0  <_  ( Re ` 
0 ) ) )
209 eldif 3468 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( RR  \  D )  <->  ( x  e.  RR  /\  -.  x  e.  D ) )
210209baibr 902 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  RR  ->  ( -.  x  e.  D  <->  x  e.  ( RR  \  D ) ) )
211208, 210syl5rbbr 260 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  RR  ->  (
x  e.  ( RR 
\  D )  <->  ( -.  x  e.  D  /\  0  <_  ( Re ` 
0 ) ) ) )
212211adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  e.  ( RR  \  D )  <->  ( -.  x  e.  D  /\  0  <_  ( Re ` 
0 ) ) ) )
213205, 212orbi12d 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 ) ) ) ) )
214 elun 3627 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( ( `' ( Re  o.  F
) " ( 0 [,) +oo ) )  u.  ( RR  \  D ) )  <->  ( x  e.  ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  \/  x  e.  ( RR  \  D
) ) )
215 fveq2 5852 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( if ( x  e.  D ,  ( F `  x ) ,  0 )  =  ( F `
 x )  -> 
( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  =  ( Re `  ( F `
 x ) ) )
216215breq2d 4445 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( if ( x  e.  D ,  ( F `  x ) ,  0 )  =  ( F `
 x )  -> 
( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) )  <->  0  <_  (
Re `  ( F `  x ) ) ) )
217 fveq2 5852 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( if ( x  e.  D ,  ( F `  x ) ,  0 )  =  0  -> 
( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  =  ( Re `  0 ) )
218217breq2d 4445 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( if ( x  e.  D ,  ( F `  x ) ,  0 )  =  0  -> 
( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) )  <->  0  <_  (
Re `  0 )
) )
219216, 218elimif 3956 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  <->  ( (
x  e.  D  /\  0  <_  ( Re `  ( F `  x ) ) )  \/  ( -.  x  e.  D  /\  0  <_  ( Re
`  0 ) ) ) )
220213, 214, 2193bitr4g 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 ) ) ) )
221220ifbid 3944 . . . . . . . . . . . . . . . . . . . 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 ) )
222221mpteq2dva 4519 . . . . . . . . . . . . . . . . . . 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 ) ) )
223220ifbid 3944 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
224223mpteq2dva 4519 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
225175, 179, 182, 222, 224offval2 6537 . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
226 ovif12 6362 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
22789ffvelrnda 6012 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  ( g `  x )  e.  RR )
228227recnd 9620 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  ( g `  x )  e.  CC )
229 0cn 9586 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  CC
230 ifcl 3964 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( g `  x
)  e.  CC  /\  0  e.  CC )  ->  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 )  e.  CC )
231228, 229, 230sylancl 662 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 )  e.  CC )
232231addid1d 9778 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  ( if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 )  +  0 )  =  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) )
233231mulm1d 10009 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
234233oveq2d 6293 . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
235231negcld 9918 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  -u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 )  e.  CC )
236235addid2d 9779 . . . . . . . . . . . . . . . . . . . . . 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 ) )
237234, 236eqtrd 2482 . . . . . . . . . . . . . . . . . . . . 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 ) )
238232, 237ifeq12d 3942 . . . . . . . . . . . . . . . . . . . 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 ) ) )
239226, 238syl5eq 2494 . . . . . . . . . . . . . . . . . . 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 ) ) )
240239mpteq2dva 4519 . . . . . . . . . . . . . . . . . 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 ) ) ) )
241225, 240sylan9eq 2502 . . . . . . . . . . . . . . . . 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 ) ) ) )
242 0xr 9638 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  RR*
243 pnfxr 11325 . . . . . . . . . . . . . . . . . . . . . . 23  |- +oo  e.  RR*
244 0ltpnf 11336 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  < +oo
245 snunioo 11650 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 0  e.  RR*  /\ +oo  e.  RR*  /\  0  < +oo )  ->  ( { 0 }  u.  (
0 (,) +oo )
)  =  ( 0 [,) +oo ) )
246242, 243, 244, 245mp3an 1323 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( { 0 }  u.  (
0 (,) +oo )
)  =  ( 0 [,) +oo )
247246imaeq2i 5321 . . . . . . . . . . . . . . . . . . . . 21  |-  ( `' ( Re  o.  F
) " ( { 0 }  u.  (
0 (,) +oo )
) )  =  ( `' ( Re  o.  F ) " (
0 [,) +oo )
)
248 imaundi 5404 . . . . . . . . . . . . . . . . . . . . 21  |-  ( `' ( Re  o.  F
) " ( { 0 }  u.  (
0 (,) +oo )
) )  =  ( ( `' ( Re  o.  F ) " { 0 } )  u.  ( `' ( Re  o.  F )
" ( 0 (,) +oo ) ) )
249247, 248eqtr3i 2472 . . . . . . . . . . . . . . . . . . . 20  |-  ( `' ( Re  o.  F
) " ( 0 [,) +oo ) )  =  ( ( `' ( Re  o.  F
) " { 0 } )  u.  ( `' ( Re  o.  F ) " (
0 (,) +oo )
) )
250 ismbfcn 21904 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( F : D --> CC  ->  ( F  e. MblFn  <->  ( ( Re  o.  F )  e. MblFn  /\  ( Im  o.  F
)  e. MblFn ) )
)
2514, 250syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( F  e. MblFn  <->  ( (
Re  o.  F )  e. MblFn  /\  ( Im  o.  F )  e. MblFn )
) )
25243, 251mpbid 210 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( Re  o.  F )  e. MblFn  /\  (
Im  o.  F )  e. MblFn ) )
253252simpld 459 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( Re  o.  F
)  e. MblFn )
254 mbfimasn 21907 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( Re  o.  F
)  e. MblFn  /\  (
Re  o.  F ) : D --> RR  /\  0  e.  RR )  ->  ( `' ( Re  o.  F ) " {
0 } )  e. 
dom  vol )
25588, 254mp3an3 1312 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( Re  o.  F
)  e. MblFn  /\  (
Re  o.  F ) : D --> RR )  -> 
( `' ( Re  o.  F ) " { 0 } )  e.  dom  vol )
256 mbfima 21905 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( Re  o.  F
)  e. MblFn  /\  (
Re  o.  F ) : D --> RR )  -> 
( `' ( Re  o.  F ) "
( 0 (,) +oo ) )  e.  dom  vol )
257 unmbl 21814 . . . . . . . . . . . . . . . . . . . . . 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 )
258255, 256, 257syl2anc 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 )
259253, 194, 258syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( `' ( Re  o.  F )
" { 0 } )  u.  ( `' ( Re  o.  F
) " ( 0 (,) +oo ) ) )  e.  dom  vol )
260249, 259syl5eqel 2533 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  e.  dom  vol )
261 fdm 5721 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F : D --> CC  ->  dom 
F  =  D )
2624, 261syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  dom  F  =  D )
263 mbfdm 21901 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F  e. MblFn  ->  dom  F  e.  dom  vol )
26443, 263syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  dom  F  e.  dom  vol )
265262, 264eqeltrrd 2530 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  D  e.  dom  vol )
266 difmbl 21819 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( RR  e.  dom  vol  /\  D  e.  dom  vol )  ->  ( RR  \  D )  e.  dom  vol )
26711, 265, 266sylancr 663 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( RR  \  D
)  e.  dom  vol )
268 unmbl 21814 . . . . . . . . . . . . . . . . . . 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 )
269260, 267, 268syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( `' ( Re  o.  F )
" ( 0 [,) +oo ) )  u.  ( RR  \  D ) )  e.  dom  vol )
270 fveq2 5852 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( t  =  x  ->  (
g `  t )  =  ( g `  x ) )
271270breq2d 4445 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  =  x  ->  (
0  <_  ( g `  t )  <->  0  <_  ( g `  x ) ) )
272271, 270ifbieq1d 3945 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  =  x  ->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 )  =  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )
273272, 86, 177fvmpt 5937 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  RR  ->  (
( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) `  x
)  =  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )
274273eqcomd 2449 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 )  =  ( ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) `  x
) )
275274ifeq1d 3940 . . . . . . . . . . . . . . . . . . . . 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 ) )
276275mpteq2ia 4515 . . . . . . . . . . . . . . . . . . . 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 ) )
277276i1fres 21978 . . . . . . . . . . . . . . . . . . 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 )
278 id 22 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 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.  dom  S.1 )
279 neg1rr 10641 . . . . . . . . . . . . . . . . . . . . . 22  |-  -u 1  e.  RR
280279a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  dom  S.1 
->  -u 1  e.  RR )
281278, 280i1fmulc 21976 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  dom  S.1 
->  ( ( RR  X.  { -u 1 } )  oF  x.  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) )  e. 
dom  S.1 )
282 cmmbl 21811 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) )  e.  dom  vol  ->  ( RR  \  ( ( `' ( Re  o.  F ) " (
0 [,) +oo )
)  u.  ( RR 
\  D ) ) )  e.  dom  vol )
283 ifnot 3967 . . . . . . . . . . . . . . . . . . . . . . 23  |-  if ( -.  x  e.  ( ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) ,  0 )  =  if ( x  e.  ( ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  0 ,  (
-u 1  x.  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ) )
284 eldif 3468 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( RR  \ 
( ( `' ( Re  o.  F )
" ( 0 [,) +oo ) )  u.  ( RR  \  D ) ) )  <->  ( x  e.  RR  /\  -.  x  e.  ( ( `' ( Re  o.  F )
" ( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ) )
285284baibr 902 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  RR  ->  ( -.  x  e.  (
( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) )  <-> 
x  e.  ( RR 
\  ( ( `' ( Re  o.  F
) " ( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ) ) )
286 tru 1385 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |- T.
287 negex 9818 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  -u 1  e.  _V
288287fconst 5757 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( RR 
X.  { -u 1 } ) : RR --> { -u 1 }
289 ffn 5717 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( RR  X.  { -u
1 } ) : RR --> { -u 1 }  ->  ( RR  X.  { -u 1 } )  Fn  RR )
290288, 289mp1i 12 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( T. 
->  ( RR  X.  { -u 1 } )  Fn  RR )
29199a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( T. 
->  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  Fn  RR )
292102a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( T. 
->  RR  e.  _V )
293 inidm 3689 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( RR 
i^i  RR )  =  RR
294287fvconst2 6107 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  RR  ->  (
( RR  X.  { -u 1 } ) `  x )  =  -u
1 )
295294adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( T.  /\  x  e.  RR )  ->  (
( RR  X.  { -u 1 } ) `  x )  =  -u
1 )
296273adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( T.  /\  x  e.  RR )  ->  (
( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) `  x
)  =  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )
297290, 291, 292, 292, 293, 295, 296ofval 6530 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( T.  /\  x  e.  RR )  ->  (
( ( RR  X.  { -u 1 } )  oF  x.  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) `  x )  =  (
-u 1  x.  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ) )
298286, 297mpan 670 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  RR  ->  (
( ( RR  X.  { -u 1 } )  oF  x.  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) `  x )  =  (
-u 1  x.  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ) )
299298eqcomd 2449 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  RR  ->  ( -u 1  x.  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )  =  ( ( ( RR  X.  { -u
1 } )  oF  x.  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) `  x ) )
300285, 299ifbieq1d 3945 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  RR  ->  if ( -.  x  e.  ( ( `' ( Re  o.  F )
" ( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) ,  0 )  =  if ( x  e.  ( RR  \  ( ( `' ( Re  o.  F ) " (
0 [,) +oo )
)  u.  ( RR 
\  D ) ) ) ,  ( ( ( RR  X.  { -u 1 } )  oF  x.  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) `  x ) ,  0 ) )
301283, 300syl5eqr 2496 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 ( x  e.  ( RR  \  (
( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ) ,  ( ( ( RR  X.  { -u 1 } )  oF  x.  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) `  x ) ,  0 ) )
302301mpteq2ia 4515 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ( x  e.  ( RR  \ 
( ( `' ( Re  o.  F )
" ( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ) ,  ( ( ( RR  X.  { -u 1 } )  oF  x.  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) `  x ) ,  0 ) )
303302i1fres 21978 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( RR  X.  { -u 1 } )  oF  x.  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 )