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

Theorem ftc1anc 28418
Description: ftc1a 21478 holds for functions that obey the triangle inequality in the absence of ax-cc 8596. Theorem 565Ma of [Fremlin5] p. 220. (Contributed by Brendan Leahy, 11-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 )
ftc1anc.t  |-  ( ph  ->  A. s  e.  ( (,) " ( ( A [,] B )  X.  ( A [,] B ) ) ) ( abs `  S. s ( F `  t )  _d t )  <_  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  s ,  ( abs `  ( F `  t )
) ,  0 ) ) ) )
Assertion
Ref Expression
ftc1anc  |-  ( ph  ->  G  e.  ( ( A [,] B )
-cn-> CC ) )
Distinct variable groups:    t, s, x, A    B, s, t, x    D, s, t, x    F, s, t, x    ph, s,
t, x    G, s
Allowed substitution hints:    G( x, t)

Proof of Theorem ftc1anc
Dummy variables  a 
b  f  g  r  u  w  y  z are mutually distinct and 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, 8ftc1lem2 21477 . 2  |-  ( ph  ->  G : ( A [,] B ) --> CC )
10 rphalfcl 11007 . . . . . 6  |-  ( y  e.  RR+  ->  ( y  /  2 )  e.  RR+ )
111, 2, 3, 4, 5, 6, 7, 8ftc1anclem6 28415 . . . . . 6  |-  ( (
ph  /\  ( y  /  2 )  e.  RR+ )  ->  E. f  e.  dom  S.1 E. 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
) )
1210, 11sylan2 474 . . . . 5  |-  ( (
ph  /\  y  e.  RR+ )  ->  E. f  e.  dom  S.1 E. 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
) )
1312adantrl 715 . . . 4  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  y  e.  RR+ ) )  ->  E. f  e.  dom  S.1 E. 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
) )
1410ad2antll 728 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  y  e.  RR+ ) )  ->  (
y  /  2 )  e.  RR+ )
15 2rp 10988 . . . . . . . . . . . 12  |-  2  e.  RR+
16 i1ff 21123 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  e.  dom  S.1  ->  f : RR --> RR )
17 frn 5558 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f : RR --> RR  ->  ran  f  C_  RR )
1816, 17syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  e.  dom  S.1  ->  ran  f  C_  RR )
1918adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ran  f  C_  RR )
20 i1ff 21123 . . . . . . . . . . . . . . . . . . . . 21  |-  ( g  e.  dom  S.1  ->  g : RR --> RR )
21 frn 5558 . . . . . . . . . . . . . . . . . . . . 21  |-  ( g : RR --> RR  ->  ran  g  C_  RR )
2220, 21syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( g  e.  dom  S.1  ->  ran  g  C_  RR )
2322adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ran  g  C_  RR )
2419, 23unssd 3525 . . . . . . . . . . . . . . . . . 18  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( ran  f  u.  ran  g )  C_  RR )
25 ax-resscn 9331 . . . . . . . . . . . . . . . . . 18  |-  RR  C_  CC
2624, 25syl6ss 3361 . . . . . . . . . . . . . . . . 17  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( ran  f  u.  ran  g )  C_  CC )
27 i1f0rn 21129 . . . . . . . . . . . . . . . . . . 19  |-  ( f  e.  dom  S.1  ->  0  e.  ran  f )
28 elun1 3516 . . . . . . . . . . . . . . . . . . 19  |-  ( 0  e.  ran  f  -> 
0  e.  ( ran  f  u.  ran  g
) )
2927, 28syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( f  e.  dom  S.1  ->  0  e.  ( ran  f  u.  ran  g ) )
3029adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  0  e.  ( ran  f  u.  ran  g ) )
31 absf 12817 . . . . . . . . . . . . . . . . . . 19  |-  abs : CC
--> RR
32 ffn 5552 . . . . . . . . . . . . . . . . . . 19  |-  ( abs
: CC --> RR  ->  abs 
Fn  CC )
3331, 32ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  abs  Fn  CC
34 fnfvima 5948 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) ) )
3533, 34mp3an1 1301 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ran  f  u. 
ran  g )  C_  CC  /\  0  e.  ( ran  f  u.  ran  g ) )  -> 
( abs `  0
)  e.  ( abs " ( ran  f  u.  ran  g ) ) )
3626, 30, 35syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs `  0
)  e.  ( abs " ( ran  f  u.  ran  g ) ) )
37 ne0i 3636 . . . . . . . . . . . . . . . 16  |-  ( ( abs `  0 )  e.  ( abs " ( ran  f  u.  ran  g ) )  -> 
( abs " ( ran  f  u.  ran  g ) )  =/=  (/) )
3836, 37syl 16 . . . . . . . . . . . . . . 15  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs " ( ran  f  u.  ran  g ) )  =/=  (/) )
39 imassrn 5173 . . . . . . . . . . . . . . . . 17  |-  ( abs " ( ran  f  u.  ran  g ) ) 
C_  ran  abs
40 frn 5558 . . . . . . . . . . . . . . . . . 18  |-  ( abs
: CC --> RR  ->  ran 
abs  C_  RR )
4131, 40ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ran  abs  C_  RR
4239, 41sstri 3358 . . . . . . . . . . . . . . . 16  |-  ( abs " ( ran  f  u.  ran  g ) ) 
C_  RR
43 ffun 5554 . . . . . . . . . . . . . . . . . 18  |-  ( abs
: CC --> RR  ->  Fun 
abs )
4431, 43ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  Fun  abs
45 i1frn 21124 . . . . . . . . . . . . . . . . . 18  |-  ( f  e.  dom  S.1  ->  ran  f  e.  Fin )
46 i1frn 21124 . . . . . . . . . . . . . . . . . 18  |-  ( g  e.  dom  S.1  ->  ran  g  e.  Fin )
47 unfi 7571 . . . . . . . . . . . . . . . . . 18  |-  ( ( ran  f  e.  Fin  /\ 
ran  g  e.  Fin )  ->  ( ran  f  u.  ran  g )  e. 
Fin )
4845, 46, 47syl2an 477 . . . . . . . . . . . . . . . . 17  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( ran  f  u.  ran  g )  e. 
Fin )
49 imafi 7596 . . . . . . . . . . . . . . . . 17  |-  ( ( Fun  abs  /\  ( ran  f  u.  ran  g )  e.  Fin )  ->  ( abs " ( ran  f  u.  ran  g ) )  e. 
Fin )
5044, 48, 49sylancr 663 . . . . . . . . . . . . . . . 16  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs " ( ran  f  u.  ran  g ) )  e. 
Fin )
51 fimaxre2 10270 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 )
5242, 50, 51sylancr 663 . . . . . . . . . . . . . . 15  |-  ( ( 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 )
53 suprcl 10282 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 )
5442, 53mp3an1 1301 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 )
5538, 52, 54syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  sup ( ( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  )  e.  RR )
5655adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  E. r  e.  ( ran  f  u. 
ran  g ) r  =/=  0 )  ->  sup ( ( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  )  e.  RR )
57 0re 9378 . . . . . . . . . . . . . . . . 17  |-  0  e.  RR
5857a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  ( r  e.  ( ran  f  u.  ran  g )  /\  r  =/=  0 ) )  ->  0  e.  RR )
5926sselda 3349 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  r  e.  ( ran  f  u. 
ran  g ) )  ->  r  e.  CC )
6059abscld 12914 . . . . . . . . . . . . . . . . 17  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  r  e.  ( ran  f  u. 
ran  g ) )  ->  ( abs `  r
)  e.  RR )
6160adantrr 716 . . . . . . . . . . . . . . . 16  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  ( r  e.  ( ran  f  u.  ran  g )  /\  r  =/=  0 ) )  ->  ( abs `  r
)  e.  RR )
6255adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 )
63 absgt0 12804 . . . . . . . . . . . . . . . . . . 19  |-  ( r  e.  CC  ->  (
r  =/=  0  <->  0  <  ( abs `  r
) ) )
6459, 63syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  r  e.  ( ran  f  u. 
ran  g ) )  ->  ( r  =/=  0  <->  0  <  ( abs `  r ) ) )
6564biimpd 207 . . . . . . . . . . . . . . . . 17  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  r  e.  ( ran  f  u. 
ran  g ) )  ->  ( r  =/=  0  ->  0  <  ( abs `  r ) ) )
6665impr 619 . . . . . . . . . . . . . . . 16  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  ( r  e.  ( ran  f  u.  ran  g )  /\  r  =/=  0 ) )  ->  0  <  ( abs `  r ) )
6742a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( abs " ( ran  f  u.  ran  g ) )  C_  RR )
6867, 38, 523jca 1168 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 ) )
6968adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 ) )
70 fnfvima 5948 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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 ) ) )
7133, 70mp3an1 1301 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ran  f  u. 
ran  g )  C_  CC  /\  r  e.  ( ran  f  u.  ran  g ) )  -> 
( abs `  r
)  e.  ( abs " ( ran  f  u.  ran  g ) ) )
7226, 71sylan 471 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 ) ) )
73 suprub 10283 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 )  /\  ( abs `  r )  e.  ( abs " ( ran  f  u.  ran  g ) ) )  ->  ( abs `  r
)  <_  sup (
( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  )
)
7469, 72, 73syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  r  e.  ( ran  f  u. 
ran  g ) )  ->  ( abs `  r
)  <_  sup (
( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  )
)
7574adantrr 716 . . . . . . . . . . . . . . . 16  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  ( r  e.  ( ran  f  u.  ran  g )  /\  r  =/=  0 ) )  ->  ( abs `  r
)  <_  sup (
( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  )
)
7658, 61, 62, 66, 75ltletrd 9523 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  ( r  e.  ( ran  f  u.  ran  g )  /\  r  =/=  0 ) )  ->  0  <  sup ( ( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  )
)
7776rexlimdvaa 2836 . . . . . . . . . . . . . 14  |-  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  ->  ( E. r  e.  ( ran  f  u. 
ran  g ) r  =/=  0  ->  0  <  sup ( ( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  ) ) )
7877imp 429 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  E. r  e.  ( ran  f  u. 
ran  g ) r  =/=  0 )  -> 
0  <  sup (
( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  )
)
7956, 78elrpd 11017 . . . . . . . . . . . 12  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  E. r  e.  ( ran  f  u. 
ran  g ) r  =/=  0 )  ->  sup ( ( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  )  e.  RR+ )
80 rpmulcl 11004 . . . . . . . . . . . 12  |-  ( ( 2  e.  RR+  /\  sup ( ( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  )  e.  RR+ )  ->  (
2  x.  sup (
( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  )
)  e.  RR+ )
8115, 79, 80sylancr 663 . . . . . . . . . . 11  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  E. r  e.  ( ran  f  u. 
ran  g ) r  =/=  0 )  -> 
( 2  x.  sup ( ( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  )
)  e.  RR+ )
82 rpdivcl 11005 . . . . . . . . . . 11  |-  ( ( ( y  /  2
)  e.  RR+  /\  (
2  x.  sup (
( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  )
)  e.  RR+ )  ->  ( ( y  / 
2 )  /  (
2  x.  sup (
( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  )
) )  e.  RR+ )
8314, 81, 82syl2an 477 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  y  e.  RR+ ) )  /\  ( ( f  e.  dom  S.1  /\  g  e.  dom  S.1 )  /\  E. r  e.  ( ran  f  u.  ran  g ) r  =/=  0 ) )  -> 
( ( y  / 
2 )  /  (
2  x.  sup (
( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  )
) )  e.  RR+ )
8483anassrs 648 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( u  e.  ( A [,] B )  /\  y  e.  RR+ ) )  /\  ( f  e. 
dom  S.1  /\  g  e. 
dom  S.1 ) )  /\  E. r  e.  ( ran  f  u.  ran  g
) r  =/=  0
)  ->  ( (
y  /  2 )  /  ( 2  x. 
sup ( ( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  ) ) )  e.  RR+ )
8584adantlr 714 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  ( u  e.  ( A [,] B )  /\  y  e.  RR+ ) )  /\  (
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  /  2 )  / 
( 2  x.  sup ( ( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  )
) )  e.  RR+ )
86 ancom 450 . . . . . . . . . . . 12  |-  ( ( u  e.  ( A [,] B )  /\  y  e.  RR+ )  <->  ( y  e.  RR+  /\  u  e.  ( A [,] B
) ) )
8786anbi2i 694 . . . . . . . . . . 11  |-  ( ( ( ( ( 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 )  /\  ( u  e.  ( A [,] B
)  /\  y  e.  RR+ ) )  <->  ( (
( ( 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 ) ) ) )
88 an32 796 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  y  e.  RR+ ) )  /\  ( f  e. 
dom  S.1  /\  g  e. 
dom  S.1 ) )  <->  ( ( ph  /\  ( f  e. 
dom  S.1  /\  g  e. 
dom  S.1 ) )  /\  ( u  e.  ( A [,] B )  /\  y  e.  RR+ ) ) )
8988anbi1i 695 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( u  e.  ( A [,] B )  /\  y  e.  RR+ ) )  /\  ( 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 ) )  <-> 
( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  y  e.  RR+ ) )  /\  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ) )  < 
( y  /  2
) ) )
90 an32 796 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  y  e.  RR+ ) )  /\  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( if ( t  e.  D ,  ( F `  t ) ,  0 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ) )  < 
( y  /  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
) )  /\  (
u  e.  ( A [,] B )  /\  y  e.  RR+ ) ) )
9189, 90bitri 249 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( u  e.  ( A [,] B )  /\  y  e.  RR+ ) )  /\  ( 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 ) )  <-> 
( ( ( 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
) )  /\  (
u  e.  ( A [,] B )  /\  y  e.  RR+ ) ) )
9291anbi1i 695 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  ( u  e.  ( A [,] B )  /\  y  e.  RR+ ) )  /\  (
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 )  <-> 
( ( ( (
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 ) )  /\  ( u  e.  ( A [,] B
)  /\  y  e.  RR+ ) )  /\  E. r  e.  ( ran  f  u.  ran  g ) r  =/=  0 ) )
93 an32 796 . . . . . . . . . . . 12  |-  ( ( ( ( ( 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
) )  /\  (
u  e.  ( A [,] B )  /\  y  e.  RR+ ) )  /\  E. r  e.  ( ran  f  u. 
ran  g ) r  =/=  0 )  <->  ( (
( ( 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 )  /\  ( u  e.  ( A [,] B
)  /\  y  e.  RR+ ) ) )
9492, 93bitri 249 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  ( u  e.  ( A [,] B )  /\  y  e.  RR+ ) )  /\  (
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 )  <-> 
( ( ( (
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 )  /\  ( u  e.  ( A [,] B )  /\  y  e.  RR+ ) ) )
95 anass 649 . . . . . . . . . . 11  |-  ( ( ( ( ( (
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 ) )  <->  ( (
( ( 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 ) ) ) )
9687, 94, 953bitr4i 277 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  ( u  e.  ( A [,] B )  /\  y  e.  RR+ ) )  /\  (
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 )  <-> 
( ( ( ( ( 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 ) ) )
97 oveq12 6095 . . . . . . . . . . . . . . . 16  |-  ( ( b  =  w  /\  a  =  u )  ->  ( b  -  a
)  =  ( w  -  u ) )
9897ancoms 453 . . . . . . . . . . . . . . 15  |-  ( ( a  =  u  /\  b  =  w )  ->  ( b  -  a
)  =  ( w  -  u ) )
9998fveq2d 5688 . . . . . . . . . . . . . 14  |-  ( ( a  =  u  /\  b  =  w )  ->  ( abs `  (
b  -  a ) )  =  ( abs `  ( w  -  u
) ) )
10099breq1d 4295 . . . . . . . . . . . . 13  |-  ( ( a  =  u  /\  b  =  w )  ->  ( ( abs `  (
b  -  a ) )  <  ( ( y  /  2 )  /  ( 2  x. 
sup ( ( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  ) ) )  <->  ( abs `  ( w  -  u
) )  <  (
( y  /  2
)  /  ( 2  x.  sup ( ( abs " ( ran  f  u.  ran  g
) ) ,  RR ,  <  ) ) ) ) )
101 fveq2 5684 . . . . . . . . . . . . . . . 16  |-  ( b  =  w  ->  ( G `  b )  =  ( G `  w ) )
102 fveq2 5684 . . . . . . . . . . . . . . . 16  |-  ( a  =  u  ->  ( G `  a )  =  ( G `  u ) )
103101, 102oveqan12rd 6106 . . . . . . . . . . . . . . 15  |-  ( ( a  =  u  /\  b  =  w )  ->  ( ( G `  b )  -  ( G `  a )
)  =  ( ( G `  w )  -  ( G `  u ) ) )
104103fveq2d 5688 . . . . . . . . . . . . . 14  |-  ( ( a  =  u  /\  b  =  w )  ->  ( abs `  (
( G `  b
)  -  ( G `
 a ) ) )  =  ( abs `  ( ( G `  w )  -  ( G `  u )
) ) )
105104breq1d 4295 . . . . . . . . . . . . 13  |-  ( ( a  =  u  /\  b  =  w )  ->  ( ( abs `  (
( G `  b
)  -  ( G `
 a ) ) )  <  y  <->  ( abs `  ( ( G `  w )  -  ( G `  u )
) )  <  y
) )
106100, 105imbi12d 320 . . . . . . . . . . . 12  |-  ( ( a  =  u  /\  b  =  w )  ->  ( ( ( abs `  ( b  -  a
) )  <  (
( y  /  2
)  /  ( 2  x.  sup ( ( abs " ( ran  f  u.  ran  g
) ) ,  RR ,  <  ) ) )  ->  ( abs `  (
( G `  b
)  -  ( G `
 a ) ) )  <  y )  <-> 
( ( abs `  (
w  -  u ) )  <  ( ( y  /  2 )  /  ( 2  x. 
sup ( ( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  ) ) )  ->  ( abs `  ( ( G `
 w )  -  ( G `  u ) ) )  <  y
) ) )
107 oveq12 6095 . . . . . . . . . . . . . . . 16  |-  ( ( b  =  u  /\  a  =  w )  ->  ( b  -  a
)  =  ( u  -  w ) )
108107ancoms 453 . . . . . . . . . . . . . . 15  |-  ( ( a  =  w  /\  b  =  u )  ->  ( b  -  a
)  =  ( u  -  w ) )
109108fveq2d 5688 . . . . . . . . . . . . . 14  |-  ( ( a  =  w  /\  b  =  u )  ->  ( abs `  (
b  -  a ) )  =  ( abs `  ( u  -  w
) ) )
110109breq1d 4295 . . . . . . . . . . . . 13  |-  ( ( a  =  w  /\  b  =  u )  ->  ( ( abs `  (
b  -  a ) )  <  ( ( y  /  2 )  /  ( 2  x. 
sup ( ( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  ) ) )  <->  ( abs `  ( u  -  w
) )  <  (
( y  /  2
)  /  ( 2  x.  sup ( ( abs " ( ran  f  u.  ran  g
) ) ,  RR ,  <  ) ) ) ) )
111 fveq2 5684 . . . . . . . . . . . . . . . 16  |-  ( b  =  u  ->  ( G `  b )  =  ( G `  u ) )
112 fveq2 5684 . . . . . . . . . . . . . . . 16  |-  ( a  =  w  ->  ( G `  a )  =  ( G `  w ) )
113111, 112oveqan12rd 6106 . . . . . . . . . . . . . . 15  |-  ( ( a  =  w  /\  b  =  u )  ->  ( ( G `  b )  -  ( G `  a )
)  =  ( ( G `  u )  -  ( G `  w ) ) )
114113fveq2d 5688 . . . . . . . . . . . . . 14  |-  ( ( a  =  w  /\  b  =  u )  ->  ( abs `  (
( G `  b
)  -  ( G `
 a ) ) )  =  ( abs `  ( ( G `  u )  -  ( G `  w )
) ) )
115114breq1d 4295 . . . . . . . . . . . . 13  |-  ( ( a  =  w  /\  b  =  u )  ->  ( ( abs `  (
( G `  b
)  -  ( G `
 a ) ) )  <  y  <->  ( abs `  ( ( G `  u )  -  ( G `  w )
) )  <  y
) )
116110, 115imbi12d 320 . . . . . . . . . . . 12  |-  ( ( a  =  w  /\  b  =  u )  ->  ( ( ( abs `  ( b  -  a
) )  <  (
( y  /  2
)  /  ( 2  x.  sup ( ( abs " ( ran  f  u.  ran  g
) ) ,  RR ,  <  ) ) )  ->  ( abs `  (
( G `  b
)  -  ( G `
 a ) ) )  <  y )  <-> 
( ( abs `  (
u  -  w ) )  <  ( ( y  /  2 )  /  ( 2  x. 
sup ( ( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  ) ) )  ->  ( abs `  ( ( G `
 u )  -  ( G `  w ) ) )  <  y
) ) )
117 iccssre 11369 . . . . . . . . . . . . . 14  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A [,] B
)  C_  RR )
1182, 3, 117syl2anc 661 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A [,] B
)  C_  RR )
119118ad4antr 731 . . . . . . . . . . . 12  |-  ( ( ( ( ( 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+ )  ->  ( A [,] B )  C_  RR )
120 simp-4l 765 . . . . . . . . . . . . 13  |-  ( ( ( ( ( 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 )
121118, 25syl6ss 3361 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( A [,] B
)  C_  CC )
122121sselda 3349 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  w  e.  ( A [,] B ) )  ->  w  e.  CC )
123121sselda 3349 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( A [,] B ) )  ->  u  e.  CC )
124 abssub 12806 . . . . . . . . . . . . . . . . 17  |-  ( ( w  e.  CC  /\  u  e.  CC )  ->  ( abs `  (
w  -  u ) )  =  ( abs `  ( u  -  w
) ) )
125122, 123, 124syl2anr 478 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  u  e.  ( A [,] B
) )  /\  ( ph  /\  w  e.  ( A [,] B ) ) )  ->  ( abs `  ( w  -  u ) )  =  ( abs `  (
u  -  w ) ) )
126125anandis 826 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  ( abs `  ( w  -  u ) )  =  ( abs `  (
u  -  w ) ) )
127126breq1d 4295 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  (
( abs `  (
w  -  u ) )  <  ( ( y  /  2 )  /  ( 2  x. 
sup ( ( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  ) ) )  <->  ( abs `  ( u  -  w
) )  <  (
( y  /  2
)  /  ( 2  x.  sup ( ( abs " ( ran  f  u.  ran  g
) ) ,  RR ,  <  ) ) ) ) )
1289ffvelrnda 5836 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  w  e.  ( A [,] B ) )  ->  ( G `  w )  e.  CC )
1299ffvelrnda 5836 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( A [,] B ) )  ->  ( G `  u )  e.  CC )
130 abssub 12806 . . . . . . . . . . . . . . . . 17  |-  ( ( ( G `  w
)  e.  CC  /\  ( G `  u )  e.  CC )  -> 
( abs `  (
( G `  w
)  -  ( G `
 u ) ) )  =  ( abs `  ( ( G `  u )  -  ( G `  w )
) ) )
131128, 129, 130syl2anr 478 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  u  e.  ( A [,] B
) )  /\  ( ph  /\  w  e.  ( A [,] B ) ) )  ->  ( abs `  ( ( G `
 w )  -  ( G `  u ) ) )  =  ( abs `  ( ( G `  u )  -  ( G `  w ) ) ) )
132131anandis 826 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  ( abs `  ( ( G `
 w )  -  ( G `  u ) ) )  =  ( abs `  ( ( G `  u )  -  ( G `  w ) ) ) )
133132breq1d 4295 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  (
( abs `  (
( G `  w
)  -  ( G `
 u ) ) )  <  y  <->  ( abs `  ( ( G `  u )  -  ( G `  w )
) )  <  y
) )
134127, 133imbi12d 320 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  (
( ( abs `  (
w  -  u ) )  <  ( ( y  /  2 )  /  ( 2  x. 
sup ( ( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  ) ) )  ->  ( abs `  ( ( G `
 w )  -  ( G `  u ) ) )  <  y
)  <->  ( ( abs `  ( u  -  w
) )  <  (
( y  /  2
)  /  ( 2  x.  sup ( ( abs " ( ran  f  u.  ran  g
) ) ,  RR ,  <  ) ) )  ->  ( abs `  (
( G `  u
)  -  ( G `
 w ) ) )  <  y ) ) )
135120, 134sylan 471 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
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 ) ) )  ->  ( ( ( abs `  ( w  -  u ) )  <  ( ( y  /  2 )  / 
( 2  x.  sup ( ( abs " ( ran  f  u.  ran  g ) ) ,  RR ,  <  )
) )  ->  ( abs `  ( ( G `
 w )  -  ( G `  u ) ) )  <  y
)  <->  ( ( abs `  ( u  -  w
) )  <  (
( y  /  2
)  /  ( 2  x.  sup ( ( abs " ( ran  f  u.  ran  g
) ) ,  RR ,  <  ) ) )  ->  ( abs `  (
( G `  u
)  -  ( G `
 w ) ) )  <  y ) ) )
1362rexrd 9425 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  A  e.  RR* )
1373rexrd 9425 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  B  e.  RR* )
138136, 137jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( A  e.  RR*  /\  B  e.  RR* )
)
139 df-icc 11299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  [,]  =  ( x  e.  RR* ,  y  e.  RR*  |->  { t  e.  RR*  |  (
x  <_  t  /\  t  <_  y ) } )
140139elixx3g 11305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( u  e.  ( A [,] B )  <->  ( ( A  e.  RR*  /\  B  e.  RR*  /\  u  e. 
RR* )  /\  ( A  <_  u  /\  u  <_  B ) ) )
141140simprbi 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( u  e.  ( A [,] B )  ->  ( A  <_  u  /\  u  <_  B ) )
142141simpld 459 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( u  e.  ( A [,] B )  ->  A  <_  u )
143139elixx3g 11305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( w  e.  ( A [,] B )  <->  ( ( A  e.  RR*  /\  B  e.  RR*  /\  w  e. 
RR* )  /\  ( A  <_  w  /\  w  <_  B ) ) )
144143simprbi 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w  e.  ( A [,] B )  ->  ( A  <_  w  /\  w  <_  B ) )
145144simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( w  e.  ( A [,] B )  ->  w  <_  B )
146142, 145anim12i 566 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) )  -> 
( A  <_  u  /\  w  <_  B ) )
147 df-ioo 11296 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  (,)  =  ( x  e.  RR* ,  y  e.  RR*  |->  { t  e.  RR*  |  (
x  <  t  /\  t  <  y ) } )
148 xrlelttr 11122 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( A  e.  RR*  /\  u  e.  RR*  /\  z  e. 
RR* )  ->  (
( A  <_  u  /\  u  <  z )  ->  A  <  z
) )
149 xrltletr 11123 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( z  e.  RR*  /\  w  e.  RR*  /\  B  e. 
RR* )  ->  (
( z  <  w  /\  w  <_  B )  ->  z  <  B
) )
150147, 147, 148, 149ixxss12 11312 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <_  u  /\  w  <_  B ) )  ->  ( u (,) w )  C_  ( A (,) B ) )
151138, 146, 150syl2an 477 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  (
u (,) w ) 
C_  ( A (,) B ) )
1525adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  ( A (,) B )  C_  D )
153151, 152sstrd 3359 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  (
u (,) w ) 
C_  D )
154153sselda 3349 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  t  e.  D )
1558ffvelrnda 5836 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  t  e.  D )  ->  ( F `  t )  e.  CC )
156155abscld 12914 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  t  e.  D )  ->  ( abs `  ( F `  t ) )  e.  RR )
157156rexrd 9425 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  t  e.  D )  ->  ( abs `  ( F `  t ) )  e. 
RR* )
158155absge0d 12922 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  t  e.  D )  ->  0  <_  ( abs `  ( F `  t )
) )
159 elxrge0 11386 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( abs `  ( F `
 t ) )  e.  ( 0 [,] +oo )  <->  ( ( abs `  ( F `  t
) )  e.  RR*  /\  0  <_  ( abs `  ( F `  t
) ) ) )
160157, 158, 159sylanbrc 664 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  t  e.  D )  ->  ( abs `  ( F `  t ) )  e.  ( 0 [,] +oo ) )
161160adantlr 714 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  D
)  ->  ( abs `  ( F `  t
) )  e.  ( 0 [,] +oo )
)
162154, 161syldan 470 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  ( abs `  ( F `  t
) )  e.  ( 0 [,] +oo )
)
163 0e0iccpnf 11388 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  ( 0 [,] +oo )
164163a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  -.  t  e.  ( u (,) w
) )  ->  0  e.  ( 0 [,] +oo ) )
165162, 164ifclda 3814 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( F `  t )
) ,  0 )  e.  ( 0 [,] +oo ) )
166165adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  RR )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( F `
 t ) ) ,  0 )  e.  ( 0 [,] +oo ) )
