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

Theorem ftc1anclem6 31980
Description: Lemma for ftc1anc 31983- 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 11329 . . 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 31979 . . 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 477 . 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 2423 . . . . 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 9600 . . . . . . . 8  |-  _i  e.  CC
14 ine0 10056 . . . . . . . 8  |-  _i  =/=  0
1513, 14reccli 10339 . . . . . . 7  |-  ( 1  /  _i )  e.  CC
1615a1i 11 . . . . . 6  |-  ( ph  ->  ( 1  /  _i )  e.  CC )
179ffvelrnda 6035 . . . . . 6  |-  ( (
ph  /\  y  e.  D )  ->  ( F `  y )  e.  CC )
189feqmptd 5932 . . . . . . 7  |-  ( ph  ->  F  =  ( y  e.  D  |->  ( F `
 y ) ) )
1918, 8eqeltrrd 2512 . . . . . 6  |-  ( ph  ->  ( y  e.  D  |->  ( F `  y
) )  e.  L^1 )
20 divrec2 10289 . . . . . . . . . 10  |-  ( ( ( F `  y
)  e.  CC  /\  _i  e.  CC  /\  _i  =/=  0 )  ->  (
( F `  y
)  /  _i )  =  ( ( 1  /  _i )  x.  ( F `  y
) ) )
2113, 14, 20mp3an23 1353 . . . . . . . . 9  |-  ( ( F `  y )  e.  CC  ->  (
( F `  y
)  /  _i )  =  ( ( 1  /  _i )  x.  ( F `  y
) ) )
2217, 21syl 17 . . . . . . . 8  |-  ( (
ph  /\  y  e.  D )  ->  (
( F `  y
)  /  _i )  =  ( ( 1  /  _i )  x.  ( F `  y
) ) )
2322mpteq2dva 4508 . . . . . . 7  |-  ( ph  ->  ( y  e.  D  |->  ( ( F `  y )  /  _i ) )  =  ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y ) ) ) )
24 iblmbf 22717 . . . . . . . . 9  |-  ( ( y  e.  D  |->  ( F `  y ) )  e.  L^1 
->  ( y  e.  D  |->  ( F `  y
) )  e. MblFn )
2519, 24syl 17 . . . . . . . 8  |-  ( ph  ->  ( y  e.  D  |->  ( F `  y
) )  e. MblFn )
26 fveq2 5879 . . . . . . . . . . . . . . . . 17  |-  ( y  =  x  ->  ( F `  y )  =  ( F `  x ) )
2726fveq2d 5883 . . . . . . . . . . . . . . . 16  |-  ( y  =  x  ->  (
Re `  ( F `  y ) )  =  ( Re `  ( F `  x )
) )
2827cbvmptv 4514 . . . . . . . . . . . . . . 15  |-  ( y  e.  D  |->  ( Re
`  ( F `  y ) ) )  =  ( x  e.  D  |->  ( Re `  ( F `  x ) ) )
2928eleq1i 2500 . . . . . . . . . . . . . 14  |-  ( ( y  e.  D  |->  ( Re `  ( F `
 y ) ) )  e. MblFn  <->  ( x  e.  D  |->  ( Re `  ( F `  x ) ) )  e. MblFn )
3017recld 13251 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  D )  ->  (
Re `  ( F `  y ) )  e.  RR )
3130recnd 9671 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  D )  ->  (
Re `  ( F `  y ) )  e.  CC )
3231adantlr 720 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  D  |->  ( Re `  ( F `
 x ) ) )  e. MblFn )  /\  y  e.  D )  ->  ( Re `  ( F `  y )
)  e.  CC )
3329biimpri 210 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  D  |->  ( Re `  ( F `
 x ) ) )  e. MblFn  ->  ( y  e.  D  |->  ( Re
`  ( F `  y ) ) )  e. MblFn )
3433adantl 468 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  D  |->  ( Re
`  ( F `  x ) ) )  e. MblFn )  ->  (
y  e.  D  |->  ( Re `  ( F `
 y ) ) )  e. MblFn )
3532, 34mbfneg 22598 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  D  |->  ( Re
`  ( F `  x ) ) )  e. MblFn )  ->  (
y  e.  D  |->  -u ( Re `  ( F `
 y ) ) )  e. MblFn )
3629, 35sylan2b 478 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( y  e.  D  |->  ( Re
`  ( F `  y ) ) )  e. MblFn )  ->  (
y  e.  D  |->  -u ( Re `  ( F `
 y ) ) )  e. MblFn )
379ffvelrnda 6035 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  D )  ->  ( F `  x )  e.  CC )
3837recld 13251 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  D )  ->  (
Re `  ( F `  x ) )  e.  RR )
3938recnd 9671 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  D )  ->  (
Re `  ( F `  x ) )  e.  CC )
4039negnegd 9979 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  D )  ->  -u -u (
Re `  ( F `  x ) )  =  ( Re `  ( F `  x )
) )
4140mpteq2dva 4508 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( x  e.  D  |-> 
-u -u ( Re `  ( F `  x ) ) )  =  ( x  e.  D  |->  ( Re `  ( F `
 x ) ) ) )
4241, 28syl6eqr 2482 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( x  e.  D  |-> 
-u -u ( Re `  ( F `  x ) ) )  =  ( y  e.  D  |->  ( Re `  ( F `
 y ) ) ) )
4342adantr 467 . . . . . . . . . . . . . 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 9875 . . . . . . . . . . . . . . . 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 9871 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  x  ->  -u (
Re `  ( F `  y ) )  = 
-u ( Re `  ( F `  x ) ) )
4746cbvmptv 4514 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  D  |->  -u (
Re `  ( F `  y ) ) )  =  ( x  e.  D  |->  -u ( Re `  ( F `  x ) ) )
4847eleq1i 2500 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  D  |->  -u ( Re `  ( F `
 y ) ) )  e. MblFn  <->  ( x  e.  D  |->  -u ( Re `  ( F `  x ) ) )  e. MblFn )
