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

Theorem ftc1anclem8 26301
Description: Lemma for ftc1anc 26302. (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 26300 . 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 736 . . . 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 955 . . . 4  |-  ( ( u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w )  ->  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )
12 ioossre 10977 . . . . . . . . 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 19440 . . . . . . . . 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 5745 . . . . . . . . . 10  |-  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) )  e.  _V
17 c0ex 9090 . . . . . . . . . 10  |-  0  e.  _V
1816, 17ifex 3799 . . . . . . . . 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 3472 . . . . . . . . . 10  |-  ( t  e.  ( RR  \ 
( u (,) w
) )  ->  -.  t  e.  ( u (,) w ) )
2120adantl 454 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  ( RR  \  (
u (,) w ) ) )  ->  -.  t  e.  ( u (,) w ) )
22 iffalse 3748 . . . . . . . . 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 3747 . . . . . . . . . . . 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 4294 . . . . . . . . . . 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 5194 . . . . . . . . . . . 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 19571 . . . . . . . . . . . . . . . . . 18  |-  ( f  e.  dom  S.1  ->  f : RR --> RR )
3029ffvelrnda 5873 . . . . . . . . . . . . . . . . 17  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( f `  t )  e.  RR )
3130recnd 9119 . . . . . . . . . . . . . . . 16  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( f `  t )  e.  CC )
32 ax-icn 9054 . . . . . . . . . . . . . . . . 17  |-  _i  e.  CC
33 i1ff 19571 . . . . . . . . . . . . . . . . . . 19  |-  ( g  e.  dom  S.1  ->  g : RR --> RR )
3433ffvelrnda 5873 . . . . . . . . . . . . . . . . . 18  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  e.  RR )
3534recnd 9119 . . . . . . . . . . . . . . . . 17  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  e.  CC )
36 mulcl 9079 . . . . . . . . . . . . . . . . 17  |-  ( ( _i  e.  CC  /\  ( g `  t
)  e.  CC )  ->  ( _i  x.  ( g `  t
) )  e.  CC )
3732, 35, 36sylancr 646 . . . . . . . . . . . . . . . 16  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( _i  x.  ( g `  t
) )  e.  CC )
38 addcl 9077 . . . . . . . . . . . . . . . 16  |-  ( ( ( f `  t
)  e.  CC  /\  ( _i  x.  (
g `  t )
)  e.  CC )  ->  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) )  e.  CC )
3931, 37, 38syl2an 465 . . . . . . . . . . . . . . 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 806 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) )  e.  CC )
41 reex 9086 . . . . . . . . . . . . . . . 16  |-  RR  e.  _V
4241a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  RR  e.  _V )
4330adantlr 697 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
f `  t )  e.  RR )
4437adantll 696 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
_i  x.  ( g `  t ) )  e.  CC )
4529feqmptd 5782 . . . . . . . . . . . . . . . 16  |-  ( f  e.  dom  S.1  ->  f  =  ( t  e.  RR  |->  ( f `  t ) ) )
4645adantr 453 . . . . . . . . . . . . . . 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 4924 . . . . . . . . . . . . . . . . . 18  |-  ( RR 
X.  { _i }
)  =  ( t  e.  RR  |->  _i )
5049a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( g  e.  dom  S.1  ->  ( RR  X.  { _i } )  =  ( t  e.  RR  |->  _i ) )
5133feqmptd 5782 . . . . . . . . . . . . . . . . 17  |-  ( g  e.  dom  S.1  ->  g  =  ( t  e.  RR  |->  ( g `  t ) ) )
5247, 48, 34, 50, 51offval2 6325 . . . . . . . . . . . . . . . 16  |-  ( g  e.  dom  S.1  ->  ( ( RR  X.  {
_i } )  o F  x.  g )  =  ( t  e.  RR  |->  ( _i  x.  ( g `  t
) ) ) )
5352adantl 454 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( ( RR 
X.  { _i }
)  o F  x.  g )  =  ( t  e.  RR  |->  ( _i  x.  ( g `
 t ) ) ) )
5442, 43, 44, 46, 53offval2 6325 . . . . . . . . . . . . . 14  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( f  o F  +  ( ( RR  X.  { _i } )  o F  x.  g ) )  =  ( t  e.  RR  |->  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) )
55 absf 12146 . . . . . . . . . . . . . . . 16  |-  abs : CC
--> RR
5655a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  abs : CC --> RR )
5756feqmptd 5782 . . . . . . . . . . . . . 14  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  abs  =  (
x  e.  CC  |->  ( abs `  x ) ) )
58 fveq2 5731 . . . . . . . . . . . . . 14  |-  ( x  =  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) )  ->  ( abs `  x )  =  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
5940, 54, 57, 58fmptco 5904 . . . . . . . . . . . . 13  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  ( f  o F  +  ( ( RR 
X.  { _i }
)  o F  x.  g ) ) )  =  ( t  e.  RR  |->  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ) )
60 ftc1anclem3 26296 . . . . . . . . . . . . 13  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  ( f  o F  +  ( ( RR 
X.  { _i }
)  o F  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 19570 . . . . . . . . . . . 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 19464 . . . . . . . . . . 11  |-  ( u (,) w )  e. 
dom  vol
65 mbfres 19539 . . . . . . . . . . 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 645 . . . . . . . . . 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 454 . . . . . . . 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 19541 . . . . . . 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 453 . . . . . 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 12243 . . . . . . . . . 10  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  e.  RR )
7240absge0d 12251 . . . . . . . . . 10  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  0  <_  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
73 elrege0 11012 . . . . . . . . . 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 647 . . . . . . . . 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 0re 9096 . . . . . . . . . 10  |-  0  e.  RR
76 0le0 10086 . . . . . . . . . 10  |-  0  <_  0
77 elrege0 11012 . . . . . . . . . 10  |-  ( 0  e.  ( 0 [,) 
+oo )  <->  ( 0  e.  RR  /\  0  <_  0 ) )
7875, 76, 77mpbir2an 888 . . . . . . . . 9  |-  0  e.  ( 0 [,)  +oo )
79 ifcl 3777 . . . . . . . . 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 ) )
8074, 78, 79sylancl 645 . . . . . . . 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 ) )
81 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 ) )
8280, 81fmptd 5896 . . . . . . 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 ) )
8382ad2antlr 709 . . . . . 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 ) )
8471rexrd 9139 . . . . . . . . . . 11  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  e. 
RR* )
85 elxrge0 11013 . . . . . . . . . . 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
) ) ) ) ) )
8684, 72, 85sylanbrc 647 . . . . . . . . . 10  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  e.  ( 0 [,]  +oo ) )
87 0xr 9136 . . . . . . . . . . 11  |-  0  e.  RR*
88 elxrge0 11013 . . . . . . . . . . 11  |-  ( 0  e.  ( 0 [,] 
+oo )  <->  ( 0  e.  RR*  /\  0  <_  0 ) )
8987, 76, 88mpbir2an 888 . . . . . . . . . 10  |-  0  e.  ( 0 [,]  +oo )
90 ifcl 3777 . . . . . . . . . 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 ) )
9186, 89, 90sylancl 645 . . . . . . . . 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 ) )
9291, 81fmptd 5896 . . . . . . . 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 ) )
9392ad2antlr 709 . . . . . . 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 ) )
94 ifcl 3777 . . . . . . . . . . 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 ) )
9586, 89, 94sylancl 645 . . . . . . . . . 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 ) )
96 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 ) )
9795, 96fmptd 5896 . . . . . . . . 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 ) )
98 ffn 5594 . . . . . . . . . . . . . . 15  |-  ( f : RR --> RR  ->  f  Fn  RR )
99 frn 5600 . . . . . . . . . . . . . . . 16  |-  ( f : RR --> RR  ->  ran  f  C_  RR )
100 ax-resscn 9052 . . . . . . . . . . . . . . . 16  |-  RR  C_  CC
10199, 100syl6ss 3362 . . . . . . . . . . . . . . 15  |-  ( f : RR --> RR  ->  ran  f  C_  CC )
102 ffn 5594 . . . . . . . . . . . . . . . . 17  |-  ( abs
: CC --> RR  ->  abs 
Fn  CC )
10355, 102ax-mp 5 . . . . . . . . . . . . . . . 16  |-  abs  Fn  CC
104 fnco 5556 . . . . . . . . . . . . . . . 16  |-  ( ( abs  Fn  CC  /\  f  Fn  RR  /\  ran  f  C_  CC )  -> 
( abs  o.  f
)  Fn  RR )
105103, 104mp3an1 1267 . . . . . . . . . . . . . . 15  |-  ( ( f  Fn  RR  /\  ran  f  C_  CC )  ->  ( abs  o.  f )  Fn  RR )
10698, 101, 105syl2anc 644 . . . . . . . . . . . . . 14  |-  ( f : RR --> RR  ->  ( abs  o.  f )  Fn  RR )
10729, 106syl 16 . . . . . . . . . . . . 13  |-  ( f  e.  dom  S.1  ->  ( abs  o.  f )  Fn  RR )
108107adantr 453 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  f )  Fn  RR )
109 ffn 5594 . . . . . . . . . . . . . . 15  |-  ( g : RR --> RR  ->  g  Fn  RR )
110 frn 5600 . . . . . . . . . . . . . . . 16  |-  ( g : RR --> RR  ->  ran  g  C_  RR )
111110, 100syl6ss 3362 . . . . . . . . . . . . . . 15  |-  ( g : RR --> RR  ->  ran  g  C_  CC )
112 fnco 5556 . . . . . . . . . . . . . . . 16  |-  ( ( abs  Fn  CC  /\  g  Fn  RR  /\  ran  g  C_  CC )  -> 
( abs  o.  g
)  Fn  RR )
113103, 112mp3an1 1267 . . . . . . . . . . . . . . 15  |-  ( ( g  Fn  RR  /\  ran  g  C_  CC )  ->  ( abs  o.  g )  Fn  RR )
114109, 111, 113syl2anc 644 . . . . . . . . . . . . . 14  |-  ( g : RR --> RR  ->  ( abs  o.  g )  Fn  RR )
11533, 114syl 16 . . . . . . . . . . . . 13  |-  ( g  e.  dom  S.1  ->  ( abs  o.  g )  Fn  RR )
116115adantl 454 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  g )  Fn  RR )
117 inidm 3552 . . . . . . . . . . . 12  |-  ( RR 
i^i  RR )  =  RR
11829adantr 453 . . . . . . . . . . . . 13  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  f : RR --> RR )
119 fvco3 5803 . . . . . . . . . . . . 13  |-  ( ( f : RR --> RR  /\  t  e.  RR )  ->  ( ( abs  o.  f ) `  t
)  =  ( abs `  ( f `  t
) ) )
120118, 119sylan 459 . . . . . . . . . . . 12  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( abs  o.  f
) `  t )  =  ( abs `  (
f `  t )
) )
12133adantl 454 . . . . . . . . . . . . 13  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  g : RR --> RR )
122 fvco3 5803 . . . . . . . . . . . . 13  |-  ( ( g : RR --> RR  /\  t  e.  RR )  ->  ( ( abs  o.  g ) `  t
)  =  ( abs `  ( g `  t
) ) )
123121, 122sylan 459 . . . . . . . . . . . 12  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( abs  o.  g
) `  t )  =  ( abs `  (
g `  t )
) )
124108, 116, 42, 42, 117, 120, 123offval 6315 . . . . . . . . . . 11  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( ( abs 
o.  f )  o F  +  ( abs 
o.  g ) )  =  ( t  e.  RR  |->  ( ( abs `  ( f `  t
) )  +  ( abs `  ( g `
 t ) ) ) ) )
12531addid1d 9271 . . . . . . . . . . . . . . . . 17  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( ( f `
 t )  +  0 )  =  ( f `  t ) )
126125mpteq2dva 4298 . . . . . . . . . . . . . . . 16  |-  ( f  e.  dom  S.1  ->  ( t  e.  RR  |->  ( ( f `  t
)  +  0 ) )  =  ( t  e.  RR  |->  ( f `
 t ) ) )
12741a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( f  e.  dom  S.1  ->  RR  e.  _V )
12817a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  0  e.  _V )
12932a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  _i  e.  CC )
13049a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( f  e.  dom  S.1  ->  ( RR  X.  { _i } )  =  ( t  e.  RR  |->  _i ) )
131 fconstmpt 4924 . . . . . . . . . . . . . . . . . . . 20  |-  ( RR 
X.  { 0 } )  =  ( t  e.  RR  |->  0 )
132131a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( f  e.  dom  S.1  ->  ( RR  X.  { 0 } )  =  ( t  e.  RR  |->  0 ) )
133127, 129, 128, 130, 132offval2 6325 . . . . . . . . . . . . . . . . . 18  |-  ( f  e.  dom  S.1  ->  ( ( RR  X.  {
_i } )  o F  x.  ( RR 
X.  { 0 } ) )  =  ( t  e.  RR  |->  ( _i  x.  0 ) ) )
13432mul01i 9261 . . . . . . . . . . . . . . . . . . 19  |-  ( _i  x.  0 )  =  0
135134mpteq2i 4295 . . . . . . . . . . . . . . . . . 18  |-  ( t  e.  RR  |->  ( _i  x.  0 ) )  =  ( t  e.  RR  |->  0 )
136133, 135syl6eq 2486 . . . . . . . . . . . . . . . . 17  |-  ( f  e.  dom  S.1  ->  ( ( RR  X.  {
_i } )  o F  x.  ( RR 
X.  { 0 } ) )  =  ( t  e.  RR  |->  0 ) )
137127, 30, 128, 45, 136offval2 6325 . . . . . . . . . . . . . . . 16  |-  ( f  e.  dom  S.1  ->  ( f  o F  +  ( ( RR  X.  { _i } )  o F  x.  ( RR 
X.  { 0 } ) ) )  =  ( t  e.  RR  |->  ( ( f `  t )  +  0 ) ) )
138126, 137, 453eqtr4d 2480 . . . . . . . . . . . . . . 15  |-  ( f  e.  dom  S.1  ->  ( f  o F  +  ( ( RR  X.  { _i } )  o F  x.  ( RR 
X.  { 0 } ) ) )  =  f )
139138coeq2d 5038 . . . . . . . . . . . . . 14  |-  ( f  e.  dom  S.1  ->  ( abs  o.  ( f  o F  +  ( ( RR  X.  {
_i } )  o F  x.  ( RR 
X.  { 0 } ) ) ) )  =  ( abs  o.  f ) )
140 i1f0 19582 . . . . . . . . . . . . . . 15  |-  ( RR 
X.  { 0 } )  e.  dom  S.1
141 ftc1anclem3 26296 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  ( RR  X.  {
0 } )  e. 
dom  S.1 )  ->  ( abs  o.  ( f  o F  +  ( ( RR  X.  { _i } )  o F  x.  ( RR  X.  { 0 } ) ) ) )  e. 
dom  S.1 )
142140, 141mpan2 654 . . . . . . . . . . . . . 14  |-  ( f  e.  dom  S.1  ->  ( abs  o.  ( f  o F  +  ( ( RR  X.  {
_i } )  o F  x.  ( RR 
X.  { 0 } ) ) ) )  e.  dom  S.1 )
143139, 142eqeltrrd 2513 . . . . . . . . . . . . 13  |-  ( f  e.  dom  S.1  ->  ( abs  o.  f )  e.  dom  S.1 )
144143adantr 453 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  f )  e.  dom  S.1 )
145 coeq2 5034 . . . . . . . . . . . . . . 15  |-  ( f  =  g  ->  ( abs  o.  f )  =  ( abs  o.  g
) )
146145eleq1d 2504 . . . . . . . . . . . . . 14  |-  ( f  =  g  ->  (
( abs  o.  f
)  e.  dom  S.1  <->  ( abs  o.  g )  e. 
dom  S.1 ) )
147146, 143vtoclga 3019 . . . . . . . . . . . . 13  |-  ( g  e.  dom  S.1  ->  ( abs  o.  g )  e.  dom  S.1 )
148147adantl 454 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  g )  e.  dom  S.1 )
149144, 148i1fadd 19590 . . . . . . . . . . 11  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( ( abs 
o.  f )  o F  +  ( abs 
o.  g ) )  e.  dom  S.1 )
150124, 149eqeltrrd 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 )
15131abscld 12243 . . . . . . . . . . . . . . . 16  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
f `  t )
)  e.  RR )
15231absge0d 12251 . . . . . . . . . . . . . . . 16  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  0  <_  ( abs `  ( f `  t ) ) )
153 elrege0 11012 . . . . . . . . . . . . . . . 16  |-  ( ( abs `  ( f `
 t ) )  e.  ( 0 [,) 
+oo )  <->  ( ( abs `  ( f `  t ) )  e.  RR  /\  0  <_ 
( abs `  (
f `  t )
) ) )
154151, 152, 153sylanbrc 647 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
f `  t )
)  e.  ( 0 [,)  +oo ) )
15535abscld 12243 . . . . . . . . . . . . . . . 16  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
g `  t )
)  e.  RR )
15635absge0d 12251 . . . . . . . . . . . . . . . 16  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  0  <_  ( abs `  ( g `  t ) ) )
157 elrege0 11012 . . . . . . . . . . . . . . . 16  |-  ( ( abs `  ( g `
 t ) )  e.  ( 0 [,) 
+oo )  <->  ( ( abs `  ( g `  t ) )  e.  RR  /\  0  <_ 
( abs `  (
g `  t )
) ) )
158155, 156, 157sylanbrc 647 . . . . . . . . . . . . . . 15  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
g `  t )
)  e.  ( 0 [,)  +oo ) )
159 ge0addcl 11014 . . . . . . . . . . . . . . 15  |-  ( ( ( abs `  (
f `  t )
)  e.  ( 0 [,)  +oo )  /\  ( abs `  ( g `  t ) )  e.  ( 0 [,)  +oo ) )  ->  (
( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) )  e.  ( 0 [,)  +oo ) )
160154, 158, 159syl2an 465 . . . . . . . . . . . . . 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 ) )
161160anandirs 806 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) )  e.  ( 0 [,)  +oo ) )
162 eqid 2438 . . . . . . . . . . . . 13  |-  ( t  e.  RR  |->  ( ( abs `  ( f `
 t ) )  +  ( abs `  (
g `  t )
) ) )  =  ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) )
163161, 162fmptd 5896 . . . . . . . . . . . 12  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( t  e.  RR  |->  ( ( abs `  ( f `  t
) )  +  ( abs `  ( g `
 t ) ) ) ) : RR --> ( 0 [,)  +oo ) )
