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

Theorem ftc1anclem6 28381
Description: Lemma for ftc1anc 28384- construction of simple functions within an arbitrary absolute distance of the given function. Similar to Lemma 565Ib of [Fremlin5] p. 218, but without Fremlin's additional step of converting the simple function into a continuous one, which is unnecessary to this lemma's use; also, two simple functions are used to allow for complex-valued  F. (Contributed by Brendan Leahy, 31-May-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
ftc1anclem6  |-  ( (
ph  /\  Y  e.  RR+ )  ->  E. f  e.  dom  S.1 E. g  e. 
dom  S.1 ( S.2 `  (
t  e.  RR  |->  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ) )  < 
Y )
Distinct variable groups:    f, g,
t, x, A    B, f, g, t, x    D, f, g, t, x    f, F, g, t, x    ph, f,
g, t, x    f, G, g    f, Y, g, t, x
Allowed substitution hints:    G( x, t)

Proof of Theorem ftc1anclem6
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 rphalfcl 11011 . . 3  |-  ( Y  e.  RR+  ->  ( Y  /  2 )  e.  RR+ )
2 ftc1anc.g . . . 4  |-  G  =  ( x  e.  ( A [,] B ) 
|->  S. ( A (,) x ) ( F `
 t )  _d t )
3 ftc1anc.a . . . 4  |-  ( ph  ->  A  e.  RR )
4 ftc1anc.b . . . 4  |-  ( ph  ->  B  e.  RR )
5 ftc1anc.le . . . 4  |-  ( ph  ->  A  <_  B )
6 ftc1anc.s . . . 4  |-  ( ph  ->  ( A (,) B
)  C_  D )
7 ftc1anc.d . . . 4  |-  ( ph  ->  D  C_  RR )
8 ftc1anc.i . . . 4  |-  ( ph  ->  F  e.  L^1 )
9 ftc1anc.f . . . 4  |-  ( ph  ->  F : D --> CC )
102, 3, 4, 5, 6, 7, 8, 9ftc1anclem5 28380 . . 3  |-  ( (
ph  /\  ( Y  /  2 )  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  /  2
) )
111, 10sylan2 471 . 2  |-  ( (
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  /  2
) )
12 eqid 2441 . . . . 5  |-  ( x  e.  ( A [,] B )  |->  S. ( A (,) x ) ( ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y
) ) ) `  t )  _d t )  =  ( x  e.  ( A [,] B )  |->  S. ( A (,) x ) ( ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y
) ) ) `  t )  _d t )
13 ax-icn 9337 . . . . . . . 8  |-  _i  e.  CC
14 ine0 9776 . . . . . . . 8  |-  _i  =/=  0
1513, 14reccli 10057 . . . . . . 7  |-  ( 1  /  _i )  e.  CC
1615a1i 11 . . . . . 6  |-  ( ph  ->  ( 1  /  _i )  e.  CC )
179ffvelrnda 5840 . . . . . 6  |-  ( (
ph  /\  y  e.  D )  ->  ( F `  y )  e.  CC )
189feqmptd 5741 . . . . . . 7  |-  ( ph  ->  F  =  ( y  e.  D  |->  ( F `
 y ) ) )
1918, 8eqeltrrd 2516 . . . . . 6  |-  ( ph  ->  ( y  e.  D  |->  ( F `  y
) )  e.  L^1 )
20 divrec2 10007 . . . . . . . . . 10  |-  ( ( ( F `  y
)  e.  CC  /\  _i  e.  CC  /\  _i  =/=  0 )  ->  (
( F `  y
)  /  _i )  =  ( ( 1  /  _i )  x.  ( F `  y
) ) )
2113, 14, 20mp3an23 1301 . . . . . . . . 9  |-  ( ( F `  y )  e.  CC  ->  (
( F `  y
)  /  _i )  =  ( ( 1  /  _i )  x.  ( F `  y
) ) )
2217, 21syl 16 . . . . . . . 8  |-  ( (
ph  /\  y  e.  D )  ->  (
( F `  y
)  /  _i )  =  ( ( 1  /  _i )  x.  ( F `  y
) ) )
2322mpteq2dva 4375 . . . . . . 7  |-  ( ph  ->  ( y  e.  D  |->  ( ( F `  y )  /  _i ) )  =  ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y ) ) ) )
24 iblmbf 21145 . . . . . . . . 9  |-  ( ( y  e.  D  |->  ( F `  y ) )  e.  L^1 
->  ( y  e.  D  |->  ( F `  y
) )  e. MblFn )
2519, 24syl 16 . . . . . . . 8  |-  ( ph  ->  ( y  e.  D  |->  ( F `  y
) )  e. MblFn )
26 fveq2 5688 . . . . . . . . . . . . . . . . 17  |-  ( y  =  x  ->  ( F `  y )  =  ( F `  x ) )
2726fveq2d 5692 . . . . . . . . . . . . . . . 16  |-  ( y  =  x  ->  (
Re `  ( F `  y ) )  =  ( Re `  ( F `  x )
) )
2827cbvmptv 4380 . . . . . . . . . . . . . . 15  |-  ( y  e.  D  |->  ( Re
`  ( F `  y ) ) )  =  ( x  e.  D  |->  ( Re `  ( F `  x ) ) )
2928eleq1i 2504 . . . . . . . . . . . . . 14  |-  ( ( y  e.  D  |->  ( Re `  ( F `
 y ) ) )  e. MblFn  <->  ( x  e.  D  |->  ( Re `  ( F `  x ) ) )  e. MblFn )
3017recld 12679 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  D )  ->  (
Re `  ( F `  y ) )  e.  RR )
3130recnd 9408 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  D )  ->  (
Re `  ( F `  y ) )  e.  CC )
3231adantlr 709 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  D  |->  ( Re `  ( F `
 x ) ) )  e. MblFn )  /\  y  e.  D )  ->  ( Re `  ( F `  y )
)  e.  CC )
3329biimpri 206 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  D  |->  ( Re `  ( F `
 x ) ) )  e. MblFn  ->  ( y  e.  D  |->  ( Re
`  ( F `  y ) ) )  e. MblFn )
3433adantl 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  D  |->  ( Re
`  ( F `  x ) ) )  e. MblFn )  ->  (
y  e.  D  |->  ( Re `  ( F `
 y ) ) )  e. MblFn )
3532, 34mbfneg 21028 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  D  |->  ( Re
`  ( F `  x ) ) )  e. MblFn )  ->  (
y  e.  D  |->  -u ( Re `  ( F `
 y ) ) )  e. MblFn )
3629, 35sylan2b 472 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( y  e.  D  |->  ( Re
`  ( F `  y ) ) )  e. MblFn )  ->  (
y  e.  D  |->  -u ( Re `  ( F `
 y ) ) )  e. MblFn )
379ffvelrnda 5840 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  D )  ->  ( F `  x )  e.  CC )
3837recld 12679 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  D )  ->  (
Re `  ( F `  x ) )  e.  RR )
3938recnd 9408 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  D )  ->  (
Re `  ( F `  x ) )  e.  CC )
4039negnegd 9706 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  D )  ->  -u -u (
Re `  ( F `  x ) )  =  ( Re `  ( F `  x )
) )
4140mpteq2dva 4375 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( x  e.  D  |-> 
-u -u ( Re `  ( F `  x ) ) )  =  ( x  e.  D  |->  ( Re `  ( F `
 x ) ) ) )
4241, 28syl6eqr 2491 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( x  e.  D  |-> 
-u -u ( Re `  ( F `  x ) ) )  =  ( y  e.  D  |->  ( Re `  ( F `
 y ) ) ) )
4342adantr 462 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( y  e.  D  |->  -u (
Re `  ( F `  y ) ) )  e. MblFn )  ->  (
x  e.  D  |->  -u -u ( Re `  ( F `  x )
) )  =  ( y  e.  D  |->  ( Re `  ( F `
 y ) ) ) )
