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

Theorem ftc1anclem8 28427
Description: Lemma for ftc1anc 28428. (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
Dummy variable  z is distinct from all other variables.
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 28426 . 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 985 . . . 4  |-  ( ( u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w )  ->  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )
12 ioossre 11349 . . . . . . . . 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 20997 . . . . . . . . 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 5696 . . . . . . . . . 10  |-  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) )  e.  _V
17 c0ex 9372 . . . . . . . . . 10  |-  0  e.  _V
1816, 17ifex 3853 . . . . . . . . 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 3474 . . . . . . . . . 10  |-  ( t  e.  ( RR  \ 
( u (,) w
) )  ->  -.  t  e.  ( u (,) w ) )
2120adantl 466 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  ( RR  \  (
u (,) w ) ) )  ->  -.  t  e.  ( u (,) w ) )
22 iffalse 3794 . . . . . . . . 9  |-  ( -.  t  e.  ( u (,) w )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  =  0 )
2321, 22syl 16 . . . . . . . 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 )
24 iftrue 3792 . . . . . . . . . . . 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 ) ) ) ) )
2524mpteq2ia 4369 . . . . . . . . . . 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 ) ) ) ) )
26 resmpt 5151 . . . . . . . . . . . 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 ) ) ) ) ) )
2712, 26ax-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 ) ) ) ) )
2825, 27eqtr4i 2461 . . . . . . . . . 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 ) )
29 i1ff 21129 . . . . . . . . . . . . . . . . . 18  |-  ( f  e.  dom  S.1  ->  f : RR --> RR )
3029ffvelrnda 5838 . . . . . . . . . . . . . . . . 17  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( f `  t )  e.  RR )
3130recnd 9404 . . . . . . . . . . . . . . . 16  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( f `  t )  e.  CC )
32 ax-icn 9333 . . . . . . . . . . . . . . . . 17  |-  _i  e.  CC
33 i1ff 21129 . . . . . . . . . . . . . . . . . . 19  |-  ( g  e.  dom  S.1  ->  g : RR --> RR )
3433ffvelrnda 5838 . . . . . . . . . . . . . . . . . 18  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  e.  RR )
3534recnd 9404 . . . . . . . . . . . . . . . . 17  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  e.  CC )
36 mulcl 9358 . . . . . . . . . . . . . . . . 17  |-  ( ( _i  e.  CC  /\  ( g `  t
)  e.  CC )  ->  ( _i  x.  ( g `  t
) )  e.  CC )
3732, 35, 36sylancr 663 . . . . . . . . . . . . . . . 16  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( _i  x.  ( g `  t
) )  e.  CC )
38 addcl 9356 . . . . . . . . . . . . . . . 16  |-  ( ( ( f `  t
)  e.  CC  /\  ( _i  x.  (
g `  t )
)  e.  CC )  ->  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) )  e.  CC )
3931, 37, 38syl2an 477 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  dom  S.1 
/\  t  e.  RR )  /\  ( g  e. 
dom  S.1  /\  t  e.  RR ) )  -> 
( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) )  e.  CC )
4039anandirs 827 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) )  e.  CC )
41 reex 9365 . . . . . . . . . . . . . . . 16  |-  RR  e.  _V
4241a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  RR  e.  _V )
4330adantlr 714 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
f `  t )  e.  RR )
4437adantll 713 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
_i  x.  ( g `  t ) )  e.  CC )
4529feqmptd 5739 . . . . . . . . . . . . . . . 16  |-  ( f  e.  dom  S.1  ->  f  =  ( t  e.  RR  |->  ( f `  t ) ) )
4645adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  f  =  ( t  e.  RR  |->  ( f `  t ) ) )
4741a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( g  e.  dom  S.1  ->  RR  e.  _V )
4832a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  _i  e.  CC )
49 fconstmpt 4877 . . . . . . . . . . . . . . . . . 18  |-  ( RR 
X.  { _i }
)  =  ( t  e.  RR  |->  _i )
5049a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( g  e.  dom  S.1  ->  ( RR  X.  { _i } )  =  ( t  e.  RR  |->  _i ) )
5133feqmptd 5739 . . . . . . . . . . . . . . . . 17  |-  ( g  e.  dom  S.1  ->  g  =  ( t  e.  RR  |->  ( g `  t ) ) )
5247, 48, 34, 50, 51offval2 6331 . . . . . . . . . . . . . . . 16  |-  ( g  e.  dom  S.1  ->  ( ( RR  X.  {
_i } )  oF  x.  g )  =  ( t  e.  RR  |->  ( _i  x.  ( g `  t
) ) ) )
5352adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( ( RR 
X.  { _i }
)  oF  x.  g )  =  ( t  e.  RR  |->  ( _i  x.  ( g `
 t ) ) ) )
