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

Theorem ftc1anclem8 31931
Description: Lemma for ftc1anc 31932. (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 31930 . 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 766 . . . 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 1002 . . . 4  |-  ( ( u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w )  ->  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )
12 ioossre 11647 . . . . . . . . 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 22436 . . . . . . . . 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 5835 . . . . . . . . . 10  |-  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) )  e.  _V
17 c0ex 9588 . . . . . . . . . 10  |-  0  e.  _V
1816, 17ifex 3922 . . . . . . . . 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 3531 . . . . . . . . . 10  |-  ( t  e.  ( RR  \ 
( u (,) w
) )  ->  -.  t  e.  ( u (,) w ) )
2120adantl 467 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  ( RR  \  (
u (,) w ) ) )  ->  -.  t  e.  ( u (,) w ) )
2221iffalsed 3865 . . . . . . . 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 3860 . . . . . . . . . . . 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 5116 . . . . . . . . . . . 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 2453 . . . . . . . . . 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 22576 . . . . . . . . . . . . . . . . . 18  |-  ( f  e.  dom  S.1  ->  f : RR --> RR )
2928ffvelrnda 5981 . . . . . . . . . . . . . . . . 17  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( f `  t )  e.  RR )
3029recnd 9620 . . . . . . . . . . . . . . . 16  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( f `  t )  e.  CC )
31 ax-icn 9549 . . . . . . . . . . . . . . . . 17  |-  _i  e.  CC
32 i1ff 22576 . . . . . . . . . . . . . . . . . . 19  |-  ( g  e.  dom  S.1  ->  g : RR --> RR )
3332ffvelrnda 5981 . . . . . . . . . . . . . . . . . 18  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  e.  RR )
3433recnd 9620 . . . . . . . . . . . . . . . . 17  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  e.  CC )
35 mulcl 9574 . . . . . . . . . . . . . . . . 17  |-  ( ( _i  e.  CC  /\  ( g `  t
)  e.  CC )  ->  ( _i  x.  ( g `  t
) )  e.  CC )
3631, 34, 35sylancr 667 . . . . . . . . . . . . . . . 16  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( _i  x.  ( g `  t
) )  e.  CC )
37 addcl 9572 . . . . . . . . . . . . . . . 16  |-  ( ( ( f `  t
)  e.  CC  /\  ( _i  x.  (
g `  t )
)  e.  CC )  ->  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) )  e.  CC )
3830, 36, 37syl2an 479 . . . . . . . . . . . . . . 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 838 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) )  e.  CC )
40 reex 9581 . . . . . . . . . . . . . . . 16  |-  RR  e.  _V
4140a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  RR  e.  _V )
4229adantlr 719 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
f `  t )  e.  RR )
4336adantll 718 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
_i  x.  ( g `  t ) )  e.  CC )
4428feqmptd 5878 . . . . . . . . . . . . . . . 16  |-  ( f  e.  dom  S.1  ->  f  =  ( t  e.  RR  |->  ( f `  t ) ) )
4544adantr 466 . . . . . . . . . . . . . . 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 4840 . . . . . . . . . . . . . . . . . 18  |-  ( RR 
X.  { _i }
)  =  ( t  e.  RR  |->  _i )
4948a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( g  e.  dom  S.1  ->  ( RR  X.  { _i } )  =  ( t  e.  RR  |->  _i ) )
5032feqmptd 5878 . . . . . . . . . . . . . . . . 17  |-  ( g  e.  dom  S.1  ->  g  =  ( t  e.  RR  |->  ( g `  t ) ) )
5146, 47, 33, 49, 50offval2 6506 . . . . . . . . . . . . . . . 16  |-  ( g  e.  dom  S.1  ->  ( ( RR  X.  {
_i } )  oF  x.  g )  =  ( t  e.  RR  |->  ( _i  x.  ( g `  t
) ) ) )
5251adantl 467 . . . . . . . . . . . . . . 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 6506 . . . . . . . . . . . . . 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 13344 . . . . . . . . . . . . . . . 16  |-  abs : CC
--> RR
5554a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  abs : CC --> RR )
5655feqmptd 5878 . . . . . . . . . . . . . 14  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  abs  =  (
x  e.  CC  |->  ( abs `  x ) ) )
57 fveq2 5825 . . . . . . . . . . . . . 14  |-  ( x  =  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) )  ->  ( abs `  x )  =  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
5839, 53, 56, 57fmptco 6015 . . . . . . . . . . . . 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 31926 . . . . . . . . . . . . 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 2507 . . . . . . . . . . . 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 22575 . . . . . . . . . . . 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 17 . . . . . . . . . . 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 22460 . . . . . . . . . . 11  |-  ( u (,) w )  e. 
dom  vol
64 mbfres 22542 . . . . . . . . . . 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 666 . . . . . . . . . 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 2510 . . . . . . . . 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 467 . . . . . . . 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 22544 . . . . . . 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 466 . . . . . 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 13441 . . . . . . . . . 10  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  e.  RR )
7139absge0d 13449 . . . . . . . . . 10  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  0  <_  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
72 elrege0 11689 . . . . . . . . . 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 668 . . . . . . . . 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 11693 . . . . . . . . 9  |-  0  e.  ( 0 [,) +oo )
75 ifcl 3896 . . . . . . . . 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 666 . . . . . . . 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 2428 . . . . . . . 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 6005 . . . . . . 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 731 . . . . . 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 9641 . . . . . . . . . . 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 11692 . . . . . . . . . . 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 668 . . . . . . . . . 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 11694 . . . . . . . . . 10  |-  0  e.  ( 0 [,] +oo )
84 ifcl 3896 . . . . . . . . . 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 666 . . . . . . . . 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 6005 . . . . . . . 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 731 . . . . . . 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 3896 . . . . . . . . . . 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 666 . . . . . . . . . 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 2428 . . . . . . . . . 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 6005 . . . . . . . . 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 5689 . . . . . . . . . . . . . . 15  |-  ( f : RR --> RR  ->  f  Fn  RR )
93 frn 5695 . . . . . . . . . . . . . . . 16  |-  ( f : RR --> RR  ->  ran  f  C_  RR )
94 ax-resscn 9547 . . . . . . . . . . . . . . . 16  |-  RR  C_  CC
9593, 94syl6ss 3419 . . . . . . . . . . . . . . 15  |-  ( f : RR --> RR  ->  ran  f  C_  CC )
96 ffn 5689 . . . . . . . . . . . . . . . . 17  |-  ( abs
: CC --> RR  ->  abs 
Fn  CC )
9754, 96ax-mp 5 . . . . . . . . . . . . . . . 16  |-  abs  Fn  CC
98 fnco 5645 . . . . . . . . . . . . . . . 16  |-  ( ( abs  Fn  CC  /\  f  Fn  RR  /\  ran  f  C_  CC )  -> 
( abs  o.  f
)  Fn  RR )
9997, 98mp3an1 1347 . . . . . . . . . . . . . . 15  |-  ( ( f  Fn  RR  /\  ran  f  C_  CC )  ->  ( abs  o.  f )  Fn  RR )
10092, 95, 99syl2anc 665 . . . . . . . . . . . . . 14  |-  ( f : RR --> RR  ->  ( abs  o.  f )  Fn  RR )
10128, 100syl 17 . . . . . . . . . . . . 13  |-  ( f  e.  dom  S.1  ->  ( abs  o.  f )  Fn  RR )
102101adantr 466 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  f )  Fn  RR )
103 ffn 5689 . . . . . . . . . . . . . . 15  |-  ( g : RR --> RR  ->  g  Fn  RR )
104 frn 5695 . . . . . . . . . . . . . . . 16  |-  ( g : RR --> RR  ->  ran  g  C_  RR )
105104, 94syl6ss 3419 . . . . . . . . . . . . . . 15  |-  ( g : RR --> RR  ->  ran  g  C_  CC )
106 fnco 5645 . . . . . . . . . . . . . . . 16  |-  ( ( abs  Fn  CC  /\  g  Fn  RR  /\  ran  g  C_  CC )  -> 
( abs  o.  g
)  Fn  RR )
10797, 106mp3an1 1347 . . . . . . . . . . . . . . 15  |-  ( ( g  Fn  RR  /\  ran  g  C_  CC )  ->  ( abs  o.  g )  Fn  RR )
108103, 105, 107syl2anc 665 . . . . . . . . . . . . . 14  |-  ( g : RR --> RR  ->  ( abs  o.  g )  Fn  RR )
10932, 108syl 17 . . . . . . . . . . . . 13  |-  ( g  e.  dom  S.1  ->  ( abs  o.  g )  Fn  RR )
110109adantl 467 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  g )  Fn  RR )
111 inidm 3614 . . . . . . . . . . . 12  |-  ( RR 
i^i  RR )  =  RR
11228adantr 466 . . . . . . . . . . . . 13  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  f : RR --> RR )
113 fvco3 5902 . . . . . . . . . . . . 13  |-  ( ( f : RR --> RR  /\  t  e.  RR )  ->  ( ( abs  o.  f ) `  t
)  =  ( abs `  ( f `  t
) ) )
114112, 113sylan 473 . . . . . . . . . . . 12  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( abs  o.  f
) `  t )  =  ( abs `  (
f `  t )
) )
11532adantl 467 . . . . . . . . . . . . 13  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  g : RR --> RR )
116 fvco3 5902 . . . . . . . . . . . . 13  |-  ( ( g : RR --> RR  /\  t  e.  RR )  ->  ( ( abs  o.  g ) `  t
)  =  ( abs `  ( g `  t
) ) )
117115, 116sylan 473 . . . . . . . . . . . 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 6496 . . . . . . . . . . 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 9784 . . . . . . . . . . . . . . . . 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 4840 . . . . . . . . . . . . . . . . . . . 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 6506 . . . . . . . . . . . . . . . . . 18  |-  ( f  e.  dom  S.1  ->  ( ( RR  X.  {
_i } )  oF  x.  ( RR 
X.  { 0 } ) )  =  ( t  e.  RR  |->  ( _i  x.  0 ) ) )
128 it0e0 10786 . . . . . . . . . . . . . . . . . . 19  |-  ( _i  x.  0 )  =  0
129128mpteq2i 4450 . . . . . . . . . . . . . . . . . 18  |-  ( t  e.  RR  |->  ( _i  x.  0 ) )  =  ( t  e.  RR  |->  0 )
130127, 129syl6eq 2478 . . . . . . . . . . . . . . . . 17  |-  ( f  e.  dom  S.1  ->  ( ( RR  X.  {
_i } )  oF  x.  ( RR 
X.  { 0 } ) )  =  ( t  e.  RR  |->  0 ) )
131121, 29, 122, 44, 130offval2 6506 . . . . . . . . . . . . . . . 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 2472 . . . . . . . . . . . . . . 15  |-  ( f  e.  dom  S.1  ->  ( f  oF  +  ( ( RR  X.  { _i } )  oF  x.  ( RR 
X.  { 0 } ) ) )  =  f )
133132coeq2d 4959 . . . . . . . . . . . . . 14  |-  ( f  e.  dom  S.1  ->  ( abs  o.  ( f  oF  +  ( ( RR  X.  {
_i } )  oF  x.  ( RR 
X.  { 0 } ) ) ) )  =  ( abs  o.  f ) )
134 i1f0 22587 . . . . . . . . . . . . . . 15  |-  ( RR 
X.  { 0 } )  e.  dom  S.1
135 ftc1anclem3 31926 . . . . . . . . . . . . . . 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 675 . . . . . . . . . . . . . 14  |-  ( f  e.  dom  S.1  ->  ( abs  o.  ( f  oF  +  ( ( RR  X.  {
_i } )  oF  x.  ( RR 
X.  { 0 } ) ) ) )  e.  dom  S.1 )
137133, 136eqeltrrd 2507 . . . . . . . . . . . . 13  |-  ( f  e.  dom  S.1  ->  ( abs  o.  f )  e.  dom  S.1 )
138137adantr 466 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  f )  e.  dom  S.1 )
139 coeq2 4955 . . . . . . . . . . . . . . 15  |-  ( f  =  g  ->  ( abs  o.  f )  =  ( abs  o.  g
) )
140139eleq1d 2490 . . . . . . . . . . . . . 14  |-  ( f  =  g  ->  (
( abs  o.  f
)  e.  dom  S.1  <->  ( abs  o.  g )  e. 
dom  S.1 ) )
141140, 137vtoclga 3088 . . . . . . . . . . . . 13  |-  ( g  e.  dom  S.1  ->  ( abs  o.  g )  e.  dom  S.1 )
142141adantl 467 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  g )  e.  dom  S.1 )
143138, 142i1fadd 22595 . . . . . . . . . . 11  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( ( abs 
o.  f )  oF  +  ( abs 
o.  g ) )  e.  dom  S.1 )
144118, 143eqeltrrd 2507 . . . . . . . . . 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 13441 . . . . . . . . . . . . . . . 16  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
f `  t )
)  e.  RR )
14630absge0d 13449 . . . . . . . . . . . . . . . 16  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  0  <_  ( abs `  ( f `  t ) ) )
147 elrege0 11689 . . . . . . . . . . . . . . . 16  |-  ( ( abs `  ( f `
 t ) )  e.  ( 0 [,) +oo )  <->  ( ( abs `  ( f `  t
) )  e.  RR  /\  0  <_  ( abs `  ( f `  t
) ) ) )
148145, 146, 147sylanbrc 668 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
f `  t )
)  e.  ( 0 [,) +oo ) )
14934abscld 13441 . . . . . . . . . . . . . . . 16  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
g `  t )
)  e.  RR )
15034absge0d 13449 . . . . . . . . . . . . . . . 16  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  0  <_  ( abs `  ( g `  t ) ) )
151 elrege0 11689 . . . . . . . . . . . . . . . 16  |-  ( ( abs `  ( g `
 t ) )  e.  ( 0 [,) +oo )  <->  ( ( abs `  ( g `  t
) )  e.  RR  /\  0  <_  ( abs `  ( g `  t
) ) ) )
152149, 150, 151sylanbrc 668 . . . . . . . . . . . . . . 15  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
g `  t )
)  e.  ( 0 [,) +oo ) )
153 ge0addcl 11695 . . . . . . . . . . . . . . 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 479 . . . . . . . . . . . . . 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 838 . . . . . . . . . . . . 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 2428 . . . . . . . . . . . . 13  |-  ( t  e.  RR  |->  ( ( abs `  ( f `
 t ) )  +  ( abs `  (
g `  t )
) ) )  =  ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) )
157155, 156fmptd 6005 . . . . . . . . . . . 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 22572 . . . . . . . . . . . 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 199 . . . . . . . . . . 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 464 . . . . . . . . . 10  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  0p  oR  <_  ( t  e.  RR  |->  ( ( abs `  ( f `  t
) )  +  ( abs `  ( g `
 t ) ) ) ) )
161 itg2itg1 22636 . . . . . . . . . . 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 22585 . . . . . . . . . . . 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 466 . . . . . . . . . . 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 2506 . . . . . . . . . 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 665 . . . . . . . . 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 11672 . . . . . . . . . . 11  |-  ( 0 [,) +oo )  C_  ( 0 [,] +oo )
167 fss 5697 . . . . . . . . . . 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 666 . . . . . . . . . 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 9594 . . . . . . . . . . . . . 14  |-  0  e.  RR
170 ifcl 3896 . . . . . . . . . . . . . 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 666 . . . . . . . . . . . . 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 9573 . . . . . . . . . . . . . . 15  |-  ( ( ( abs `  (
f `  t )
)  e.  RR  /\  ( abs `  ( g `
 t ) )  e.  RR )  -> 
( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) )  e.  RR )
173145, 149, 172syl2an 479 . . . . . . . . . . . . . 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 838 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) )  e.  RR )
17570leidd 10131 . . . . . . . . . . . . . 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 4369 . . . . . . . . . . . . . . 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 4369 . . . . . . . . . . . . . . 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 3890 . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . 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 13337 . . . . . . . . . . . . . . . 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 479 . . . . . . . . . . . . . . 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 838 . . . . . . . . . . . . . 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 13301 . . . . . . . . . . . . . . . . . . 19  |-  ( ( _i  e.  CC  /\  ( g `  t
)  e.  CC )  ->  ( abs `  (
_i  x.  ( g `  t ) ) )  =  ( ( abs `  _i )  x.  ( abs `  ( g `  t ) ) ) )
18431, 34, 183sylancr 667 . . . . . . . . . . . . . . . . . 18  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
_i  x.  ( g `  t ) ) )  =  ( ( abs `  _i )  x.  ( abs `  ( g `  t ) ) ) )
185 absi 13293 . . . . . . . . . . . . . . . . . . 19  |-  ( abs `  _i )  =  1
186185oveq1i 6259 . . . . . . . . . . . . . . . . . 18  |-  ( ( abs `  _i )  x.  ( abs `  (
g `  t )
) )  =  ( 1  x.  ( abs `  ( g `  t
) ) )
187184, 186syl6eq 2478 . . . . . . . . . . . . . . . . 17  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
_i  x.  ( g `  t ) ) )  =  ( 1  x.  ( abs `  (
g `  t )
) ) )
188149recnd 9620 . . . . . . . . . . . . . . . . . 18  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
g `  t )
)  e.  CC )
189188mulid2d 9612 . . . . . . . . . . . . . . . . 17  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( 1  x.  ( abs `  (
g `  t )
) )  =  ( abs `  ( g `
 t ) ) )
190187, 189eqtrd 2462 . . . . . . . . . . . . . . . 16  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
_i  x.  ( g `  t ) ) )  =  ( abs `  (
g `  t )
) )
191190adantll 718 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( _i  x.  ( g `  t
) ) )  =  ( abs `  (
g `  t )
) )
192191oveq2d 6265 . . . . . . . . . . . . . 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 9743 . . . . . . . . . . . 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 2779 . . . . . . . . . . 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 2429 . . . . . . . . . . . 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 2429 . . . . . . . . . . . 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 6507 . . . . . . . . . . 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 235 . . . . . . . . . 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 22639 . . . . . . . . . 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 1264 . . . . . . . . 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 22638 . . . . . . . . 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 1264 . . . . . . . 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 731 . . . . . . 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 731 . . . . . . . 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 4369 . . . . . . . . . . 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 4369 . . . . . . . . . . 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 11617 . . . . . . . . . . . . . . 15  |-  ( t  e.  ( u (,) w )  ->  t  e.  RR )
209208, 175sylan2 476 . . . . . . . . . . . . . 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 718 . . . . . . . . . . . . 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 719 . . . . . . . . . . . 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 9641 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A  e.  RR* )
2133rexrd 9641 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  B  e.  RR* )
214212, 213jca 534 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( A  e.  RR*  /\  B  e.  RR* )
)
215 df-icc 11593 . . . . . . . . . . . . . . . . . . . . 21  |-  [,]  =  ( x  e.  RR* ,  y  e.  RR*  |->  { t  e.  RR*  |  (
x  <_  t  /\  t  <_  y ) } )
216215elixx3g 11599 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  e.  ( A [,] B )  <->  ( ( A  e.  RR*  /\  B  e.  RR*  /\  u  e. 
RR* )  /\  ( A  <_  u  /\  u  <_  B ) ) )
217216simprbi 465 . . . . . . . . . . . . . . . . . . 19  |-  ( u  e.  ( A [,] B )  ->  ( A  <_  u  /\  u  <_  B ) )
218217simpld 460 . . . . . . . . . . . . . . . . . 18  |-  ( u  e.  ( A [,] B )  ->  A  <_  u )
219215elixx3g 11599 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  e.  ( A [,] B )  <->  ( ( A  e.  RR*  /\  B  e.  RR*  /\  w  e. 
RR* )  /\  ( A  <_  w  /\  w  <_  B ) ) )
220219simprbi 465 . . . . . . . . . . . . . . . . . . 19  |-  ( w  e.  ( A [,] B )  ->  ( A  <_  w  /\  w  <_  B ) )
221220simprd 464 . . . . . . . . . . . . . . . . . 18  |-  ( w  e.  ( A [,] B )  ->  w  <_  B )
222218, 221anim12i 568 . . . . . . . . . . . . . . . . 17  |-  ( ( u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) )  -> 
( A  <_  u  /\  w  <_  B ) )
223 ioossioo 11677 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <_  u  /\  w  <_  B ) )  ->  ( u (,) w )  C_  ( A (,) B ) )
224214, 222, 223syl2an 479 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  (
u (,) w ) 
C_  ( A (,) B ) )
2255adantr 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  ( A (,) B )  C_  D )
226224, 225sstrd 3417 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  (
u (,) w ) 
C_  D )
227226sselda 3407 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  t  e.  D )
228 iftrue 3860 . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . 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 723 . . . . . . . . . . . 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 4370 . . . . . . . . . . . . 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 4370 . . . . . . . . . . . . 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 3407 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  D )  ->  t  e.  RR )
235234adantlr 719 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  D )  ->  t  e.  RR )
23671adantll 718 . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . 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 10650 . . . . . . . . . . . . . 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 3889 . . . . . . . . . . . 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 730 . . . . . . . . . . 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 3889 . . . . . . . . . 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 2780 . . . . . . . . 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 3922 . . . . . . . . . . . 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 2429 . . . . . . . . . . 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 2429 . . . . . . . . . . 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 6507 . . . . . . . . . 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 730 . . . . . . . . 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 235 . . . . . . . 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 22639 . . . . . . . 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 1264 . . . . . . 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 22638 . . . . . . 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 1264 . . . . . 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 5981 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  D )  ->  ( F `  t )  e.  CC )
258257adantlr 719 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  D
)  ->  ( F `  t )  e.  CC )
259227, 258syldan 472 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  ( F `  t )  e.  CC )
260259adantllr 723 . . . . . . . . . . . 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 476 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  ( u (,) w
) )  ->  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) )  e.  CC )
262261adantll 718 . . . . . . . . . . . . 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 719 . . . . . . . . . . . 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 9937 . . . . . . . . . . 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 13441 . . . . . . . . . 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 13449 . . . . . . . . . 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 11689 . . . . . . . . . 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 668 . . . . . . . . 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 3886 . . . . . . . 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 466 . . . . . . 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 2428 . . . . . . 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 6005 . . . . . 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 9641 . . . . . . . . . . 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 11692 . . . . . . . . . . 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 668 . . . . . . . . . 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 3886 . . . . . . . . 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 466 . . . . . . . 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 6005 . . . . . . 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 21876 . . . . . . . . . . . . 13  |-  Re  e.  ( CC -cn-> RR )
282 prid1g 4049 . . . . . . . . . . . . 13  |-  ( Re  e.  ( CC -cn-> RR )  ->  Re  e.  { Re ,  Im }
)
283281, 282ax-mp 5 . . . . . . . . . . . 12  |-  Re  e.  { Re ,  Im }
284 ftc1anclem2 31925 . . . . . . . . . . . 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 1349 . . . . . . . . . . 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 665 . . . . . . . . . 10  |-  ( ph  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
Re `  ( F `  t ) ) ) ,  0 ) ) )  e.  RR )
287 imcncf 21877 . . . . . . . . . . . . 13  |-  Im  e.  ( CC -cn-> RR )
288 prid2g 4050 . . . . . . . . . . . . 13  |-  ( Im  e.  ( CC -cn-> RR )  ->  Im  e.  { Re ,  Im }
)
289287, 288ax-mp 5 . . . . . . . . . . . 12  |-  Im  e.  { Re ,  Im }
290 ftc1anclem2 31925 . . . . . . . . . . . 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 1349 . . . . . . . . . . 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 665 . . . . . . . . . 10  |-  ( ph  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
Im `  ( F `  t ) ) ) ,  0 ) ) )  e.  RR )
293286, 292readdcld 9621 . . . . . . . . 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 730 . . . . . . . 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 9621 . . . . . . 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 11695 . . . . . . . . . . . . 13  |-  ( ( x  e.  ( 0 [,) +oo )  /\  y  e.  ( 0 [,) +oo ) )  ->  ( x  +  y )  e.  ( 0 [,) +oo )
)
297296adantl 467 . . . . . . . . . . . 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 3896 . . . . . . . . . . . . . . 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 666 . . . . . . . . . . . . . 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 6005 . . . . . . . . . . . . 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 467 . . . . . . . . . . . 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 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  ( 0 [,) +oo )  /\  y  e.  ( 0 [,) +oo )
) )  ->  (
x  +  y )  e.  ( 0 [,) +oo ) )
303257recld 13201 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  D )  ->  (
Re `  ( F `  t ) )  e.  RR )
304303recnd 9620 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  D )  ->  (
Re `  ( F `  t ) )  e.  CC )
305304abscld 13441 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  D )  ->  ( abs `  ( Re `  ( F `  t ) ) )  e.  RR )
306304absge0d 13449 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  D )  ->  0  <_  ( abs `  (
Re `  ( F `  t ) ) ) )
307 elrege0 11689 . . . . . . . . . . . . . . . . . 18  |-  ( ( abs `  ( Re
`  ( F `  t ) ) )  e.  ( 0 [,) +oo )  <->  ( ( abs `  ( Re `  ( F `  t )
) )  e.  RR  /\  0  <_  ( abs `  ( Re `  ( F `  t )
) ) ) )
308305, 306, 307sylanbrc 668 . . . . . . . . . . . . . . . . 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 3886 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  if ( t  e.  D ,  ( abs `  ( Re `  ( F `  t )
) ) ,  0 )  e.  ( 0 [,) +oo ) )
311310adantr 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  RR )  ->  if ( t  e.