164 0plef 19567 . . . . . . . . . . . 12  |-  ( ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) : RR --> ( 0 [,)  +oo )  <->  ( (
t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) : RR --> RR  /\  0 p  o R  <_  ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) ) )
165163, 164sylib 190 . . . . . . . . . . 11  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( ( t  e.  RR  |->  ( ( abs `  ( f `
 t ) )  +  ( abs `  (
g `  t )
) ) ) : RR --> RR  /\  0 p  o R  <_  (
t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) ) )
166165simprd 451 . . . . . . . . . 10  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  0 p  o R  <_  ( t  e.  RR  |->  ( ( abs `  ( f `  t
) )  +  ( abs `  ( g `
 t ) ) ) ) )
167 itg2itg1 19631 . . . . . . . . . . 11  |-  ( ( ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) )  e.  dom  S.1  /\  0 p  o R  <_  ( 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
) ) ) ) ) )
168 itg1cl 19580 . . . . . . . . . . . 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 )
169168adantr 453 . . . . . . . . . . 11  |-  ( ( ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) )  e.  dom  S.1  /\  0 p  o R  <_  ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) )  ->  ( S.1 `  ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) )  e.  RR )
170167, 169eqeltrd 2512 . . . . . . . . . 10  |-  ( ( ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) )  e.  dom  S.1  /\  0 p  o R  <_  ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) )  ->  ( S.2 `  ( t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) )  e.  RR )
171150, 166, 170syl2anc 644 . . . . . . . . 9  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( S.2 `  (
t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) )  e.  RR )
172 rexr 9135 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  x  e.  RR* )
173172anim1i 553 . . . . . . . . . . . . 13  |-  ( ( x  e.  RR  /\  0  <_  x )  -> 
( x  e.  RR*  /\  0  <_  x )
)
174 elrege0 11012 . . . . . . . . . . . . 13  |-  ( x  e.  ( 0 [,) 
+oo )  <->  ( x  e.  RR  /\  0  <_  x ) )
175 elxrge0 11013 . . . . . . . . . . . . 13  |-  ( x  e.  ( 0 [,] 
+oo )  <->  ( x  e.  RR*  /\  0  <_  x ) )
176173, 174, 1753imtr4i 259 . . . . . . . . . . . 12  |-  ( x  e.  ( 0 [,) 
+oo )  ->  x  e.  ( 0 [,]  +oo ) )
177176ssriv 3354 . . . . . . . . . . 11  |-  ( 0 [,)  +oo )  C_  (
0 [,]  +oo )
178 fss 5602 . . . . . . . . . . 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 ) )
179163, 177, 178sylancl 645 . . . . . . . . . 10  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( t  e.  RR  |->  ( ( abs `  ( f `  t
) )  +  ( abs `  ( g `
 t ) ) ) ) : RR --> ( 0 [,]  +oo ) )
180 ifcl 3777 . . . . . . . . . . . . . 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 )
18171, 75, 180sylancl 645 . . . . . . . . . . . . 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 )
182 readdcl 9078 . . . . . . . . . . . . . . 15  |-  ( ( ( abs `  (
f `  t )
)  e.  RR  /\  ( abs `  ( g `
 t ) )  e.  RR )  -> 
( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) )  e.  RR )
183151, 155, 182syl2an 465 . . . . . . . . . . . . . 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 )
184183anandirs 806 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) )  e.  RR )
18571leidd 9598 . . . . . . . . . . . . . 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 ) ) ) ) )
186 breq1 4218 . . . . . . . . . . . . . . 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 ) ) ) ) ) )
187 breq1 4218 . . . . . . . . . . . . . . 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 ) ) ) ) ) )
188186, 187ifboth 3772 . . . . . . . . . . . . . 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 ) ) ) ) )
189185, 72, 188syl2anc 644 . . . . . . . . . . . . 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 ) ) ) ) )
190 abstri 12139 . . . . . . . . . . . . . . . 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 ) ) ) ) )
19131, 37, 190syl2an 465 . . . . . . . . . . . . . . 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 ) ) ) ) )
192191anandirs 806 . . . . . . . . . . . . . 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 )
) ) ) )
193 absmul 12104 . . . . . . . . . . . . . . . . . . 19  |-  ( ( _i  e.  CC  /\  ( g `  t
)  e.  CC )  ->  ( abs `  (
_i  x.  ( g `  t ) ) )  =  ( ( abs `  _i )  x.  ( abs `  ( g `  t ) ) ) )
19432, 35, 193sylancr 646 . . . . . . . . . . . . . . . . . 18  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
_i  x.  ( g `  t ) ) )  =  ( ( abs `  _i )  x.  ( abs `  ( g `  t ) ) ) )
195 absi 12096 . . . . . . . . . . . . . . . . . . 19  |-  ( abs `  _i )  =  1
196195oveq1i 6094 . . . . . . . . . . . . . . . . . 18  |-  ( ( abs `  _i )  x.  ( abs `  (
g `  t )
) )  =  ( 1  x.  ( abs `  ( g `  t
) ) )
197194, 196syl6eq 2486 . . . . . . . . . . . . . . . . 17  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
_i  x.  ( g `  t ) ) )  =  ( 1  x.  ( abs `  (
g `  t )
) ) )
198155recnd 9119 . . . . . . . . . . . . . . . . . 18  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
g `  t )
)  e.  CC )
199198mulid2d 9111 . . . . . . . . . . . . . . . . 17  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( 1  x.  ( abs `  (
g `  t )
) )  =  ( abs `  ( g `
 t ) ) )
200197, 199eqtrd 2470 . . . . . . . . . . . . . . . 16  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( abs `  (
_i  x.  ( g `  t ) ) )  =  ( abs `  (
g `  t )
) )
201200adantll 696 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( _i  x.  ( g `  t
) ) )  =  ( abs `  (
g `  t )
) )
202201oveq2d 6100 . . . . . . . . . . . . . 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
) ) ) )
203192, 202breqtrd 4239 . . . . . . . . . . . . 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
) ) ) )
204181, 71, 184, 189, 203letrd 9232 . . . . . . . . . . . 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 ) ) ) )
205204ralrimiva 2791 . . . . . . . . . . 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 ) ) ) )
206 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 ) ) )
207 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
) ) ) ) )
20842, 181, 184, 206, 207ofrfval2 6326 . . . . . . . . . . 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 ) )  o R  <_ 
( 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 ) ) ) ) )
209205, 208mpbird 225 . . . . . . . . . 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 ) )  o R  <_  (
t  e.  RR  |->  ( ( abs `  (
f `  t )
)  +  ( abs `  ( g `  t
) ) ) ) )
210 itg2le 19634 . . . . . . . . . 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 ) )  o R  <_ 
( 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 ) ) ) ) ) )
21197, 179, 209, 210syl3anc 1185 . . . . . . . . 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 ) ) ) ) ) )
212 itg2lecl 19633 . . . . . . . . 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 )
21397, 171, 211, 212syl3anc 1185 . . . . . . . 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 )
214213ad2antlr 709 . . . . . . 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 )
21597ad2antlr 709 . . . . . . . 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 ) )
216 breq1 4218 . . . . . . . . . . 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 ) ) )
217 breq1 4218 . . . . . . . . . . 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 ) ) )
218 elioore 10951 . . . . . . . . . . . . . . 15  |-  ( t  e.  ( u (,) w )  ->  t  e.  RR )
219218, 185sylan2 462 . . . . . . . . . . . . . 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 ) ) ) ) )
220219adantll 696 . . . . . . . . . . . . 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 ) ) ) ) )
221220adantlr 697 . . . . . . . . . . . 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 )
) ) ) )
2222rexrd 9139 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A  e.  RR* )
2233rexrd 9139 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  B  e.  RR* )
224222, 223jca 520 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( A  e.  RR*  /\  B  e.  RR* )
)
225 df-icc 10928 . . . . . . . . . . . . . . . . . . . . 21  |-  [,]  =  ( x  e.  RR* ,  y  e.  RR*  |->  { t  e.  RR*  |  (
x  <_  t  /\  t  <_  y ) } )
226225elixx3g 10934 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  e.  ( A [,] B )  <->  ( ( A  e.  RR*  /\  B  e.  RR*  /\  u  e. 
RR* )  /\  ( A  <_  u  /\  u  <_  B ) ) )
227226simprbi 452 . . . . . . . . . . . . . . . . . . 19  |-  ( u  e.  ( A [,] B )  ->  ( A  <_  u  /\  u  <_  B ) )
228227simpld 447 . . . . . . . . . . . . . . . . . 18  |-  ( u  e.  ( A [,] B )  ->  A  <_  u )
229225elixx3g 10934 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  e.  ( A [,] B )  <->  ( ( A  e.  RR*  /\  B  e.  RR*  /\  w  e. 
RR* )  /\  ( A  <_  w  /\  w  <_  B ) ) )
230229simprbi 452 . . . . . . . . . . . . . . . . . . 19  |-  ( w  e.  ( A [,] B )  ->  ( A  <_  w  /\  w  <_  B ) )
231230simprd 451 . . . . . . . . . . . . . . . . . 18  |-  ( w  e.  ( A [,] B )  ->  w  <_  B )
232228, 231anim12i 551 . . . . . . . . . . . . . . . . 17  |-  ( ( u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) )  -> 
( A  <_  u  /\  w  <_  B ) )
233 df-ioo 10925 . . . . . . . . . . . . . . . . . 18  |-  (,)  =  ( x  e.  RR* ,  y  e.  RR*  |->  { t  e.  RR*  |  (
x  <  t  /\  t  <  y ) } )
234 xrlelttr 10751 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  RR*  /\  u  e.  RR*  /\  z  e. 
RR* )  ->  (
( A  <_  u  /\  u  <  z )  ->  A  <  z
) )
235 xrltletr 10752 . . . . . . . . . . . . . . . . . 18  |-  ( ( z  e.  RR*  /\  w  e.  RR*  /\  B  e. 
RR* )  ->  (
( z  <  w  /\  w  <_  B )  ->  z  <  B
) )
236233, 233, 234, 235ixxss12 10941 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <_  u  /\  w  <_  B ) )  ->  ( u (,) w )  C_  ( A (,) B ) )
237224, 232, 236syl2an 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  (
u (,) w ) 
C_  ( A (,) B ) )
2385adantr 453 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  ( A (,) B )  C_  D )
239237, 238sstrd 3360 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  (
u (,) w ) 
C_  D )
240239sselda 3350 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  t  e.  D )
241 iftrue 3747 . . . . . . . . . . . . . 14  |-  ( t  e.  D  ->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  =  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
242240, 241syl 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 ) ) ) ) )
243242adantllr 701 . . . . . . . . . . . 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 ) ) ) ) )
244221, 243breqtrrd 4241 . . . . . . . . . . 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 ) )
245 breq2 4219 . . . . . . . . . . . . 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 ) ) )
246 breq2 4219 . . . . . . . . . . . . 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 ) ) )
2476sselda 3350 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  D )  ->  t  e.  RR )
248247adantlr 697 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  D )  ->  t  e.  RR )
24972adantll 696 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  RR )  ->  0  <_  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
250248, 249syldan 458 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  D )  ->  0  <_  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
25176a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  -.  t  e.  D )  ->  0  <_  0 )
252245, 246, 250, 251ifbothda 3771 . . . . . . . . . . . 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 ) )
253252ad2antrr 708 . . . . . . . . . . 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 ) )
254216, 217, 244, 253ifbothda 3771 . . . . . . . . . 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 ) )
255254ralrimivw 2792 . . . . . . . . 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 ) )
25641a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  RR  e.  _V )
25718a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  RR )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  e.  _V )
25816, 17ifex 3799 . . . . . . . . . . . 12  |-  if ( t  e.  D , 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  e.  _V
259258a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  RR )  ->  if ( t  e.  D , 
( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  e.  _V )
260 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 ) ) )
261 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 ) ) )
262256, 257, 259, 260, 261ofrfval2 6326 . . . . . . . . . 10  |-  ( ph  ->  ( ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) )  o R  <_  (
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 ) ) )
263262ad2antrr 708 . . . . . . . . 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 ) )  o R  <_ 
( 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 ) ) )
264255, 263mpbird 225 . . . . . . . 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 ) )  o R  <_  (
t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )
265 itg2le 19634 . . . . . . . 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 ) )  o R  <_ 
( 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 ) ) ) )
26693, 215, 264, 265syl3anc 1185 . . . . . . 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 ) ) ) )
267 itg2lecl 19633 . . . . . . 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 )
26893, 214, 266, 267syl3anc 1185 . . . . . 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 )
2698ffvelrnda 5873 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  D )  ->  ( F `  t )  e.  CC )
270269adantlr 697 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  D
)  ->  ( F `  t )  e.  CC )
271240, 270syldan 458 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  ( F `  t )  e.  CC )
272271adantllr 701 . . . . . . . . . . . 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 )
273218, 40sylan2 462 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  ( u (,) w
) )  ->  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) )  e.  CC )
274273adantll 696 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  ( u (,) w
) )  ->  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) )  e.  CC )
275274adantlr 697 . . . . . . . . . . . 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 )
276272, 275subcld 9416 . . . . . . . . . . 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 )
277276abscld 12243 . . . . . . . . . 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 )
278276absge0d 12251 . . . . . . . . . 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 )
) ) ) ) )
279 elrege0 11012 . . . . . . . . . 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
) ) ) ) ) ) )
280277, 278, 279sylanbrc 647 . . . . . . . . 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 )
)
28178a1i 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 ) )
282280, 281ifclda 3768 . . . . . . . 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 ) )
283282adantr 453 . . . . . . 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 ) )
284 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 ) )
285283, 284fmptd 5896 . . . . . 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 ) )
286277rexrd 9139 . . . . . . . . . . 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* )
287 elxrge0 11013 . . . . . . . . . . 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 )
) ) ) ) ) )
288286, 278, 287sylanbrc 647 . . . . . . . . . 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 )
)
28989a1i 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 ) )
290288, 289ifclda 3768 . . . . . . . . 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 ) )
291290adantr 453 . . . . . . . 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 ) )
292291, 284fmptd 5896 . . . . . . 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 ) )
293 recncf 18937 . . . . . . . . . . . . 13  |-  Re  e.  ( CC -cn-> RR )
294 prid1g 3912 . . . . . . . . . . . . 13  |-  ( Re  e.  ( CC -cn-> RR )  ->  Re  e.  { Re ,  Im }
)
295293, 294ax-mp 5 . . . . . . . . . . . 12  |-  Re  e.  { Re ,  Im }
296 ftc1anclem2 26295 . . . . . . . . . . . 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 )
297295, 296mp3an3 1269 . . . . . . . . . . 11  |-  ( ( F : D --> CC  /\  F  e.  L ^1 )  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
Re `  ( F `  t ) ) ) ,  0 ) ) )  e.  RR )
2988, 7, 297syl2anc 644 . . . . . . . . . 10  |-  ( ph  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
Re `  ( F `  t ) ) ) ,  0 ) ) )  e.  RR )
299 imcncf 18938 . . . . . . . . . . . . 13  |-  Im  e.  ( CC -cn-> RR )
300 prid2g 3913 . . . . . . . . . . . . 13  |-  ( Im  e.  ( CC -cn-> RR )  ->  Im  e.  { Re ,  Im }
)
301299, 300ax-mp 5 . . . . . . . . . . . 12  |-  Im  e.  { Re ,  Im }
302 ftc1anclem2 26295 . . . . . . . . . . . 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 )
303301, 302mp3an3 1269 . . . . . . . . . . 11  |-  ( ( F : D --> CC  /\  F  e.  L ^1 )  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
Im `  ( F `  t ) ) ) ,  0 ) ) )  e.  RR )
3048, 7, 303syl2anc 644 . . . . . . . . . 10  |-  ( ph  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  D ,  ( abs `  (
Im `  ( F `  t ) ) ) ,  0 ) ) )  e.  RR )
305298, 304readdcld 9120 . . . . . . . . 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 )
306305ad2antrr 708 . . . . . . . 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 )
307214, 306readdcld 9120 . . . . . . 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 )
308 ge0addcl 11014 . . . . . . . . . . . . 13  |-  ( ( x  e.  ( 0 [,)  +oo )  /\  y  e.  ( 0 [,)  +oo ) )  ->  (
x  +  y )  e.  ( 0 [,) 
+oo ) )
309308adantl 454 . . . . . . . . . . . 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 ) )
310 ifcl 3777 . . . . . . . . . . . . . . 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 ) )
31174, 78, 310sylancl 645 . . . . . . . . . . . . . 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 ) )
312311, 96fmptd 5896 . . . . . . . . . . . . 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 ) )
313312adantl 454 . . . . . . . . . . . 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 ) ) ) ) ,