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

Theorem ftc1anclem8 30073
Description: Lemma for ftc1anc 30074. (Contributed by Brendan Leahy, 29-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
ftc1anclem8  |-  ( ( ( ( ( ( ( ph  /\  (
f  e.  dom  S.1  /\  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  /  2
) )  /\  E. r  e.  ( ran  f  u.  ran  g ) r  =/=  0 )  /\  y  e.  RR+ )  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B )  /\  u  <_  w
) )  /\  ( abs `  ( w  -  u ) )  < 
( ( y  / 
2 )  /  (
2  x.  sup (
( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  )
) ) )  -> 
( S.2 `  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ) ,  0 ) ) )  <  y )
Distinct variable groups:    f, g,
r, t, u, w, x, y, A    B, f, g, r, t, u, w, x, y    D, f, g, r, t, u, w, x, y    f, F, g, r, t, u, w, x, y    ph, f,
g, r, t, u, w, x, y    f, G, g, r, u, w, y
Allowed substitution hints:    G( x, t)

Proof of Theorem ftc1anclem8
StepHypRef Expression
1 ftc1anc.g . . 3  |-  G  =  ( x  e.  ( A [,] B ) 
|->  S. ( A (,) x ) ( F `
 t )  _d t )
2 ftc1anc.a . . 3  |-  ( ph  ->  A  e.  RR )
3 ftc1anc.b . . 3  |-  ( ph  ->  B  e.  RR )
4 ftc1anc.le . . 3  |-  ( ph  ->  A  <_  B )
5 ftc1anc.s . . 3  |-  ( ph  ->  ( A (,) B
)  C_  D )
6 ftc1anc.d . . 3  |-  ( ph  ->  D  C_  RR )
7 ftc1anc.i . . 3  |-  ( ph  ->  F  e.  L^1 )
8 ftc1anc.f . . 3  |-  ( ph  ->  F : D --> CC )
91, 2, 3, 4, 5, 6, 7, 8ftc1anclem7 30072 . 2  |-  ( ( ( ( ( ( ( ph  /\  (
f  e.  dom  S.1  /\  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  /  2
) )  /\  E. r  e.  ( ran  f  u.  ran  g ) r  =/=  0 )  /\  y  e.  RR+ )  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B )  /\  u  <_  w
) )  /\  ( abs `  ( w  -  u ) )  < 
( ( y  / 
2 )  /  (
2  x.  sup (
( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  )
) ) )  -> 
( ( S.2 `  (
t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )  +  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) ) ) )  < 
( ( y  / 
2 )  +  ( y  /  2 ) ) )
10 simplll 759 . . . 4  |-  ( ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  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  /  2
) )  /\  E. r  e.  ( ran  f  u.  ran  g ) r  =/=  0 )  /\  y  e.  RR+ )  ->  ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) ) )
11 3simpa 994 . . . 4  |-  ( ( u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w )  ->  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )
12 ioossre 11597 . . . . . . . . 9  |-  ( u (,) w )  C_  RR
1312a1i 11 . . . . . . . 8  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  -> 
( u (,) w
)  C_  RR )
14 rembl 21929 . . . . . . . . 9  |-  RR  e.  dom  vol
1514a1i 11 . . . . . . . 8  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  ->  RR  e.  dom  vol )
16 fvex 5866 . . . . . . . . . 10  |-  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) )  e.  _V
17 c0ex 9593 . . . . . . . . . 10  |-  0  e.  _V
1816, 17ifex 3995 . . . . . . . . 9  |-  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  e.  _V
1918a1i 11 . . . . . . . 8  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  ( u (,) w
) )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  e.  _V )
20 eldifn 3612 . . . . . . . . . 10  |-  ( t  e.  ( RR  \ 
( u (,) w
) )  ->  -.  t  e.  ( u (,) w ) )
2120adantl 466 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  ( RR  \  (
u (,) w ) ) )  ->  -.  t  e.  ( u (,) w ) )
2221iffalsed 3937 . . . . . . . 8  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  ( RR  \  (
u (,) w ) ) )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  =  0 )
23 iftrue 3932 . . . . . . . . . . . 12  |-  ( t  e.  ( u (,) w )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  =  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
2423mpteq2ia 4519 . . . . . . . . . . 11  |-  ( t  e.  ( u (,) w )  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )  =  ( t  e.  ( u (,) w )  |->  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) )
25 resmpt 5313 . . . . . . . . . . . 12  |-  ( ( u (,) w ) 
C_  RR  ->  ( ( t  e.  RR  |->  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  |`  ( u (,) w ) )  =  ( t  e.  ( u (,) w ) 
|->  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ) )
2612, 25ax-mp 5 . . . . . . . . . . 11  |-  ( ( t  e.  RR  |->  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  |`  ( u (,) w ) )  =  ( t  e.  ( u (,) w ) 
|->  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
2724, 26eqtr4i 2475 . . . . . . . . . 10  |-  ( t  e.  ( u (,) w )  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )  =  ( ( t  e.  RR  |->  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  |`  ( u (,) w ) )
28 i1ff 22061 . . . . . . . . . . . . . . . . . 18  |-  ( f  e.  dom  S.1  ->  f : RR --> RR )
2928ffvelrnda 6016 . . . . . . . . . . . . . . . . 17  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( f `  t )  e.  RR )
3029recnd 9625 . . . . . . . . . . . . . . . 16  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( f `  t )  e.  CC )
31 ax-icn 9554 . . . . . . . . . . . . . . . . 17  |-  _i  e.  CC
32 i1ff 22061 . . . . . . . . . . . . . . . . . . 19  |-  ( g  e.  dom  S.1  ->  g : RR --> RR )
3332ffvelrnda 6016 . . . . . . . . . . . . . . . . . 18  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  e.  RR )
3433recnd 9625 . . . . . . . . . . . . . . . . 17  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  e.  CC )
35 mulcl 9579 . . . . . . . . . . . . . . . . 17  |-  ( ( _i  e.  CC  /\  ( g `  t
)  e.  CC )  ->  ( _i  x.  ( g `  t
) )  e.  CC )
3631, 34, 35sylancr 663 . . . . . . . . . . . . . . . 16  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( _i  x.  ( g `  t
) )  e.  CC )
37 addcl 9577 . . . . . . . . . . . . . . . 16  |-  ( ( ( f `  t
)  e.  CC  /\  ( _i  x.  (
g `  t )
)  e.  CC )  ->  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) )  e.  CC )
3830, 36, 37syl2an 477 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  dom  S.1 
/\  t  e.  RR )  /\  ( g  e. 
dom  S.1  /\  t  e.  RR ) )  -> 
( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) )  e.  CC )
3938anandirs 831 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) )  e.  CC )
40 reex 9586 . . . . . . . . . . . . . . . 16  |-  RR  e.  _V
4140a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  RR  e.  _V )
4229adantlr 714 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
f `  t )  e.  RR )
4336adantll 713 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
_i  x.  ( g `  t ) )  e.  CC )
4428feqmptd 5911 . . . . . . . . . . . . . . . 16  |-  ( f  e.  dom  S.1  ->  f  =  ( t  e.  RR  |->  ( f `  t ) ) )
4544adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  f  =  ( t  e.  RR  |->  ( f `  t ) ) )
4640a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( g  e.  dom  S.1  ->  RR  e.  _V )
4731a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  _i  e.  CC )
48 fconstmpt 5033 . . . . . . . . . . . . . . . . . 18  |-  ( RR 
X.  { _i }
)  =  ( t  e.  RR  |->  _i )
4948a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( g  e.  dom  S.1  ->  ( RR  X.  { _i } )  =  ( t  e.  RR  |->  _i ) )
5032feqmptd 5911 . . . . . . . . . . . . . . . . 17  |-  ( g  e.  dom  S.1  ->  g  =  ( t  e.  RR  |->  ( g `  t ) ) )
5146, 47, 33, 49, 50offval2 6541 . . . . . . . . . . . . . . . 16  |-  ( g  e.  dom  S.1  ->  ( ( RR  X.  {
_i } )  oF  x.  g )  =  ( t  e.  RR  |->  ( _i  x.  ( g `  t
) ) ) )
5251adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( ( RR 
X.  { _i }
)  oF  x.  g )  =  ( t  e.  RR  |->  ( _i  x.  ( g `
 t ) ) ) )