5442, 43, 44, 46, 53offval2 6331 . . . . . . . . . . . . . 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 )
) ) ) )
55 absf 12817 . . . . . . . . . . . . . . . 16  |-  abs : CC
--> RR
5655a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  abs : CC --> RR )
5756feqmptd 5739 . . . . . . . . . . . . . 14  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  abs  =  (
x  e.  CC  |->  ( abs `  x ) ) )
58 fveq2 5686 . . . . . . . . . . . . . 14  |-  ( x  =  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) )  ->  ( abs `  x )  =  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
5940, 54, 57, 58fmptco 5871 . . . . . . . . . . . . 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 ) ) ) ) ) )
60 ftc1anclem3 28422 . . . . . . . . . . . . 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 )
6159, 60eqeltrrd 2513 . . . . . . . . . . . 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 )
62 i1fmbf 21128 . . . . . . . . . . . 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 )
6361, 62syl 16 . . . . . . . . . . 11  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( t  e.  RR  |->  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  e. MblFn )
64 ioombl 21021 . . . . . . . . . . 11  |-  ( u (,) w )  e. 
dom  vol
65 mbfres 21097 . . . . . . . . . . 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 )
6663, 64, 65sylancl 662 . . . . . . . . . 10  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( ( t  e.  RR  |->  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) )  |`  ( u (,) w
) )  e. MblFn )
6728, 66syl5eqel 2522 . . . . . . . . 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 )
6867adantl 466 . . . . . . . 8  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  -> 
( t  e.  ( u (,) w ) 
|->  if ( t  e.  ( u (,) w
) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ,  0 ) )  e. MblFn )
6913, 15, 19, 23, 68mbfss 21099 . . . . . . 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 )
7069adantr 465 . . . . . 6  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) )  e. MblFn )
7140abscld 12914 . . . . . . . . . 10  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  e.  RR )
7240absge0d 12922 . . . . . . . . . 10  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  0  <_  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
73 elrege0 11384 . . . . . . . . . 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 ) ) ) ) ) )
7471, 72, 73sylanbrc 664 . . . . . . . . 9  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  e.  ( 0 [,) +oo ) )
75 0e0icopnf 11387 . . . . . . . . 9  |-  0  e.  ( 0 [,) +oo )
76 ifcl 3826 . . . . . . . . 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 ) )
7774, 75, 76sylancl 662 . . . . . . . 8  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  e.  ( 0 [,) +oo ) )
78 eqid 2438 . . . . . . . 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 ) )
7977, 78fmptd 5862 . . . . . . 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 ) )
8079ad2antlr 726 . . . . . 6  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) : RR --> ( 0 [,) +oo ) )
8171rexrd 9425 . . . . . . . . . . 11  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  e. 
RR* )
82 elxrge0 11386 . . . . . . . . . . 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 ) ) ) ) ) )
8381, 72, 82sylanbrc 664 . . . . . . . . . 10  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  e.  ( 0 [,] +oo ) )
84 0e0iccpnf 11388 . . . . . . . . . 10  |-  0  e.  ( 0 [,] +oo )
85 ifcl 3826 . . . . . . . . . 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 ) )
8683, 84, 85sylancl 662 . . . . . . . . 9  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  e.  ( 0 [,] +oo ) )
8786, 78fmptd 5862 . . . . . . . 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 ) )
8887ad2antlr 726 . . . . . . 7  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) : RR --> ( 0 [,] +oo ) )
89 ifcl 3826 . . . . . . . . . . 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 ) )
9083, 84, 89sylancl 662 . . . . . . . . . 10  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  e.  ( 0 [,] +oo ) )
91 eqid 2438 . . . . . . . . . 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 ) )
9290, 91fmptd 5862 . . . . . . . . 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 ) )
93 ffn 5554 . . . . . . . . . . . . . . 15  |-  ( f : RR --> RR  ->  f  Fn  RR )
94 frn 5560 . . . . . . . . . . . . . . . 16  |-  ( f : RR --> RR  ->  ran  f  C_  RR )
95 ax-resscn 9331 . . . . . . . . . . . . . . . 16  |-  RR  C_  CC
9694, 95syl6ss 3363 . . . . . . . . . . . . . . 15  |-  ( f : RR --> RR  ->  ran  f  C_  CC )
97 ffn 5554 . . . . . . . . . . . . . . . . 17  |-  ( abs
: CC --> RR  ->  abs 
Fn  CC )
9855, 97ax-mp 5 . . . . . . . . . . . . . . . 16  |-  abs  Fn  CC
99 fnco 5514 . . . . . . . . . . . . . . . 16  |-  ( ( abs  Fn  CC  /\  f  Fn  RR  /\  ran  f  C_  CC )  -> 
( abs  o.  f
)  Fn  RR )
10098, 99mp3an1 1301 . . . . . . . . . . . . . . 15  |-  ( ( f  Fn  RR  /\  ran  f  C_  CC )  ->  ( abs  o.  f )  Fn  RR )
10193, 96, 100syl2anc 661 . . . . . . . . . . . . . 14  |-  ( f : RR --> RR  ->  ( abs  o.  f )  Fn  RR )
10229, 101syl 16 . . . . . . . . . . . . 13  |-  ( f  e.  dom  S.1  ->  ( abs  o.  f )  Fn  RR )
103102adantr 465 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  f )  Fn  RR )
104 ffn 5554 . . . . . . . . . . . . . . 15  |-  ( g : RR --> RR  ->  g  Fn  RR )
105 frn 5560 . . . . . . . . . . . . . . . 16  |-  ( g : RR --> RR  ->  ran  g  C_  RR )
106105, 95syl6ss 3363 . . . . . . . . . . . . . . 15  |-  ( g : RR --> RR  ->  ran  g  C_  CC )
107 fnco 5514 . . . . . . . . . . . . . . . 16  |-  ( ( abs  Fn  CC  /\  g  Fn  RR  /\  ran  g  C_  CC )  -> 
( abs  o.  g
)  Fn  RR )
10898, 107mp3an1 1301 . . . . . . . . . . . . . . 15  |-  ( ( g  Fn  RR  /\  ran  g  C_  CC )  ->  ( abs  o.  g )  Fn  RR )
109104, 106, 108syl2anc 661 . . . . . . . . . . . . . 14  |-  ( g : RR --> RR  ->  ( abs  o.  g )  Fn  RR )
11033, 109syl 16 . . . . . . . . . . . . 13  |-  ( g  e.  dom  S.1  ->  ( abs  o.  g )  Fn  RR )
111110adantl 466 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  g )  Fn  RR )
112 inidm 3554 . . . . . . . . . . . 12  |-  ( RR 
i^i  RR )  =  RR
11329adantr 465 . . . . . . . . . . . . 13  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  f : RR --> RR )
114 fvco3 5763 . . . . . . . . . . . . 13  |-  ( ( f : RR --> RR  /\  t  e.  RR )  ->  ( ( abs  o.  f ) `  t
)  =  ( abs `  ( f `  t
) ) )
115113, 114sylan 471 . . . . . . . . . . . 12  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( abs  o.  f
) `  t )  =  ( abs `  (
f `  t )
) )
11633adantl 466 . . . . . . . . . . . . 13  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  g : RR --> RR )
117 fvco3 5763 . . . . . . . . . . . . 13  |-  ( ( g : RR --> RR  /\  t  e.  RR )  ->  ( ( abs  o.  g ) `  t
)  =  ( abs `  ( g `  t
) ) )
118116, 117sylan 471 . . . . . . . . . . . 12  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( abs  o.  g
) `  t )  =  ( abs `  (
g `  t )
) )
119103, 111, 42, 42, 112, 115, 118offval 6322 . . . . . . . . . . 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 ) ) ) ) )
12031addid1d 9561 . . . . . . . . . . . . . . . . 17  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( ( f `
 t )  +  0 )  =  ( f `  t ) )
121120mpteq2dva 4373 . . . . . . . . . . . . . . . 16  |-  ( f  e.  dom  S.1  ->  ( t  e.  RR  |->  ( ( f `  t
)  +  0 ) )  =  ( t  e.  RR  |->  ( f `
 t ) ) )
12241a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( f  e.  dom  S.1  ->  RR  e.  _V )
12317a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  0  e.  _V )
12432a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  _i  e.  CC )
12549a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( f  e.  dom  S.1  ->  ( RR  X.  { _i } )  =  ( t  e.  RR  |->  _i ) )
126 fconstmpt 4877 . . . . . . . . . . . . . . . . . . . 20  |-  ( RR 
X.  { 0 } )  =  ( t  e.  RR  |->  0 )
127126a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( f  e.  dom  S.1  ->  ( RR  X.  { 0 } )  =  ( t  e.  RR  |->  0 ) )
128122, 124, 123, 125, 127offval2 6331 . . . . . . . . . . . . . . . . . 18  |-  ( f  e.  dom  S.1  ->  ( ( RR  X.  {
_i } )  oF  x.  ( RR 
X.  { 0 } ) )  =  ( t  e.  RR  |->  ( _i  x.  0 ) ) )
129 it0e0 10539 . . . . . . . . . . . . . . . . . . 19  |-  ( _i  x.  0 )  =  0
130129mpteq2i 4370 . . . . . . . . . . . . . . . . . 18  |-  ( t  e.  RR  |->  ( _i  x.  0 ) )  =  ( t  e.  RR  |->  0 )
131128, 130syl6eq 2486 . . . . . . . . . . . . . . . . 17  |-  ( f  e.  dom  S.1  ->  ( ( RR  X.  {
_i } )  oF  x.  ( RR 
X.  { 0 } ) )  =  ( t  e.  RR  |->  0 ) )
132122, 30, 123, 45, 131offval2 6331 . . . . . . . . . . . . . . . 16  |-  ( f  e.  dom  S.1  ->  ( f  oF  +  ( ( RR  X.  { _i } )  oF  x.  ( RR 
X.  { 0 } ) ) )  =  ( t  e.  RR  |->  ( ( f `  t )  +  0 ) ) )
133121, 132, 453eqtr4d 2480 . . . . . . . . . . . . . . 15  |-  ( f  e.  dom  S.1  ->  ( f  oF  +  ( ( RR  X.  { _i } )  oF  x.  ( RR 
X.  { 0 } ) ) )  =  f )
134133coeq2d 4997 . . . . . . . . . . . . . 14  |-  ( f  e.  dom  S.1  ->  ( abs  o.  ( f  oF  +  ( ( RR  X.  {
_i } )  oF  x.  ( RR 
X.  { 0 } ) ) ) )  =  ( abs  o.  f ) )
135 i1f0 21140 . . . . . . . . . . . . . . 15  |-  ( RR 
X.  { 0 } )  e.  dom  S.1
136 ftc1anclem3 28422 . . . . . . . . . . . . . . 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 )
137135, 136mpan2 671 . . . . . . . . . . . . . 14  |-  ( f  e.  dom  S.1  ->  ( abs  o.  ( f  oF  +  ( ( RR  X.  {
_i } )  oF  x.  ( RR 
X.  { 0 } ) ) ) )  e.  dom  S.1 )
138134, 137eqeltrrd 2513 . . . . . . . . . . . . 13  |-  ( f  e.  dom  S.1  ->  ( abs  o.  f )  e.  dom  S.1 )
139138adantr 465 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  f )  e.  dom  S.1 )
140 coeq2 4993 . . . . . . . . . . . . . . 15  |-  ( f  =  g  ->  ( abs  o.  f )  =  ( abs  o.  g
) )
141140eleq1d 2504 . . . . . . . . . . . . . 14  |-  ( f  =  g  ->  (
( abs  o.  f
)  e.  dom  S.1  <->  ( abs  o.  g )  e. 
dom  S.1 ) )
142141, 138vtoclga 3031 . . . . . . . . . . . . 13  |-  ( g  e.  dom  S.1  ->  ( abs  o.  g )  e.  dom  S.1 )
143142adantl 466 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  g )  e.  dom  S.1 )
144139, 143i1fadd 21148 . . . . . . . . . . 11  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( ( abs 
o.  f )  oF  +  ( abs 
o.  g ) )  e.  dom  S.1 )
145119, 144eqeltrrd 2513 . . . . . . . . . 10  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( t  e.  RR  |->  ( ( abs `  ( f `  t
) )  +  ( abs `  ( g `
 t ) ) ) )  e.  dom  S.1 )
