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

Theorem ftc1anclem7 26328
Description: Lemma for ftc1anc 26330. (Contributed by Brendan Leahy, 13-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
ftc1anclem7  |-  ( ( ( ( ( ( ( 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 ) ) )
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 ftc1anclem7
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 i1ff 19604 . . . . . . . . . . 11  |-  ( f  e.  dom  S.1  ->  f : RR --> RR )
21ffvelrnda 5906 . . . . . . . . . 10  |-  ( ( f  e.  dom  S.1  /\  x  e.  RR )  ->  ( f `  x )  e.  RR )
32recnd 9152 . . . . . . . . 9  |-  ( ( f  e.  dom  S.1  /\  x  e.  RR )  ->  ( f `  x )  e.  CC )
4 ax-icn 9087 . . . . . . . . . 10  |-  _i  e.  CC
5 i1ff 19604 . . . . . . . . . . . 12  |-  ( g  e.  dom  S.1  ->  g : RR --> RR )
65ffvelrnda 5906 . . . . . . . . . . 11  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  ( g `  x )  e.  RR )
76recnd 9152 . . . . . . . . . 10  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  ( g `  x )  e.  CC )
8 mulcl 9112 . . . . . . . . . 10  |-  ( ( _i  e.  CC  /\  ( g `  x
)  e.  CC )  ->  ( _i  x.  ( g `  x
) )  e.  CC )
94, 7, 8sylancr 646 . . . . . . . . 9  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  ( _i  x.  ( g `  x
) )  e.  CC )
10 addcl 9110 . . . . . . . . 9  |-  ( ( ( f `  x
)  e.  CC  /\  ( _i  x.  (
g `  x )
)  e.  CC )  ->  ( ( f `
 x )  +  ( _i  x.  (
g `  x )
) )  e.  CC )
113, 9, 10syl2an 465 . . . . . . . 8  |-  ( ( ( f  e.  dom  S.1 
/\  x  e.  RR )  /\  ( g  e. 
dom  S.1  /\  x  e.  RR ) )  -> 
( ( f `  x )  +  ( _i  x.  ( g `
 x ) ) )  e.  CC )
1211anandirs 806 . . . . . . 7  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  x  e.  RR )  ->  (
( f `  x
)  +  ( _i  x.  ( g `  x ) ) )  e.  CC )
13 reex 9119 . . . . . . . . 9  |-  RR  e.  _V
1413a1i 11 . . . . . . . 8  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  RR  e.  _V )
152adantlr 697 . . . . . . . 8  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  x  e.  RR )  ->  (
f `  x )  e.  RR )
16 ovex 6142 . . . . . . . . 9  |-  ( _i  x.  ( g `  x ) )  e. 
_V
1716a1i 11 . . . . . . . 8  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  x  e.  RR )  ->  (
_i  x.  ( g `  x ) )  e. 
_V )
181feqmptd 5815 . . . . . . . . 9  |-  ( f  e.  dom  S.1  ->  f  =  ( x  e.  RR  |->  ( f `  x ) ) )
1918adantr 453 . . . . . . . 8  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  f  =  ( x  e.  RR  |->  ( f `  x ) ) )
2013a1i 11 . . . . . . . . . 10  |-  ( g  e.  dom  S.1  ->  RR  e.  _V )
214a1i 11 . . . . . . . . . 10  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  _i  e.  CC )
22 fconstmpt 4956 . . . . . . . . . . 11  |-  ( RR 
X.  { _i }
)  =  ( x  e.  RR  |->  _i )
2322a1i 11 . . . . . . . . . 10  |-  ( g  e.  dom  S.1  ->  ( RR  X.  { _i } )  =  ( x  e.  RR  |->  _i ) )
245feqmptd 5815 . . . . . . . . . 10  |-  ( g  e.  dom  S.1  ->  g  =  ( x  e.  RR  |->  ( g `  x ) ) )
2520, 21, 6, 23, 24offval2 6358 . . . . . . . . 9  |-  ( g  e.  dom  S.1  ->  ( ( RR  X.  {
_i } )  o F  x.  g )  =  ( x  e.  RR  |->  ( _i  x.  ( g `  x
) ) ) )
2625adantl 454 . . . . . . . 8  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( ( RR 
X.  { _i }
)  o F  x.  g )  =  ( x  e.  RR  |->  ( _i  x.  ( g `
 x ) ) ) )
2714, 15, 17, 19, 26offval2 6358 . . . . . . 7  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( f  o F  +  ( ( RR  X.  { _i } )  o F  x.  g ) )  =  ( x  e.  RR  |->  ( ( f `
 x )  +  ( _i  x.  (
g `  x )
) ) ) )
28 absf 12179 . . . . . . . . 9  |-  abs : CC
--> RR
2928a1i 11 . . . . . . . 8  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  abs : CC --> RR )
3029feqmptd 5815 . . . . . . 7  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  abs  =  (
t  e.  CC  |->  ( abs `  t ) ) )
31 fveq2 5763 . . . . . . 7  |-  ( t  =  ( ( f `
 x )  +  ( _i  x.  (
g `  x )
) )  ->  ( abs `  t )  =  ( abs `  (
( f `  x
)  +  ( _i  x.  ( g `  x ) ) ) ) )
3212, 27, 30, 31fmptco 5937 . . . . . 6  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs  o.  ( f  o F  +  ( ( RR 
X.  { _i }
)  o F  x.  g ) ) )  =  ( x  e.  RR  |->  ( abs `  (
( f `  x
)  +  ( _i  x.  ( g `  x ) ) ) ) ) )
33 ftc1anclem3 26324 . . . . . 6  |-  ( ( 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 )
3432, 33eqeltrrd 2518 . . . . 5  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( x  e.  RR  |->  ( abs `  (
( f `  x
)  +  ( _i  x.  ( g `  x ) ) ) ) )  e.  dom  S.1 )
35 ioombl 19497 . . . . 5  |-  ( u (,) w )  e. 
dom  vol
36 fveq2 5763 . . . . . . . . . . . 12  |-  ( x  =  t  ->  (
f `  x )  =  ( f `  t ) )
37 fveq2 5763 . . . . . . . . . . . . 13  |-  ( x  =  t  ->  (
g `  x )  =  ( g `  t ) )
3837oveq2d 6133 . . . . . . . . . . . 12  |-  ( x  =  t  ->  (
_i  x.  ( g `  x ) )  =  ( _i  x.  (
g `  t )
) )
3936, 38oveq12d 6135 . . . . . . . . . . 11  |-  ( x  =  t  ->  (
( f `  x
)  +  ( _i  x.  ( g `  x ) ) )  =  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )
4039fveq2d 5767 . . . . . . . . . 10  |-  ( x  =  t  ->  ( abs `  ( ( f `
 x )  +  ( _i  x.  (
g `  x )
) ) )  =  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
41 eqid 2443 . . . . . . . . . 10  |-  ( x  e.  RR  |->  ( abs `  ( ( f `  x )  +  ( _i  x.  ( g `
 x ) ) ) ) )  =  ( x  e.  RR  |->  ( abs `  ( ( f `  x )  +  ( _i  x.  ( g `  x
) ) ) ) )
42 fvex 5773 . . . . . . . . . 10  |-  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) )  e.  _V
4340, 41, 42fvmpt 5842 . . . . . . . . 9  |-  ( t  e.  RR  ->  (
( x  e.  RR  |->  ( abs `  ( ( f `  x )  +  ( _i  x.  ( g `  x
) ) ) ) ) `  t )  =  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
4443eqcomd 2448 . . . . . . . 8  |-  ( t  e.  RR  ->  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  =  ( ( x  e.  RR  |->  ( abs `  (
( f `  x
)  +  ( _i  x.  ( g `  x ) ) ) ) ) `  t
) )
4544ifeq1d 3781 . . . . . . 7  |-  ( t  e.  RR  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  =  if ( t  e.  ( u (,) w ) ,  ( ( x  e.  RR  |->  ( abs `  ( ( f `  x )  +  ( _i  x.  ( g `  x
) ) ) ) ) `  t ) ,  0 ) )
4645mpteq2ia 4322 . . . . . 6  |-  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )  =  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( ( x  e.  RR  |->  ( abs `  (
( f `  x
)  +  ( _i  x.  ( g `  x ) ) ) ) ) `  t
) ,  0 ) )
4746i1fres 19633 . . . . 5  |-  ( ( ( x  e.  RR  |->  ( abs `  ( ( f `  x )  +  ( _i  x.  ( g `  x
) ) ) ) )  e.  dom  S.1  /\  ( u (,) w
)  e.  dom  vol )  ->  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) )  e.  dom  S.1 )
4834, 35, 47sylancl 645 . . . 4  |-  ( ( 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.  dom  S.1 )
49 breq2 4247 . . . . . . 7  |-  ( ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) )  =  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 )  -> 
( 0  <_  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  <->  0  <_  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )
50 breq2 4247 . . . . . . 7  |-  ( 0  =  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 )  -> 
( 0  <_  0  <->  0  <_  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) )
51 elioore 10984 . . . . . . . 8  |-  ( t  e.  ( u (,) w )  ->  t  e.  RR )
52 eleq1 2503 . . . . . . . . . . . 12  |-  ( x  =  t  ->  (
x  e.  RR  <->  t  e.  RR ) )
5352anbi2d 686 . . . . . . . . . . 11  |-  ( x  =  t  ->  (
( ( f  e. 
dom  S.1  /\  g  e. 
dom  S.1 )  /\  x  e.  RR )  <->  ( (
f  e.  dom  S.1  /\  g  e.  dom  S.1 )  /\  t  e.  RR ) ) )
5439eleq1d 2509 . . . . . . . . . . 11  |-  ( x  =  t  ->  (
( ( f `  x )  +  ( _i  x.  ( g `
 x ) ) )  e.  CC  <->  ( (
f `  t )  +  ( _i  x.  ( g `  t
) ) )  e.  CC ) )
5553, 54imbi12d 313 . . . . . . . . . 10  |-  ( x  =  t  ->  (
( ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  /\  x  e.  RR )  ->  ( ( f `
 x )  +  ( _i  x.  (
g `  x )
) )  e.  CC ) 
<->  ( ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) )  e.  CC ) ) )
5655, 12chvarv 1973 . . . . . . . . 9  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) )  e.  CC )
5756absge0d 12284 . . . . . . . 8  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  0  <_  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
5851, 57sylan2 462 . . . . . . 7  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  ( u (,) w
) )  ->  0  <_  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
59 0le0 10119 . . . . . . . 8  |-  0  <_  0
6059a1i 11 . . . . . . 7  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  -.  t  e.  ( u (,) w
) )  ->  0  <_  0 )
6149, 50, 58, 60ifbothda 3796 . . . . . 6  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  0  <_  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )
6261ralrimivw 2797 . . . . 5  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  A. t  e.  RR  0  <_  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) )
63 ax-resscn 9085 . . . . . . . 8  |-  RR  C_  CC
6463a1i 11 . . . . . . 7  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  RR  C_  CC )
65 c0ex 9123 . . . . . . . . . 10  |-  0  e.  _V
6642, 65ifex 3826 . . . . . . . . 9  |-  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 )  e.  _V
67 eqid 2443 . . . . . . . . 9  |-  ( 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 ) )
6866, 67fnmpti 5608 . . . . . . . 8  |-  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )  Fn  RR
6968a1i 11 . . . . . . 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 ) )  Fn  RR )
7064, 690pledm 19601 . . . . . 6  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( 0 p  o R  <_  (
t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )  <->  ( RR  X.  { 0 } )  o R  <_  (
t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) ) )
7165a1i 11 . . . . . . 7  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  0  e.  _V )
7266a1i 11 . . . . . . 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 )  e.  _V )
73 fconstmpt 4956 . . . . . . . 8  |-  ( RR 
X.  { 0 } )  =  ( t  e.  RR  |->  0 )
7473a1i 11 . . . . . . 7  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( RR  X.  { 0 } )  =  ( t  e.  RR  |->  0 ) )
75 eqidd 2444 . . . . . . 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 ) )  =  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) )
7614, 71, 72, 74, 75ofrfval2 6359 . . . . . 6  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( ( RR 
X.  { 0 } )  o R  <_ 
( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )  <->  A. t  e.  RR  0  <_  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) )
7770, 76bitrd 246 . . . . 5  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( 0 p  o R  <_  (
t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )  <->  A. t  e.  RR  0  <_  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) )
7862, 77mpbird 225 . . . 4  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  0 p  o R  <_  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) )
79 itg2itg1 19664 . . . . 5  |-  ( ( ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )  e.  dom  S.1  /\  0 p  o R  <_  ( 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
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )  =  ( S.1 `  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) ) )
80 itg1cl 19613 . . . . . 6  |-  ( ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )  e.  dom  S.1  ->  ( S.1 `  (
t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )  e.  RR )
8180adantr 453 . . . . 5  |-  ( ( ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )  e.  dom  S.1  /\  0 p  o R  <_  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ,  0 ) ) )  ->  ( S.1 `  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )  e.  RR )
8279, 81eqeltrd 2517 . . . 4  |-  ( ( ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) )  e.  dom  S.1  /\  0 p  o R  <_  ( 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
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )  e.  RR )
8348, 78, 82syl2anc 644 . . 3  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )  e.  RR )
8483ad6antlr 719 . 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 ) ) )  e.  RR )
85 simplll 736 . . . . 5  |-  ( ( ( ( ( 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 ) ) )
86 ftc1anc.a . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  A  e.  RR )
8786rexrd 9172 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  e.  RR* )
88 ftc1anc.b . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  B  e.  RR )
8988rexrd 9172 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  B  e.  RR* )
9087, 89jca 520 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( A  e.  RR*  /\  B  e.  RR* )
)
91 df-icc 10961 . . . . . . . . . . . . . . . . . . . . . 22  |-  [,]  =  ( x  e.  RR* ,  y  e.  RR*  |->  { t  e.  RR*  |  (
x  <_  t  /\  t  <_  y ) } )
9291elixx3g 10967 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  e.  ( A [,] B )  <->  ( ( A  e.  RR*  /\  B  e.  RR*  /\  u  e. 
RR* )  /\  ( A  <_  u  /\  u  <_  B ) ) )
9392simprbi 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  e.  ( A [,] B )  ->  ( A  <_  u  /\  u  <_  B ) )
9493simpld 447 . . . . . . . . . . . . . . . . . . 19  |-  ( u  e.  ( A [,] B )  ->  A  <_  u )
9591elixx3g 10967 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  ( A [,] B )  <->  ( ( A  e.  RR*  /\  B  e.  RR*  /\  w  e. 
RR* )  /\  ( A  <_  w  /\  w  <_  B ) ) )
9695simprbi 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  e.  ( A [,] B )  ->  ( A  <_  w  /\  w  <_  B ) )
9796simprd 451 . . . . . . . . . . . . . . . . . . 19  |-  ( w  e.  ( A [,] B )  ->  w  <_  B )
9894, 97anim12i 551 . . . . . . . . . . . . . . . . . 18  |-  ( ( u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) )  -> 
( A  <_  u  /\  w  <_  B ) )
99 df-ioo 10958 . . . . . . . . . . . . . . . . . . 19  |-  (,)  =  ( x  e.  RR* ,  y  e.  RR*  |->  { t  e.  RR*  |  (
x  <  t  /\  t  <  y ) } )
100 xrlelttr 10784 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  RR*  /\  u  e.  RR*  /\  z  e. 
RR* )  ->  (
( A  <_  u  /\  u  <  z )  ->  A  <  z
) )
101 xrltletr 10785 . . . . . . . . . . . . . . . . . . 19  |-  ( ( z  e.  RR*  /\  w  e.  RR*  /\  B  e. 
RR* )  ->  (
( z  <  w  /\  w  <_  B )  ->  z  <  B
) )
10299, 99, 100, 101ixxss12 10974 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <_  u  /\  w  <_  B ) )  ->  ( u (,) w )  C_  ( A (,) B ) )
10390, 98, 102syl2an 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  (
u (,) w ) 
C_  ( A (,) B ) )
104 ftc1anc.s . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( A (,) B
)  C_  D )
105104adantr 453 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  ( A (,) B )  C_  D )
106103, 105sstrd 3347 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  (
u (,) w ) 
C_  D )
1071063adantr3 1119 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B )  /\  u  <_  w
) )  ->  (
u (,) w ) 
C_  D )
108107sselda 3337 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w ) )  /\  t  e.  ( u (,) w ) )  -> 
t  e.  D )
109 ftc1anc.f . . . . . . . . . . . . . . . 16  |-  ( ph  ->  F : D --> CC )
110109ffvelrnda 5906 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  D )  ->  ( F `  t )  e.  CC )
111110adantlr 697 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w ) )  /\  t  e.  D )  ->  ( F `  t
)  e.  CC )
112108, 111syldan 458 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w ) )  /\  t  e.  ( u (,) w ) )  -> 
( F `  t
)  e.  CC )
113112adantllr 701 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w ) )  /\  t  e.  ( u (,) w ) )  -> 
( F `  t
)  e.  CC )
11456adantll 696 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  RR )  ->  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) )  e.  CC )
11551, 114sylan2 462 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  ( u (,) w
) )  ->  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) )  e.  CC )
116115adantlr 697 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w ) )  /\  t  e.  ( u (,) w ) )  -> 
( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) )  e.  CC )
117113, 116subcld 9449 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w ) )  /\  t  e.  ( u (,) w ) )  -> 
( ( F `  t )  -  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) )  e.  CC )
118117abscld 12276 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w ) )  /\  t  e.  ( u (,) w ) )  -> 
( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  e.  RR )
119118rexrd 9172 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w ) )  /\  t  e.  ( u (,) w ) )  -> 
( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  e.  RR* )
120117absge0d 12284 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w ) )  /\  t  e.  ( u (,) w ) )  -> 
0  <_  ( abs `  ( ( F `  t )  -  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ) )
121 elxrge0 11046 . . . . . . . . 9  |-  ( ( 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 )
) ) ) ) ) )
122119, 120, 121sylanbrc 647 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w ) )  /\  t  e.  ( u (,) w ) )  -> 
( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  e.  ( 0 [,]  +oo ) )
123 0xr 9169 . . . . . . . . . 10  |-  0  e.  RR*
124 elxrge0 11046 . . . . . . . . . 10  |-  ( 0  e.  ( 0 [,] 
+oo )  <->  ( 0  e.  RR*  /\  0  <_  0 ) )
125123, 59, 124mpbir2an 888 . . . . . . . . 9  |-  0  e.  ( 0 [,]  +oo )
126125a1i 11 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w ) )  /\  -.  t  e.  (
u (,) w ) )  ->  0  e.  ( 0 [,]  +oo ) )
127122, 126ifclda 3794 . . . . . . 7  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w ) )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 )  e.  ( 0 [,] 
+oo ) )
128127adantr 453 . . . . . 6  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w ) )  /\  t  e.  RR )  ->  if ( t  e.  ( u (,) w
) ,  ( abs `  ( ( F `  t )  -  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ) ,  0 )  e.  ( 0 [,]  +oo ) )
129 eqid 2443 . . . . . 6  |-  ( 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 ) )
130128, 129fmptd 5929 . . . . 5  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w ) )  -> 
( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) ) : RR --> ( 0 [,]  +oo ) )
13185, 130sylan 459 . . . 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+ )  /\  ( u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w ) )  -> 
( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) ) : RR --> ( 0 [,]  +oo ) )
132 rpre 10656 . . . . . 6  |-  ( y  e.  RR+  ->  y  e.  RR )
133132rehalfcld 10252 . . . . 5  |-  ( y  e.  RR+  ->  ( y  /  2 )  e.  RR )
134133ad2antlr 709 . . . 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+ )  /\  ( u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w ) )  -> 
( y  /  2
)  e.  RR )
135 simpll 732 . . . . . . . . 9  |-  ( ( ( ( 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
) )  /\  y  e.  RR+ )  ->  ( ph  /\  ( f  e. 
dom  S.1  /\  g  e. 
dom  S.1 ) ) )
136106sselda 3337 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  t  e.  D )
137136adantllr 701 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  t  e.  D )
138110adantlr 697 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  D )  ->  ( F `  t )  e.  CC )
139 ftc1anc.d . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  D  C_  RR )
140139sselda 3337 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  t  e.  D )  ->  t  e.  RR )
141140adantlr 697 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  D )  ->  t  e.  RR )
142141, 114syldan 458 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  D )  ->  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) )  e.  CC )
143138, 142subcld 9449 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  D )  ->  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) )  e.  CC )
144143abscld 12276 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  D )  ->  ( abs `  ( ( F `
 t )  -  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) )  e.  RR )
145144rexrd 9172 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  D )  ->  ( abs `  ( ( F `
 t )  -  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) )  e. 
RR* )
146145adantlr 697 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  D
)  ->  ( abs `  ( ( F `  t )  -  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  e.  RR* )
147137, 146syldan 458 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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* )
148143absge0d 12284 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  D )  ->  0  <_  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) )
149148adantlr 697 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  D
)  ->  0  <_  ( abs `  ( ( F `  t )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) ) )
150137, 149syldan 458 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
) ) ) ) )
151147, 150, 121sylanbrc 647 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
)
152125a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ) )
153151, 152ifclda 3794 . . . . . . . . . . . 12  |-  ( ( ( 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 ) )
154153adantr 453 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) )
155154, 129fmptd 5929 . . . . . . . . . 10  |-  ( ( ( 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 ) )
156 itg2cl 19660 . . . . . . . . . 10  |-  ( ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) ) : RR --> ( 0 [,]  +oo )  ->  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( F `  t )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) ) ,  0 ) ) )  e.  RR* )
157155, 156syl 16 . . . . . . . . 9  |-  ( ( ( 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
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) ) )  e.  RR* )
158135, 157sylan 459 . . . . . . . 8  |-  ( ( ( ( ( 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
) )  /\  y  e.  RR+ )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) ) )  e.  RR* )
159 0cn 9122 . . . . . . . . . . . . . . . . . 18  |-  0  e.  CC
160159a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  -.  t  e.  D )  ->  0  e.  CC )
161110, 160ifclda 3794 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  if ( t  e.  D ,  ( F `
 t ) ,  0 )  e.  CC )
162 subcl 9343 . . . . . . . . . . . . . . . 16  |-  ( ( if ( t  e.  D ,  ( F `
 t ) ,  0 )  e.  CC  /\  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) )  e.  CC )  ->  ( if ( t  e.  D , 
( F `  t
) ,  0 )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  e.  CC )
163161, 56, 162syl2an 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
f  e.  dom  S.1  /\  g  e.  dom  S.1 )  /\  t  e.  RR ) )  ->  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) )  e.  CC )
164163anassrs 631 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  RR )  ->  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) )  e.  CC )
165164abscld 12276 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  RR )  ->  ( abs `  ( if ( t  e.  D , 
( F `  t
) ,  0 )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) )  e.  RR )
166165rexrd 9172 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  RR )  ->  ( abs `  ( if ( t  e.  D , 
( F `  t
) ,  0 )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) )  e.  RR* )
167164absge0d 12284 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  RR )  ->  0  <_  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) )
168 elxrge0 11046 . . . . . . . . . . . 12  |-  ( ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  e.  ( 0 [,]  +oo )  <->  ( ( abs `  ( if ( t  e.  D , 
( F `  t
) ,  0 )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) )  e.  RR*  /\  0  <_  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ) )
169166, 167, 168sylanbrc 647 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  RR )  ->  ( abs `  ( if ( t  e.  D , 
( F `  t
) ,  0 )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) )  e.  ( 0 [,] 
+oo ) )
170 eqid 2443 . . . . . . . . . . 11  |-  ( t  e.  RR  |->  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ) )  =  ( t  e.  RR  |->  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) )
171169, 170fmptd 5929 . . . . . . . . . 10  |-  ( (
ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  -> 
( t  e.  RR  |->  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ) : RR --> ( 0 [,]  +oo ) )
172 itg2cl 19660 . . . . . . . . . 10  |-  ( ( t  e.  RR  |->  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ) : RR --> ( 0 [,]  +oo )  ->  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ) )  e. 
RR* )
173171, 172syl 16 . . . . . . . . 9  |-  ( (
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 ) ) ) ) ) ) )  e.  RR* )
174173ad3antrrr 712 . . . . . . . 8  |-  ( ( ( ( ( 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
) )  /\  y  e.  RR+ )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ) )  e. 
RR* )
175 rphalfcl 10674 . . . . . . . . . 10  |-  ( y  e.  RR+  ->  ( y  /  2 )  e.  RR+ )
176175rpxrd 10687 . . . . . . . . 9  |-  ( y  e.  RR+  ->  ( y  /  2 )  e. 
RR* )
177176ad2antlr 709 . . . . . . . 8  |-  ( ( ( ( ( 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
) )  /\  y  e.  RR+ )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( y  / 
2 )  e.  RR* )
178171adantr 453 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( t  e.  RR  |->  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ) : RR --> ( 0 [,]  +oo ) )
179 breq1 4246 . . . . . . . . . . . . 13  |-  ( ( abs `  ( ( F `  t )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) )  =  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( F `  t )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) ) ,  0 )  -> 
( ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  <_  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) )  <->  if (
t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 )  <_  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ) )
180 breq1 4246 . . . . . . . . . . . . 13  |-  ( 0  =  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( F `  t )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) ) ,  0 )  -> 
( 0  <_  ( abs `  ( if ( t  e.  D , 
( F `  t
) ,  0 )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) )  <-> 
if ( t  e.  ( u (,) w
) ,  ( abs `  ( ( F `  t )  -  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ) ,  0 )  <_  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ) ) )
181144leidd 9631 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  D )  ->  ( abs `  ( ( F `
 t )  -  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) )  <_ 
( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) )
182 iftrue 3773 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  e.  D  ->  if ( t  e.  D ,  ( F `  t ) ,  0 )  =  ( F `
 t ) )
183182oveq1d 6132 . . . . . . . . . . . . . . . . . . 19  |-  ( t  e.  D  ->  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) )  =  ( ( F `
 t )  -  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) )
184183fveq2d 5767 . . . . . . . . . . . . . . . . . 18  |-  ( t  e.  D  ->  ( abs `  ( if ( t  e.  D , 
( F `  t
) ,  0 )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) )  =  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) )
185184adantl 454 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  D )  ->  ( abs `  ( if ( t  e.  D , 
( F `  t
) ,  0 )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) )  =  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) )
186181, 185breqtrrd 4269 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  D )  ->  ( abs `  ( ( F `
 t )  -  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) )  <_ 
( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) )
187186adantlr 697 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  D
)  ->  ( abs `  ( ( F `  t )  -  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  <_  ( abs `  ( if ( t  e.  D , 
( F `  t
) ,  0 )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) ) )
188137, 187syldan 458 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 ) ) ) ) )  <_  ( abs `  ( if ( t  e.  D , 
( F `  t
) ,  0 )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) ) )
189188adantlr 697 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  RR )  /\  t  e.  ( u (,) w ) )  ->  ( abs `  ( ( F `  t )  -  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  <_  ( abs `  ( if ( t  e.  D , 
( F `  t
) ,  0 )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) ) )
190167adantlr 697 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  RR )  ->  0  <_  ( abs `  ( if ( t  e.  D , 
( F `  t
) ,  0 )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) ) )
191190adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  RR )  /\  -.  t  e.  ( u (,) w
) )  ->  0  <_  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) )
192179, 180, 189, 191ifbothda 3796 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )  <_ 
( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) )
193192ralrimiva 2796 . . . . . . . . . . 11  |-  ( ( ( 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
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 )  <_  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) )
19413a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  RR  e.  _V )
195 fvex 5773 . . . . . . . . . . . . . . 15  |-  ( abs `  ( ( F `  t )  -  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  e.  _V
196195, 65ifex 3826 . . . . . . . . . . . . . 14  |-  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 )  e.  _V
197196a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  RR )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 )  e.  _V )
198 fvex 5773 . . . . . . . . . . . . . 14  |-  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) )  e. 
_V
199198a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  RR )  ->  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) )  e. 
_V )
200 eqidd 2444 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 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 ) ) )
201 eqidd 2444 . . . . . . . . . . . . 13  |-  ( ph  ->  ( t  e.  RR  |->  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) )  =  ( t  e.  RR  |->  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ) )
202194, 197, 199, 200, 201ofrfval2 6359 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( F `  t )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) ) ,  0 ) )  o R  <_  (
t  e.  RR  |->  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) )  <->  A. t  e.  RR  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( F `  t )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) ) ,  0 )  <_ 
( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ) )
203202ad2antrr 708 . . . . . . . . . . 11  |-  ( ( ( 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 ) )  o R  <_ 
( t  e.  RR  |->  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) )  <->  A. t  e.  RR  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( F `  t )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) ) ,  0 )  <_ 
( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ) )
204193, 203mpbird 225 . . . . . . . . . 10  |-  ( ( ( 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 ) )  o R  <_  (
t  e.  RR  |->  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ) )
205 itg2le 19667 . . . . . . . . . 10  |-  ( ( ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) ) : RR --> ( 0 [,]  +oo )  /\  (
t  e.  RR  |->  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ) : RR --> ( 0 [,]  +oo )  /\  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( F `  t )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) ) ,  0 ) )  o R  <_  (
t  e.  RR  |->  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ) )  -> 
( S.2 `  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) ) )  <_  ( S.2 `  ( t  e.  RR  |->  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ) ) )
206155, 178, 204, 205syl3anc 1185 . . . . . . . . 9  |-  ( ( ( 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
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) ) )  <_  ( S.2 `  ( t  e.  RR  |->  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ) ) )
207135, 206sylan 459 . . . . . . . 8  |-  ( ( ( ( ( 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
) )  /\  y  e.  RR+ )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) ) )  <_  ( S.2 `  ( t  e.  RR  |->  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ) ) )
208 simpllr 737 . . . . . . . 8  |-  ( ( ( ( ( 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
) )  /\  y  e.  RR+ )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ) )  < 
( y  /  2
) )
209158, 174, 177, 207, 208xrlelttrd 10788 . . . . . . 7  |-  ( ( ( ( ( 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
) )  /\  y  e.  RR+ )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) ) )  <  (
y  /  2 ) )
210 xrltle 10780 . . . . . . . 8  |-  ( ( ( S.2 `  (
t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) ) )  e.  RR*  /\  ( y  /  2
)  e.  RR* )  ->  ( ( S.2 `  (
t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) ) )  <  (
y  /  2 )  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) ) )  <_  (
y  /  2 ) ) )
211158, 177, 210syl2anc 644 . . . . . . 7  |-  ( ( ( ( ( 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
) )  /\  y  e.  RR+ )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( ( S.2 `  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) ) )  <  (
y  /  2 )  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) ) )  <_  (
y  /  2 ) ) )
212209, 211mpd 15 . . . . . 6  |-  ( ( ( ( ( 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
) )  /\  y  e.  RR+ )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) ) )  <_  (
y  /  2 ) )
213212adantllr 701 . . . . 5  |-  ( ( ( ( ( (
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 ) ) )  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) ) )  <_  (
y  /  2 ) )
2142133adantr3 1119 . . . 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+ )  /\  ( u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w ) )  -> 
( S.2 `  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) ) )  <_  (
y  /  2 ) )
215 itg2lecl 19666 . . . 4  |-  ( ( ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) ) : RR --> ( 0 [,]  +oo )  /\  (
y  /  2 )  e.  RR  /\  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( F `  t )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) ) ,  0 ) ) )  <_  ( y  /  2 ) )  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) ) )  e.  RR )
216131, 134, 214, 215syl3anc 1185 . . 3  |-  ( ( ( ( ( (
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 ) )  -> 
( S.2 `  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) ) )  e.  RR )
217216adantr 453 . 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
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) ) )  e.  RR )
218133ad3antlr 713 . 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 ,  <  )
) ) )  -> 
( y  /  2
)  e.  RR )
21983adantr 453 . . . . . . . 8  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  E. r  e.  ( ran  f  u. 
ran  g ) r  =/=  0 )  -> 
( S.2 `  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )  e.  RR )
220 2rp 10655 . . . . . . . . 9  |-  2  e.  RR+
221 imassrn 5249 . . . . . . . . . . . . . . . 16  |-  ( abs " ( ran  f  u.  ran  g ) ) 
C_  ran  abs
222 frn 5632 . . . . . . . . . . . . . . . . 17  |-  ( abs
: CC --> RR  ->  ran 
abs  C_  RR )
22328, 222ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ran  abs  C_  RR
224221, 223sstri 3346 . . . . . . . . . . . . . . 15  |-  ( abs " ( ran  f  u.  ran  g ) ) 
C_  RR
225224a1i 11 . . . . . . . . . . . . . 14  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs " ( ran  f  u.  ran  g ) )  C_  RR )
226 frn 5632 . . . . . . . . . . . . . . . . . . . 20  |-  ( f : RR --> RR  ->  ran  f  C_  RR )
2271, 226syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( f  e.  dom  S.1  ->  ran  f  C_  RR )
228227adantr 453 . . . . . . . . . . . . . . . . . 18  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ran  f  C_  RR )
229 frn 5632 . . . . . . . . . . . . . . . . . . . 20  |-  ( g : RR --> RR  ->  ran  g  C_  RR )
2305, 229syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( g  e.  dom  S.1  ->  ran  g  C_  RR )
231230adantl 454 . . . . . . . . . . . . . . . . . 18  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ran  g  C_  RR )
232228, 231unssd 3512 . . . . . . . . . . . . . . . . 17  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( ran  f  u.  ran  g )  C_  RR )
233232, 63syl6ss 3349 . . . . . . . . . . . . . . . 16  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( ran  f  u.  ran  g )  C_  CC )
234 i1f0rn 19610 . . . . . . . . . . . . . . . . . 18  |-  ( f  e.  dom  S.1  ->  0  e.  ran  f )
235 elun1 3503 . . . . . . . . . . . . . . . . . 18  |-  ( 0  e.  ran  f  -> 
0  e.  ( ran  f  u.  ran  g
) )
236234, 235syl 16 . . . . . . . . . . . . . . . . 17  |-  ( f  e.  dom  S.1  ->  0  e.  ( ran  f  u.  ran  g ) )
237236adantr 453 . . . . . . . . . . . . . . . 16  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  0  e.  ( ran  f  u.  ran  g ) )
238 ffn 5626 . . . . . . . . . . . . . . . . . 18  |-  ( abs
: CC --> RR  ->  abs 
Fn  CC )
23928, 238ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  abs  Fn  CC
240 fnfvima 6012 . . . . . . . . . . . . . . . . 17  |-  ( ( abs  Fn  CC  /\  ( ran  f  u.  ran  g )  C_  CC  /\  0  e.  ( ran  f  u.  ran  g
) )  ->  ( abs `  0 )  e.  ( abs " ( ran  f  u.  ran  g ) ) )
241239, 240mp3an1 1267 . . . . . . . . . . . . . . . 16  |-  ( ( ( ran  f  u. 
ran  g )  C_  CC  /\  0  e.  ( ran  f  u.  ran  g ) )  -> 
( abs `  0
)  e.  ( abs " ( ran  f  u.  ran  g ) ) )
242233, 237, 241syl2anc 644 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs `  0
)  e.  ( abs " ( ran  f  u.  ran  g ) ) )
243 ne0i 3622 . . . . . . . . . . . . . . 15  |-  ( ( abs `  0 )  e.  ( abs " ( ran  f  u.  ran  g ) )  -> 
( abs " ( ran  f  u.  ran  g ) )  =/=  (/) )
244242, 243syl 16 . . . . . . . . . . . . . 14  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs " ( ran  f  u.  ran  g ) )  =/=  (/) )
245 ffun 5628 . . . . . . . . . . . . . . . . 17  |-  ( abs
: CC --> RR  ->  Fun 
abs )
24628, 245ax-mp 5 . . . . . . . . . . . . . . . 16  |-  Fun  abs
247 i1frn 19605 . . . . . . . . . . . . . . . . 17  |-  ( f  e.  dom  S.1  ->  ran  f  e.  Fin )
248 i1frn 19605 . . . . . . . . . . . . . . . . 17  |-  ( g  e.  dom  S.1  ->  ran  g  e.  Fin )
249 unfi 7410 . . . . . . . . . . . . . . . . 17  |-  ( ( ran  f  e.  Fin  /\ 
ran  g  e.  Fin )  ->  ( ran  f  u.  ran  g )  e. 
Fin )
250247, 248, 249syl2an 465 . . . . . . . . . . . . . . . 16  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( ran  f  u.  ran  g )  e. 
Fin )
251 imafi 7435 . . . . . . . . . . . . . . . 16  |-  ( ( Fun  abs  /\  ( ran  f  u.  ran  g )  e.  Fin )  ->  ( abs " ( ran  f  u.  ran  g ) )  e. 
Fin )
252246, 250, 251sylancr 646 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs " ( ran  f  u.  ran  g ) )  e. 
Fin )
253 fimaxre2 9994 . . . . . . . . . . . . . . 15  |-  ( ( ( abs " ( ran  f  u.  ran  g ) )  C_  RR  /\  ( abs " ( ran  f  u.  ran  g ) )  e. 
Fin )  ->  E. x  e.  RR  A. y  e.  ( abs " ( ran  f  u.  ran  g ) ) y  <_  x )
254224, 252, 253sylancr 646 . . . . . . . . . . . . . 14  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  E. x  e.  RR  A. y  e.  ( abs " ( ran  f  u.  ran  g ) ) y  <_  x )
255 suprcl 10006 . . . . . . . . . . . . . 14  |-  ( ( ( abs " ( ran  f  u.  ran  g ) )  C_  RR  /\  ( abs " ( ran  f  u.  ran  g ) )  =/=  (/)  /\  E. x  e.  RR  A. y  e.  ( abs " ( ran  f  u.  ran  g ) ) y  <_  x )  ->  sup ( ( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  )  e.  RR )
256225, 244, 254, 255syl3anc 1185 . . . . . . . . . . . . 13  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  sup ( ( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  )  e.  RR )
257256adantr 453 . . . . . . . . . . . 12  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  ( r  e.  ( ran  f  u.  ran  g )  /\  r  =/=  0 ) )  ->  sup ( ( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  )  e.  RR )
258 0re 9129 . . . . . . . . . . . . . 14  |-  0  e.  RR
259258a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  ( r  e.  ( ran  f  u.  ran  g )  /\  r  =/=  0 ) )  ->  0  e.  RR )
260233sselda 3337 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  r  e.  ( ran  f  u. 
ran  g ) )  ->  r  e.  CC )
261260abscld 12276 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  r  e.  ( ran  f  u. 
ran  g ) )  ->  ( abs `  r
)  e.  RR )
262261adantrr 699 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  ( r  e.  ( ran  f  u.  ran  g )  /\  r  =/=  0 ) )  ->  ( abs `  r
)  e.  RR )
263 absgt0 12166 . . . . . . . . . . . . . . . 16  |-  ( r  e.  CC  ->  (
r  =/=  0  <->  0  <  ( abs `  r
) ) )
264260, 263syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  r  e.  ( ran  f  u. 
ran  g ) )  ->  ( r  =/=  0  <->  0  <  ( abs `  r ) ) )
265264biimpa 472 . . . . . . . . . . . . . 14  |-  ( ( ( ( f  e. 
dom  S.1  /\  g  e. 
dom  S.1 )  /\  r  e.  ( ran  f  u. 
ran  g ) )  /\  r  =/=  0
)  ->  0  <  ( abs `  r ) )
266265anasss 630 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  ( r  e.  ( ran  f  u.  ran  g )  /\  r  =/=  0 ) )  ->  0  <  ( abs `  r ) )
267225, 244, 2543jca 1135 . . . . . . . . . . . . . . . 16  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( ( abs " ( ran  f  u.  ran  g ) ) 
C_  RR  /\  ( abs " ( ran  f  u.  ran  g ) )  =/=  (/)  /\  E. x  e.  RR  A. y  e.  ( abs " ( ran  f  u.  ran  g ) ) y  <_  x ) )
268267adantr 453 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  r  e.  ( ran  f  u. 
ran  g ) )  ->  ( ( abs " ( ran  f  u.  ran  g ) ) 
C_  RR  /\  ( abs " ( ran  f  u.  ran  g ) )  =/=  (/)  /\  E. x  e.  RR  A. y  e.  ( abs " ( ran  f  u.  ran  g ) ) y  <_  x ) )
269 fnfvima 6012 . . . . . . . . . . . . . . . . 17  |-  ( ( abs  Fn  CC  /\  ( ran  f  u.  ran  g )  C_  CC  /\  r  e.  ( ran  f  u.  ran  g
) )  ->  ( abs `  r )  e.  ( abs " ( ran  f  u.  ran  g ) ) )
270239, 269mp3an1 1267 . . . . . . . . . . . . . . . 16  |-  ( ( ( ran  f  u. 
ran  g )  C_  CC  /\  r  e.  ( ran  f  u.  ran  g ) )  -> 
( abs `  r
)  e.  ( abs " ( ran  f  u.  ran  g ) ) )
271233, 270sylan 459 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  r  e.  ( ran  f  u. 
ran  g ) )  ->  ( abs `  r
)  e.  ( abs " ( ran  f  u.  ran  g ) ) )
272 suprub 10007 . . . . . . . . . . . . . . 15  |-  ( ( ( ( abs " ( ran  f