5341, 42, 43, 45, 52offval2 6541 . . . . . . . . . . . . . 14  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( f  oF  +  ( ( RR  X.  { _i } )  oF  x.  g ) )  =  ( t  e.  RR  |->  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) )
54 absf 13152 . . . . . . . . . . . . . . . 16  |-  abs : CC
--> RR
5554a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  abs : CC --> RR )
5655feqmptd 5911 . . . . . . . . . . . . . 14  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  abs  =  (
x  e.  CC  |->  ( abs `  x ) ) )
57 fveq2 5856 . . . . . . . . . . . . . 14  |-  ( x  =  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) )  ->  ( abs `  x )  =  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
5839, 53, 56, 57fmptco 6049 . . . . . . . . . . . . 13  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  ( f  oF  +  ( ( RR 
X.  { _i }
)  oF  x.  g ) ) )  =  ( t  e.  RR  |->  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ) )
59 ftc1anclem3 30068 . . . . . . . . . . . . 13  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  ( f  oF  +  ( ( RR 
X.  { _i }
)  oF  x.  g ) ) )  e.  dom  S.1 )
6058, 59eqeltrrd 2532 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( t  e.  RR  |->  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  e.  dom  S.1 )
61 i1fmbf 22060 . . . . . . . . . . . 12  |-  ( ( t  e.  RR  |->  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  e.  dom  S.1  ->  ( t  e.  RR  |->  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  e. MblFn )
6260, 61syl 16 . . . . . . . . . . 11  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( t  e.  RR  |->  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  e. MblFn )
63 ioombl 21953 . . . . . . . . . . 11  |-  ( u (,) w )  e. 
dom  vol
64 mbfres 22029 . . . . . . . . . . 11  |-  ( ( ( t  e.  RR  |->  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  e. MblFn  /\  (
u (,) w )  e.  dom  vol )  ->  ( ( t  e.  RR  |->  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  |`  (
u (,) w ) )  e. MblFn )
6562, 63, 64sylancl 662 . . . . . . . . . 10  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( ( t  e.  RR  |->  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) )  |`  ( u (,) w
) )  e. MblFn )
6627, 65syl5eqel 2535 . . . . . . . . 9  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( t  e.  ( u (,) w
)  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) )  e. MblFn )
6766adantl 466 . . . . . . . 8  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  -> 
( t  e.  ( u (,) w ) 
|->  if ( t  e.  ( u (,) w
) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ,  0 ) )  e. MblFn )
6813, 15, 19, 22, 67mbfss 22031 . . . . . . 7  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  -> 
( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )  e. MblFn )
6968adantr 465 . . . . . 6  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) )  e. MblFn )
7039abscld 13249 . . . . . . . . . 10  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  e.  RR )
7139absge0d 13257 . . . . . . . . . 10  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  0  <_  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
72 elrege0 11638 . . . . . . . . . 10  |-  ( ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) )  e.  ( 0 [,) +oo )  <->  ( ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) )  e.  RR  /\  0  <_  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ) )
7370, 71, 72sylanbrc 664 . . . . . . . . 9  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  e.  ( 0 [,) +oo ) )
74 0e0icopnf 11641 . . . . . . . . 9  |-  0  e.  ( 0 [,) +oo )
75 ifcl 3968 . . . . . . . . 9  |-  ( ( ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) )  e.  ( 0 [,) +oo )  /\  0  e.  ( 0 [,) +oo ) )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 )  e.  ( 0 [,) +oo ) )
7673, 74, 75sylancl 662 . . . . . . . 8  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  e.  ( 0 [,) +oo ) )
77 eqid 2443 . . . . . . . 8  |-  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )  =  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )
7876, 77fmptd 6040 . . . . . . 7  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) : RR --> ( 0 [,) +oo ) )
7978ad2antlr 726 . . . . . 6  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) : RR --> ( 0 [,) +oo ) )
8070rexrd 9646 . . . . . . . . . . 11  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  e. 
RR* )
81 elxrge0 11640 . . . . . . . . . . 11  |-  ( ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) )  e.  ( 0 [,] +oo )  <->  ( ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) )  e.  RR*  /\  0  <_  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ) )
8280, 71, 81sylanbrc 664 . . . . . . . . . 10  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  e.  ( 0 [,] +oo ) )
83 0e0iccpnf 11642 . . . . . . . . . 10  |-  0  e.  ( 0 [,] +oo )
84 ifcl 3968 . . . . . . . . . 10  |-  ( ( ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) )  e.  ( 0 [,] +oo )  /\  0  e.  ( 0 [,] +oo ) )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 )  e.  ( 0 [,] +oo ) )
8582, 83, 84sylancl 662 . . . . . . . . 9  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  e.  ( 0 [,] +oo ) )
8685, 77fmptd 6040 . . . . . . . 8  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) : RR --> ( 0 [,] +oo ) )
8786ad2antlr 726 . . . . . . 7  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) : RR --> ( 0 [,] +oo ) )
88 ifcl 3968 . . . . . . . . . . 11  |-  ( ( ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) )  e.  ( 0 [,] +oo )  /\  0  e.  ( 0 [,] +oo ) )  ->  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 )  e.  ( 0 [,] +oo ) )
8982, 83, 88sylancl 662 . . . . . . . . . 10  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  e.  ( 0 [,] +oo ) )
90 eqid 2443 . . . . . . . . . 10  |-  ( t  e.  RR  |->  if ( t  e.  D , 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )  =  ( t  e.  RR  |->  if ( t  e.  D , 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )
9189, 90fmptd 6040 . . . . . . . . 9  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) : RR --> ( 0 [,] +oo ) )
92 ffn 5721 . . . . . . . . . . . . . . 15  |-  ( f : RR --> RR  ->  f  Fn  RR )
93 frn 5727 . . . . . . . . . . . . . . . 16  |-  ( f : RR --> RR  ->  ran  f  C_  RR )
94 ax-resscn 9552 . . . . . . . . . . . . . . . 16  |-  RR  C_  CC
9593, 94syl6ss 3501 . . . . . . . . . . . . . . 15  |-  ( f : RR --> RR  ->  ran  f  C_  CC )
96 ffn 5721 . . . . . . . . . . . . . . . . 17  |-  ( abs
: CC --> RR  ->  abs 
Fn  CC )
9754, 96ax-mp 5 . . . . . . . . . . . . . . . 16  |-  abs  Fn  CC
98 fnco 5679 . . . . . . . . . . . . . . . 16  |-  ( ( abs  Fn  CC  /\  f  Fn  RR  /\  ran  f  C_  CC )  -> 
( abs  o.  f
)  Fn  RR )
9997, 98mp3an1 1312 . . . . . . . . . . . . . . 15  |-  ( ( f  Fn  RR  /\  ran  f  C_  CC )  ->  ( abs  o.  f )  Fn  RR )
10092, 95, 99syl2anc 661 . . . . . . . . . . . . . 14  |-  ( f : RR --> RR  ->  ( abs  o.  f )  Fn  RR )
10128, 100syl 16 . . . . . . . . . . . . 13  |-  ( f  e.  dom  S.1  ->  ( abs  o.  f )  Fn  RR )
102101adantr 465 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  f )  Fn  RR )
103 ffn 5721 . . . . . . . . . . . . . . 15  |-  ( g : RR --> RR  ->  g  Fn  RR )
104 frn 5727 . . . . . . . . . . . . . . . 16  |-  ( g : RR --> RR  ->  ran  g  C_  RR )
105104, 94syl6ss 3501 . . . . . . . . . . . . . . 15  |-  ( g : RR --> RR  ->  ran  g  C_  CC )
106 fnco 5679 . . . . . . . . . . . . . . . 16  |-  ( ( abs  Fn  CC  /\  g  Fn  RR  /\  ran  g  C_  CC )  -> 
( abs  o.  g
)  Fn  RR )
10797, 106mp3an1 1312 . . . . . . . . . . . . . . 15  |-  ( ( g  Fn  RR  /\  ran  g  C_  CC )  ->  ( abs  o.  g )  Fn  RR )
108103, 105, 107syl2anc 661 . . . . . . . . . . . . . 14  |-  ( g : RR --> RR  ->  ( abs  o.  g )  Fn  RR )
10932, 108syl 16 . . . . . . . . . . . . 13  |-  ( g  e.  dom  S.1  ->  ( abs  o.  g )  Fn  RR )
110109adantl 466 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  g )  Fn  RR )
111 inidm 3692 . . . . . . . . . . . 12  |-  ( RR 
i^i  RR )  =  RR
11228adantr 465 . . . . . . . . . . . . 13  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  f : RR --> RR )
113 fvco3 5935 . . . . . . . . . . . . 13  |-  ( ( f : RR --> RR  /\  t  e.  RR )  ->  ( ( abs  o.  f ) `  t
)  =  ( abs `  ( f `  t
) ) )
114112, 113sylan 471 . . . . . . . . . . . 12  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( abs  o.  f
) `  t )  =  ( abs `  (
f `  t )
) )
11532adantl 466 . . . . . . . . . . . . 13  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  g : RR --> RR )
116 fvco3 5935 . . . . . . . . . . . . 13  |-  ( ( g : RR --> RR  /\  t  e.  RR )  ->  ( ( abs  o.  g ) `  t
)  =  ( abs `  ( g `  t
) ) )
117115, 116sylan 471 . . . . . . . . . . . 12  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( abs  o.  g
) `  t )  =  ( abs `  (
g `  t )
) )
118102, 110, 41, 41, 111, 114, 117offval 6532 . . . . . . . . . . 11  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( ( abs 
o.  f )  oF  +  ( abs 
o.  g ) )  =  ( t  e.  RR  |->  ( ( abs `  ( f `  t
) )  +  ( abs `  ( g `
 t ) ) ) ) )