14631abscld 12914 . . . . . . . . . . . . . . . 16  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
f `  t )
)  e.  RR )
14731absge0d 12922 . . . . . . . . . . . . . . . 16  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  0  <_  ( abs `  ( f `  t ) ) )
148 elrege0 11384 . . . . . . . . . . . . . . . 16  |-  ( ( abs `  ( f `
 t ) )  e.  ( 0 [,) +oo )  <->  ( ( abs `  ( f `  t
) )  e.  RR  /\  0  <_  ( abs `  ( f `  t
) ) ) )
149146, 147, 148sylanbrc 664 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
f `  t )
)  e.  ( 0 [,) +oo ) )
15035abscld 12914 . . . . . . . . . . . . . . . 16  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
g `  t )
)  e.  RR )
15135absge0d 12922 . . . . . . . . . . . . . . . 16  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  0  <_  ( abs `  ( g `  t ) ) )
152 elrege0 11384 . . . . . . . . . . . . . . . 16  |-  ( ( abs `  ( g `
 t ) )  e.  ( 0 [,) +oo )  <->  ( ( abs `  ( g `  t
) )  e.  RR  /\  0  <_  ( abs `  ( g `  t
) ) ) )
153150, 151, 152sylanbrc 664 . . . . . . . . . . . . . . 15  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
g `  t )
)  e.  ( 0 [,) +oo ) )
154 ge0addcl 11389 . . . . . . . . . . . . . . 15  |-  ( ( ( abs `  (
f `  t )
)  e.  ( 0 [,) +oo )  /\  ( abs `  ( g `
 t ) )  e.  ( 0 [,) +oo ) )  ->  (
( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) )  e.  ( 0 [,) +oo ) )
155149, 153, 154syl2an 477 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  dom  S.1 
/\  t  e.  RR )  /\  ( g  e. 
dom  S.1  /\  t  e.  RR ) )  -> 
( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) )  e.  ( 0 [,) +oo ) )
156155anandirs 827 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) )  e.  ( 0 [,) +oo ) )
157 eqid 2438 . . . . . . . . . . . . 13  |-  ( t  e.  RR  |->  ( ( abs `  ( f `
 t ) )  +  ( abs `  (
g `  t )
) ) )  =  ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) )
158156, 157fmptd 5862 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( t  e.  RR  |->  ( ( abs `  ( f `  t
) )  +  ( abs `  ( g `
 t ) ) ) ) : RR --> ( 0 [,) +oo ) )