4948biimpi 198 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  D  |->  -u ( Re `  ( F `
 y ) ) )  e. MblFn  ->  ( x  e.  D  |->  -u (
Re `  ( F `  x ) ) )  e. MblFn )
5049adantl 468 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( y  e.  D  |->  -u (
Re `  ( F `  y ) ) )  e. MblFn )  ->  (
x  e.  D  |->  -u ( Re `  ( F `
 x ) ) )  e. MblFn )
5145, 50mbfneg 22598 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( y  e.  D  |->  -u (
Re `  ( F `  y ) ) )  e. MblFn )  ->  (
x  e.  D  |->  -u -u ( Re `  ( F `  x )
) )  e. MblFn )
5243, 51eqeltrrd 2512 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( y  e.  D  |->  -u (
Re `  ( F `  y ) ) )  e. MblFn )  ->  (
y  e.  D  |->  ( Re `  ( F `
 y ) ) )  e. MblFn )
5336, 52impbida 841 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( y  e.  D  |->  ( Re `  ( F `  y ) ) )  e. MblFn  <->  ( y  e.  D  |->  -u (
Re `  ( F `  y ) ) )  e. MblFn ) )
54 divcl 10278 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F `  y
)  e.  CC  /\  _i  e.  CC  /\  _i  =/=  0 )  ->  (
( F `  y
)  /  _i )  e.  CC )
55 imre 13165 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F `  y
)  /  _i )  e.  CC  ->  (
Im `  ( ( F `  y )  /  _i ) )  =  ( Re `  ( -u _i  x.  ( ( F `  y )  /  _i ) ) ) )
5654, 55syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  y
)  e.  CC  /\  _i  e.  CC  /\  _i  =/=  0 )  ->  (
Im `  ( ( F `  y )  /  _i ) )  =  ( Re `  ( -u _i  x.  ( ( F `  y )  /  _i ) ) ) )
5713, 14, 56mp3an23 1353 . . . . . . . . . . . . . . . 16  |-  ( ( F `  y )  e.  CC  ->  (
Im `  ( ( F `  y )  /  _i ) )  =  ( Re `  ( -u _i  x.  ( ( F `  y )  /  _i ) ) ) )
5813, 14, 54mp3an23 1353 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F `  y )  e.  CC  ->  (
( F `  y
)  /  _i )  e.  CC )
59 mulneg1 10057 . . . . . . . . . . . . . . . . . . 19  |-  ( ( _i  e.  CC  /\  ( ( F `  y )  /  _i )  e.  CC )  ->  ( -u _i  x.  ( ( F `  y )  /  _i ) )  =  -u ( _i  x.  (
( F `  y
)  /  _i ) ) )
6013, 58, 59sylancr 668 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  y )  e.  CC  ->  ( -u _i  x.  ( ( F `  y )  /  _i ) )  =  -u ( _i  x.  ( ( F `  y )  /  _i ) ) )
61 divcan2 10280 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( F `  y
)  e.  CC  /\  _i  e.  CC  /\  _i  =/=  0 )  ->  (
_i  x.  ( ( F `  y )  /  _i ) )  =  ( F `  y
) )
6213, 14, 61mp3an23 1353 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F `  y )  e.  CC  ->  (
_i  x.  ( ( F `  y )  /  _i ) )  =  ( F `  y
) )
6362negeqd 9871 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  y )  e.  CC  ->  -u (
_i  x.  ( ( F `  y )  /  _i ) )  = 
-u ( F `  y ) )
6460, 63eqtrd 2464 . . . . . . . . . . . . . . . . 17  |-  ( ( F `  y )  e.  CC  ->  ( -u _i  x.  ( ( F `  y )  /  _i ) )  =  -u ( F `  y ) )
6564fveq2d 5883 . . . . . . . . . . . . . . . 16  |-  ( ( F `  y )  e.  CC  ->  (
Re `  ( -u _i  x.  ( ( F `  y )  /  _i ) ) )  =  ( Re `  -u ( F `  y )
) )
66 reneg 13182 . . . . . . . . . . . . . . . 16  |-  ( ( F `  y )  e.  CC  ->  (
Re `  -u ( F `
 y ) )  =  -u ( Re `  ( F `  y ) ) )
6757, 65, 663eqtrd 2468 . . . . . . . . . . . . . . 15  |-  ( ( F `  y )  e.  CC  ->  (
Im `  ( ( F `  y )  /  _i ) )  = 
-u ( Re `  ( F `  y ) ) )
6817, 67syl 17 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  D )  ->  (
Im `  ( ( F `  y )  /  _i ) )  = 
-u ( Re `  ( F `  y ) ) )
6968mpteq2dva 4508 . . . . . . . . . . . . 13  |-  ( ph  ->  ( y  e.  D  |->  ( Im `  (
( F `  y
)  /  _i ) ) )  =  ( y  e.  D  |->  -u ( Re `  ( F `
 y ) ) ) )
7069eleq1d 2492 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( y  e.  D  |->  ( Im `  ( ( F `  y )  /  _i ) ) )  e. MblFn  <->  ( y  e.  D  |->  -u ( Re `  ( F `
 y ) ) )  e. MblFn ) )
7153, 70bitr4d 260 . . . . . . . . . . 11  |-  ( ph  ->  ( ( y  e.  D  |->  ( Re `  ( F `  y ) ) )  e. MblFn  <->  ( y  e.  D  |->  ( Im
`  ( ( F `
 y )  /  _i ) ) )  e. MblFn
) )
72 imval 13164 . . . . . . . . . . . . . 14  |-  ( ( F `  y )  e.  CC  ->  (
Im `  ( F `  y ) )  =  ( Re `  (
( F `  y
)  /  _i ) ) )
7317, 72syl 17 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  D )  ->  (
Im `  ( F `  y ) )  =  ( Re `  (
( F `  y
)  /  _i ) ) )
7473mpteq2dva 4508 . . . . . . . . . . . 12  |-  ( ph  ->  ( y  e.  D  |->  ( Im `  ( F `  y )
) )  =  ( y  e.  D  |->  ( Re `  ( ( F `  y )  /  _i ) ) ) )
7574eleq1d 2492 . . . . . . . . . . 11  |-  ( ph  ->  ( ( y  e.  D  |->  ( Im `  ( F `  y ) ) )  e. MblFn  <->  ( y  e.  D  |->  ( Re
`  ( ( F `
 y )  /  _i ) ) )  e. MblFn
) )
7671, 75anbi12d 716 . . . . . . . . . 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 452 . . . . . . . . . 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 265 . . . . . . . . 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 22587 . . . . . . . . 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 17 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  D )  ->  (
( F `  y
)  /  _i )  e.  CC )
8180ismbfcn2 22587 . . . . . . . . 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 289 . . . . . . . 8  |-  ( ph  ->  ( ( y  e.  D  |->  ( F `  y ) )  e. MblFn  <->  ( y  e.  D  |->  ( ( F `  y
)  /  _i ) )  e. MblFn ) )
8325, 82mpbid 214 . . . . . . 7  |-  ( ph  ->  ( y  e.  D  |->  ( ( F `  y )  /  _i ) )  e. MblFn )
8423, 83eqeltrrd 2512 . . . . . 6  |-  ( ph  ->  ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y )
) )  e. MblFn )
8516, 17, 19, 84iblmulc2nc 31965 . . . . 5  |-  ( ph  ->  ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y )
) )  e.  L^1 )
86 mulcl 9625 . . . . . . 7  |-  ( ( ( 1  /  _i )  e.  CC  /\  ( F `  y )  e.  CC )  ->  (
( 1  /  _i )  x.  ( F `  y ) )  e.  CC )
8715, 17, 86sylancr 668 . . . . . 6  |-  ( (
ph  /\  y  e.  D )  ->  (
( 1  /  _i )  x.  ( F `  y ) )  e.  CC )
88 eqid 2423 . . . . . 6  |-  ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y ) ) )  =  ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y
) ) )
8987, 88fmptd 6059 . . . . 5  |-  ( ph  ->  ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y )
) ) : D --> CC )
9012, 3, 4, 5, 6, 7, 85, 89ftc1anclem5 31979 . . . 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 477 . . 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 6035 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  D )  ->  ( F `  t )  e.  CC )
93 0cnd 9638 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  t  e.  D )  ->  0  e.  CC )
9492, 93ifclda 3942 . . . . . . . . . . . 12  |-  ( ph  ->  if ( t  e.  D ,  ( F `
 t ) ,  0 )  e.  CC )
95 imval 13164 . . . . . . . . . . . 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 17 . . . . . . . . . . 11  |-  ( ph  ->  ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  =  ( Re `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  /  _i ) ) )
97 fveq2 5879 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  t  ->  ( F `  y )  =  ( F `  t ) )
9897oveq2d 6319 . . . . . . . . . . . . . . . . 17  |-  ( y  =  t  ->  (
( 1  /  _i )  x.  ( F `  y ) )  =  ( ( 1  /  _i )  x.  ( F `  t )
) )
99 ovex 6331 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  /  _i )  x.  ( F `  t ) )  e. 
_V
10098, 88, 99fvmpt 5962 . . . . . . . . . . . . . . . 16  |-  ( t  e.  D  ->  (
( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y )
) ) `  t
)  =  ( ( 1  /  _i )  x.  ( F `  t ) ) )
101100adantl 468 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  D )  ->  (
( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y )
) ) `  t
)  =  ( ( 1  /  _i )  x.  ( F `  t ) ) )
102 divrec2 10289 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  t
)  e.  CC  /\  _i  e.  CC  /\  _i  =/=  0 )  ->  (
( F `  t
)  /  _i )  =  ( ( 1  /  _i )  x.  ( F `  t
) ) )
10313, 14, 102mp3an23 1353 . . . . . . . . . . . . . . . 16  |-  ( ( F `  t )  e.  CC  ->  (
( F `  t
)  /  _i )  =  ( ( 1  /  _i )  x.  ( F `  t
) ) )
10492, 103syl 17 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  D )  ->  (
( F `  t
)  /  _i )  =  ( ( 1  /  _i )  x.  ( F `  t
) ) )
105101, 104eqtr4d 2467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  D )  ->  (
( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y )
) ) `  t
)  =  ( ( F `  t )  /  _i ) )
106105ifeq1da 3940 . . . . . . . . . . . . 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 ovif 6385 . . . . . . . . . . . . . 14  |-  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  /  _i )  =  if ( t  e.  D ,  ( ( F `  t
)  /  _i ) ,  ( 0  /  _i ) )
10813, 14div0i 10343 . . . . . . . . . . . . . . 15  |-  ( 0  /  _i )  =  0
109 ifeq2 3915 . . . . . . . . . . . . . . 15  |-  ( ( 0  /  _i )  =  0  ->  if ( t  e.  D ,  ( ( F `
 t )  /  _i ) ,  ( 0  /  _i ) )  =  if ( t  e.  D ,  ( ( F `  t
)  /  _i ) ,  0 ) )
110108, 109ax-mp 5 . . . . . . . . . . . . . 14  |-  if ( t  e.  D , 
( ( F `  t )  /  _i ) ,  ( 0  /  _i ) )  =  if ( t  e.  D ,  ( ( F `  t
)  /  _i ) ,  0 )
111107, 110eqtri 2452 . . . . . . . . . . . . 13  |-  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  /  _i )  =  if ( t  e.  D ,  ( ( F `  t
)  /  _i ) ,  0 )
112106, 111syl6eqr 2482 . . . . . . . . . . . 12  |-  ( ph  ->  if ( t  e.  D ,  ( ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y ) ) ) `
 t ) ,  0 )  =  ( if ( t  e.  D ,  ( F `
 t ) ,  0 )  /  _i ) )