44 negex 9604 . . . . . . . . . . . . . . . 16  |-  -u (
Re `  ( F `  x ) )  e. 
_V
4544a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
y  e.  D  |->  -u ( Re `  ( F `
 y ) ) )  e. MblFn )  /\  x  e.  D )  -> 
-u ( Re `  ( F `  x ) )  e.  _V )
4627negeqd 9600 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  x  ->  -u (
Re `  ( F `  y ) )  = 
-u ( Re `  ( F `  x ) ) )
4746cbvmptv 4380 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  D  |->  -u (
Re `  ( F `  y ) ) )  =  ( x  e.  D  |->  -u ( Re `  ( F `  x ) ) )
4847eleq1i 2504 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  D  |->  -u ( Re `  ( F `
 y ) ) )  e. MblFn  <->  ( x  e.  D  |->  -u ( Re `  ( F `  x ) ) )  e. MblFn )
4948biimpi 194 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  D  |->  -u ( Re `  ( F `
 y ) ) )  e. MblFn  ->  ( x  e.  D  |->  -u (
Re `  ( F `  x ) ) )  e. MblFn )
5049adantl 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( y  e.  D  |->  -u (
Re `  ( F `  y ) ) )  e. MblFn )  ->  (
x  e.  D  |->  -u ( Re `  ( F `
 x ) ) )  e. MblFn )
5145, 50mbfneg 21028 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( y  e.  D  |->  -u (
Re `  ( F `  y ) ) )  e. MblFn )  ->  (
x  e.  D  |->  -u -u ( Re `  ( F `  x )
) )  e. MblFn )
5243, 51eqeltrrd 2516 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( y  e.  D  |->  -u (
Re `  ( F `  y ) ) )  e. MblFn )  ->  (
y  e.  D  |->  ( Re `  ( F `
 y ) ) )  e. MblFn )