159 0plef 21125 . . . . . . . . . . . 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
) ) ) ) ) )
160158, 159sylib 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
) ) ) ) ) )
161160simprd 463 . . . . . . . . . 10  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  0p  oR  <_  ( t  e.  RR  |->  ( ( abs `  ( f `  t
) )  +  ( abs `  ( g `
 t ) ) ) ) )
162 itg2itg1 21189 . . . . . . . . . . 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
) ) ) ) ) )
163 itg1cl 21138 . . . . . . . . . . . 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 )
164163adantr 465 . . . . . . . . . . 11  |-  ( ( ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) )  e.  dom  S.1  /\  0p  oR 
<_  ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) )  ->  ( S.1 `  ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) )  e.  RR )
165162, 164eqeltrd 2512 . . . . . . . . . 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 )
166145, 161, 165syl2anc 661 . . . . . . . . 9  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( S.2 `  (
t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) )  e.  RR )
167 rexr 9421 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  x  e.  RR* )
168167anim1i 568 . . . . . . . . . . . . 13  |-  ( ( x  e.  RR  /\  0  <_  x )  -> 
( x  e.  RR*  /\  0  <_  x )
)
169 elrege0 11384 . . . . . . . . . . . . 13  |-  ( x  e.  ( 0 [,) +oo )  <->  ( x  e.  RR  /\  0  <_  x ) )
170 elxrge0 11386 . . . . . . . . . . . . 13  |-  ( x  e.  ( 0 [,] +oo )  <->  ( x  e. 
RR*  /\  0  <_  x ) )
171168, 169, 1703imtr4i 266 . . . . . . . . . . . 12  |-  ( x  e.  ( 0 [,) +oo )  ->  x  e.  ( 0 [,] +oo ) )
172171ssriv 3355 . . . . . . . . . . 11  |-  ( 0 [,) +oo )  C_  ( 0 [,] +oo )
173 fss 5562 . . . . . . . . . . 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 ) )
174158, 172, 173sylancl 662 . . . . . . . . . 10  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( t  e.  RR  |->  ( ( abs `  ( f `  t
) )  +  ( abs `  ( g `
 t ) ) ) ) : RR --> ( 0 [,] +oo ) )
