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

Theorem ftc1anclem6 28472
Description: Lemma for ftc1anc 28475- 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 11015 . . 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 28471 . . 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 474 . 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 2443 . . . . 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 9341 . . . . . . . 8  |-  _i  e.  CC
14 ine0 9780 . . . . . . . 8  |-  _i  =/=  0
1513, 14reccli 10061 . . . . . . 7  |-  ( 1  /  _i )  e.  CC
1615a1i 11 . . . . . 6  |-  ( ph  ->  ( 1  /  _i )  e.  CC )
179ffvelrnda 5843 . . . . . 6  |-  ( (
ph  /\  y  e.  D )  ->  ( F `  y )  e.  CC )
189feqmptd 5744 . . . . . . 7  |-  ( ph  ->  F  =  ( y  e.  D  |->  ( F `
 y ) ) )
1918, 8eqeltrrd 2518 . . . . . 6  |-  ( ph  ->  ( y  e.  D  |->  ( F `  y
) )  e.  L^1 )
20 divrec2 10011 . . . . . . . . . 10  |-  ( ( ( F `  y
)  e.  CC  /\  _i  e.  CC  /\  _i  =/=  0 )  ->  (
( F `  y
)  /  _i )  =  ( ( 1  /  _i )  x.  ( F `  y
) ) )
2113, 14, 20mp3an23 1306 . . . . . . . . 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 4378 . . . . . . 7  |-  ( ph  ->  ( y  e.  D  |->  ( ( F `  y )  /  _i ) )  =  ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y ) ) ) )
24 iblmbf 21245 . . . . . . . . 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 5691 . . . . . . . . . . . . . . . . 17  |-  ( y  =  x  ->  ( F `  y )  =  ( F `  x ) )
2726fveq2d 5695 . . . . . . . . . . . . . . . 16  |-  ( y  =  x  ->  (
Re `  ( F `  y ) )  =  ( Re `  ( F `  x )
) )
2827cbvmptv 4383 . . . . . . . . . . . . . . 15  |-  ( y  e.  D  |->  ( Re
`  ( F `  y ) ) )  =  ( x  e.  D  |->  ( Re `  ( F `  x ) ) )
2928eleq1i 2506 . . . . . . . . . . . . . 14  |-  ( ( y  e.  D  |->  ( Re `  ( F `
 y ) ) )  e. MblFn  <->  ( x  e.  D  |->  ( Re `  ( F `  x ) ) )  e. MblFn )
3017recld 12683 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  D )  ->  (
Re `  ( F `  y ) )  e.  RR )
3130recnd 9412 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  D )  ->  (
Re `  ( F `  y ) )  e.  CC )
3231adantlr 714 . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  D  |->  ( Re
`  ( F `  x ) ) )  e. MblFn )  ->  (
y  e.  D  |->  ( Re `  ( F `
 y ) ) )  e. MblFn )
3532, 34mbfneg 21128 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  D  |->  ( Re
`  ( F `  x ) ) )  e. MblFn )  ->  (
y  e.  D  |->  -u ( Re `  ( F `
 y ) ) )  e. MblFn )
3629, 35sylan2b 475 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( y  e.  D  |->  ( Re
`  ( F `  y ) ) )  e. MblFn )  ->  (
y  e.  D  |->  -u ( Re `  ( F `
 y ) ) )  e. MblFn )
379ffvelrnda 5843 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  D )  ->  ( F `  x )  e.  CC )
3837recld 12683 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  D )  ->  (
Re `  ( F `  x ) )  e.  RR )
3938recnd 9412 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  D )  ->  (
Re `  ( F `  x ) )  e.  CC )
4039negnegd 9710 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  D )  ->  -u -u (
Re `  ( F `  x ) )  =  ( Re `  ( F `  x )
) )
4140mpteq2dva 4378 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( x  e.  D  |-> 
-u -u ( Re `  ( F `  x ) ) )  =  ( x  e.  D  |->  ( Re `  ( F `
 x ) ) ) )
4241, 28syl6eqr 2493 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( x  e.  D  |-> 
-u -u ( Re `  ( F `  x ) ) )  =  ( y  e.  D  |->  ( Re `  ( F `
 y ) ) ) )