113112fveq2d 5883 . . . . . . . . . . 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 ) ) )
11496, 113eqtr4d 2467 . . . . . . . . . 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 ) ) )
115114oveq1d 6318 . . . . . . . . 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 )
) )
116115fveq2d 5883 . . . . . . . 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 )
) ) )
117116mpteq2dv 4509 . . . . . . 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 )
) ) ) )
118117fveq2d 5883 . . . . . 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 )
) ) ) ) )
119118breq1d 4431 . . . . 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 ) ) )
120119rexbidv 2940 . . . 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 ) ) )
121120adantr 467 . . 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 ) ) )
12291, 121mpbird 236 . 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
) )
123 reeanv 2997 . . 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 ) ) )
124 eleq1 2495 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  t  ->  (
x  e.  D  <->  t  e.  D ) )
125 fveq2 5879 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  t  ->  ( F `  x )  =  ( F `  t ) )
126124, 125ifbieq1d 3933 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  t  ->  if ( x  e.  D ,  ( F `  x ) ,  0 )  =  if ( t  e.  D , 
( F `  t
) ,  0 ) )
127126fveq2d 5883 . . . . . . . . . . . . . . . . 17  |-  ( x  =  t  ->  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) )  =  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )
128 eqid 2423 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  RR  |->  ( Re
`  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) )  =  ( x  e.  RR  |->  ( Re
`  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) )
129 fvex 5889 . . . . . . . . . . . . . . . . 17  |-  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  _V
130127, 128, 129fvmpt 5962 . . . . . . . . . . . . . . . 16  |-  ( t  e.  RR  ->  (
( x  e.  RR  |->  ( Re `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) `  t
)  =  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )
131130oveq1d 6318 . . . . . . . . . . . . . . 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 ) ) )
132131fveq2d 5883 . . . . . . . . . . . . . 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 )
) ) )
133132mpteq2ia 4504 . . . . . . . . . . . . 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 )
) ) )
134133fveq2i 5882 . . . . . . . . . . . 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 ) ) ) ) )
135 rembl 22486 . . . . . . . . . . . . . . . . . . 19  |-  RR  e.  dom  vol
136135a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  RR  e.  dom  vol )
137 0cnd 9638 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  -.  x  e.  D )  ->  0  e.  CC )
13837, 137ifclda 3942 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  if ( x  e.  D ,  ( F `
 x ) ,  0 )  e.  CC )
139138adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  D )  ->  if ( x  e.  D ,  ( F `  x ) ,  0 )  e.  CC )
140 eldifn 3589 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( RR  \  D )  ->  -.  x  e.  D )
141140adantl 468 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( RR  \  D ) )  ->  -.  x  e.  D )
142141iffalsed 3921 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( RR  \  D ) )  ->  if (
x  e.  D , 
( F `  x
) ,  0 )  =  0 )
1439feqmptd 5932 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  F  =  ( x  e.  D  |->  ( F `
 x ) ) )