175 0re 9378 . . . . . . . . . . . . . 14  |-  0  e.  RR
176 ifcl 3826 . . . . . . . . . . . . . 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 )
17771, 175, 176sylancl 662 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  e.  RR )
178 readdcl 9357 . . . . . . . . . . . . . . 15  |-  ( ( ( abs `  (
f `  t )
)  e.  RR  /\  ( abs `  ( g `
 t ) )  e.  RR )  -> 
( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) )  e.  RR )
179146, 150, 178syl2an 477 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  dom  S.1 
/\  t  e.  RR )  /\  ( g  e. 
dom  S.1  /\  t  e.  RR ) )  -> 
( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) )  e.  RR )
180179anandirs 827 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) )  e.  RR )
18171leidd 9898 . . . . . . . . . . . . . 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 ) ) ) ) )
182 breq1 4290 . . . . . . . . . . . . . . 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 ) ) ) ) ) )
183 breq1 4290 . . . . . . . . . . . . . . 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 ) ) ) ) ) )
184182, 183ifboth 3820 . . . . . . . . . . . . . 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 ) ) ) ) )
185181, 72, 184syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  <_  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
186 abstri 12810 . . . . . . . . . . . . . . . 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 ) ) ) ) )
18731, 37, 186syl2an 477 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  dom  S.1 
/\  t  e.  RR )  /\  ( g  e. 
dom  S.1  /\  t  e.  RR ) )  -> 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) )  <_  ( ( abs `  ( f `  t ) )  +  ( abs `  (
_i  x.  ( g `  t ) ) ) ) )
188187anandirs 827 . . . . . . . . . . . . . 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 )
) ) ) )
189 absmul 12775 . . . . . . . . . . . . . . . . . . 19  |-  ( ( _i  e.  CC  /\  ( g `  t
)  e.  CC )  ->  ( abs `  (
_i  x.  ( g `  t ) ) )  =  ( ( abs `  _i )  x.  ( abs `  ( g `  t ) ) ) )
19032, 35, 189sylancr 663 . . . . . . . . . . . . . . . . . 18  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
_i  x.  ( g `  t ) ) )  =  ( ( abs `  _i )  x.  ( abs `  ( g `  t ) ) ) )
191 absi 12767 . . . . . . . . . . . . . . . . . . 19  |-  ( abs `  _i )  =  1
192191oveq1i 6096 . . . . . . . . . . . . . . . . . 18  |-  ( ( abs `  _i )  x.  ( abs `  (
g `  t )
) )  =  ( 1  x.  ( abs `  ( g `  t
) ) )
193190, 192syl6eq 2486 . . . . . . . . . . . . . . . . 17  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
_i  x.  ( g `  t ) ) )  =  ( 1  x.  ( abs `  (
g `  t )
) ) )
194150recnd 9404 . . . . . . . . . . . . . . . . . 18  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
g `  t )
)  e.  CC )
195194mulid2d 9396 . . . . . . . . . . . . . . . . 17  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( 1  x.  ( abs `  (
g `  t )
) )  =  ( abs `  ( g `
 t ) ) )