4342adantr 465 . . . . . . . . . . . . . 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 9608 . . . . . . . . . . . . . . . 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 9604 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  x  ->  -u (
Re `  ( F `  y ) )  = 
-u ( Re `  ( F `  x ) ) )
4746cbvmptv 4383 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  D  |->  -u (
Re `  ( F `  y ) ) )  =  ( x  e.  D  |->  -u ( Re `  ( F `  x ) ) )
4847eleq1i 2506 . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( y  e.  D  |->  -u (
Re `  ( F `  y ) ) )  e. MblFn )  ->  (
x  e.  D  |->  -u ( Re `  ( F `
 x ) ) )  e. MblFn )
5145, 50mbfneg 21128 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( y  e.  D  |->  -u (
Re `  ( F `  y ) ) )  e. MblFn )  ->  (
x  e.  D  |->  -u -u ( Re `  ( F `  x )
) )  e. MblFn )
5243, 51eqeltrrd 2518 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( y  e.  D  |->  -u (
Re `  ( F `  y ) ) )  e. MblFn )  ->  (
y  e.  D  |->  ( Re `  ( F `
 y ) ) )  e. MblFn )
5336, 52impbida 828 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( y  e.  D  |->  ( Re `  ( F `  y ) ) )  e. MblFn  <->  ( y  e.  D  |->  -u (
Re `  ( F `  y ) ) )  e. MblFn ) )
54 divcl 10000 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F `  y
)  e.  CC  /\  _i  e.  CC  /\  _i  =/=  0 )  ->  (
( F `  y
)  /  _i )  e.  CC )
55 imre 12597 . . . . . . . . . . . . . . . . . 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 1306 . . . . . . . . . . . . . . . 16  |-  ( ( F `  y )  e.  CC  ->  (
Im `  ( ( F `  y )  /  _i ) )  =  ( Re `  ( -u _i  x.  ( ( F `  y )  /  _i ) ) ) )
5813, 14, 54mp3an23 1306 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F `  y )  e.  CC  ->  (
( F `  y
)  /  _i )  e.  CC )
59 mulneg1 9781 . . . . . . . . . . . . . . . . . . 19  |-  ( ( _i  e.  CC  /\  ( ( F `  y )  /  _i )  e.  CC )  ->  ( -u _i  x.  ( ( F `  y )  /  _i ) )  =  -u ( _i  x.  (
( F `  y
)  /  _i ) ) )
6013, 58, 59sylancr 663 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  y )  e.  CC  ->  ( -u _i  x.  ( ( F `  y )  /  _i ) )  =  -u ( _i  x.  ( ( F `  y )  /  _i ) ) )
61 divcan2 10002 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( F `  y
)  e.  CC  /\  _i  e.  CC  /\  _i  =/=  0 )  ->  (
_i  x.  ( ( F `  y )  /  _i ) )  =  ( F `  y
) )
6213, 14, 61mp3an23 1306 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F `  y )  e.  CC  ->  (
_i  x.  ( ( F `  y )  /  _i ) )  =  ( F `  y
) )
6362negeqd 9604 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  y )  e.  CC  ->  -u (
_i  x.  ( ( F `  y )  /  _i ) )  = 
-u ( F `  y ) )
6460, 63eqtrd 2475 . . . . . . . . . . . . . . . . 17  |-  ( ( F `  y )  e.  CC  ->  ( -u _i  x.  ( ( F `  y )  /  _i ) )  =  -u ( F `  y ) )
6564fveq2d 5695 . . . . . . . . . . . . . . . 16  |-  ( ( F `  y )  e.  CC  ->  (
Re `  ( -u _i  x.  ( ( F `  y )  /  _i ) ) )  =  ( Re `  -u ( F `  y )
) )
66 reneg 12614 . . . . . . . . . . . . . . . 16  |-  ( ( F `  y )  e.  CC  ->  (
Re `  -u ( F `
 y ) )  =  -u ( Re `  ( F `  y ) ) )
6757, 65, 663eqtrd 2479 . . . . . . . . . . . . . . 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 4378 . . . . . . . . . . . . 13  |-  ( ph  ->  ( y  e.  D  |->  ( Im `  (
( F `  y
)  /  _i ) ) )  =  ( y  e.  D  |->  -u ( Re `  ( F `
 y ) ) ) )
7069eleq1d 2509 . . . . . . . . . . . 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 12596 . . . . . . . . . . . . . 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 4378 . . . . . . . . . . . 12  |-  ( ph  ->  ( y  e.  D  |->  ( Im `  ( F `  y )
) )  =  ( y  e.  D  |->  ( Re `  ( ( F `  y )  /  _i ) ) ) )
7574eleq1d 2509 . . . . . . . . . . 11  |-  ( ph  ->  ( ( y  e.  D  |->  ( Im `  ( F `  y ) ) )  e. MblFn  <->  ( y  e.  D  |->  ( Re
`  ( ( F `
 y )  /  _i ) ) )  e. MblFn
) )
7671, 75anbi12d 710 . . . . . . . . . 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 450 . . . . . . . . . 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 21117 . . . . . . . . 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 21117 . . . . . . . . 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 2518 . . . . . 6  |-  ( ph  ->  ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y )
) )  e. MblFn )
8516, 17, 19, 84iblmulc2nc 28457 . . . . 5  |-  ( ph  ->  ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y )
) )  e.  L^1 )
86 mulcl 9366 . . . . . . 7  |-  ( ( ( 1  /  _i )  e.  CC  /\  ( F `  y )  e.  CC )  ->  (
( 1  /  _i )  x.  ( F `  y ) )  e.  CC )
8715, 17, 86sylancr 663 . . . . . 6  |-  ( (
ph  /\  y  e.  D )  ->  (
( 1  /  _i )  x.  ( F `  y ) )  e.  CC )
88 eqid 2443 . . . . . 6  |-  ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y ) ) )  =  ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y
) ) )
8987, 88fmptd 5867 . . . . 5  |-  ( ph  ->  ( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y )
) ) : D --> CC )
9012, 3, 4, 5, 6, 7, 85, 89ftc1anclem5 28471 . . . 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 474 . . 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 5843 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  D )  ->  ( F `  t )  e.  CC )
93 0cnd 9379 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  t  e.  D )  ->  0  e.  CC )
9492, 93ifclda 3821 . . . . . . . . . . . 12  |-  ( ph  ->  if ( t  e.  D ,  ( F `
 t ) ,  0 )  e.  CC )