144 iftrue 3916 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  D  ->  if ( x  e.  D ,  ( F `  x ) ,  0 )  =  ( F `
 x ) )
145144mpteq2ia 4504 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  D  |->  if ( x  e.  D , 
( F `  x
) ,  0 ) )  =  ( x  e.  D  |->  ( F `
 x ) )
146143, 145syl6eqr 2482 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  F  =  ( x  e.  D  |->  if ( x  e.  D , 
( F `  x
) ,  0 ) ) )
147146, 8eqeltrrd 2512 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( x  e.  D  |->  if ( x  e.  D ,  ( F `
 x ) ,  0 ) )  e.  L^1 )
1487, 136, 139, 142, 147iblss2 22755 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( x  e.  RR  |->  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  e.  L^1 )
149138adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  if ( x  e.  D , 
( F `  x
) ,  0 )  e.  CC )
150149iblcn 22748 . . . . . . . . . . . . . . . . 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 ) ) )
151148, 150mpbid 214 . . . . . . . . . . . . . . . 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 ) )
152151simpld 461 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( x  e.  RR  |->  ( Re `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) )  e.  L^1 )
153149recld 13251 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ( Re
`  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  e.  RR )
154153, 128fmptd 6059 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( x  e.  RR  |->  ( Re `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) : RR --> RR )
155152, 154jca 535 . . . . . . . . . . . . . 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 ) )
156 ftc1anclem4 31978 . . . . . . . . . . . . . . 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 )
1571563expb 1207 . . . . . . . . . . . . . 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 )
158155, 157sylan2 477 . . . . . . . . . . . . 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 )
159158ancoms 455 . . . . . . . . . . . 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 )
160134, 159syl5eqelr 2516 . . . . . . . . . . 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 )
161126fveq2d 5883 . . . . . . . . . . . . . . . . 17  |-  ( x  =  t  ->  (
Im `  if (
x  e.  D , 
( F `  x
) ,  0 ) )  =  ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )
162 eqid 2423 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  RR  |->  ( Im
`  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) )  =  ( x  e.  RR  |->  ( Im
`  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) )
163 fvex 5889 . . . . . . . . . . . . . . . . 17  |-  ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  _V
164161, 162, 163fvmpt 5962 . . . . . . . . . . . . . . . 16  |-  ( t  e.  RR  ->  (
( x  e.  RR  |->  ( Im `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) `  t
)  =  ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )
165164oveq1d 6318 . . . . . . . . . . . . . . 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 ) ) )
166165fveq2d 5883 . . . . . . . . . . . . . 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 )
) ) )
167166mpteq2ia 4504 . . . . . . . . . . . . 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 )
) ) )
168167fveq2i 5882 . . . . . . . . . . . 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 ) ) ) ) )
169151simprd 465 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( x  e.  RR  |->  ( Im `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) )  e.  L^1 )
170138imcld 13252 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( Im `  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  e.  RR )
171170adantr 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ( Im
`  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  e.  RR )
172171, 162fmptd 6059 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( x  e.  RR  |->  ( Im `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) : RR --> RR )
173169, 172jca 535 . . . . . . . . . . . . . 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 ) )
174 ftc1anclem4 31978 . . . . . . . . . . . . . . 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 )
1751743expb 1207 . . . . . . . . . . . . . 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 )
176173, 175sylan2 477 . . . . . . . . . . . . 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 )
177176ancoms 455 . . . . . . . . . . . 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 )
178168, 177syl5eqelr 2516 . . . . . . . . . . 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 )
179160, 178anim12dan 846 . . . . . . . . . 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 ) )
1801rpred 11343 . . . . . . . . . . 11  |-  ( Y  e.  RR+  ->  ( Y  /  2 )  e.  RR )
181180, 180jca 535 . . . . . . . . . 10  |-  ( Y  e.  RR+  ->  ( ( Y  /  2 )  e.  RR  /\  ( Y  /  2 )  e.  RR ) )
182 lt2add 10101 . . . . . . . . . 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
) ) ) )
183179, 181, 182syl2an 480 . . . . . . . . 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
) ) ) )
184183an32s 812 . . . . . . . 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
) ) ) )
18594recld 13251 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  RR )
186185recnd 9671 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  CC )
187 i1ff 22626 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  e.  dom  S.1  ->  f : RR --> RR )
188187ffvelrnda 6035 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( f `  t )  e.  RR )
189188recnd 9671 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( f `  t )  e.  CC )
190 subcl 9876 . . . . . . . . . . . . . . . . . . . 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 )
191186, 189, 190syl2an 480 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  t  e.  RR ) )  -> 
( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  e.  CC )
192191anassrs 653 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  f  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  e.  CC )
193192adantlrr 726 . . . . . . . . . . . . . . . . 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 )
19494imcld 13252 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  RR )
195194recnd 9671 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  CC )
196 i1ff 22626 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g  e.  dom  S.1  ->  g : RR --> RR )
197196ffvelrnda 6035 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  e.  RR )
198197recnd 9671 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  e.  CC )
199 subcl 9876 . . . . . . . . . . . . . . . . . . . . 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 )
200195, 198, 199syl2an 480 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( g  e.  dom  S.1  /\  t  e.  RR ) )  -> 
( ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
)  e.  CC )
201200anassrs 653 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
)  e.  CC )
202 mulcl 9625 . . . . . . . . . . . . . . . . . . 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 )
20313, 201, 202sylancr 668 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
_i  x.  ( (
Im `  if (
t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) )  e.  CC )
204203adantlrl 725 . . . . . . . . . . . . . . . . 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 )
205193, 204addcld 9664 . . . . . . . . . . . . . . . 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 )
206205abscld 13491 . . . . . . . . . . . . . . 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 )
207206rexrd 9692 . . . . . . . . . . . . . 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* )
208205absge0d 13499 . . . . . . . . . . . . . 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 ) ) ) ) ) )
209 elxrge0 11743 . . . . . . . . . . . . . 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 )
) ) ) ) ) )
210207, 208, 209sylanbrc 669 . . . . . . . . . . . . 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 ) )
211 eqid 2423 . . . . . . . . . . . . 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 )
) ) ) ) )
212210, 211fmptd 6059 . . . . . . . . . . . 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 ) )
213 icossicc 11723 . . . . . . . . . . . . . . 15  |-  ( 0 [,) +oo )  C_  ( 0 [,] +oo )
214 ge0addcl 11746 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  ( 0 [,) +oo )  /\  y  e.  ( 0 [,) +oo ) )  ->  ( x  +  y )  e.  ( 0 [,) +oo )
)
215213, 214sseldi 3463 . . . . . . . . . . . . . 14  |-  ( ( x  e.  ( 0 [,) +oo )  /\  y  e.  ( 0 [,) +oo ) )  ->  ( x  +  y )  e.  ( 0 [,] +oo )
)
216215adantl 468 . . . . . . . . . . . . 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 ) )
217192abscld 13491 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  f  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( f `  t ) ) )  e.  RR )
218192absge0d 13499 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  f  e.  dom  S.1 )  /\  t  e.  RR )  ->  0  <_  ( abs `  (
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) )
219 elrege0 11740 . . . . . . . . . . . . . . . 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 )
) ) ) )
220217, 218, 219sylanbrc 669 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  f  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( f `  t ) ) )  e.  ( 0 [,) +oo ) )
221 eqid 2423 . . . . . . . . . . . . . . 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 ) ) ) )
222220, 221fmptd 6059 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  f  e.  dom  S.1 )  ->  (
t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) ) ) : RR --> ( 0 [,) +oo ) )
223222adantrr 722 . . . . . . . . . . . . 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 ) )
224201abscld 13491 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) )  e.  RR )
225201absge0d 13499 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  0  <_  ( abs `  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) )
226 elrege0 11740 . . . . . . . . . . . . . . . 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 )
) ) ) )
227224, 225, 226sylanbrc 669 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) )  e.  ( 0 [,) +oo ) )
228 eqid 2423 . . . . . . . . . . . . . . 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 ) ) ) )
229227, 228fmptd 6059 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  g  e.  dom  S.1 )  ->  (
t  e.  RR  |->  ( abs `  ( ( Im `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( g `
 t ) ) ) ) : RR --> ( 0 [,) +oo ) )
