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

Theorem ftc1anclem8 30263
Description: Lemma for ftc1anc 30264. (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 30262 . 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 757 . . . 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 991 . . . 4  |-  ( ( u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w )  ->  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )
12 ioossre 11507 . . . . . . . . 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 22036 . . . . . . . . 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 5784 . . . . . . . . . 10  |-  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) )  e.  _V
17 c0ex 9501 . . . . . . . . . 10  |-  0  e.  _V
1816, 17ifex 3925 . . . . . . . . 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 3541 . . . . . . . . . 10  |-  ( t  e.  ( RR  \ 
( u (,) w
) )  ->  -.  t  e.  ( u (,) w ) )
2120adantl 464 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  ( RR  \  (
u (,) w ) ) )  ->  -.  t  e.  ( u (,) w ) )
2221iffalsed 3868 . . . . . . . 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 3863 . . . . . . . . . . . 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 4449 . . . . . . . . . . 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 5235 . . . . . . . . . . . 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 2414 . . . . . . . . . 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 22168 . . . . . . . . . . . . . . . . . 18  |-  ( f  e.  dom  S.1  ->  f : RR --> RR )
2928ffvelrnda 5933 . . . . . . . . . . . . . . . . 17  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( f `  t )  e.  RR )
3029recnd 9533 . . . . . . . . . . . . . . . 16  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( f `  t )  e.  CC )
31 ax-icn 9462 . . . . . . . . . . . . . . . . 17  |-  _i  e.  CC
32 i1ff 22168 . . . . . . . . . . . . . . . . . . 19  |-  ( g  e.  dom  S.1  ->  g : RR --> RR )
3332ffvelrnda 5933 . . . . . . . . . . . . . . . . . 18  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  e.  RR )
3433recnd 9533 . . . . . . . . . . . . . . . . 17  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  e.  CC )
35 mulcl 9487 . . . . . . . . . . . . . . . . 17  |-  ( ( _i  e.  CC  /\  ( g `  t
)  e.  CC )  ->  ( _i  x.  ( g `  t
) )  e.  CC )
3631, 34, 35sylancr 661 . . . . . . . . . . . . . . . 16  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( _i  x.  ( g `  t
) )  e.  CC )
37 addcl 9485 . . . . . . . . . . . . . . . 16  |-  ( ( ( f `  t
)  e.  CC  /\  ( _i  x.  (
g `  t )
)  e.  CC )  ->  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) )  e.  CC )
3830, 36, 37syl2an 475 . . . . . . . . . . . . . . 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 829 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) )  e.  CC )
40 reex 9494 . . . . . . . . . . . . . . . 16  |-  RR  e.  _V
4140a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  RR  e.  _V )
4229adantlr 712 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
f `  t )  e.  RR )
4336adantll 711 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
_i  x.  ( g `  t ) )  e.  CC )
4428feqmptd 5827 . . . . . . . . . . . . . . . 16  |-  ( f  e.  dom  S.1  ->  f  =  ( t  e.  RR  |->  ( f `  t ) ) )
4544adantr 463 . . . . . . . . . . . . . . 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 4957 . . . . . . . . . . . . . . . . . 18  |-  ( RR 
X.  { _i }
)  =  ( t  e.  RR  |->  _i )
4948a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( g  e.  dom  S.1  ->  ( RR  X.  { _i } )  =  ( t  e.  RR  |->  _i ) )
5032feqmptd 5827 . . . . . . . . . . . . . . . . 17  |-  ( g  e.  dom  S.1  ->  g  =  ( t  e.  RR  |->  ( g `  t ) ) )
5146, 47, 33, 49, 50offval2 6455 . . . . . . . . . . . . . . . 16  |-  ( g  e.  dom  S.1  ->  ( ( RR  X.  {
_i } )  oF  x.  g )  =  ( t  e.  RR  |->  ( _i  x.  ( g `  t
) ) ) )
5251adantl 464 . . . . . . . . . . . . . . 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 6455 . . . . . . . . . . . . . 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 13172 . . . . . . . . . . . . . . . 16  |-  abs : CC
--> RR
5554a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  abs : CC --> RR )
5655feqmptd 5827 . . . . . . . . . . . . . 14  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  abs  =  (
x  e.  CC  |->  ( abs `  x ) ) )
57 fveq2 5774 . . . . . . . . . . . . . 14  |-  ( x  =  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) )  ->  ( abs `  x )  =  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
5839, 53, 56, 57fmptco 5966 . . . . . . . . . . . . 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 30258 . . . . . . . . . . . . 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 2471 . . . . . . . . . . . 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 22167 . . . . . . . . . . . 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 22060 . . . . . . . . . . 11  |-  ( u (,) w )  e. 
dom  vol
64 mbfres 22136 . . . . . . . . . . 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 660 . . . . . . . . . 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 2474 . . . . . . . . 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 464 . . . . . . . 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 22138 . . . . . . 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 463 . . . . . 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 13269 . . . . . . . . . 10  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  e.  RR )
7139absge0d 13277 . . . . . . . . . 10  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  0  <_  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
72 elrege0 11548 . . . . . . . . . 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 662 . . . . . . . . 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 11551 . . . . . . . . 9  |-  0  e.  ( 0 [,) +oo )
75 ifcl 3899 . . . . . . . . 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 660 . . . . . . . 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 2382 . . . . . . . 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 5957 . . . . . . 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 724 . . . . . 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 9554 . . . . . . . . . . 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 11550 . . . . . . . . . . 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 662 . . . . . . . . . 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 11552 . . . . . . . . . 10  |-  0  e.  ( 0 [,] +oo )
84 ifcl 3899 . . . . . . . . . 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 660 . . . . . . . . 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 5957 . . . . . . . 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 724 . . . . . . 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 3899 . . . . . . . . . . 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 660 . . . . . . . . . 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 2382 . . . . . . . . . 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 5957 . . . . . . . . 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 5639 . . . . . . . . . . . . . . 15  |-  ( f : RR --> RR  ->  f  Fn  RR )
93 frn 5645 . . . . . . . . . . . . . . . 16  |-  ( f : RR --> RR  ->  ran  f  C_  RR )
94 ax-resscn 9460 . . . . . . . . . . . . . . . 16  |-  RR  C_  CC
9593, 94syl6ss 3429 . . . . . . . . . . . . . . 15  |-  ( f : RR --> RR  ->  ran  f  C_  CC )
96 ffn 5639 . . . . . . . . . . . . . . . . 17  |-  ( abs
: CC --> RR  ->  abs 
Fn  CC )
9754, 96ax-mp 5 . . . . . . . . . . . . . . . 16  |-  abs  Fn  CC
98 fnco 5597 . . . . . . . . . . . . . . . 16  |-  ( ( abs  Fn  CC  /\  f  Fn  RR  /\  ran  f  C_  CC )  -> 
( abs  o.  f
)  Fn  RR )
9997, 98mp3an1 1309 . . . . . . . . . . . . . . 15  |-  ( ( f  Fn  RR  /\  ran  f  C_  CC )  ->  ( abs  o.  f )  Fn  RR )
10092, 95, 99syl2anc 659 . . . . . . . . . . . . . 14  |-  ( f : RR --> RR  ->  ( abs  o.  f )  Fn  RR )
10128, 100syl 16 . . . . . . . . . . . . 13  |-  ( f  e.  dom  S.1  ->  ( abs  o.  f )  Fn  RR )
102101adantr 463 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  f )  Fn  RR )
103 ffn 5639 . . . . . . . . . . . . . . 15  |-  ( g : RR --> RR  ->  g  Fn  RR )
104 frn 5645 . . . . . . . . . . . . . . . 16  |-  ( g : RR --> RR  ->  ran  g  C_  RR )
105104, 94syl6ss 3429 . . . . . . . . . . . . . . 15  |-  ( g : RR --> RR  ->  ran  g  C_  CC )
106 fnco 5597 . . . . . . . . . . . . . . . 16  |-  ( ( abs  Fn  CC  /\  g  Fn  RR  /\  ran  g  C_  CC )  -> 
( abs  o.  g
)  Fn  RR )
10797, 106mp3an1 1309 . . . . . . . . . . . . . . 15  |-  ( ( g  Fn  RR  /\  ran  g  C_  CC )  ->  ( abs  o.  g )  Fn  RR )
108103, 105, 107syl2anc 659 . . . . . . . . . . . . . 14  |-  ( g : RR --> RR  ->  ( abs  o.  g )  Fn  RR )
10932, 108syl 16 . . . . . . . . . . . . 13  |-  ( g  e.  dom  S.1  ->  ( abs  o.  g )  Fn  RR )
110109adantl 464 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  g )  Fn  RR )
111 inidm 3621 . . . . . . . . . . . 12  |-  ( RR 
i^i  RR )  =  RR
11228adantr 463 . . . . . . . . . . . . 13  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  f : RR --> RR )
113 fvco3 5851 . . . . . . . . . . . . 13  |-  ( ( f : RR --> RR  /\  t  e.  RR )  ->  ( ( abs  o.  f ) `  t
)  =  ( abs `  ( f `  t
) ) )
114112, 113sylan 469 . . . . . . . . . . . 12  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( abs  o.  f
) `  t )  =  ( abs `  (
f `  t )
) )
11532adantl 464 . . . . . . . . . . . . 13  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  g : RR --> RR )
116 fvco3 5851 . . . . . . . . . . . . 13  |-  ( ( g : RR --> RR  /\  t  e.  RR )  ->  ( ( abs  o.  g ) `  t
)  =  ( abs `  ( g `  t
) ) )
117115, 116sylan 469 . . . . . . . . . . . 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 6446 . . . . . . . . . . 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 9691 . . . . . . . . . . . . . . . . 17  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( ( f `
 t )  +  0 )  =  ( f `  t ) )
120119mpteq2dva 4453 . . . . . . . . . . . . . . . 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 4957 . . . . . . . . . . . . . . . . . . . 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 6455 . . . . . . . . . . . . . . . . . 18  |-  ( f  e.  dom  S.1  ->  ( ( RR  X.  {
_i } )  oF  x.  ( RR 
X.  { 0 } ) )  =  ( t  e.  RR  |->  ( _i  x.  0 ) ) )
128 it0e0 10678 . . . . . . . . . . . . . . . . . . 19  |-  ( _i  x.  0 )  =  0
129128mpteq2i 4450 . . . . . . . . . . . . . . . . . 18  |-  ( t  e.  RR  |->  ( _i  x.  0 ) )  =  ( t  e.  RR  |->  0 )
130127, 129syl6eq 2439 . . . . . . . . . . . . . . . . 17  |-  ( f  e.  dom  S.1  ->  ( ( RR  X.  {
_i } )  oF  x.  ( RR 
X.  { 0 } ) )  =  ( t  e.  RR  |->  0 ) )
131121, 29, 122, 44, 130offval2 6455 . . . . . . . . . . . . . . . 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 2433 . . . . . . . . . . . . . . 15  |-  ( f  e.  dom  S.1  ->  ( f  oF  +  ( ( RR  X.  { _i } )  oF  x.  ( RR 
X.  { 0 } ) ) )  =  f )
133132coeq2d 5078 . . . . . . . . . . . . . 14  |-  ( f  e.  dom  S.1  ->  ( abs  o.  ( f  oF  +  ( ( RR  X.  {
_i } )  oF  x.  ( RR 
X.  { 0 } ) ) ) )  =  ( abs  o.  f ) )
134 i1f0 22179 . . . . . . . . . . . . . . 15  |-  ( RR 
X.  { 0 } )  e.  dom  S.1
135 ftc1anclem3 30258 . . . . . . . . . . . . . . 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 669 . . . . . . . . . . . . . 14  |-  ( f  e.  dom  S.1  ->  ( abs  o.  ( f  oF  +  ( ( RR  X.  {
_i } )  oF  x.  ( RR 
X.  { 0 } ) ) ) )  e.  dom  S.1 )
137133, 136eqeltrrd 2471 . . . . . . . . . . . . 13  |-  ( f  e.  dom  S.1  ->  ( abs  o.  f )  e.  dom  S.1 )
138137adantr 463 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  f )  e.  dom  S.1 )
139 coeq2 5074 . . . . . . . . . . . . . . 15  |-  ( f  =  g  ->  ( abs  o.  f )  =  ( abs  o.  g
) )
140139eleq1d 2451 . . . . . . . . . . . . . 14  |-  ( f  =  g  ->  (
( abs  o.  f
)  e.  dom  S.1  <->  ( abs  o.  g )  e. 
dom  S.1 ) )
141140, 137vtoclga 3098 . . . . . . . . . . . . 13  |-  ( g  e.  dom  S.1  ->  ( abs  o.  g )  e.  dom  S.1 )
142141adantl 464 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  g )  e.  dom  S.1 )
143138, 142i1fadd 22187 . . . . . . . . . . 11  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( ( abs 
o.  f )  oF  +  ( abs 
o.  g ) )  e.  dom  S.1 )
144118, 143eqeltrrd 2471 . . . . . . . . . 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 13269 . . . . . . . . . . . . . . . 16  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
f `  t )
)  e.  RR )
14630absge0d 13277 . . . . . . . . . . . . . . . 16  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  0  <_  ( abs `  ( f `  t ) ) )
147 elrege0 11548 . . . . . . . . . . . . . . . 16  |-  ( ( abs `  ( f `
 t ) )  e.  ( 0 [,) +oo )  <->  ( ( abs `  ( f `  t
) )  e.  RR  /\  0  <_  ( abs `  ( f `  t
) ) ) )
148145, 146, 147sylanbrc 662 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
f `  t )
)  e.  ( 0 [,) +oo ) )
14934abscld 13269 . . . . . . . . . . . . . . . 16  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
g `  t )
)  e.  RR )
15034absge0d 13277 . . . . . . . . . . . . . . . 16  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  0  <_  ( abs `  ( g `  t ) ) )
151 elrege0 11548 . . . . . . . . . . . . . . . 16  |-  ( ( abs `  ( g `
 t ) )  e.  ( 0 [,) +oo )  <->  ( ( abs `  ( g `  t
) )  e.  RR  /\  0  <_  ( abs `  ( g `  t
) ) ) )
152149, 150, 151sylanbrc 662 . . . . . . . . . . . . . . 15  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
g `  t )
)  e.  ( 0 [,) +oo ) )
153 ge0addcl 11553 . . . . . . . . . . . . . . 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 475 . . . . . . . . . . . . . 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 829 . . . . . . . . . . . . 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 2382 . . . . . . . . . . . . 13  |-  ( t  e.  RR  |->  ( ( abs `  ( f `
 t ) )  +  ( abs `  (
g `  t )
) ) )  =  ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) )
157155, 156fmptd 5957 . . . . . . . . . . . 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 22164 . . . . . . . . . . . 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 461 . . . . . . . . . 10  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  0p  oR  <_  ( t  e.  RR  |->  ( ( abs `  ( f `  t
) )  +  ( abs `  ( g `
 t ) ) ) ) )
161 itg2itg1 22228 . . . . . . . . . . 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 22177 . . . . . . . . . . . 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 463 . . . . . . . . . . 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 2470 . . . . . . . . . 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 659 . . . . . . . . 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 11532 . . . . . . . . . . 11  |-  ( 0 [,) +oo )  C_  ( 0 [,] +oo )
167 fss 5647 . . . . . . . . . . 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 660 . . . . . . . . . 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 9507 . . . . . . . . . . . . . 14  |-  0  e.  RR
170 ifcl 3899 . . . . . . . . . . . . . 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 660 . . . . . . . . . . . . 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 9486 . . . . . . . . . . . . . . 15  |-  ( ( ( abs `  (
f `  t )
)  e.  RR  /\  ( abs `  ( g `
 t ) )  e.  RR )  -> 
( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) )  e.  RR )
173145, 149, 172syl2an 475 . . . . . . . . . . . . . 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 829 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) )  e.  RR )
17570leidd 10036 . . . . . . . . . . . . . 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 4370 . . . . . . . . . . . . . . 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 4370 . . . . . . . . . . . . . . 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 3893 . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . 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 13165 . . . . . . . . . . . . . . . 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 475 . . . . . . . . . . . . . . 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 829 . . . . . . . . . . . . . 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 13129 . . . . . . . . . . . . . . . . . . 19  |-  ( ( _i  e.  CC  /\  ( g `  t
)  e.  CC )  ->  ( abs `  (
_i  x.  ( g `  t ) ) )  =  ( ( abs `  _i )  x.  ( abs `  ( g `  t ) ) ) )
18431, 34, 183sylancr 661 . . . . . . . . . . . . . . . . . 18  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
_i  x.  ( g `  t ) ) )  =  ( ( abs `  _i )  x.  ( abs `  ( g `  t ) ) ) )
185 absi 13121 . . . . . . . . . . . . . . . . . . 19  |-  ( abs `  _i )  =  1
186185oveq1i 6206 . . . . . . . . . . . . . . . . . 18  |-  ( ( abs `  _i )  x.  ( abs `  (
g `  t )
) )  =  ( 1  x.  ( abs `  ( g `  t
) ) )
187184, 186syl6eq 2439 . . . . . . . . . . . . . . . . 17  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
_i  x.  ( g `  t ) ) )  =  ( 1  x.  ( abs `  (
g `  t )
) ) )
188149recnd 9533 . . . . . . . . . . . . . . . . . 18  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
g `  t )
)  e.  CC )
189188mulid2d 9525 . . . . . . . . . . . . . . . . 17  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( 1  x.  ( abs `  (
g `  t )
) )  =  ( abs `  ( g `
 t ) ) )
190187, 189eqtrd 2423 . . . . . . . . . . . . . . . 16  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
_i  x.  ( g `  t ) ) )  =  ( abs `  (
g `  t )
) )
191190adantll 711 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( _i  x.  ( g `  t
) ) )  =  ( abs `  (
g `  t )
) )
192191oveq2d 6212 . . . . . . . . . . . . . 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 4391 . . . . . . . . . . . . 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 9650 . . . . . . . . . . . 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 2796 . . . . . . . . . . 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 2383 . . . . . . . . . . . 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 2383 . . . . . . . . . . . 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 6456 . . . . . . . . . . 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 22231 . . . . . . . . . 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 1226 . . . . . . . . 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 22230 . . . . . . . . 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 1226 . . . . . . . 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 724 . . . . . . 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 724 . . . . . . . 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 4370 . . . . . . . . . . 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 4370 . . . . . . . . . . 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 11480 . . . . . . . . . . . . . . 15  |-  ( t  e.  ( u (,) w )  ->  t  e.  RR )
209208, 175sylan2 472 . . . . . . . . . . . . . 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 711 . . . . . . . . . . . . 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 712 . . . . . . . . . . . 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 9554 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A  e.  RR* )
2133rexrd 9554 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  B  e.  RR* )
214212, 213jca 530 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( A  e.  RR*  /\  B  e.  RR* )
)
215 df-icc 11457 . . . . . . . . . . . . . . . . . . . . 21  |-  [,]  =  ( x  e.  RR* ,  y  e.  RR*  |->  { t  e.  RR*  |  (
x  <_  t  /\  t  <_  y ) } )
216215elixx3g 11463 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  e.  ( A [,] B )  <->  ( ( A  e.  RR*  /\  B  e.  RR*  /\  u  e. 
RR* )  /\  ( A  <_  u  /\  u  <_  B ) ) )
217216simprbi 462 . . . . . . . . . . . . . . . . . . 19  |-  ( u  e.  ( A [,] B )  ->  ( A  <_  u  /\  u  <_  B ) )
218217simpld 457 . . . . . . . . . . . . . . . . . 18  |-  ( u  e.  ( A [,] B )  ->  A  <_  u )
219215elixx3g 11463 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  e.  ( A [,] B )  <->  ( ( A  e.  RR*  /\  B  e.  RR*  /\  w  e. 
RR* )  /\  ( A  <_  w  /\  w  <_  B ) ) )
220219simprbi 462 . . . . . . . . . . . . . . . . . . 19  |-  ( w  e.  ( A [,] B )  ->  ( A  <_  w  /\  w  <_  B ) )
221220simprd 461 . . . . . . . . . . . . . . . . . 18  |-  ( w  e.  ( A [,] B )  ->  w  <_  B )
222218, 221anim12i 564 . . . . . . . . . . . . . . . . 17  |-  ( ( u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) )  -> 
( A  <_  u  /\  w  <_  B ) )
223 ioossioo 11537 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <_  u  /\  w  <_  B ) )  ->  ( u (,) w )  C_  ( A (,) B ) )
224214, 222, 223syl2an 475 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  (
u (,) w ) 
C_  ( A (,) B ) )
2255adantr 463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  ( A (,) B )  C_  D )
226224, 225sstrd 3427 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  (
u (,) w ) 
C_  D )
227226sselda 3417 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  t  e.  D )
228 iftrue 3863 . . . . . . . . . . . . . 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 716 . . . . . . . . . . . 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 4393 . . . . . . . . . . 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 4371 . . . . . . . . . . . . 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 4371 . . . . . . . . . . . . 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 3417 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  D )  ->  t  e.  RR )
235234adantlr 712 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  D )  ->  t  e.  RR )
23671adantll 711 . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . 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 10542 . . . . . . . . . . . . . 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 3892 . . . . . . . . . . . 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 723 . . . . . . . . . . 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 3892 . . . . . . . . . 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 2797 . . . . . . . . 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 3925 . . . . . . . . . . . 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 2383 . . . . . . . . . . 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 2383 . . . . . . . . . . 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 6456 . . . . . . . . . 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 723 . . . . . . . . 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 22231 . . . . . . . 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 1226 . . . . . . 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 22230 . . . . . . 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 1226 . . . . . 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 5933 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  D )  ->  ( F `  t )  e.  CC )
258257adantlr 712 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  D
)  ->  ( F `  t )  e.  CC )
259227, 258syldan 468 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  ( F `  t )  e.  CC )
260259adantllr 716 . . . . . . . . . . . 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 472 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  ( u (,) w
) )  ->  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) )  e.  CC )
262261adantll 711 . . . . . . . . . . . . 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 712 . . . . . . . . . . . 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 9844 . . . . . . . . . . 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 13269 . . . . . . . . . 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 13277 . . . . . . . . . 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 11548 . . . . . . . . . 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 662 . . . . . . . . 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 3889 . . . . . . . 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 463 . . . . . . 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 2382 . . . . . . 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 5957 . . . . . 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 9554 . . . . . . . . . . 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 11550 . . . . . . . . . . 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 662 . . . . . . . . . 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 3889 . . . . . . . . 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 463 . . . . . . . 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 5957 . . . . . . 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 21491 . . . . . . . . . . . . 13  |-  Re  e.  ( CC -cn-> RR )
282 prid1g 4050 . . . . . . . . . . . . 13  |-  ( Re  e.  ( CC -cn-> RR )  ->  Re  e.  { Re ,  Im }
)
283281, 282ax-mp 5 . . . . . . . . . . . 12  |-  Re  e.  { Re ,  Im }
284 ftc1anclem2 30257 . . . . . . . . . . . 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 1311 . . . . . . . . . . 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 659 . . . . . . . . . 10  |-  ( ph  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
Re `  ( F `  t ) ) ) ,  0 ) ) )  e.  RR )
287 imcncf 21492 . . . . . . . . . . . . 13  |-  Im  e.  ( CC -cn-> RR )
288 prid2g 4051 . . . . . . . . . . . . 13  |-  ( Im  e.  ( CC -cn-> RR )  ->  Im  e.  { Re ,  Im }
)
289287, 288ax-mp 5 . . . . . . . . . . . 12  |-  Im  e.  { Re ,  Im }
290 ftc1anclem2 30257 . . . . . . . . . . . 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 1311 . . . . . . . . . . 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 659 . . . . . . . . . 10  |-  ( ph  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
Im `  ( F `  t ) ) ) ,  0 ) ) )  e.  RR )
293286, 292readdcld 9534 . . . . . . . . 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 723 . . . . . . . 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 9534 . . . . . . 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 11553 . . . . . . . . . . . . 13  |-  ( ( x  e.  ( 0 [,) +oo )  /\  y  e.  ( 0 [,) +oo ) )  ->  ( x  +  y )  e.  ( 0 [,) +oo )
)
297296adantl 464 . . . . . . . . . . . 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 3899 . . . . . . . . . . . . . . 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 660 . . . . . . . . . . . . . 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 5957 . . . . . . . . . . . . 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 464 . . . . . . . . . . . 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 464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  ( 0 [,) +oo )  /\  y  e.  ( 0 [,) +oo )
) )  ->  (
x  +  y )  e.  ( 0 [,) +oo ) )
303257recld 13029 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  D )  ->  (
Re `  ( F `  t ) )  e.  RR )
304303recnd 9533 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  D )  ->  (
Re `  ( F `  t ) )  e.  CC )
305304abscld 13269 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  D )  ->  ( abs `  ( Re `  ( F `  t ) ) )  e.  RR )
306304absge0d 13277 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  D )  ->  0  <_  ( abs `  (
Re `  ( F `  t ) ) ) )
307 elrege0 11548 . . . . . . . . . . . . . . . . . 18  |-  ( ( abs `  ( Re
`  ( F `  t ) ) )  e.  ( 0 [,) +oo )  <->  ( ( abs `  ( Re `  ( F `  t )
) )  e.  RR  /\  0  <_  ( abs `  ( Re `  ( F `  t )
) ) ) )
308305, 306, 307sylanbrc 662 . . . . . . . . . . . . . . . . 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 3889 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  if ( t  e.  D ,  ( abs `  ( Re `  ( F `  t )
) ) ,  0 )  e.  ( 0 [,) +oo ) )
311310adantr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  RR )  ->  if