95 imval 12596 . . . . . . . . . . . 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 5691 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  t  ->  ( F `  y )  =  ( F `  t ) )
9897oveq2d 6107 . . . . . . . . . . . . . . . . 17  |-  ( y  =  t  ->  (
( 1  /  _i )  x.  ( F `  y ) )  =  ( ( 1  /  _i )  x.  ( F `  t )
) )
99 ovex 6116 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  /  _i )  x.  ( F `  t ) )  e. 
_V
10098, 88, 99fvmpt 5774 . . . . . . . . . . . . . . . 16  |-  ( t  e.  D  ->  (
( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y )
) ) `  t
)  =  ( ( 1  /  _i )  x.  ( F `  t ) ) )
101100adantl 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  D )  ->  (
( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y )
) ) `  t
)  =  ( ( 1  /  _i )  x.  ( F `  t ) ) )
102 divrec2 10011 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  t
)  e.  CC  /\  _i  e.  CC  /\  _i  =/=  0 )  ->  (
( F `  t
)  /  _i )  =  ( ( 1  /  _i )  x.  ( F `  t
) ) )
10313, 14, 102mp3an23 1306 . . . . . . . . . . . . . . . 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 2478 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  D )  ->  (
( y  e.  D  |->  ( ( 1  /  _i )  x.  ( F `  y )
) ) `  t
)  =  ( ( F `  t )  /  _i ) )
106105ifeq1da 3819 . . . . . . . . . . . . 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 6098 . . . . . . . . . . . . . . 15  |-  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  =  ( F `
 t )  -> 
( if ( t  e.  D ,  ( F `  t ) ,  0 )  /  _i )  =  (
( F `  t
)  /  _i ) )
108 oveq1 6098 . . . . . . . . . . . . . . 15  |-  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  =  0  -> 
( if ( t  e.  D ,  ( F `  t ) ,  0 )  /  _i )  =  (
0  /  _i ) )
109107, 108ifsb 3802 . . . . . . . . . . . . . 14  |-  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  /  _i )  =  if ( t  e.  D ,  ( ( F `  t
)  /  _i ) ,  ( 0  /  _i ) )
11013, 14div0i 10065 . . . . . . . . . . . . . . 15  |-  ( 0  /  _i )  =  0
111 ifeq2 3796 . . . . . . . . . . . . . . 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 2463 . . . . . . . . . . . . 13  |-  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  /  _i )  =  if ( t  e.  D ,  ( ( F `  t
)  /  _i ) ,  0 )
114106, 113syl6eqr 2493 . . . . . . . . . . . 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 5695 . . . . . . . . . . 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 2478 . . . . . . . . . 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 6106 . . . . . . . . 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 5695 . . . . . . . 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 4379 . . . . . . 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 5695 . . . . . 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 4302 . . . . 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 2736 . . . 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 465 . . 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 2888 . . 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 2503 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  t  ->  (
x  e.  D  <->  t  e.  D ) )
127 fveq2 5691 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  t  ->  ( F `  x )  =  ( F `  t ) )
128 eqidd 2444 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  t  ->  0  =  0 )
129126, 127, 128ifbieq12d 3816 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  t  ->  if ( x  e.  D ,  ( F `  x ) ,  0 )  =  if ( t  e.  D , 
( F `  t
) ,  0 ) )
130129fveq2d 5695 . . . . . . . . . . . . . . . . 17  |-  ( x  =  t  ->  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) )  =  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )
131 eqid 2443 . . . . . . . . . . . . . . . . 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 5701 . . . . . . . . . . . . . . . . 17  |-  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  _V
133130, 131, 132fvmpt 5774 . . . . . . . . . . . . . . . 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 6106 . . . . . . . . . . . . . . 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 5695 . . . . . . . . . . . . . 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 4374 . . . . . . . . . . . . 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 5694 . . . . . . . . . . . 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 21022 . . . . . . . . . . . . . . . . . . 19  |-  RR  e.  dom  vol
139138a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  RR  e.  dom  vol )
140 0cnd 9379 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  -.  x  e.  D )  ->  0  e.  CC )
14137, 140ifclda 3821 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  if ( x  e.  D ,  ( F `
 x ) ,  0 )  e.  CC )
142141adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  D )  ->  if ( x  e.  D ,  ( F `  x ) ,  0 )  e.  CC )
143 eldifn 3479 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( RR  \  D )  ->  -.  x  e.  D )
144143adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( RR  \  D ) )  ->  -.  x  e.  D )
145 iffalse 3799 . . . . . . . . . . . . . . . . . . 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 5744 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  F  =  ( x  e.  D  |->  ( F `
 x ) ) )
148 iftrue 3797 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  D  ->  if ( x  e.  D ,  ( F `  x ) ,  0 )  =  ( F `
 x ) )
149148mpteq2ia 4374 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  D  |->  if ( x  e.  D , 
( F `  x
) ,  0 ) )  =  ( x  e.  D  |->  ( F `
 x ) )
150147, 149syl6eqr 2493 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  F  =  ( x  e.  D  |->  if ( x  e.  D , 
( F `  x
) ,  0 ) ) )
151150, 8eqeltrrd 2518 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( x  e.  D  |->  if ( x  e.  D ,  ( F `
 x ) ,  0 ) )  e.  L^1 )
1527, 139, 142, 146, 151iblss2 21283 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( x  e.  RR  |->  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  e.  L^1 )
153141adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  if ( x  e.  D , 
( F `  x
) ,  0 )  e.  CC )
154153iblcn 21276 . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( x  e.  RR  |->  ( Re `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) )  e.  L^1 )
157153recld 12683 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ( Re
`  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  e.  RR )
158157, 131fmptd 5867 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( x  e.  RR  |->  ( Re `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) : RR --> RR )
159156, 158jca 532 . . . . . . . . . . . . . 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 28470 . . . . . . . . . . . . . . 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 1188 . . . . . . . . . . . . . 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 474 . . . . . . . . . . . . 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 453 . . . . . . . . . . . 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 2528 . . . . . . . . . . 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 5695 . . . . . . . . . . . . . . . . 17  |-  ( x  =  t  ->  (
Im `  if (
x  e.  D , 
( F `  x
) ,  0 ) )  =  ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )
166 eqid 2443 . . . . . . . . . . . . . . . . 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 5701 . . . . . . . . . . . . . . . . 17  |-  ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  _V
168165, 166, 167fvmpt 5774 . . . . . . . . . . . . . . . 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 6106 . . . . . . . . . . . . . . 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 5695 . . . . . . . . . . . . . 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 4374 . . . . . . . . . . . . 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 5694 . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( x  e.  RR  |->  ( Im `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) )  e.  L^1 )
174141imcld 12684 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( Im `  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  e.  RR )
175174adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ( Im
`  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  e.  RR )
176175, 166fmptd 5867 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( x  e.  RR  |->  ( Im `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) : RR --> RR )
177173, 176jca 532 . . . . . . . . . . . . . 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 28470 . . . . . . . . . . . . . . 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 1188 . . . . . . . . . . . . . 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 474 . . . . . . . . . . . . 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 453 . . . . . . . . . . . 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 2528 . . . . . . . . . . 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 833 . . . . . . . . . 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 11027 . . . . . . . . . . 11  |-  ( Y  e.  RR+  ->  ( Y  /  2 )  e.  RR )
185184, 184jca 532 . . . . . . . . . 10  |-  ( Y  e.  RR+  ->  ( ( Y  /  2 )  e.  RR  /\  ( Y  /  2 )  e.  RR ) )
186 lt2add 9824 . . . . . . . . . 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 477 . . . . . . . . 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 802 . . . . . . . 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 12683 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  RR )
190189recnd 9412 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  CC )
191 i1ff 21154 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  e.  dom  S.1  ->  f : RR --> RR )
192191ffvelrnda 5843 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( f `  t )  e.  RR )
193192recnd 9412 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( f `  t )  e.  CC )
194 subcl 9609 . . . . . . . . . . . . . . . . . . . 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 477 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  t  e.  RR ) )  -> 
( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  e.  CC )
196195anassrs 648 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  f  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  e.  CC )
197196adantlrr 720 . . . . . . . . . . . . . . . . 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 12684 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  RR )
199198recnd 9412 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  CC )
200 i1ff 21154 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g  e.  dom  S.1  ->  g : RR --> RR )
201200ffvelrnda 5843 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  e.  RR )
202201recnd 9412 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  e.  CC )
203 subcl 9609 . . . . . . . . . . . . . . . . . . . . 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 477 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( g  e.  dom  S.1  /\  t  e.  RR ) )  -> 
( ( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
)  e.  CC )
205204anassrs 648 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
)  e.  CC )
206 mulcl 9366 . . . . . . . . . . . . . . . . . . 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 663 . . . . . . . . . . . . . . . . . 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 719 . . . . . . . . . . . . . . . . 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 9405 . . . . . . . . . . . . . . . 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 12922 . . . . . . . . . . . . . . 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 9433 . . . . . . . . . . . . . 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 12930 . . . . . . . . . . . . . 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 11394 . . . . . . . . . . . . . 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 664 . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . 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 5867 . . . . . . . . . . . 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 9429 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  RR  ->  x  e.  RR* )
218217anim1i 568 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  RR  /\  0  <_  x )  -> 
( x  e.  RR*  /\  0  <_  x )
)
219 elrege0 11392 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( 0 [,) +oo )  <->  ( x  e.  RR  /\  0  <_  x ) )
220 elxrge0 11394 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( 0 [,] +oo )  <->  ( x  e. 
RR*  /\  0  <_  x ) )
221218, 219, 2203imtr4i 266 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( 0 [,) +oo )  ->  x  e.  ( 0 [,] +oo ) )
222221ssriv 3360 . . . . . . . . . . . . . . 15  |-  ( 0 [,) +oo )  C_  ( 0 [,] +oo )
223 ge0addcl 11397 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  ( 0 [,) +oo )  /\  y  e.  ( 0 [,) +oo ) )  ->  ( x  +  y )  e.  ( 0 [,) +oo )
)
224222, 223sseldi 3354 . . . . . . . . . . . . . 14  |-  ( ( x  e.  ( 0 [,) +oo )  /\  y  e.  ( 0 [,) +oo ) )  ->  ( x  +  y )  e.  ( 0 [,] +oo )
)
225224adantl 466 . . . . . . . . . . . . 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 12922 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  f  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( f `  t ) ) )  e.  RR )
227196absge0d 12930 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  f  e.  dom  S.1 )  /\  t  e.  RR )  ->  0  <_  ( abs `  (
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) )
228 elrege0 11392 . . . . . . . . . . . . . . . 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 664 . . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . . 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 5867 . . . . . . . . . . . . . 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 716 . . . . . . . . . . . . 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 12922 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) )  e.  RR )
234205absge0d 12930 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  0  <_  ( abs `  (
( Im `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
g `  t )
) ) )
235 elrege0 11392 . . . . . . . . . . . . . . . 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 664 . . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . . 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 5867 . . . . . . . . . . . . . 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 715 . . . . . . . . . . . . 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 9373 . . . . . . . . . . . . . 14  |-  RR  e.  _V
241240a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  ->  RR  e.  _V )
242 inidm 3559 . . . . . . . . . . . . 13  |-  ( RR 
i^i  RR )  =  RR
243225, 232, 239, 241, 241, 242off 6334 . . . . . . . . . . . 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 12942 . . . . . . . . . . . . . 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 2799 . . . . . . . . . . . . 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 6116 . . . . . . . . . . . . . . 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 2444 . . . . . . . . . . . . . 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 5701 . . . . . . . . . . . . . . . 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 5701 . . . . . . . . . . . . . . . 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 2444 . . . . . . . . . . . . . . 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 12783 . . . . . . . . . . . . . . . . . . 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 663 . . . . . . . . . . . . . . . . . 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 12775 . . . . . . . . . . . . . . . . . . . 20  |-  ( abs `  _i )  =  1
257256oveq1i 6101 . . . . . . . . . . . . . . . . . . 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 9412 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( Im
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( g `  t ) ) )  e.  CC )
259258mulid2d 9404 . . . . . . . . . . . . . . . . . . 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 2487 . . . . . . . . . . . . . . . . . 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 2476 . . . . . . . . . . . . . . . . 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 4378 . . . . . . . . . . . . . . . 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 715 . . . . . . . . . . . . . . 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 6336 . . . . . . . . . . . . . 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 6337 . . . . . . . . . . . . 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 21217 . . . . . . . . . . . 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 1218 . . . . . . . . . . 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 2444 . . . . . . . . . . . . . . 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 12825 . . . . . . . . . . . . . . . . 17  |-  abs : CC
--> RR
271270a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  f  e.  dom  S.1 )  ->  abs : CC --> RR )
272271feqmptd 5744 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  f  e.  dom  S.1 )  ->  abs  =  ( x  e.  CC  |->  ( abs `  x
) ) )
273 fveq2 5691 . . . . . . . . . . . . . . 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 5876 . . . . . . . . . . . . . 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 9673 . . . . . . . . . . . . . . . . . 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 477 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  t  e.  RR ) )  -> 
( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  e.  RR )
277276anassrs 648 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  f  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
)  e.  RR )
278 eqid 2443 . . . . . . . . . . . . . . . 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 5867 . . . . . . . . . . . . . . 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 4234 . . . . . . . . . . . . . . . . . . . . 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 5962 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( `' f " U_ y  e.  ran  f { y } )  =  U_ y  e.  ran  f ( `' f " {
y } )
283 iunid 4225 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  U_ y  e.  ran  f { y }  =  ran  f
284283imaeq2i 5167 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( `' f " U_ y  e.  ran  f { y } )  =  ( `' f " ran  f )
285282, 284eqtr3i 2465 . . . . . . . . . . . . . . . . . . . . . 22  |-  U_ y  e.  ran  f ( `' f " { y } )  =  ( `' f " ran  f )
286285ineq2i 3549 . . . . . . . . . . . . . . . . . . . . 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 2463 . . . . . . . . . . . . . . . . . . . 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 5189 . . . . . . . . . . . . . . . . . . . . . . 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 6116 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) )  e.  _V
290289, 278dmmpti 5540 . . . . . . . . . . . . . . . . . . . . . . 23  |-  dom  (
t  e.  RR  |->  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) )  =  RR
291288, 290sseqtri 3388 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( `' ( t  e.  RR  |->  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  (
f `  t )
) ) " (
x (,) +oo )
)  C_  RR
292 cnvimarndm 5190 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( `' f " ran  f
)  =  dom  f
293 fdm 5563 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f : RR --> RR  ->  dom  f  =  RR )
294191, 293syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f  e.  dom  S.1  ->  dom  f  =  RR )
295292, 294syl5eq 2487 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  e.  dom  S.1  ->  ( `' f " ran  f )  =  RR )
296291, 295syl5sseqr 3405 . . . . . . . . . . . . . . . . . . . . 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 3342 . . . . . . . . . . . . . . . . . . . . 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