167 eqid 2437 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( F `  t )
) ,  0 ) )  =  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( F `  t )
) ,  0 ) )
168166, 167fmptd 5860 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  (
t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( F `  t )
) ,  0 ) ) : RR --> ( 0 [,] +oo ) )
169 itg2cl 21179 . . . . . . . . . . . . . . . . . . 19  |-  ( ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( F `  t )
) ,  0 ) ) : RR --> ( 0 [,] +oo )  -> 
( S.2 `  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( F `  t )
) ,  0 ) ) )  e.  RR* )
170168, 169syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B ) ) )  ->  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( F `
 t ) ) ,  0 ) ) )  e.  RR* )
1711703adantr3 1149 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( u  e.  ( A [,] B
)  /\  w  e.  ( A [,] B )  /\  u  <_  w
) )  ->  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( F `
 t ) ) ,  0 ) ) )  e.  RR* )
172120, 171sylan 471 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
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 )
) ,  0 ) ) )  e.  RR* )
173172adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( 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 )
) ,  0 ) ) )  e.  RR* )
174 simplll 757 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( 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 ) ) )
175155adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  D
)  ->  ( F `  t )  e.  CC )
176154, 175syldan 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B ) ) )  /\  t  e.  ( u (,) w ) )  ->  ( F `  t )  e.  CC )
177176adantllr 718 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( 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 )
178 elioore 11322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( t  e.  ( u (,) w )  ->  t  e.  RR )
17916ffvelrnda 5836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( f `  t )  e.  RR )
180179recnd 9404 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( f  e.  dom  S.1  /\  t  e.  RR )  ->  ( f `  t )  e.  CC )
181 ax-icn 9333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  _i  e.  CC
18220ffvelrnda 5836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  e.  RR )
183182recnd 9404 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  e.  CC )
184 mulcl 9358 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( _i  e.  CC  /\  ( g `  t
)  e.  CC )  ->  ( _i  x.  ( g `  t
) )  e.  CC )
185181, 183, 184sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( _i  x.  ( g `  t
) )  e.  CC )
186 addcl 9356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( f `  t
)  e.  CC  /\  ( _i  x.  (
g `  t )
)  e.  CC )  ->  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) )  e.  CC )
187180, 185, 186syl2an 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( f  e.  dom  S.1 
/\  t  e.  RR )  /\  ( g  e. 
dom  S.1  /\  t  e.  RR ) )  -> 
( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) )  e.  CC )
188187anandirs 827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) )  e.  CC )
189178, 188sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  ( u (,) w
) )  ->  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) )  e.  CC )
190189adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  ( u (,) w
) )  ->  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) )  e.  CC )
191190adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( 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 )
192177, 191subcld 9711 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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 )
193192abscld 12914 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 )
194189abscld 12914 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  ( u (,) w
) )  ->  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  e.  RR )
195194adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  ( u (,) w
) )  ->  ( abs `  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  e.  RR )
196195adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 ) ) ) )  e.  RR )
197193, 196readdcld 9405 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  e.  RR )
198197rexrd 9425 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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 `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  e.  RR* )
199192absge0d 12922 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 )
) ) ) ) )
200188absge0d 12922 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  0  <_  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
201178, 200sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( f  e.  dom  S.1 
/\  g  e.  dom  S.1 )  /\  t  e.  ( u (,) w
) )  ->  0  <_  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
202201adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  t  e.  ( u (,) w
) )  ->  0  <_  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )
203202adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 )  +  ( _i  x.  ( g `  t
) ) ) ) )
204193, 196, 199, 203addge0d 9907 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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
) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ) )
205 elxrge0 11386 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) )  e.  ( 0 [,] +oo ) 
<->  ( ( ( abs `  ( ( F `  t )  -  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  e.  RR*  /\  0  <_  ( ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ) ) )
206198, 204, 205sylanbrc 664 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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 `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  e.  ( 0 [,] +oo )
)
207163a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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 ) )
208206, 207ifclda 3814 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 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
) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ) ,  0 )  e.  ( 0 [,] +oo )
)
209208adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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
) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ) ,  0 )  e.  ( 0 [,] +oo )
)
210 eqid 2437 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 ) )  =  ( 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 ) )
211209, 210fmptd 5860 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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
) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ) ,  0 ) ) : RR --> ( 0 [,] +oo ) )
212 itg2cl 21179 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 ) ) : RR --> ( 0 [,] +oo )  -> 
( 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 ) ) )  e.  RR* )
213211, 212syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 ) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) ) )  e.  RR* )
2142133adantr3 1149 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
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
) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ) ,  0 ) ) )  e.  RR* )
215174, 214sylan 471 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
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
) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ) ,  0 ) ) )  e.  RR* )
216215adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( 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 ) ) )  e.  RR* )
217 rpxr 10990 . . . . . . . . . . . . . . . 16  |-  ( y  e.  RR+  ->  y  e. 
RR* )
218217ad3antlr 730 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( 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  e.  RR* )
219165adantlr 714 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 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 ) ) ,  0 )  e.  ( 0 [,] +oo ) )
220219adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 ) ) ,  0 )  e.  ( 0 [,] +oo ) )
221220, 167fmptd 5860 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 ) ) ,  0 ) ) : RR --> ( 0 [,] +oo ) )
222177, 191npcand 9715 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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
) ) ) )  +  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) )  =  ( F `  t
) )
223222fveq2d 5688 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 ) ) ) )  +  ( ( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  =  ( abs `  ( F `
 t ) ) )