196193, 195eqtrd 2470 . . . . . . . . . . . . . . . 16  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
_i  x.  ( g `  t ) ) )  =  ( abs `  (
g `  t )
) )
197196adantll 713 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( _i  x.  ( g `  t
) ) )  =  ( abs `  (
g `  t )
) )
198197oveq2d 6102 . . . . . . . . . . . . . 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
) ) ) )
199188, 198breqtrd 4311 . . . . . . . . . . . . 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
) ) ) )
200177, 71, 180, 185, 199letrd 9520 . . . . . . . . . . . 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 ) ) ) )
201200ralrimiva 2794 . . . . . . . . . . 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 ) ) ) )
202 eqidd 2439 . . . . . . . . . . . 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 ) ) )
203 eqidd 2439 . . . . . . . . . . . 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
) ) ) ) )
20442, 177, 180, 202, 203ofrfval2 6332 . . . . . . . . . . 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 ) ) ) ) )
205201, 204mpbird 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
) ) ) ) )
206 itg2le 21192 . . . . . . . . . 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 ) ) ) ) ) )
20792, 174, 205, 206syl3anc 1218 . . . . . . . . 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 ) ) ) ) ) )
208 itg2lecl 21191 . . . . . . . . 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 )
20992, 166, 207, 208syl3anc 1218 . . . . . . . 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 )
210209ad2antlr 726 . . . . . . 7  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )  e.  RR )
21192ad2antlr 726 . . . . . . . 8  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) : RR --> ( 0 [,] +oo ) )
212 breq1 4290 . . . . . . . . . . 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 ) ) )
213 breq1 4290 . . . . . . . . . . 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 ) ) )
214 elioore 11322 . . . . . . . . . . . . . . 15  |-  ( t  e.  ( u (,) w )  ->  t  e.  RR )
215214, 181sylan2 474 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  ( u (,) w
) )  ->  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  <_ 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
216215adantll 713 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  ( u (,) w
) )  ->  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  <_ 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
217216adantlr 714 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) )  <_  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) )
2182rexrd 9425 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A  e.  RR* )
2193rexrd 9425 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  B  e.  RR* )
220218, 219jca 532 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( A  e.  RR*  /\  B  e.  RR* )
)
221 df-icc 11299 . . . . . . . . . . . . . . . . . . . . 21  |-  [,]  =  ( x  e.  RR* ,  y  e.  RR*  |->  { t  e.  RR*  |  (
x  <_  t  /\  t  <_  y ) } )
222221elixx3g 11305 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  e.  ( A [,] B )  <->  ( ( A  e.  RR*  /\  B  e.  RR*  /\  u  e. 
RR* )  /\  ( A  <_  u  /\  u  <_  B ) ) )
223222simprbi 464 . . . . . . . . . . . . . . . . . . 19  |-  ( u  e.  ( A [,] B )  ->  ( A  <_  u  /\  u  <_  B ) )
224223simpld 459 . . . . . . . . . . . . . . . . . 18  |-  ( u  e.  ( A [,] B )  ->  A  <_  u )
225221elixx3g 11305 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  e.  ( A [,] B )  <->  ( ( A  e.  RR*  /\  B  e.  RR*  /\  w  e. 
RR* )  /\  ( A  <_  w  /\  w  <_  B ) ) )
226225simprbi 464 . . . . . . . . . . . . . . . . . . 19  |-  ( w  e.  ( A [,] B )  ->  ( A  <_  w  /\  w  <_  B ) )
227226simprd 463 . . . . . . . . . . . . . . . . . 18  |-  ( w  e.  ( A [,] B )  ->  w  <_  B )
228224, 227anim12i 566 . . . . . . . . . . . . . . . . 17  |-  ( ( u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) )  -> 
( A  <_  u  /\  w  <_  B ) )
229 df-ioo 11296 . . . . . . . . . . . . . . . . . 18  |-  (,)  =  ( x  e.  RR* ,  y  e.  RR*  |->  { t  e.  RR*  |  (
x  <  t  /\  t  <  y ) } )
230 xrlelttr 11122 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  RR*  /\  u  e.  RR*  /\  z  e. 
RR* )  ->  (
( A  <_  u  /\  u  <  z )  ->  A  <  z
) )
231 xrltletr 11123 . . . . . . . . . . . . . . . . . 18  |-  ( ( z  e.  RR*  /\  w  e.  RR*  /\  B  e. 
RR* )  ->  (
( z  <  w  /\  w  <_  B )  ->  z  <  B
) )
232229, 229, 230, 231ixxss12 11312 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <_  u  /\  w  <_  B ) )  ->  ( u (,) w )  C_  ( A (,) B ) )
233220, 228, 232syl2an 477 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  (
u (,) w ) 
C_  ( A (,) B ) )
2345adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  ( A (,) B )  C_  D )
235233, 234sstrd 3361 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  (
u (,) w ) 
C_  D )
236235sselda 3351 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  t  e.  D )
237 iftrue 3792 . . . . . . . . . . . . . 14  |-  ( t  e.  D  ->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  =  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
238236, 237syl 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 ) ) ) ) )
239238adantllr 718 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  if (
t  e.  D , 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  =  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
240217, 239breqtrrd 4313 . . . . . . . . . . 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 ) )
241 breq2 4291 . . . . . . . . . . . . 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 ) ) )
242 breq2 4291 . . . . . . . . . . . . 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 ) ) )
2436sselda 3351 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  D )  ->  t  e.  RR )
244243adantlr 714 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  D )  ->  t  e.  RR )
24572adantll 713 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  RR )  ->  0  <_  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
246244, 245syldan 470 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  D )  ->  0  <_  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
247 0le0 10403 . . . . . . . . . . . . . 14  |-  0  <_  0
248247a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  -.  t  e.  D )  ->  0  <_  0 )
249241, 242, 246, 248ifbothda 3819 . . . . . . . . . . . 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 ) )
250249ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  -.  t  e.  ( u (,) w
) )  ->  0  <_  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ,  0 ) )
251212, 213, 240, 250ifbothda 3819 . . . . . . . . . 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 ) )
252251ralrimivw 2795 . . . . . . . . 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 ) )
25341a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  RR  e.  _V )
25418a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  RR )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  e.  _V )
25516, 17ifex 3853 . . . . . . . . . . . 12  |-  if ( t  e.  D , 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  e.  _V
256255a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  RR )  ->  if ( t  e.  D , 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  e.  _V )
257 eqidd 2439 . . . . . . . . . . 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 ) ) )
258 eqidd 2439 . . . . . . . . . . 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 ) ) )
259253, 254, 256, 257, 258ofrfval2 6332 . . . . . . . . . 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 ) ) )
260259ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )  oR  <_ 
( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )  <->  A. t  e.  RR  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  <_  if ( t  e.  D ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) )
261252, 260mpbird 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 ) ) )
262 itg2le 21192 . . . . . . . 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 ) ) ) )
26388, 211, 261, 262syl3anc 1218 . . . . . . 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 ) ) ) )
264 itg2lecl 21191 . . . . . . 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 )
26588, 210, 263, 264syl3anc 1218 . . . . . 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 )
2668ffvelrnda 5838 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  D )  ->  ( F `  t )  e.  CC )
267266adantlr 714 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  D
)  ->  ( F `  t )  e.  CC )
268236, 267syldan 470 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  ( F `  t )  e.  CC )
269268adantllr 718 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  ( F `  t )  e.  CC )
270214, 40sylan2 474 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  ( u (,) w
) )  ->  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) )  e.  CC )
271270adantll 713 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  ( u (,) w
) )  ->  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) )  e.  CC )
272271adantlr 714 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  ( (
f `  t )  +  ( _i  x.  ( g `  t
) ) )  e.  CC )
273269, 272subcld 9711 . . . . . . . . . . 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 )
274273abscld 12914 . . . . . . . . . 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 )
275273absge0d 12922 . . . . . . . . . 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 )
) ) ) ) )
276 elrege0 11384 . . . . . . . . . 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 ) ) ) ) ) ) )
277274, 275, 276sylanbrc 664 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  ( abs `  ( ( F `  t )  -  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  e.  ( 0 [,) +oo )
)
27875a1i 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 ) )
279277, 278ifclda 3816 . . . . . . . 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 ) )
280279adantr 465 . . . . . . 7  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  RR )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( F `  t )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) ) ,  0 )  e.  ( 0 [,) +oo ) )
281 eqid 2438 . . . . . . 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 ) )
282280, 281fmptd 5862 . . . . . 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 ) )
283274rexrd 9425 . . . . . . . . . . 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* )
284 elxrge0 11386 . . . . . . . . . . 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 ) ) ) ) ) ) )
285283, 275, 284sylanbrc 664 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  ( abs `  ( ( F `  t )  -  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  e.  ( 0 [,] +oo )
)
28684a1i 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 ) )
287285, 286ifclda 3816 . . . . . . . . 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 ) )
288287adantr 465 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  RR )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( F `  t )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) ) ,  0 )  e.  ( 0 [,] +oo ) )
289288, 281fmptd 5862 . . . . . . 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 ) )
290 recncf 20453 . . . . . . . . . . . . 13  |-  Re  e.  ( CC -cn-> RR )
291 prid1g 3976 . . . . . . . . . . . . 13  |-  ( Re  e.  ( CC -cn-> RR )  ->  Re  e.  { Re ,  Im }
)
292290, 291ax-mp 5 . . . . . . . . . . . 12  |-  Re  e.  { Re ,  Im }
293 ftc1anclem2 28421 . . . . . . . . . . . 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 )
294292, 293mp3an3 1303 . . . . . . . . . . 11  |-  ( ( F : D --> CC  /\  F  e.  L^1
)  ->  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
Re `  ( F `  t ) ) ) ,  0 ) ) )  e.  RR )
2958, 7, 294syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
Re `  ( F `  t ) ) ) ,  0 ) ) )  e.  RR )
296 imcncf 20454 . . . . . . . . . . . . 13  |-  Im  e.  ( CC -cn-> RR )
297 prid2g 3977 . . . . . . . . . . . . 13  |-  ( Im  e.  ( CC -cn-> RR )  ->  Im  e.  { Re ,  Im }
)
298296, 297ax-mp 5 . . . . . . . . . . . 12  |-  Im  e.  { Re ,  Im }
299 ftc1anclem2 28421 . . . . . . . . . . . 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 )
300298, 299mp3an3 1303 . . . . . . . . . . 11  |-  ( ( F : D --> CC  /\  F  e.  L^1
)  ->  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
Im `  ( F `  t ) ) ) ,  0 ) ) )  e.  RR )
3018, 7, 300syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
Im `  ( F `  t ) ) ) ,  0 ) ) )  e.  RR )
302295, 301readdcld 9405 . . . . . . . . 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 )
303302ad2antrr 725 . . . . . . . 8  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( ( S.2 `  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
Re `  ( F `  t ) ) ) ,  0 ) ) )  +  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
Im `  ( F `  t ) ) ) ,  0 ) ) ) )  e.  RR )
304210, 303readdcld 9405 . . . . . . 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 )
305 ge0addcl 11389 . . . . . . . . . . . . 13  |-  ( ( x  e.  ( 0 [,) +oo )  /\  y  e.  ( 0 [,) +oo ) )  ->  ( x  +  y )  e.  ( 0 [,) +oo )
)
306305adantl 466 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
x  e.  ( 0 [,) +oo )  /\  y  e.  ( 0 [,) +oo ) ) )  ->  ( x  +  y )  e.  ( 0 [,) +oo ) )
307 ifcl 3826 . . . . . . . . . . . . . . 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 ) )
30874, 75, 307sylancl 662 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  e.  ( 0 [,) +oo ) )
309308, 91fmptd 5862 . . . . . . . . . . . . 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 ) )
310309adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  -> 
( t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) : RR --> ( 0 [,) +oo ) )
311305adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  ( 0 [,) +oo )  /\  y  e.  ( 0 [,) +oo )
) )  ->  (
x  +  y )  e.  ( 0 [,) +oo ) )
312266recld 12675 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\