11930addid1d 9783 . . . . . . . . . . . . . . . . 17  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( ( f `
 t )  +  0 )  =  ( f `  t ) )
120119mpteq2dva 4523 . . . . . . . . . . . . . . . 16  |-  ( f  e.  dom  S.1  ->  ( t  e.  RR  |->  ( ( f `  t
)  +  0 ) )  =  ( t  e.  RR  |->  ( f `
 t ) ) )
12140a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( f  e.  dom  S.1  ->  RR  e.  _V )
12217a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  0  e.  _V )
12331a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  _i  e.  CC )
12448a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( f  e.  dom  S.1  ->  ( RR  X.  { _i } )  =  ( t  e.  RR  |->  _i ) )
125 fconstmpt 5033 . . . . . . . . . . . . . . . . . . . 20  |-  ( RR 
X.  { 0 } )  =  ( t  e.  RR  |->  0 )
126125a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( f  e.  dom  S.1  ->  ( RR  X.  { 0 } )  =  ( t  e.  RR  |->  0 ) )
127121, 123, 122, 124, 126offval2 6541 . . . . . . . . . . . . . . . . . 18  |-  ( f  e.  dom  S.1  ->  ( ( RR  X.  {
_i } )  oF  x.  ( RR 
X.  { 0 } ) )  =  ( t  e.  RR  |->  ( _i  x.  0 ) ) )
128 it0e0 10768 . . . . . . . . . . . . . . . . . . 19  |-  ( _i  x.  0 )  =  0
129128mpteq2i 4520 . . . . . . . . . . . . . . . . . 18  |-  ( t  e.  RR  |->  ( _i  x.  0 ) )  =  ( t  e.  RR  |->  0 )
130127, 129syl6eq 2500 . . . . . . . . . . . . . . . . 17  |-  ( f  e.  dom  S.1  ->  ( ( RR  X.  {
_i } )  oF  x.  ( RR 
X.  { 0 } ) )  =  ( t  e.  RR  |->  0 ) )
131121, 29, 122, 44, 130offval2 6541 . . . . . . . . . . . . . . . 16  |-  ( f  e.  dom  S.1  ->  ( f  oF  +  ( ( RR  X.  { _i } )  oF  x.  ( RR 
X.  { 0 } ) ) )  =  ( t  e.  RR  |->  ( ( f `  t )  +  0 ) ) )
132120, 131, 443eqtr4d 2494 . . . . . . . . . . . . . . 15  |-  ( f  e.  dom  S.1  ->  ( f  oF  +  ( ( RR  X.  { _i } )  oF  x.  ( RR 
X.  { 0 } ) ) )  =  f )
133132coeq2d 5155 . . . . . . . . . . . . . 14  |-  ( f  e.  dom  S.1  ->  ( abs  o.  ( f  oF  +  ( ( RR  X.  {
_i } )  oF  x.  ( RR 
X.  { 0 } ) ) ) )  =  ( abs  o.  f ) )
134 i1f0 22072 . . . . . . . . . . . . . . 15  |-  ( RR 
X.  { 0 } )  e.  dom  S.1
135 ftc1anclem3 30068 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  ( RR  X.  {
0 } )  e. 
dom  S.1 )  ->  ( abs  o.  ( f  oF  +  ( ( RR  X.  { _i } )  oF  x.  ( RR  X.  { 0 } ) ) ) )  e. 
dom  S.1 )
136134, 135mpan2 671 . . . . . . . . . . . . . 14  |-  ( f  e.  dom  S.1  ->  ( abs  o.  ( f  oF  +  ( ( RR  X.  {
_i } )  oF  x.  ( RR 
X.  { 0 } ) ) ) )  e.  dom  S.1 )
137133, 136eqeltrrd 2532 . . . . . . . . . . . . 13  |-  ( f  e.  dom  S.1  ->  ( abs  o.  f )  e.  dom  S.1 )
138137adantr 465 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  f )  e.  dom  S.1 )
139 coeq2 5151 . . . . . . . . . . . . . . 15  |-  ( f  =  g  ->  ( abs  o.  f )  =  ( abs  o.  g
) )
140139eleq1d 2512 . . . . . . . . . . . . . 14  |-  ( f  =  g  ->  (
( abs  o.  f
)  e.  dom  S.1  <->  ( abs  o.  g )  e. 
dom  S.1 ) )
141140, 137vtoclga 3159 . . . . . . . . . . . . 13  |-  ( g  e.  dom  S.1  ->  ( abs  o.  g )  e.  dom  S.1 )
142141adantl 466 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  g )  e.  dom  S.1 )
143138, 142i1fadd 22080 . . . . . . . . . . 11  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( ( abs 
o.  f )  oF  +  ( abs 
o.  g ) )  e.  dom  S.1 )
144118, 143eqeltrrd 2532 . . . . . . . . . 10  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( t  e.  RR  |->  ( ( abs `  ( f `  t
) )  +  ( abs `  ( g `
 t ) ) ) )  e.  dom  S.1 )
14530abscld 13249 . . . . . . . . . . . . . . . 16  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
f `  t )
)  e.  RR )
14630absge0d 13257 . . . . . . . . . . . . . . . 16  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  0  <_  ( abs `  ( f `  t ) ) )
147 elrege0 11638 . . . . . . . . . . . . . . . 16  |-  ( ( abs `  ( f `
 t ) )  e.  ( 0 [,) +oo )  <->  ( ( abs `  ( f `  t
) )  e.  RR  /\  0  <_  ( abs `  ( f `  t
) ) ) )
148145, 146, 147sylanbrc 664 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
f `  t )
)  e.  ( 0 [,) +oo ) )
14934abscld 13249 . . . . . . . . . . . . . . . 16  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
g `  t )
)  e.  RR )
15034absge0d 13257 . . . . . . . . . . . . . . . 16  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  0  <_  ( abs `  ( g `  t ) ) )
151 elrege0 11638 . . . . . . . . . . . . . . . 16  |-  ( ( abs `  ( g `
 t ) )  e.  ( 0 [,) +oo )  <->  ( ( abs `  ( g `  t
) )  e.  RR  /\  0  <_  ( abs `  ( g `  t
) ) ) )
152149, 150, 151sylanbrc 664 . . . . . . . . . . . . . . 15  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
g `  t )
)  e.  ( 0 [,) +oo ) )
153 ge0addcl 11643 . . . . . . . . . . . . . . 15  |-  ( ( ( abs `  (
f `  t )
)  e.  ( 0 [,) +oo )  /\  ( abs `  ( g `
 t ) )  e.  ( 0 [,) +oo ) )  ->  (
( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) )  e.  ( 0 [,) +oo ) )
154148, 152, 153syl2an 477 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  dom  S.1 
/\  t  e.  RR )  /\  ( g  e. 
dom  S.1  /\  t  e.  RR ) )  -> 
( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) )  e.  ( 0 [,) +oo ) )
155154anandirs 831 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) )  e.  ( 0 [,) +oo ) )
156 eqid 2443 . . . . . . . . . . . . 13  |-  ( t  e.  RR  |->  ( ( abs `  ( f `
 t ) )  +  ( abs `  (
g `  t )
) ) )  =  ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) )
157155, 156fmptd 6040 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( t  e.  RR  |->  ( ( abs `  ( f `  t
) )  +  ( abs `  ( g `
 t ) ) ) ) : RR --> ( 0 [,) +oo ) )
158 0plef 22057 . . . . . . . . . . . 12  |-  ( ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) : RR --> ( 0 [,) +oo )  <->  ( (
t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) : RR --> RR  /\  0p  oR 
<_  ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) ) )
159157, 158sylib 196 . . . . . . . . . . 11  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( ( t  e.  RR  |->  ( ( abs `  ( f `
 t ) )  +  ( abs `  (
g `  t )
) ) ) : RR --> RR  /\  0p  oR  <_  (
t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) ) )
160159simprd 463 . . . . . . . . . 10  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  0p  oR  <_  ( t  e.  RR  |->  ( ( abs `  ( f `  t
) )  +  ( abs `  ( g `
 t ) ) ) ) )
161 itg2itg1 22121 . . . . . . . . . . 11  |-  ( ( ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) )  e.  dom  S.1  /\  0p  oR 
<_  ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) )  ->  ( S.2 `  ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) )  =  ( S.1 `  ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) ) )
162 itg1cl 22070 . . . . . . . . . . . 12  |-  ( ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) )  e.  dom  S.1  ->  ( S.1 `  ( t  e.  RR  |->  ( ( abs `  ( f `
 t ) )  +  ( abs `  (
g `  t )
) ) ) )  e.  RR )
163162adantr 465 . . . . . . . . . . 11  |-  ( ( ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) )  e.  dom  S.1  /\  0p  oR 
<_  ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) )  ->  ( S.1 `  ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) )  e.  RR )
164161, 163eqeltrd 2531 . . . . . . . . . 10  |-  ( ( ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) )  e.  dom  S.1  /\  0p  oR 
<_  ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) )  ->  ( S.2 `  ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) )  e.  RR )
165144, 160, 164syl2anc 661 . . . . . . . . 9  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( S.2 `  (
t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) )  e.  RR )
166 icossicc 11622 . . . . . . . . . . 11  |-  ( 0 [,) +oo )  C_  ( 0 [,] +oo )
167 fss 5729 . . . . . . . . . . 11  |-  ( ( ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) : RR --> ( 0 [,) +oo )  /\  ( 0 [,) +oo )  C_  ( 0 [,] +oo ) )  ->  (
t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) : RR --> ( 0 [,] +oo ) )
168157, 166, 167sylancl 662 . . . . . . . . . 10  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( t  e.  RR  |->  ( ( abs `  ( f `  t
) )  +  ( abs `  ( g `
 t ) ) ) ) : RR --> ( 0 [,] +oo ) )
169 0re 9599 . . . . . . . . . . . . . 14  |-  0  e.  RR
170 ifcl 3968 . . . . . . . . . . . . . 14  |-  ( ( ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) )  e.  RR  /\  0  e.  RR )  ->  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ,  0 )  e.  RR )
17170, 169, 170sylancl 662 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  e.  RR )
172 readdcl 9578 . . . . . . . . . . . . . . 15  |-  ( ( ( abs `  (
f `  t )
)  e.  RR  /\  ( abs `  ( g `
 t ) )  e.  RR )  -> 
( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) )  e.  RR )
173145, 149, 172syl2an 477 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  dom  S.1 
/\  t  e.  RR )  /\  ( g  e. 
dom  S.1  /\  t  e.  RR ) )  -> 
( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) )  e.  RR )
174173anandirs 831 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) )  e.  RR )
17570leidd 10126 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  <_ 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
176 breq1 4440 . . . . . . . . . . . . . . 15  |-  ( ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) )  =  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 )  -> 
( ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) )  <_  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) )  <->  if (
t  e.  D , 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  <_  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ) )
177 breq1 4440 . . . . . . . . . . . . . . 15  |-  ( 0  =  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 )  -> 
( 0  <_  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  <->  if (
t  e.  D , 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  <_  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ) )
178176, 177ifboth 3962 . . . . . . . . . . . . . 14  |-  ( ( ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) )  <_  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) )  /\  0  <_  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  ->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  <_  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
179175, 71, 178syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  <_  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
180 abstri 13145 . . . . . . . . . . . . . . . 16  |-  ( ( ( f `  t
)  e.  CC  /\  ( _i  x.  (
g `  t )
)  e.  CC )  ->  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) )  <_  ( ( abs `  ( f `  t ) )  +  ( abs `  (
_i  x.  ( g `  t ) ) ) ) )
18130, 36, 180syl2an 477 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  dom  S.1 
/\  t  e.  RR )  /\  ( g  e. 
dom  S.1  /\  t  e.  RR ) )  -> 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) )  <_  ( ( abs `  ( f `  t ) )  +  ( abs `  (
_i  x.  ( g `  t ) ) ) ) )
182181anandirs 831 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  <_ 
( ( abs `  (
f `  t )
)  +  ( abs `  ( _i  x.  (
g `  t )
) ) ) )
183 absmul 13109 . . . . . . . . . . . . . . . . . . 19  |-  ( ( _i  e.  CC  /\  ( g `  t
)  e.  CC )  ->  ( abs `  (
_i  x.  ( g `  t ) ) )  =  ( ( abs `  _i )  x.  ( abs `  ( g `  t ) ) ) )
18431, 34, 183sylancr 663 . . . . . . . . . . . . . . . . . 18  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
_i  x.  ( g `  t ) ) )  =  ( ( abs `  _i )  x.  ( abs `  ( g `  t ) ) ) )
185 absi 13101 . . . . . . . . . . . . . . . . . . 19  |-  ( abs `  _i )  =  1
186185oveq1i 6291 . . . . . . . . . . . . . . . . . 18  |-  ( ( abs `  _i )  x.  ( abs `  (
g `  t )
) )  =  ( 1  x.  ( abs `  ( g `  t
) ) )
187184, 186syl6eq 2500 . . . . . . . . . . . . . . . . 17  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
_i  x.  ( g `  t ) ) )  =  ( 1  x.  ( abs `  (
g `  t )
) ) )
188149recnd 9625 . . . . . . . . . . . . . . . . . 18  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
g `  t )
)  e.  CC )
189188mulid2d 9617 . . . . . . . . . . . . . . . . 17  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( 1  x.  ( abs `  (
g `  t )
) )  =  ( abs `  ( g `
 t ) ) )
190187, 189eqtrd 2484 . . . . . . . . . . . . . . . 16  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
_i  x.  ( g `  t ) ) )  =  ( abs `  (
g `  t )
) )
191190adantll 713 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( _i  x.  ( g `  t
) ) )  =  ( abs `  (
g `  t )
) )
192191oveq2d 6297 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( abs `  (
f `  t )
)  +  ( abs `  ( _i  x.  (
g `  t )
) ) )  =  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) )
193182, 192breqtrd 4461 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  <_ 
( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) )
194171, 70, 174, 179, 193letrd 9742 . . . . . . . . . . . 12  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  <_  ( ( abs `  ( f `  t
) )  +  ( abs `  ( g `
 t ) ) ) )
195194ralrimiva 2857 . . . . . . . . . . 11  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  A. t  e.  RR  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  <_  ( ( abs `  ( f `  t
) )  +  ( abs `  ( g `
 t ) ) ) )
196 eqidd 2444 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) )  =  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) )
197 eqidd 2444 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( t  e.  RR  |->  ( ( abs `  ( f `  t
) )  +  ( abs `  ( g `
 t ) ) ) )  =  ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) )
19841, 171, 174, 196, 197ofrfval2 6542 . . . . . . . . . . 11  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( ( t  e.  RR  |->  if ( t  e.  D , 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )  oR  <_ 
( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) )  <->  A. t  e.  RR  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  <_  ( ( abs `  ( f `  t
) )  +  ( abs `  ( g `
 t ) ) ) ) )
199195, 198mpbird 232 . . . . . . . . . 10  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) )  oR  <_  (
t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) )
200 itg2le 22124 . . . . . . . . . 10  |-  ( ( ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) : RR --> ( 0 [,] +oo )  /\  ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) : RR --> ( 0 [,] +oo )  /\  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )  oR  <_ 
( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) )  ->  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )  <_  ( S.2 `  ( t  e.  RR  |->  ( ( abs `  ( f `  t
) )  +  ( abs `  ( g `
 t ) ) ) ) ) )
20191, 168, 199, 200syl3anc 1229 . . . . . . . . 9  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )  <_  ( S.2 `  ( t  e.  RR  |->  ( ( abs `  ( f `  t
) )  +  ( abs `  ( g `
 t ) ) ) ) ) )
202 itg2lecl 22123 . . . . . . . . 9  |-  ( ( ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) : RR --> ( 0 [,] +oo )  /\  ( S.2 `  ( t  e.  RR  |->  ( ( abs `  ( f `
 t ) )  +  ( abs `  (
g `  t )
) ) ) )  e.  RR  /\  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) )  <_  ( S.2 `  ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) ) )  ->  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) )  e.  RR )
20391, 165, 201, 202syl3anc 1229 . . . . . . . 8  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )  e.  RR )
204203ad2antlr 726 . . . . . . 7  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )  e.  RR )
20591ad2antlr 726 . . . . . . . 8  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) : RR --> ( 0 [,] +oo ) )
206 breq1 4440 . . . . . . . . . . 11  |-  ( ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) )  =  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 )  -> 
( ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) )  <_  if (
t  e.  D , 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  <-> 
if ( t  e.  ( u (,) w
) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ,  0 )  <_  if (
t  e.  D , 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )
207 breq1 4440 . . . . . . . . . . 11  |-  ( 0  =  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 )  -> 
( 0  <_  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  <-> 
if ( t  e.  ( u (,) w
) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ,  0 )  <_  if (
t  e.  D , 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )
208 elioore 11570 . . . . . . . . . . . . . . 15  |-  ( t  e.  ( u (,) w )  ->  t  e.  RR )
209208, 175sylan2 474 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  ( u (,) w
) )  ->  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  <_ 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
210209adantll 713 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  ( u (,) w
) )  ->  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  <_ 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
211210adantlr 714 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) )  <_  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) )
2122rexrd 9646 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A  e.  RR* )
2133rexrd 9646 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  B  e.  RR* )
214212, 213jca 532 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( A  e.  RR*  /\  B  e.  RR* )
)
215 df-icc 11547 . . . . . . . . . . . . . . . . . . . . 21  |-  [,]  =  ( x  e.  RR* ,  y  e.  RR*  |->  { t  e.  RR*  |  (
x  <_  t  /\  t  <_  y ) } )
216215elixx3g 11553 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  e.  ( A [,] B )  <->  ( ( A  e.  RR*  /\  B  e.  RR*  /\  u  e. 
RR* )  /\  ( A  <_  u  /\  u  <_  B ) ) )
217216simprbi 464 . . . . . . . . . . . . . . . . . . 19  |-  ( u  e.  ( A [,] B )  ->  ( A  <_  u  /\  u  <_  B ) )
218217simpld 459 . . . . . . . . . . . . . . . . . 18  |-  ( u  e.  ( A [,] B )  ->  A  <_  u )
219215elixx3g 11553 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  e.  ( A [,] B )  <->  ( ( A  e.  RR*  /\  B  e.  RR*  /\  w  e. 
RR* )  /\  ( A  <_  w  /\  w  <_  B ) ) )
220219simprbi 464 . . . . . . . . . . . . . . . . . . 19  |-  ( w  e.  ( A [,] B )  ->  ( A  <_  w  /\  w  <_  B ) )
221220simprd 463 . . . . . . . . . . . . . . . . . 18  |-  ( w  e.  ( A [,] B )  ->  w  <_  B )
222218, 221anim12i 566 . . . . . . . . . . . . . . . . 17  |-  ( ( u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) )  -> 
( A  <_  u  /\  w  <_  B ) )
223 ioossioo 11627 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <_  u  /\  w  <_  B ) )  ->  ( u (,) w )  C_  ( A (,) B ) )
224214, 222, 223syl2an 477 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  (
u (,) w ) 
C_  ( A (,) B ) )
2255adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  ( A (,) B )  C_  D )
226224, 225sstrd 3499 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  (
u (,) w ) 
C_  D )
227226sselda 3489 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  t  e.  D )
228 iftrue 3932 . . . . . . . . . . . . . 14  |-  ( t  e.  D  ->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  =  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
229227, 228syl 16 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  if (
t  e.  D , 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  =  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
230229adantllr 718 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  if (
t  e.  D , 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  =  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
231211, 230breqtrrd 4463 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) )  <_  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )
232 breq2 4441 . . . . . . . . . . . . 13  |-  ( ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) )  =  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 )  -> 
( 0  <_  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  <->  0  <_  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )
233 breq2 4441 . . . . . . . . . . . . 13  |-  ( 0  =  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 )  -> 
( 0  <_  0  <->  0  <_  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) )
2346sselda 3489 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  D )  ->  t  e.  RR )
235234adantlr 714 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  D )  ->  t  e.  RR )
23671adantll 713 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  RR )  ->  0  <_  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
237235, 236syldan 470 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  D )  ->  0  <_  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
238 0le0 10632 . . . . . . . . . . . . . 14  |-  0  <_  0
239238a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  -.  t  e.  D )  ->  0  <_  0 )
240232, 233, 237, 239ifbothda 3961 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  -> 
0  <_  if (
t  e.  D , 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )
241240ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  -.  t  e.  ( u (,) w
) )  ->  0  <_  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ,  0 ) )
242206, 207, 231, 241ifbothda 3961 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 )  <_  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )
243242ralrimivw 2858 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  A. t  e.  RR  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  <_  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) )
24440a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  RR  e.  _V )
24518a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  RR )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  e.  _V )
24616, 17ifex 3995 . . . . . . . . . . . 12  |-  if ( t  e.  D , 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  e.  _V
247246a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  RR )  ->  if ( t  e.  D , 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  e.  _V )
248 eqidd 2444 . . . . . . . . . . 11  |-  ( ph  ->  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )  =  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )
249 eqidd 2444 . . . . . . . . . . 11  |-  ( ph  ->  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )  =  ( t  e.  RR  |->  if ( t  e.  D , 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )
250244, 245, 247, 248, 249ofrfval2 6542 . . . . . . . . . 10  |-  ( ph  ->  ( ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) )  oR  <_  (
t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )  <->  A. t  e.  RR  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  <_  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) )
251250ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )  oR  <_ 
( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )  <->  A. t  e.  RR  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  <_  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) )
252243, 251mpbird 232 . . . . . . . 8  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) )  oR  <_  (
t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )
253 itg2le 22124 . . . . . . . 8  |-  ( ( ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) : RR --> ( 0 [,] +oo )  /\  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) : RR --> ( 0 [,] +oo )  /\  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )  oR  <_ 
( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )  ->  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) )  <_  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) ) )
25487, 205, 252, 253syl3anc 1229 . . . . . . 7  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )  <_  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) ) )
255 itg2lecl 22123 . . . . . . 7  |-  ( ( ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) : RR --> ( 0 [,] +oo )  /\  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  D , 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )  e.  RR  /\  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )  <_  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) ) )  ->  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) )  e.  RR )
25687, 204, 254, 255syl3anc 1229 . . . . . 6  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )  e.  RR )
2578ffvelrnda 6016 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  D )  ->  ( F `  t )  e.  CC )
258257adantlr 714 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  D
)  ->  ( F `  t )  e.  CC )
259227, 258syldan 470 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  ( F `  t )  e.  CC )
260259adantllr 718 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  ( F `  t )  e.  CC )
261208, 39sylan2 474 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  ( u (,) w
) )  ->  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) )  e.  CC )
262261adantll 713 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  ( u (,) w
) )  ->  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) )  e.  CC )
263262adantlr 714 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  ( (
f `  t )  +  ( _i  x.  ( g `  t
) ) )  e.  CC )
264260, 263subcld 9936 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  ( ( F `  t )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  e.  CC )
265264abscld 13249 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  ( abs `  ( ( F `  t )  -  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  e.  RR )
266264absge0d 13257 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  0  <_  ( abs `  ( ( F `  t )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) ) )
267 elrege0 11638 . . . . . . . . . 10  |-  ( ( abs `  ( ( F `  t )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) )  e.  ( 0 [,) +oo )  <->  ( ( abs `  ( ( F `  t )  -  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  e.  RR  /\  0  <_  ( abs `  ( ( F `  t )  -  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ) ) )
268265, 266, 267sylanbrc 664 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  ( abs `  ( ( F `  t )  -  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  e.  ( 0 [,) +oo )
)
26974a1i 11 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  -.  t  e.  ( u (,) w
) )  ->  0  e.  ( 0 [,) +oo ) )
270268, 269ifclda 3958 . . . . . . . 8  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( F `  t )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) ) ,  0 )  e.  ( 0 [,) +oo ) )
271270adantr 465 . . . . . . 7  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  RR )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( F `  t )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) ) ,  0 )  e.  ( 0 [,) +oo ) )
272 eqid 2443 . . . . . . 7  |-  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) )  =  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) )
273271, 272fmptd 6040 . . . . . 6  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( F `  t )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) ) ,  0 ) ) : RR --> ( 0 [,) +oo ) )
274265rexrd 9646 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  ( abs `  ( ( F `  t )  -  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  e.  RR* )
275 elxrge0 11640 . . . . . . . . . . 11  |-  ( ( abs `  ( ( F `  t )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) )  e.  ( 0 [,] +oo )  <->  ( ( abs `  ( ( F `  t )  -  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  e.  RR*  /\  0  <_  ( abs `  ( ( F `  t )  -  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ) ) )
276274, 266, 275sylanbrc 664 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  ( abs `  ( ( F `  t )  -  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  e.  ( 0 [,] +oo )
)
27783a1i 11 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  -.  t  e.  ( u (,) w
) )  ->  0  e.  ( 0 [,] +oo ) )
278276, 277ifclda 3958 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( F `  t )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) ) ,  0 )  e.  ( 0 [,] +oo ) )
279278adantr 465 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  RR )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( F `  t )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) ) ,  0 )  e.  ( 0 [,] +oo ) )
280279, 272fmptd 6040 . . . . . . 7  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( F `  t )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) ) ,  0 ) ) : RR --> ( 0 [,] +oo ) )
281 recncf 21384 . . . . . . . . . . . . 13  |-  Re  e.  ( CC -cn-> RR )
282 prid1g 4121 . . . . . . . . . . . . 13  |-  ( Re  e.  ( CC -cn-> RR )  ->  Re  e.  { Re ,  Im }
)
283281, 282ax-mp 5 . . . . . . . . . . . 12  |-  Re  e.  { Re ,  Im }
284 ftc1anclem2 30067 . . . . . . . . . . . 12  |-  ( ( F : D --> CC  /\  F  e.  L^1  /\  Re  e.  { Re ,  Im } )  -> 
( S.2 `  ( t  e.  RR  |->  if ( t  e.  D , 
( abs `  (
Re `  ( F `  t ) ) ) ,  0 ) ) )  e.  RR )
285283, 284mp3an3 1314 . . . . . . . . . . 11  |-  ( ( F : D --> CC  /\  F  e.  L^1
)  ->  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
Re `  ( F `  t ) ) ) ,  0 ) ) )  e.  RR )
2868, 7, 285syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
Re `  ( F `  t ) ) ) ,  0 ) ) )  e.  RR )
287 imcncf 21385 . . . . . . . . . . . . 13  |-  Im  e.  ( CC -cn-> RR )
288 prid2g 4122 . . . . . . . . . . . . 13  |-  ( Im  e.  ( CC -cn-> RR )  ->  Im  e.  { Re ,  Im }
)
289287, 288ax-mp 5 . . . . . . . . . . . 12  |-  Im  e.  { Re ,  Im }
290 ftc1anclem2 30067 . . . . . . . . . . . 12  |-  ( ( F : D --> CC  /\  F  e.  L^1  /\  Im  e.  { Re ,  Im } )  -> 
( S.2 `  ( t  e.  RR  |->  if ( t  e.  D , 
( abs `  (
Im `  ( F `  t ) ) ) ,  0 ) ) )  e.  RR )
291289, 290mp3an3 1314 . . . . . . . . . . 11  |-  ( ( F : D --> CC  /\  F  e.  L^1
)  ->  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
Im `  ( F `  t ) ) ) ,  0 ) ) )  e.  RR )
2928, 7, 291syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
Im `  ( F `  t ) ) ) ,  0 ) ) )  e.  RR )
293286, 292readdcld 9626 . . . . . . . . 9  |-  ( ph  ->  ( ( S.2 `  (
t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
Re `  ( F `  t ) ) ) ,  0 ) ) )  +  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
Im `  ( F `  t ) ) ) ,  0 ) ) ) )  e.  RR )
294293ad2antrr 725 . . . . . . . 8  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( ( S.2 `  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
Re `  ( F `  t ) ) ) ,  0 ) ) )  +  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
Im `  ( F `  t ) ) ) ,  0 ) ) ) )  e.  RR )
295204, 294readdcld 9626 . . . . . . 7  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( ( S.2 `  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )  +  ( ( S.2 `  (
t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
Re `  ( F `  t ) ) ) ,  0 ) ) )  +  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
Im `  ( F `  t ) ) ) ,  0 ) ) ) ) )  e.  RR )
296 ge0addcl 11643 . . . . . . . . . . . . 13  |-  ( ( x  e.  ( 0 [,) +oo )  /\  y  e.  ( 0 [,) +oo ) )  ->  ( x  +  y )  e.  ( 0 [,) +oo )
)
297296adantl 466 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
x  e.  ( 0 [,) +oo )  /\  y  e.  ( 0 [,) +oo ) ) )  ->  ( x  +  y )  e.  ( 0 [,) +oo ) )
298 ifcl 3968 . . . . . . . . . . . . . . 15  |-  ( ( ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) )  e.  ( 0 [,) +oo )  /\  0  e.  ( 0 [,) +oo ) )  ->  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 )  e.  ( 0 [,) +oo ) )
29973, 74, 298sylancl 662 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  e.  ( 0 [,) +oo ) )
300299, 90fmptd 6040 . . . . . . . . . . . . 13  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) : RR --> ( 0 [,) +oo ) )
301300adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  -> 
( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) : RR --> ( 0 [,) +oo ) )
302296adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  ( 0 [,) +oo )  /\  y  e.  ( 0 [,) +oo )
) )  ->  (
x  +  y )  e.  ( 0 [,) +oo ) )
303257recld 13009 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  D )  ->  (
Re `  ( F `  t ) )  e.  RR )
304303recnd 9625 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  D )  ->  (
Re `  ( F `  t ) )  e.  CC )
305304abscld 13249 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  D )  ->  ( abs `  ( Re `  ( F `  t ) ) )  e.  RR )
306304absge0d 13257 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  D )  ->  0  <_  ( abs `  (
Re `  ( F `  t ) ) ) )
307 elrege0 11638 . . . . . . . . . . . . . . . . . 18  |-  ( ( abs `  ( Re
`  ( F `  t ) ) )  e.  ( 0 [,) +oo )  <->  ( ( abs `  ( Re `  ( F `  t )
) )  e.  RR  /\  0  <_  ( abs `  ( Re `  ( F `  t )
) ) ) )
308305, 306, 307sylanbrc 664 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  D )  ->  ( abs `  ( Re `  ( F `  t ) ) )  e.  ( 0 [,) +oo )
)
30974a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  -.  t  e.  D )  ->  0  e.  ( 0 [,) +oo ) )
310308, 309ifclda 3958 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  if ( t  e.  D ,  ( abs `  ( Re `  ( F `  t )
) ) ,  0 )  e.  ( 0 [,) +oo ) )
311310adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  RR )  ->  if