230229adantrl 721 . . . . . . . . . . . . 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 ) )
231 reex 9632 . . . . . . . . . . . . . 14  |-  RR  e.  _V
232231a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  ->  RR  e.  _V )
233 inidm 3672 . . . . . . . . . . . . 13  |-  ( RR 
i^i  RR )  =  RR
234216, 223, 230, 232, 232, 233off 6558 . . . . . . . . . . . 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 ) )
235193, 204abstrid 13511 . . . . . . . . . . . . . 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 ) ) ) ) ) )
236235ralrimiva 2840 . . . . . . . . . . . . 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 ) ) ) ) ) )
237 ovex 6331 . . . . . . . . . . . . . . 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
238237a1i 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 )
239 eqidd 2424 . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
240 fvex 5889 . . . . . . . . . . . . . . . 16  |-  ( abs `  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) )  e.  _V
241240a1i 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 )
242 fvex 5889 . . . . . . . . . . . . . . . 16  |-  ( abs `  ( _i  x.  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) )  e. 
_V
243242a1i 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 )
244 eqidd 2424 . . . . . . . . . . . . . . 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 ) ) ) ) )
245 absmul 13351 . . . . . . . . . . . . . . . . . . 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 )
) ) ) )
24613, 201, 245sylancr 668 . . . . . . . . . . . . . . . . . 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 )
) ) ) )
247 absi 13343 . . . . . . . . . . . . . . . . . . . 20  |-  ( abs `  _i )  =  1
248247oveq1i 6313 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
249224recnd 9671 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) )  e.  CC )
250249mulid2d 9663 . . . . . . . . . . . . . . . . . . 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 )
) ) )
251248, 250syl5eq 2476 . . . . . . . . . . . . . . . . . 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 )
) ) )
252246, 251eqtr2d 2465 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
253252mpteq2dva 4508 . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
254253adantrl 721 . . . . . . . . . . . . . . 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 ) ) ) ) ) )
255232, 241, 243, 244, 254offval2 6560 . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
256232, 206, 238, 239, 255ofrfval2 6561 . . . . . . . . . . . . 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 ) ) ) ) ) ) )
257236, 256mpbird 236 . . . . . . . . . . . 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 )
) ) ) ) )
258 itg2le 22689 . . . . . . . . . . . 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 )
) ) ) ) ) )
259212, 234, 257, 258syl3anc 1265 . . . . . . . . . . 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 )
) ) ) ) ) )
260 eqidd 2424 . . . . . . . . . . . . . . 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 )
) ) )
261 absf 13394 . . . . . . . . . . . . . . . . 17  |-  abs : CC
--> RR
262261a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  f  e.  dom  S.1 )  ->  abs : CC --> RR )
263262feqmptd 5932 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  f  e.  dom  S.1 )  ->  abs  =  ( x  e.  CC  |->  ( abs `  x
) ) )
264 fveq2 5879 . . . . . . . . . . . . . . 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 )
) ) )
265192, 260, 263, 264fmptco 6069 . . . . . . . . . . . . . 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 )
) ) ) )
266 resubcl 9940 . . . . . . . . . . . . . . . . . 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 )
267185, 188, 266syl2an 480 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  t  e.  RR ) )  -> 
( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  e.  RR )
268267anassrs 653 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  f  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  e.  RR )
269 eqid 2423 . . . . . . . . . . . . . . . 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 ) ) )
270268, 269fmptd 6059 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  f  e.  dom  S.1 )  ->  (
t  e.  RR  |->  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) : RR --> RR )
271135a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  f  e.  dom  S.1 )  ->  RR  e.  dom  vol )
272 iunin2 4361 . . . . . . . . . . . . . . . . . . . . 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 } ) )
273 imaiun 6163 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( `' f " U_ y  e.  ran  f { y } )  =  U_ y  e.  ran  f ( `' f " {
y } )
274 iunid 4352 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  U_ y  e.  ran  f { y }  =  ran  f
275274imaeq2i 5183 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( `' f " U_ y  e.  ran  f { y } )  =  ( `' f " ran  f )
276273, 275eqtr3i 2454 . . . . . . . . . . . . . . . . . . . . . 22  |-  U_ y  e.  ran  f ( `' f " { y } )  =  ( `' f " ran  f )
277276ineq2i 3662 . . . . . . . . . . . . . . . . . . . . 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 ) )
278272, 277eqtri 2452 . . . . . . . . . . . . . . . . . . . 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 ) )
279 cnvimass 5205 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
280 ovex 6331 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) )  e.  _V
281280, 269dmmpti 5723 . . . . . . . . . . . . . . . . . . . . . . 23  |-  dom  (
t  e.  RR  |->  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) )  =  RR
282279, 281sseqtri 3497 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( `' ( t  e.  RR  |->  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) " (
x (,) +oo )
)  C_  RR
283 cnvimarndm 5206 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( `' f " ran  f
)  =  dom  f
284 fdm 5748 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f : RR --> RR  ->  dom  f  =  RR )
285187, 284syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f  e.  dom  S.1  ->  dom  f  =  RR )
286283, 285syl5eq 2476 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  e.  dom  S.1  ->  ( `' f " ran  f )  =  RR )
287282, 286syl5sseqr 3514 . . . . . . . . . . . . . . . . . . . . 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 ) )
288 df-ss 3451 . . . . . . . . . . . . . . . . . . . . 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
) ,  0 ) )  -  ( f `
 t ) ) ) " ( x (,) +oo ) ) )
289287, 288sylib 200 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  e.  dom  S.1  ->  ( ( `' ( 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 ) ,  0 ) )  -  (
f `  t )
) ) " (
x (,) +oo )
) )
290278, 289syl5eq 2476 . . . . . . . . . . . . . . . . . . 19  |-  ( f  e.  dom  S.1  ->  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 ) ) )
291290ad2antlr 732 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  f  e.  dom  S.1 )  /\  x  e.  RR )  ->  U_ y  e.  ran  f ( ( `' (