5336, 52impbida 823 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( y  e.  D  |->  ( Re `  ( F `  y ) ) )  e. MblFn  <->  ( y  e.  D  |->  -u (
Re `  ( F `  y ) ) )  e. MblFn ) )
54 divcl 9996 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F `  y
)  e.  CC  /\  _i  e.  CC  /\  _i  =/=  0 )  ->  (
( F `  y
)  /  _i )  e.  CC )
55 imre 12593 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F `  y
)  /  _i )  e.  CC  ->  (
Im `  ( ( F `  y )  /  _i ) )  =  ( Re `  ( -u _i  x.  ( ( F `  y )  /  _i ) ) ) )
5654, 55syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  y
)  e.  CC  /\  _i  e.  CC  /\  _i  =/=  0 )  ->  (
Im `  ( ( F `  y )  /  _i ) )  =  ( Re `  ( -u _i  x.  ( ( F `  y )  /  _i ) ) ) )
5713, 14, 56mp3an23 1301 . . . . . . . . . . . . . . . 16  |-  ( ( F `  y )  e.  CC  ->  (
Im `  ( ( F `  y )  /  _i ) )  =  ( Re `  ( -u _i  x.  ( ( F `  y )  /  _i ) ) ) )
5813, 14, 54mp3an23 1301 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F `  y )  e.  CC  ->  (
( F `  y
)  /  _i )  e.  CC )
59 mulneg1 9777 . . . . . . . . . . . . . . . . . . 19  |-  ( ( _i  e.  CC  /\  ( ( F `  y )  /  _i )  e.  CC )  ->  ( -u _i  x.  ( ( F `  y )  /  _i ) )  =  -u ( _i  x.  (
( F `  y
)  /  _i ) ) )
6013, 58, 59sylancr 658 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  y )  e.  CC  ->  ( -u _i  x.  ( ( F `  y )  /  _i ) )  =  -u ( _i  x.  ( ( F `  y )  /  _i ) ) )
61 divcan2 9998 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( F `  y
)  e.  CC  /\  _i  e.  CC  /\  _i  =/=  0 )  ->  (
_i  x.  ( ( F `  y )  /  _i ) )  =  ( F `  y
) )
6213, 14, 61mp3an23 1301 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F `  y )  e.  CC  ->  (
_i  x.  ( ( F `  y )  /  _i ) )  =  ( F `  y
) )
6362negeqd 9600 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  y )  e.  CC  ->  -u (
_i  x.  ( ( F `  y )  /  _i ) )  = 
-u ( F `  y ) )
6460, 63eqtrd 2473 . . . . . . . . . . . . . . . . 17  |-  ( ( F `  y )  e.  CC  ->  ( -u _i  x.  ( ( F `  y )  /  _i ) )  =  -u ( F `  y ) )
6564fveq2d 5692 . . . . . . . . . . . . . . . 16  |-  ( ( F `  y )  e.  CC  ->  (
Re `  ( -u _i  x.  ( ( F `  y )  /  _i ) ) )  =  ( Re `  -u ( F `  y )
) )
66 reneg 12610 . . . . . . . . . . . . . . . 16  |-  ( ( F `  y )  e.  CC  ->  (
Re `  -u ( F `
 y ) )  =  -u ( Re `  ( F `  y ) ) )
6757, 65, 663eqtrd 2477 . . . . . . . . . . . . . . 15  |-  ( ( F `  y )  e.  CC  ->  (
Im `  ( ( F `  y )  /  _i ) )  = 
-u ( Re `  ( F `  y ) ) )
6817, 67syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  D )  ->  (
Im `  ( ( F `  y )  /  _i ) )  = 
-u ( Re `  ( F `  y ) ) )
6968mpteq2dva 4375 . . . . . . . . . . . . 13  |-  ( ph  ->  ( y  e.  D  |->  ( Im `  (
( F `  y
)  /  _i ) ) )  =  ( y  e.  D  |->  -u ( Re `  ( F `
 y ) ) ) )
7069eleq1d 2507 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( y  e.  D  |->  ( Im `  ( ( F `  y )  /  _i ) ) )  e. MblFn  <->  ( y  e.  D  |->  -u ( Re `  ( F `
 y ) ) )  e. MblFn ) )
7153, 70bitr4d 256 . . . . . . . . . . 11  |-  ( ph  ->  ( ( y  e.  D  |->  ( Re `  ( F `  y ) ) )  e. MblFn  <->  ( y  e.  D  |->  ( Im
`  ( ( F `
 y )  /  _i ) ) )  e. MblFn
) )
72 imval 12592 . . . . . . . . . . . . . 14  |-  ( ( F `  y )  e.  CC  ->  (
Im `  ( F `  y ) )  =  ( Re `  (
( F `  y
)  /  _i ) ) )
7317, 72syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  D )  ->  (
Im `  ( F `  y ) )  =  ( Re `  (
( F `  y
)  /  _i ) ) )
7473mpteq2dva 4375 . . . . . . . . . . . 12  |-  ( ph  ->  ( y  e.  D  |->  ( Im `  ( F `  y )
) )  =  ( y  e.  D  |->  ( Re `  ( ( F `  y )  /  _i ) ) ) )
7574eleq1d 2507 . . . . . . . . . . 11  |-  ( ph  ->  ( ( y  e.  D  |->  ( Im `  ( F `  y ) ) )  e. MblFn  <->  ( y  e.  D  |->  ( Re
`  ( ( F `
 y )  /  _i ) ) )  e. MblFn
) )
7671, 75anbi12d 705 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( y  e.  D  |->  ( Re
`  ( F `  y ) ) )  e. MblFn  /\  ( y  e.  D  |->  ( Im
`  ( F `  y ) ) )  e. MblFn )  <->  ( (
y  e.  D  |->  ( Im `  ( ( F `  y )  /  _i ) ) )  e. MblFn  /\  (
y  e.  D  |->  ( Re `  ( ( F `  y )  /  _i ) ) )  e. MblFn ) ) )
77 ancom 448 . . . . . . . . . 10  |-  ( ( ( y  e.  D  |->  ( Im `  (
( F `  y
)  /  _i ) ) )  e. MblFn  /\  (
y  e.  D  |->  ( Re `  ( ( F `  y )  /  _i ) ) )  e. MblFn )  <->  ( (
y  e.  D  |->  ( Re `  ( ( F `  y )  /  _i ) ) )  e. MblFn  /\  (
y  e.  D  |->  ( Im `  ( ( F `  y )  /  _i ) ) )  e. MblFn ) )
7876, 77syl6bb 261 . . . . . . . . 9  |-  ( ph  ->  ( ( ( y  e.  D  |->  ( Re
`  ( F `  y ) ) )  e. MblFn  /\  ( y  e.  D  |->  ( Im
`  ( F `  y ) ) )  e. MblFn )  <->  ( (
y  e.  D  |->  ( Re `  ( ( F `  y )  /  _i ) ) )  e. MblFn  /\  (
y  e.  D  |->  ( Im `  ( ( F `  y )  /  _i ) ) )  e. MblFn ) ) )
7917ismbfcn2 21017 . . . . . . . . 9  |-  ( ph  ->  ( ( y  e.  D  |->  ( F `  y ) )  e. MblFn  <->  ( ( y  e.  D  |->  ( Re `  ( F `  y )
) )  e. MblFn  /\  (
y  e.  D  |->  ( Im `  ( F `
 y ) ) )  e. MblFn ) ) )
8017, 58syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  D )  ->  (
( F `  y
)  /  _i )  e.  CC )
8180ismbfcn2 21017 . . . . . . . . 9  |-  ( ph  ->  ( ( y  e.  D  |->  ( ( F `
 y )  /  _i ) )  e. MblFn  <->  ( (
y  e.  D  |->  ( Re `  ( ( F `  y )  /  _i ) ) )  e. MblFn  /\  (
y  e.  D  |->  ( Im `  ( ( F `  y )  /  _i ) ) )  e. MblFn ) ) )
8278, 79, 813bitr4d 285 . . . . . . . 8  |-  ( ph  ->  ( ( y  e.  D  |->  ( F `  y ) )  e. MblFn  <->  ( y  e.  D  |->  ( ( F `  y
)  /  _i ) )  e. MblFn ) )
8325, 82mpbid 210 . . . . . . 7  |-  ( ph  ->  ( y  e.  D  |->  ( ( F `  y )  /  _i ) )  e. MblFn )
8423, 83eqeltrrd 2516 . . . . . 6  |-  ( ph  ->  ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y )
) )  e. MblFn )
8516, 17, 19, 84iblmulc2nc 28366 . . . . 5  |-  ( ph  ->  ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y )
) )  e.  L^1 )
86 mulcl 9362 . . . . . . 7  |-  ( ( ( 1  /  _i )  e.  CC  /\  ( F `  y )  e.  CC )  ->  (
( 1  /  _i )  x.  ( F `  y ) )  e.  CC )
8715, 17, 86sylancr 658 . . . . . 6  |-  ( (
ph  /\  y  e.  D )  ->  (
( 1  /  _i )  x.  ( F `  y ) )  e.  CC )
88 eqid 2441 . . . . . 6  |-  ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y ) ) )  =  ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y
) ) )
8987, 88fmptd 5864 . . . . 5  |-  ( ph  ->  ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y )
) ) : D --> CC )
9012, 3, 4, 5, 6, 7, 85, 89ftc1anclem5 28380 . . . 4  |-  ( (
ph  /\  ( Y  /  2 )  e.  RR+ )  ->  E. g  e.  dom  S.1 ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y
) ) ) `  t ) ,  0 ) )  -  (
g `  t )
) ) ) )  <  ( Y  / 
2 ) )
911, 90sylan2 471 . . 3  |-  ( (
ph  /\  Y  e.  RR+ )  ->  E. g  e.  dom  S.1 ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y
) ) ) `  t ) ,  0 ) )  -  (
g `  t )
) ) ) )  <  ( Y  / 
2 ) )
929ffvelrnda 5840 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  D )  ->  ( F `  t )  e.  CC )
93 0cnd 9375 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  t  e.  D )  ->  0  e.  CC )
9492, 93ifclda 3818 . . . . . . . . . . . 12  |-  ( ph  ->  if ( t  e.  D ,  ( F `
 t ) ,  0 )  e.  CC )
95 imval 12592 . . . . . . . . . . . 12  |-  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  e.  CC  ->  ( Im `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  =  ( Re
`  ( if ( t  e.  D , 
( F `  t
) ,  0 )  /  _i ) ) )
9694, 95syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  =  ( Re `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  /  _i ) ) )
97 fveq2 5688 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  t  ->  ( F `  y )  =  ( F `  t ) )
9897oveq2d 6106 . . . . . . . . . . . . . . . . 17  |-  ( y  =  t  ->  (
( 1  /  _i )  x.  ( F `  y ) )  =  ( ( 1  /  _i )  x.  ( F `  t )
) )
99 ovex 6115 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  /  _i )  x.  ( F `  t ) )  e. 
_V
10098, 88, 99fvmpt 5771 . . . . . . . . . . . . . . . 16  |-  ( t  e.  D  ->  (
( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y )
) ) `  t
)  =  ( ( 1  /  _i )  x.  ( F `  t ) ) )
101100adantl 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  D )  ->  (
( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y )
) ) `  t
)  =  ( ( 1  /  _i )  x.  ( F `  t ) ) )
102 divrec2 10007 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  t
)  e.  CC  /\  _i  e.  CC  /\  _i  =/=  0 )  ->  (
( F `  t
)  /  _i )  =  ( ( 1  /  _i )  x.  ( F `  t
) ) )
10313, 14, 102mp3an23 1301 . . . . . . . . . . . . . . . 16  |-  ( ( F `  t )  e.  CC  ->  (
( F `  t
)  /  _i )  =  ( ( 1  /  _i )  x.  ( F `  t
) ) )
10492, 103syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  D )  ->  (
( F `  t
)  /  _i )  =  ( ( 1  /  _i )  x.  ( F `  t
) ) )
105101, 104eqtr4d 2476 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  D )  ->  (
( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y )
) ) `  t
)  =  ( ( F `  t )  /  _i ) )
106105ifeq1da 3816 . . . . . . . . . . . . 13  |-  ( ph  ->  if ( t  e.  D ,  ( ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y ) ) ) `
 t ) ,  0 )  =  if ( t  e.  D ,  ( ( F `
 t )  /  _i ) ,  0 ) )
107 oveq1 6097 . . . . . . . . . . . . . . 15  |-  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  =  ( F `
 t )  -> 
( if ( t  e.  D ,  ( F `  t ) ,  0 )  /  _i )  =  (
( F `  t
)  /  _i ) )
108 oveq1 6097 . . . . . . . . . . . . . . 15  |-  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  =  0  -> 
( if ( t  e.  D ,  ( F `  t ) ,  0 )  /  _i )  =  (
0  /  _i ) )
109107, 108ifsb 3799 . . . . . . . . . . . . . 14  |-  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  /  _i )  =  if ( t  e.  D ,  ( ( F `  t
)  /  _i ) ,  ( 0  /  _i ) )
11013, 14div0i 10061 . . . . . . . . . . . . . . 15  |-  ( 0  /  _i )  =  0
111 ifeq2 3793 . . . . . . . . . . . . . . 15  |-  ( ( 0  /  _i )  =  0  ->  if ( t  e.  D ,  ( ( F `
 t )  /  _i ) ,  ( 0  /  _i ) )  =  if ( t  e.  D ,  ( ( F `  t
)  /  _i ) ,  0 ) )
112110, 111ax-mp 5 . . . . . . . . . . . . . 14  |-  if ( t  e.  D , 
( ( F `  t )  /  _i ) ,  ( 0  /  _i ) )  =  if ( t  e.  D ,  ( ( F `  t
)  /  _i ) ,  0 )
113109, 112eqtri 2461 . . . . . . . . . . . . 13  |-  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  /  _i )  =  if ( t  e.  D ,  ( ( F `  t
)  /  _i ) ,  0 )
114106, 113syl6eqr 2491 . . . . . . . . . . . 12  |-  ( ph  ->  if ( t  e.  D ,  ( ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y ) ) ) `
 t ) ,  0 )  =  ( if ( t  e.  D ,  ( F `
 t ) ,  0 )  /  _i ) )
115114fveq2d 5692 . . . . . . . . . . 11  |-  ( ph  ->  ( Re `  if ( t  e.  D ,  ( ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y ) ) ) `
 t ) ,  0 ) )  =  ( Re `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  /  _i ) ) )
11696, 115eqtr4d 2476 . . . . . . . . . 10  |-  ( ph  ->  ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  =  ( Re `  if ( t  e.  D , 
( ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y
) ) ) `  t ) ,  0 ) ) )
117116oveq1d 6105 . . . . . . . . 9  |-  ( ph  ->  ( ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
)  =  ( ( Re `  if ( t  e.  D , 
( ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y
) ) ) `  t ) ,  0 ) )  -  (
g `  t )
) )
118117fveq2d 5692 . . . . . . . 8  |-  ( ph  ->  ( abs `  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) )  =  ( abs `  ( ( Re `  if ( t  e.  D , 
( ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y
) ) ) `  t ) ,  0 ) )  -  (
g `  t )
) ) )
119118mpteq2dv 4376 . . . . . . 7  |-  ( ph  ->  ( t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) ) )  =  ( t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y
) ) ) `  t ) ,  0 ) )  -  (
g `  t )
) ) ) )
120119fveq2d 5692 . . . . . 6  |-  ( ph  ->  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) ) ) )  =  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y
) ) ) `  t ) ,  0 ) )  -  (
g `  t )
) ) ) ) )
121120breq1d 4299 . . . . 5  |-  ( ph  ->  ( ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) ) ) )  < 
( Y  /  2
)  <->  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y
) ) ) `  t ) ,  0 ) )  -  (
g `  t )
) ) ) )  <  ( Y  / 
2 ) ) )
122121rexbidv 2734 . . . 4  |-  ( ph  ->  ( E. g  e. 
dom  S.1 ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) ) ) )  < 
( Y  /  2
)  <->  E. g  e.  dom  S.1 ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y
) ) ) `  t ) ,  0 ) )  -  (
g `  t )
) ) ) )  <  ( Y  / 
2 ) ) )
123122adantr 462 . . 3  |-  ( (
ph  /\  Y  e.  RR+ )  ->  ( E. g  e.  dom  S.1 ( S.2 `  ( t  e.  RR  |->  ( abs `  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) ) )  <  ( Y  / 
2 )  <->  E. g  e.  dom  S.1 ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y
) ) ) `  t ) ,  0 ) )  -  (
g `  t )
) ) ) )  <  ( Y  / 
2 ) ) )
12491, 123mpbird 232 . 2  |-  ( (
ph  /\  Y  e.  RR+ )  ->  E. g  e.  dom  S.1 ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) ) ) )  < 
( Y  /  2
) )
125 reeanv 2886 . . 3  |-  ( E. f  e.  dom  S.1 E. g  e.  dom  S.1 ( ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) ) ) )  < 
( Y  /  2
)  /\  ( S.2 `  ( t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) ) ) )  < 
( Y  /  2
) )  <->  ( E. f  e.  dom  S.1 ( S.2 `  ( t  e.  RR  |->  ( abs `  (
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) ) )  <  ( Y  / 
2 )  /\  E. g  e.  dom  S.1 ( S.2 `  ( t  e.  RR  |->  ( abs `  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) ) )  <  ( Y  / 
2 ) ) )
126 eleq1 2501 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  t  ->  (
x  e.  D  <->  t  e.  D ) )
127 fveq2 5688 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  t  ->  ( F `  x )  =  ( F `  t ) )
128 eqidd 2442 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  t  ->  0  =  0 )
129126, 127, 128ifbieq12d 3813 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  t  ->  if ( x  e.  D ,  ( F `  x ) ,  0 )  =  if ( t  e.  D , 
( F `  t
) ,  0 ) )
130129fveq2d 5692 . . . . . . . . . . . . . . . . 17  |-  ( x  =  t  ->  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) )  =  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )
131 eqid 2441 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  RR  |->  ( Re
`  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) )  =  ( x  e.  RR  |->  ( Re
`  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) )
132 fvex 5698 . . . . . . . . . . . . . . . . 17  |-  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  _V
133130, 131, 132fvmpt 5771 . . . . . . . . . . . . . . . 16  |-  ( t  e.  RR  ->  (
( x  e.  RR  |->  ( Re `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) `  t
)  =  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )
134133oveq1d 6105 . . . . . . . . . . . . . . 15  |-  ( t  e.  RR  ->  (
( ( x  e.  RR  |->  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ) `  t )  -  (
f `  t )
)  =  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) )
135134fveq2d 5692 . . . . . . . . . . . . . 14  |-  ( t  e.  RR  ->  ( abs `  ( ( ( x  e.  RR  |->  ( Re `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) `  t
)  -  ( f `
 t ) ) )  =  ( abs `  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) )
136135mpteq2ia 4371 . . . . . . . . . . . . 13  |-  ( t  e.  RR  |->  ( abs `  ( ( ( x  e.  RR  |->  ( Re
`  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ) `  t )  -  ( f `  t ) ) ) )  =  ( t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) )
137136fveq2i 5691 . . . . . . . . . . . 12  |-  ( S.2 `  ( t  e.  RR  |->  ( abs `  ( ( ( x  e.  RR  |->  ( Re `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) `  t
)  -  ( f `
 t ) ) ) ) )  =  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) ) ) )
138 rembl 20922 . . . . . . . . . . . . . . . . . . 19  |-  RR  e.  dom  vol
139138a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  RR  e.  dom  vol )
140 0cnd 9375 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  -.  x  e.  D )  ->  0  e.  CC )
14137, 140ifclda 3818 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  if ( x  e.  D ,  ( F `
 x ) ,  0 )  e.  CC )
142141adantr 462 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  D )  ->  if ( x  e.  D ,  ( F `  x ) ,  0 )  e.  CC )
143 eldifn 3476 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( RR  \  D )  ->  -.  x  e.  D )
144143adantl 463 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( RR  \  D ) )  ->  -.  x  e.  D )
145 iffalse 3796 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  x  e.  D  ->  if ( x  e.  D ,  ( F `  x ) ,  0 )  =  0 )
146144, 145syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( RR  \  D ) )  ->  if (
x  e.  D , 
( F `  x
) ,  0 )  =  0 )
1479feqmptd 5741 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  F  =  ( x  e.  D  |->  ( F `
 x ) ) )