224192, 191abstrid 12934 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 ) ) ) )  +  ( ( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  <_  (
( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ) )
225223, 224eqbrtrrd 4307 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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
) )  <_  (
( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ) )
226 iftrue 3790 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  e.  ( u (,) w )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( F `  t )
) ,  0 )  =  ( abs `  ( F `  t )
) )
227226adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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.  ( u (,) w ) ,  ( abs `  ( F `  t )
) ,  0 )  =  ( abs `  ( F `  t )
) )
228 iftrue 3790 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  e.  ( u (,) w )  ->  if ( t  e.  ( u (,) w ) ,  ( ( abs `  ( ( F `  t )  -  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 )  =  ( ( abs `  ( ( F `  t )  -  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) )
229228adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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.  ( u (,) w ) ,  ( ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ) ,  0 )  =  ( ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ) )
230225, 227, 2293brtr4d 4315 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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.  ( u (,) w ) ,  ( abs `  ( F `  t )
) ,  0 )  <_  if ( t  e.  ( u (,) w ) ,  ( ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ) ,  0 ) )
231230ex 434 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 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.  ( u (,) w ) ,  ( abs `  ( F `  t )
) ,  0 )  <_  if ( t  e.  ( u (,) w ) ,  ( ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ) ,  0 ) ) )
232 0le0 10403 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  0  <_  0
233232a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  t  e.  ( u (,) w )  -> 
0  <_  0 )
234 iffalse 3792 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  t  e.  ( u (,) w )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( F `  t )
) ,  0 )  =  0 )
235 iffalse 3792 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  t  e.  ( u (,) w )  ->  if ( t  e.  ( u (,) w ) ,  ( ( abs `  ( ( F `  t )  -  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 )  =  0 )
236233, 234, 2353brtr4d 4315 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( -.  t  e.  ( u (,) w )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( F `  t )
) ,  0 )  <_  if ( t  e.  ( u (,) w ) ,  ( ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ) ,  0 ) )
237231, 236pm2.61d1 159 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 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 ) ) ,  0 )  <_  if ( t  e.  ( u (,) w ) ,  ( ( abs `  ( ( F `  t )  -  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) ) ,  0 ) )
238237ralrimivw 2794 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 )
) ,  0 )  <_  if ( t  e.  ( u (,) w ) ,  ( ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ) ,  0 ) )
239 reex 9365 . . . . . . . . . . . . . . . . . . . . . . 23  |-  RR  e.  _V
240239a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  RR  e.  _V )
241 fvex 5694 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( abs `  ( F `  t
) )  e.  _V
242 c0ex 9372 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  0  e.  _V
243241, 242ifex 3851 . . . . . . . . . . . . . . . . . . . . . . 23  |-  if ( t  e.  ( u (,) w ) ,  ( abs `  ( F `  t )
) ,  0 )  e.  _V
244243a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  t  e.  RR )  ->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( F `  t )
) ,  0 )  e.  _V )
245 ovex 6111 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( abs `  ( ( F `  t )  -  ( ( f `
 t )  +  ( _i  x.  (
g `  t )
) ) ) )  +  ( abs `  (
( f `  t
)  +  ( _i  x.  ( g `  t ) ) ) ) )  e.  _V
246245, 242ifex 3851 . . . . . . . . . . . . . . . . . . . . . . 23  |-  if ( t  e.  ( u (,) w ) ,  ( ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ) ,  0 )  e.  _V
247246a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  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 )  e.  _V )
248 eqidd 2438 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( F `  t )
) ,  0 ) )  =  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( F `  t )
) ,  0 ) ) )
249 eqidd 2438 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( 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 ) )  =  ( 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 ) ) )
250240, 244, 247, 248, 249ofrfval2 6332 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( F `
 t ) ) ,  0 ) )  oR  <_  (
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 ) )  <->  A. t  e.  RR  if ( t  e.  ( u (,) w ) ,  ( abs `  ( F `  t )
) ,  0 )  <_  if ( t  e.  ( u (,) w ) ,  ( ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ) ,  0 ) ) )
251250ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 )
) ,  0 ) )  oR  <_ 
( 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 ) )  <->  A. t  e.  RR  if ( t  e.  ( u (,) w ) ,  ( abs `  ( F `  t )
) ,  0 )  <_  if ( t  e.  ( u (,) w ) ,  ( ( abs `  (
( F `  t
)  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `
 t ) ) ) ) ) ,  0 ) ) )
252238, 251mpbird 232 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 ) ) ,  0 ) )  oR  <_  (
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 ) ) )
253 itg2le 21186 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( F `  t )
) ,  0 ) ) : RR --> ( 0 [,] +oo )  /\  ( 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 ) ) : RR --> ( 0 [,] +oo )  /\  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( F `  t )
) ,  0 ) )  oR  <_ 
( 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 ) ) )  ->  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( F `
 t ) ) ,  0 ) ) )  <_  ( 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 ) ) ) )
254221, 211, 252, 253syl3anc 1218 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 )
) ,  0 ) ) )  <_  ( 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 ) ) ) )
2552543adantr3 1149 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  (
u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w ) )  -> 
( S.2 `  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( F `  t )
) ,  0 ) ) )  <_  ( 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 ) ) ) )
256174, 255sylan 471 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
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 )
) ,  0 ) ) )  <_  ( 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 ) ) ) )
257256adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( 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 )
) ,  0 ) ) )  <_  ( 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 ) ) ) )
2581, 2, 3, 4, 5, 6, 7, 8ftc1anclem8 28417 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( 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 (
(