148 iftrue 3794 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  D  ->  if ( x  e.  D ,  ( F `  x ) ,  0 )  =  ( F `
 x ) )
149148mpteq2ia 4371 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  D  |->  if ( x  e.  D , 
( F `  x
) ,  0 ) )  =  ( x  e.  D  |->  ( F `
 x ) )
150147, 149syl6eqr 2491 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  F  =  ( x  e.  D  |->  if ( x  e.  D , 
( F `  x
) ,  0 ) ) )
151150, 8eqeltrrd 2516 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( x  e.  D  |->  if ( x  e.  D ,  ( F `
 x ) ,  0 ) )  e.  L^1 )
1527, 139, 142, 146, 151iblss2 21183 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( x  e.  RR  |->  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  e.  L^1 )
153141adantr 462 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  if ( x  e.  D , 
( F `  x
) ,  0 )  e.  CC )
154153iblcn 21176 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( x  e.  RR  |->  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  e.  L^1  <->  ( (
x  e.  RR  |->  ( Re `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) )  e.  L^1  /\  ( x  e.  RR  |->  ( Im `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) )  e.  L^1 ) ) )
155152, 154mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( x  e.  RR  |->  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) )  e.  L^1  /\  (
x  e.  RR  |->  ( Im `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) )  e.  L^1 ) )
156155simpld 456 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( x  e.  RR  |->  ( Re `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) )  e.  L^1 )
157153recld 12679 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ( Re
`  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  e.  RR )
158157, 131fmptd 5864 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( x  e.  RR  |->  ( Re `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) : RR --> RR )
159156, 158jca 529 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( x  e.  RR  |->  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) )  e.  L^1  /\  (
x  e.  RR  |->  ( Re `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) : RR --> RR ) )
160 ftc1anclem4 28379 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  ( x  e.  RR  |->  ( Re `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) )  e.  L^1  /\  ( x  e.  RR  |->  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ) : RR --> RR )  -> 
( S.2 `  ( t  e.  RR  |->  ( abs `  ( ( ( x  e.  RR  |->  ( Re
`  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ) `  t )  -  ( f `  t ) ) ) ) )  e.  RR )
1611603expb 1183 . . . . . . . . . . . . . 14  |-  ( ( f  e.  dom  S.1  /\  ( ( x  e.  RR  |->  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) )  e.  L^1  /\  (
x  e.  RR  |->  ( Re `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) : RR --> RR ) )  ->  ( S.2 `  ( t  e.  RR  |->  ( abs `  (
( ( x  e.  RR  |->  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ) `  t )  -  (
f `  t )
) ) ) )  e.  RR )
162159, 161sylan2 471 . . . . . . . . . . . . 13  |-  ( ( f  e.  dom  S.1  /\ 
ph )  ->  ( S.2 `  ( t  e.  RR  |->  ( abs `  (
( ( x  e.  RR  |->  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ) `  t )  -  (
f `  t )
) ) ) )  e.  RR )
163162ancoms 450 . . . . . . . . . . . 12  |-  ( (
ph  /\  f  e.  dom  S.1 )  ->  ( S.2 `  ( t  e.  RR  |->  ( abs `  (
( ( x  e.  RR  |->  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ) `  t )  -  (
f `  t )
) ) ) )  e.  RR )
164137, 163syl5eqelr 2526 . . . . . . . . . . 11  |-  ( (
ph  /\  f  e.  dom  S.1 )  ->  ( S.2 `  ( t  e.  RR  |->  ( abs `  (
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) ) )  e.  RR )
165129fveq2d 5692 . . . . . . . . . . . . . . . . 17  |-  ( x  =  t  ->  (
Im `  if (
x  e.  D , 
( F `  x
) ,  0 ) )  =  ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )
166 eqid 2441 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  RR  |->  ( Im
`  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) )  =  ( x  e.  RR  |->  ( Im
`  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) )
167 fvex 5698 . . . . . . . . . . . . . . . . 17  |-  ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  _V
168165, 166, 167fvmpt 5771 . . . . . . . . . . . . . . . 16  |-  ( t  e.  RR  ->  (
( x  e.  RR  |->  ( Im `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) `  t
)  =  ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )
169168oveq1d 6105 . . . . . . . . . . . . . . 15  |-  ( t  e.  RR  ->  (
( ( x  e.  RR  |->  ( Im `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ) `  t )  -  (
g `  t )
)  =  ( ( Im `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) )
170169fveq2d 5692 . . . . . . . . . . . . . 14  |-  ( t  e.  RR  ->  ( abs `  ( ( ( x  e.  RR  |->  ( Im `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) `  t
)  -  ( g `
 t ) ) )  =  ( abs `  ( ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) )
171170mpteq2ia 4371 . . . . . . . . . . . . 13  |-  ( t  e.  RR  |->  ( abs `  ( ( ( x  e.  RR  |->  ( Im
`  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ) `  t )  -  ( g `  t ) ) ) )  =  ( t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) )
172171fveq2i 5691 . . . . . . . . . . . 12  |-  ( S.2 `  ( t  e.  RR  |->  ( abs `  ( ( ( x  e.  RR  |->  ( Im `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) `  t
)  -  ( g `
 t ) ) ) ) )  =  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) ) ) )
173155simprd 460 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( x  e.  RR  |->  ( Im `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) )  e.  L^1 )
174141imcld 12680 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( Im `  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  e.  RR )
175174adantr 462 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ( Im
`  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  e.  RR )
176175, 166fmptd 5864 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( x  e.  RR  |->  ( Im `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) : RR --> RR )
177173, 176jca 529 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( x  e.  RR  |->  ( Im `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) )  e.  L^1  /\  (
x  e.  RR  |->  ( Im `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) : RR --> RR ) )
178 ftc1anclem4 28379 . . . . . . . . . . . . . . 15  |-  ( ( g  e.  dom  S.1  /\  ( x  e.  RR  |->  ( Im `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) )  e.  L^1  /\  ( x  e.  RR  |->  ( Im `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ) : RR --> RR )  -> 
( S.2 `  ( t  e.  RR  |->  ( abs `  ( ( ( x  e.  RR  |->  ( Im
`  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ) `  t )  -  ( g `  t ) ) ) ) )  e.  RR )
1791783expb 1183 . . . . . . . . . . . . . 14  |-  ( ( g  e.  dom  S.1  /\  ( ( x  e.  RR  |->  ( Im `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) )  e.  L^1  /\  (
x  e.  RR  |->  ( Im `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) : RR --> RR ) )  ->  ( S.2 `  ( t  e.  RR  |->  ( abs `  (
( ( x  e.  RR  |->  ( Im `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ) `  t )  -  (
g `  t )
) ) ) )  e.  RR )
180177, 179sylan2 471 . . . . . . . . . . . . 13  |-  ( ( g  e.  dom  S.1  /\ 
ph )  ->  ( S.2 `  ( t  e.  RR  |->  ( abs `  (
( ( x  e.  RR  |->  ( Im `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ) `  t )  -  (
g `  t )
) ) ) )  e.  RR )
181180ancoms 450 . . . . . . . . . . . 12  |-  ( (
ph  /\  g  e.  dom  S.1 )  ->  ( S.2 `  ( t  e.  RR  |->  ( abs `  (
( ( x  e.  RR  |->  ( Im `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ) `  t )  -  (
g `  t )
) ) ) )  e.  RR )
182172, 181syl5eqelr 2526 . . . . . . . . . . 11  |-  ( (
ph  /\  g  e.  dom  S.1 )  ->  ( S.2 `  ( t  e.  RR  |->  ( abs `  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) ) )  e.  RR )
183164, 182anim12dan 828 . . . . . . . . . 10  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  -> 
( ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) ) ) )  e.  RR  /\  ( S.2 `  ( t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) ) ) )  e.  RR ) )
1841rpred 11023 . . . . . . . . . . 11  |-  ( Y  e.  RR+  ->  ( Y  /  2 )  e.  RR )
185184, 184jca 529 . . . . . . . . . 10  |-  ( Y  e.  RR+  ->  ( ( Y  /  2 )  e.  RR  /\  ( Y  /  2 )  e.  RR ) )
186 lt2add 9820 . . . . . . . . . 10  |-  ( ( ( ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) ) ) )  e.  RR  /\  ( S.2 `  ( t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) ) ) )  e.  RR )  /\  (
( Y  /  2
)  e.  RR  /\  ( Y  /  2
)  e.  RR ) )  ->  ( (
( S.2 `  ( t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) ) )  <  ( Y  / 
2 )  /\  ( S.2 `  ( t  e.  RR  |->  ( abs `  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) ) )  <  ( Y  / 
2 ) )  -> 
( ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) ) ) )  +  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) ) ) ) )  <  ( ( Y  /  2 )  +  ( Y  /  2
) ) ) )
187183, 185, 186syl2an 474 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  Y  e.  RR+ )  ->  (
( ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) ) ) )  < 
( Y  /  2
)  /\  ( S.2 `  ( t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) ) ) )  < 
( Y  /  2
) )  ->  (
( S.2 `  ( t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) ) )  +  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) ) ) ) )  <  ( ( Y  /  2 )  +  ( Y  /  2
) ) ) )
188187an32s 797 . . . . . . . 8  |-  ( ( ( ph  /\  Y  e.  RR+ )  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  ->  (
( ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) ) ) )  < 
( Y  /  2
)  /\  ( S.2 `  ( t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) ) ) )  < 
( Y  /  2
) )  ->  (
( S.2 `  ( t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) ) )  +  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) ) ) ) )  <  ( ( Y  /  2 )  +  ( Y  /  2
) ) ) )
18994recld 12679 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  RR )
190189recnd 9408 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  CC )
191 i1ff 21054 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  e.  dom  S.1  ->  f : RR --> RR )
192191ffvelrnda 5840 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( f `  t )  e.  RR )
193192recnd 9408 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( f `  t )  e.  CC )
194 subcl 9605 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  CC  /\  ( f `  t
)  e.  CC )  ->  ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( f `  t ) )  e.  CC )
195190, 193, 194syl2an 474 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  t  e.  RR ) )  -> 
( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  e.  CC )
196195anassrs 643 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  f  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  e.  CC )
197196adantlrr 715 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  RR )  ->  (
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  e.  CC )
19894imcld 12680 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  RR )
199198recnd 9408 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  CC )
200 i1ff 21054 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g  e.  dom  S.1  ->  g : RR --> RR )
201200ffvelrnda 5840 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  e.  RR )
202201recnd 9408 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  e.  CC )
203 subcl 9605 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  CC  /\  ( g `  t
)  e.  CC )  ->  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) )  e.  CC )
204199, 202, 203syl2an 474 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( g  e.  dom  S.1  /\  t  e.  RR ) )  -> 
( ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
)  e.  CC )
205204anassrs 643 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
)  e.  CC )
206 mulcl 9362 . . . . . . . . . . . . . . . . . . 19  |-  ( ( _i  e.  CC  /\  ( ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
)  e.  CC )  ->  ( _i  x.  ( ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) )  e.  CC )
20713, 205, 206sylancr 658 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
_i  x.  ( (
Im `  if (
t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) )  e.  CC )
208207adantlrl 714 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  RR )  ->  (
_i  x.  ( (
Im `  if (
t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) )  e.  CC )
209197, 208addcld 9401 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  RR )  ->  (
( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  +  ( _i  x.  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) ) )  e.  CC )
210209abscld 12918 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  RR )  ->  ( abs `  ( ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) )  +  ( _i  x.  ( ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) ) )  e.  RR )
211210rexrd 9429 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  RR )  ->  ( abs `  ( ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) )  +  ( _i  x.  ( ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) ) )  e.  RR* )
212209absge0d 12926 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  RR )  ->  0  <_  ( abs `  (
( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  +  ( _i  x.  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) ) ) ) )
213 elxrge0 11390 . . . . . . . . . . . . . 14  |-  ( ( abs `  ( ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  +  ( _i  x.  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) ) ) )  e.  ( 0 [,] +oo )  <->  ( ( abs `  (
( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  +  ( _i  x.  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) ) ) )  e.  RR*  /\  0  <_  ( abs `  ( ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( f `  t ) )  +  ( _i  x.  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) ) ) ) )
214211, 212, 213sylanbrc 659 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  RR )  ->  ( abs `  ( ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) )  +  ( _i  x.  ( ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) ) )  e.  ( 0 [,] +oo ) )
215 eqid 2441 . . . . . . . . . . . . 13  |-  ( t  e.  RR  |->  ( abs `  ( ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( f `  t ) )  +  ( _i  x.  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) ) ) )  =  ( t  e.  RR  |->  ( abs `  ( ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( f `  t ) )  +  ( _i  x.  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) ) ) )
216214, 215fmptd 5864 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  -> 
( t  e.  RR  |->  ( abs `  ( ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  +  ( _i  x.  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) ) ) ) ) : RR --> ( 0 [,] +oo ) )
217 rexr 9425 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  RR  ->  x  e.  RR* )
218217anim1i 565 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  RR  /\  0  <_  x )  -> 
( x  e.  RR*  /\  0  <_  x )
)
219 elrege0 11388 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( 0 [,) +oo )  <->  ( x  e.  RR  /\  0  <_  x ) )
220 elxrge0 11390 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( 0 [,] +oo )  <->  ( x  e. 
RR*  /\  0  <_  x ) )
221218, 219, 2203imtr4i 266 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( 0 [,) +oo )  ->  x  e.  ( 0 [,] +oo ) )
222221ssriv 3357 . . . . . . . . . . . . . . 15  |-  ( 0 [,) +oo )  C_  ( 0 [,] +oo )
223 ge0addcl 11393 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  ( 0 [,) +oo )  /\  y  e.  ( 0 [,) +oo ) )  ->  ( x  +  y )  e.  ( 0 [,) +oo )
)
224222, 223sseldi 3351 . . . . . . . . . . . . . 14  |-  ( ( x  e.  ( 0 [,) +oo )  /\  y  e.  ( 0 [,) +oo ) )  ->  ( x  +  y )  e.  ( 0 [,] +oo )
)
225224adantl 463 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
x  e.  ( 0 [,) +oo )  /\  y  e.  ( 0 [,) +oo ) ) )  ->  ( x  +  y )  e.  ( 0 [,] +oo ) )
226196abscld 12918 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  f  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( f `  t ) ) )  e.  RR )
227196absge0d 12926 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  f  e.  dom  S.1 )  /\  t  e.  RR )  ->  0  <_  ( abs `  (
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) )
228 elrege0 11388 . . . . . . . . . . . . . . . 16  |-  ( ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) )  e.  ( 0 [,) +oo )  <->  ( ( abs `  ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( f `  t ) ) )  e.  RR  /\  0  <_  ( abs `  (
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) ) )
229226, 227, 228sylanbrc 659 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  f  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( f `  t ) ) )  e.  ( 0 [,) +oo ) )
230 eqid 2441 . . . . . . . . . . . . . . 15  |-  ( t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) )  =  ( t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) ) )
231229, 230fmptd 5864 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  f  e.  dom  S.1 )  ->  (
t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) ) ) : RR --> ( 0 [,) +oo ) )
232231adantrr 711 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  -> 
( t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) ) ) : RR --> ( 0 [,) +oo ) )
233205abscld 12918 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) )  e.  RR )
234205absge0d 12926 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  0  <_  ( abs `  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) )
235 elrege0 11388 . . . . . . . . . . . . . . . 16  |-  ( ( abs `  ( ( Im `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) )  e.  ( 0 [,) +oo )  <->  ( ( abs `  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) )  e.  RR  /\  0  <_  ( abs `  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) ) )
236233, 234, 235sylanbrc 659 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) )  e.  ( 0 [,) +oo ) )
237 eqid 2441 . . . . . . . . . . . . . . 15  |-  ( t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) )  =  ( t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) ) )
238236, 237fmptd 5864 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  g  e.  dom  S.1 )  ->  (
t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) ) ) : RR --> ( 0 [,) +oo ) )
239238adantrl 710 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  -> 
( t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) ) ) : RR --> ( 0 [,) +oo ) )
240 reex 9369 . . . . . . . . . . . . . 14  |-  RR  e.  _V
241240a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  ->  RR  e.  _V )
242 inidm 3556 . . . . . . . . . . . . 13  |-  ( RR 
i^i  RR )  =  RR
243225, 232, 239, 241, 241, 242off 6333 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  -> 
( ( t  e.  RR  |->  ( abs `  (
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) )  oF  +  ( t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) ) ) : RR --> ( 0 [,] +oo ) )
244197, 208abstrid 12938 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  RR )  ->  ( abs `  ( ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) )  +  ( _i  x.  ( ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) ) )  <_  ( ( abs `  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) )  +  ( abs `  ( _i  x.  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) ) ) ) )
245244ralrimiva 2797 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  ->  A. t  e.  RR  ( abs `  ( ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  +  ( _i  x.  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) ) ) )  <_  (
( abs `  (
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) )  +  ( abs `  ( _i  x.  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) ) ) ) )
246 ovex 6115 . . . . . . . . . . . . . . 15  |-  ( ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) )  +  ( abs `  ( _i  x.  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) ) )  e.  _V
247246a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  RR )  ->  (
( abs `  (
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) )  +  ( abs `  ( _i  x.  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) ) ) )  e.  _V )
248 eqidd 2442 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  -> 
( t  e.  RR  |->  ( abs `  ( ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  +  ( _i  x.  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) ) ) ) )  =  ( t  e.  RR  |->  ( abs `  ( ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  +  ( _i  x.  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) ) ) ) ) )
249 fvex 5698 . . . . . . . . . . . . . . . 16  |-  ( abs `  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) )  e.  _V
250249a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  RR )  ->  ( abs `  ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( f `  t ) ) )  e.  _V )
251 fvex 5698 . . . . . . . . . . . . . . . 16  |-  ( abs `  ( _i  x.  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) )  e. 
_V
252251a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  RR )  ->  ( abs `  ( _i  x.  ( ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) )  e. 
_V )
253 eqidd 2442 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  -> 
( t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) ) )  =  ( t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) ) ) )
254 absmul 12779 . . . . . . . . . . . . . . . . . . 19  |-  ( ( _i  e.  CC  /\  ( ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
)  e.  CC )  ->  ( abs `  (
_i  x.  ( (
Im `  if (
t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) ) )  =  ( ( abs `  _i )  x.  ( abs `  ( ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) ) )
25513, 205, 254sylancr 658 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( _i  x.  ( ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) )  =  ( ( abs `  _i )  x.  ( abs `  ( ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) ) )
256 absi 12771 . . . . . . . . . . . . . . . . . . . 20  |-  ( abs `  _i )  =  1
257256oveq1i 6100 . . . . . . . . . . . . . . . . . . 19  |-  ( ( abs `  _i )  x.  ( abs `  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) )  =  ( 1  x.  ( abs `  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) ) )
258233recnd 9408 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) )  e.  CC )
259258mulid2d 9400 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
1  x.  ( abs `  ( ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) )  =  ( abs `  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) )
260257, 259syl5eq 2485 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( abs `  _i )  x.  ( abs `  ( ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) )  =  ( abs `  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) )
261255, 260eqtr2d 2474 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) )  =  ( abs `  (
_i  x.  ( (
Im `  if (
t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) ) ) )
262261mpteq2dva 4375 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  g  e.  dom  S.1 )  ->  (
t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) ) )  =  ( t  e.  RR  |->  ( abs `  ( _i  x.  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) ) ) ) )
263262adantrl 710 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  -> 
( t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) ) )  =  ( t  e.  RR  |->  ( abs `  ( _i  x.  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) ) ) ) )
264241, 250, 252, 253, 263offval2 6335 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  -> 
( ( t  e.  RR  |->  ( abs `  (
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) )  oF  +  ( t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) ) )  =  ( t  e.  RR  |->  ( ( abs `  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) )  +  ( abs `  ( _i  x.  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) ) ) ) ) )
265241, 210, 247, 248, 264ofrfval2 6336 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  -> 
( ( t  e.  RR  |->  ( abs `  (
( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  +  ( _i  x.  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) ) ) ) )  oR  <_  ( (
t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) ) )  oF  +  ( t  e.  RR  |->  ( abs `  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) ) )  <->  A. t  e.  RR  ( abs `  ( ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  +  ( _i  x.  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) ) ) )  <_  (
( abs `  (
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) )  +  ( abs `  ( _i  x.  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) ) ) ) ) )
266245, 265mpbird 232 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  -> 
( t  e.  RR  |->  ( abs `  ( ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  +  ( _i  x.  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) ) ) ) )  oR  <_  ( (
t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) ) )  oF  +  ( t  e.  RR  |->  ( abs `  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) ) ) )
267 itg2le 21117 . . . . . . . . . . . 12  |-  ( ( ( t  e.  RR  |->  ( abs `  ( ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  +  ( _i  x.  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) ) ) ) ) : RR --> ( 0 [,] +oo )  /\  (
( t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) ) )  oF  +  ( t  e.  RR  |->  ( abs `  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) ) ) : RR --> ( 0 [,] +oo )  /\  ( t  e.  RR  |->  ( abs `  ( ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  +  ( _i  x.  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) ) ) ) )  oR  <_  ( (
t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) ) )  oF  +  ( t  e.  RR  |->  ( abs `  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) ) ) )  ->  ( S.2 `  ( t  e.  RR  |->  ( abs `  ( ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  +  ( _i  x.  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) ) ) ) ) )  <_  ( S.2 `  (
( t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) ) )  oF  +  ( t  e.  RR  |->  ( abs `  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) ) ) ) )
268216, 243, 266, 267syl3anc 1213 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  -> 
( S.2 `  ( t  e.  RR  |->  ( abs `  ( ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( f `  t ) )  +  ( _i  x.  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) ) ) ) )  <_  ( S.2 `  ( ( t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) )  oF  +  ( t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) ) ) ) )
269 eqidd 2442 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  f  e.  dom  S.1 )  ->  (
t  e.  RR  |->  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) )  =  ( t  e.  RR  |->  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) )
270 absf 12821 . . . . . . . . . . . . . . . . 17  |-  abs : CC
--> RR
271270a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  f  e.  dom  S.1 )  ->  abs : CC --> RR )
272271feqmptd 5741 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  f  e.  dom  S.1 )  ->  abs  =  ( x  e.  CC  |->  ( abs `  x
) ) )
273 fveq2 5688 . . . . . . . . . . . . . . 15  |-  ( x  =  ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( f `  t ) )  -> 
( abs `  x
)  =  ( abs `  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) )
274196, 269, 272, 273fmptco 5873 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  f  e.  dom  S.1 )  ->  ( abs  o.  ( t  e.  RR  |->  ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( f `  t ) ) ) )  =  ( t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) ) )
275 resubcl 9669 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  RR  /\  ( f `  t
)  e.  RR )  ->  ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( f `  t ) )  e.  RR )
276189, 192, 275syl2an 474 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  t  e.  RR ) )  -> 
( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  e.  RR )
277276anassrs 643 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  f  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  e.  RR )
278 eqid 2441 . . . . . . . . . . . . . . . 16  |-  ( t  e.  RR  |->  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) )  =  ( t  e.  RR  |->  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) )
279277, 278fmptd 5864 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  f  e.  dom  S.1 )  ->  (
t  e.  RR  |->  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) : RR --> RR )
280138a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  f  e.  dom  S.1 )  ->  RR  e.  dom  vol )
281 iunin2 4231 . . . . . . . . . . . . . . . . . . . . 21  |-  U_ y  e.  ran  f ( ( `' ( t  e.  RR  |->  ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( f `  t ) ) )
" ( x (,) +oo ) )  i^i  ( `' f " {
y } ) )  =  ( ( `' ( t  e.  RR  |->  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) " (
x (,) +oo )
)  i^i  U_ y  e. 
ran  f ( `' f " { y } ) )
282 imaiun 5959 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( `' f " U_ y  e.  ran  f { y } )  =  U_ y  e.  ran  f ( `' f " {
y } )
283 iunid 4222 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  U_ y  e.  ran  f { y }  =  ran  f
284283imaeq2i 5164 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( `' f " U_ y  e.  ran  f { y } )  =  ( `' f " ran  f )
285282, 284eqtr3i 2463 . . . . . . . . . . . . . . . . . . . . . 22  |-  U_ y  e.  ran  f ( `' f " { y } )  =  ( `' f " ran  f )
286285ineq2i 3546 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( `' ( t  e.  RR  |->  ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( f `  t ) ) )
" ( x (,) +oo ) )  i^i  U_ y  e.  ran  f ( `' f " {
y } ) )  =  ( ( `' ( t  e.  RR  |->  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) " (
x (,) +oo )
)  i^i  ( `' f " ran  f ) )
287281, 286eqtri 2461 . . . . . . . . . . . . . . . . . . . 20  |-  U_ y  e.  ran  f ( ( `' ( t  e.  RR  |->  ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( f `  t ) ) )
" ( x (,) +oo ) )  i^i  ( `' f " {
y } ) )  =  ( ( `' ( t  e.  RR  |->  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) " (
x (,) +oo )
)  i^i  ( `' f " ran  f ) )
288 cnvimass 5186 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( `' ( t  e.  RR  |->  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) " (
x (,) +oo )
)  C_  dom  ( t  e.  RR  |->  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) )
289 ovex 6115 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) )  e.  _V
290289, 278dmmpti 5537 . . . . . . . . . . . . . . . . . . . . . . 23  |-  dom  (
t  e.  RR  |->  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) )  =  RR
291288, 290sseqtri 3385 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( `' ( t  e.  RR  |->  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) " (
x (,) +oo )
)  C_  RR
292 cnvimarndm 5187 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( `' f " ran  f
)  =  dom  f
293 fdm 5560 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f : RR --> RR  ->  dom  f  =  RR )
294191, 293syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f  e.  dom  S.1  ->  dom  f  =  RR )
295292, 294syl5eq 2485 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  e.  dom  S.1  ->  ( `' f " ran  f )  =  RR )
296291, 295syl5sseqr 3402 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  e.  dom  S.1  ->  ( `' ( t  e.  RR  |->  ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( f `  t ) ) )
" ( x (,) +oo ) )  C_  ( `' f " ran  f ) )
297 df-ss 3339 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( `' ( t  e.  RR  |->  ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( f `  t ) ) )
" ( x (,) +oo ) )  C_  ( `' f " ran  f )  <->  ( ( `' ( t  e.  RR  |->  ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( f `  t ) ) )
" ( x (,) +oo ) )  i^i  ( `' f " ran  f ) )  =  ( `' ( t  e.  RR  |->  ( ( Re `  if ( t  e.  D , 
( F `  t
)