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

Theorem itg2gt0cn 26159
Description: itg2gt0 19605 holds on functions continuous on an open interval in the absence of ax-cc 8271. The fourth hypothesis is made unnecessary by the continuity hypothesis. (Contributed by Brendan Leahy, 16-Nov-2017.)
Hypotheses
Ref Expression
itg2gt0cn.2  |-  ( ph  ->  X  <  Y )
itg2gt0cn.3  |-  ( ph  ->  F : RR --> ( 0 [,)  +oo ) )
itg2gt0cn.5  |-  ( (
ph  /\  x  e.  ( X (,) Y ) )  ->  0  <  ( F `  x ) )
itg2gt0cn.cn  |-  ( ph  ->  ( F  |`  ( X (,) Y ) )  e.  ( ( X (,) Y ) -cn-> CC ) )
Assertion
Ref Expression
itg2gt0cn  |-  ( ph  ->  0  <  ( S.2 `  F ) )
Distinct variable groups:    x, X    x, Y    x, F    ph, x

Proof of Theorem itg2gt0cn
Dummy variables  y 
z  w  u  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0xr 9087 . . . 4  |-  0  e.  RR*
21a1i 11 . . 3  |-  ( ph  ->  0  e.  RR* )
3 imassrn 5175 . . . . 5  |-  ( F
" ( X (,) Y ) )  C_  ran  F
4 itg2gt0cn.3 . . . . . . 7  |-  ( ph  ->  F : RR --> ( 0 [,)  +oo ) )
5 frn 5556 . . . . . . 7  |-  ( F : RR --> ( 0 [,)  +oo )  ->  ran  F 
C_  ( 0 [,) 
+oo ) )
64, 5syl 16 . . . . . 6  |-  ( ph  ->  ran  F  C_  (
0 [,)  +oo ) )
7 icossxr 10951 . . . . . 6  |-  ( 0 [,)  +oo )  C_  RR*
86, 7syl6ss 3320 . . . . 5  |-  ( ph  ->  ran  F  C_  RR* )
93, 8syl5ss 3319 . . . 4  |-  ( ph  ->  ( F " ( X (,) Y ) ) 
C_  RR* )
10 supxrcl 10849 . . . 4  |-  ( ( F " ( X (,) Y ) ) 
C_  RR*  ->  sup (
( F " ( X (,) Y ) ) ,  RR* ,  <  )  e.  RR* )
119, 10syl 16 . . 3  |-  ( ph  ->  sup ( ( F
" ( X (,) Y ) ) , 
RR* ,  <  )  e. 
RR* )
12 itg2gt0cn.2 . . . . . 6  |-  ( ph  ->  X  <  Y )
13 ltrelxr 9095 . . . . . . . . . 10  |-  <  C_  ( RR*  X.  RR* )
1413ssbri 4214 . . . . . . . . 9  |-  ( X  <  Y  ->  X
( RR*  X.  RR* ) Y )
1512, 14syl 16 . . . . . . . 8  |-  ( ph  ->  X ( RR*  X.  RR* ) Y )
16 brxp 4868 . . . . . . . 8  |-  ( X ( RR*  X.  RR* ) Y 
<->  ( X  e.  RR*  /\  Y  e.  RR* )
)
1715, 16sylib 189 . . . . . . 7  |-  ( ph  ->  ( X  e.  RR*  /\  Y  e.  RR* )
)
18 ioon0 10898 . . . . . . 7  |-  ( ( X  e.  RR*  /\  Y  e.  RR* )  ->  (
( X (,) Y
)  =/=  (/)  <->  X  <  Y ) )
1917, 18syl 16 . . . . . 6  |-  ( ph  ->  ( ( X (,) Y )  =/=  (/)  <->  X  <  Y ) )
2012, 19mpbird 224 . . . . 5  |-  ( ph  ->  ( X (,) Y
)  =/=  (/) )
21 itg2gt0cn.5 . . . . . 6  |-  ( (
ph  /\  x  e.  ( X (,) Y ) )  ->  0  <  ( F `  x ) )
2221ralrimiva 2749 . . . . 5  |-  ( ph  ->  A. x  e.  ( X (,) Y ) 0  <  ( F `
 x ) )
23 r19.2z 3677 . . . . 5  |-  ( ( ( X (,) Y
)  =/=  (/)  /\  A. x  e.  ( X (,) Y ) 0  < 
( F `  x
) )  ->  E. x  e.  ( X (,) Y
) 0  <  ( F `  x )
)
2420, 22, 23syl2anc 643 . . . 4  |-  ( ph  ->  E. x  e.  ( X (,) Y ) 0  <  ( F `
 x ) )
25 supxrlub 10860 . . . . . 6  |-  ( ( ( F " ( X (,) Y ) ) 
C_  RR*  /\  0  e. 
RR* )  ->  (
0  <  sup (
( F " ( X (,) Y ) ) ,  RR* ,  <  )  <->  E. y  e.  ( F
" ( X (,) Y ) ) 0  <  y ) )
269, 1, 25sylancl 644 . . . . 5  |-  ( ph  ->  ( 0  <  sup ( ( F "
( X (,) Y
) ) ,  RR* ,  <  )  <->  E. y  e.  ( F " ( X (,) Y ) ) 0  <  y ) )
27 ffn 5550 . . . . . . 7  |-  ( F : RR --> ( 0 [,)  +oo )  ->  F  Fn  RR )
284, 27syl 16 . . . . . 6  |-  ( ph  ->  F  Fn  RR )
29 ioossre 10928 . . . . . 6  |-  ( X (,) Y )  C_  RR
30 breq2 4176 . . . . . . 7  |-  ( y  =  ( F `  x )  ->  (
0  <  y  <->  0  <  ( F `  x ) ) )
3130rexima 5936 . . . . . 6  |-  ( ( F  Fn  RR  /\  ( X (,) Y ) 
C_  RR )  -> 
( E. y  e.  ( F " ( X (,) Y ) ) 0  <  y  <->  E. x  e.  ( X (,) Y
) 0  <  ( F `  x )
) )
3228, 29, 31sylancl 644 . . . . 5  |-  ( ph  ->  ( E. y  e.  ( F " ( X (,) Y ) ) 0  <  y  <->  E. x  e.  ( X (,) Y
) 0  <  ( F `  x )
) )
3326, 32bitrd 245 . . . 4  |-  ( ph  ->  ( 0  <  sup ( ( F "
( X (,) Y
) ) ,  RR* ,  <  )  <->  E. x  e.  ( X (,) Y
) 0  <  ( F `  x )
) )
3424, 33mpbird 224 . . 3  |-  ( ph  ->  0  <  sup (
( F " ( X (,) Y ) ) ,  RR* ,  <  )
)
35 qbtwnxr 10742 . . 3  |-  ( ( 0  e.  RR*  /\  sup ( ( F "
( X (,) Y
) ) ,  RR* ,  <  )  e.  RR*  /\  0  <  sup (
( F " ( X (,) Y ) ) ,  RR* ,  <  )
)  ->  E. y  e.  QQ  ( 0  < 
y  /\  y  <  sup ( ( F "
( X (,) Y
) ) ,  RR* ,  <  ) ) )
362, 11, 34, 35syl3anc 1184 . 2  |-  ( ph  ->  E. y  e.  QQ  ( 0  <  y  /\  y  <  sup (
( F " ( X (,) Y ) ) ,  RR* ,  <  )
) )
37 qre 10535 . . . . . . . . 9  |-  ( y  e.  QQ  ->  y  e.  RR )
3837adantr 452 . . . . . . . 8  |-  ( ( y  e.  QQ  /\  0  <  y )  -> 
y  e.  RR )
39 simpr 448 . . . . . . . 8  |-  ( ( y  e.  QQ  /\  0  <  y )  -> 
0  <  y )
4038, 39elrpd 10602 . . . . . . 7  |-  ( ( y  e.  QQ  /\  0  <  y )  -> 
y  e.  RR+ )
4140anim1i 552 . . . . . 6  |-  ( ( ( y  e.  QQ  /\  0  <  y )  /\  y  <  sup ( ( F "
( X (,) Y
) ) ,  RR* ,  <  ) )  -> 
( y  e.  RR+  /\  y  <  sup (
( F " ( X (,) Y ) ) ,  RR* ,  <  )
) )
4241anasss 629 . . . . 5  |-  ( ( y  e.  QQ  /\  ( 0  <  y  /\  y  <  sup (
( F " ( X (,) Y ) ) ,  RR* ,  <  )
) )  ->  (
y  e.  RR+  /\  y  <  sup ( ( F
" ( X (,) Y ) ) , 
RR* ,  <  ) ) )
43 simplr 732 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  y  <  sup ( ( F
" ( X (,) Y ) ) , 
RR* ,  <  ) )  ->  y  e.  RR+ )
44 rpxr 10575 . . . . . . . . . . 11  |-  ( y  e.  RR+  ->  y  e. 
RR* )
45 supxrlub 10860 . . . . . . . . . . 11  |-  ( ( ( F " ( X (,) Y ) ) 
C_  RR*  /\  y  e. 
RR* )  ->  (
y  <  sup (
( F " ( X (,) Y ) ) ,  RR* ,  <  )  <->  E. z  e.  ( F
" ( X (,) Y ) ) y  <  z ) )
469, 44, 45syl2an 464 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  RR+ )  ->  ( y  <  sup ( ( F
" ( X (,) Y ) ) , 
RR* ,  <  )  <->  E. z  e.  ( F " ( X (,) Y ) ) y  <  z ) )
47 breq2 4176 . . . . . . . . . . . . 13  |-  ( z  =  ( F `  x )  ->  (
y  <  z  <->  y  <  ( F `  x ) ) )
4847rexima 5936 . . . . . . . . . . . 12  |-  ( ( F  Fn  RR  /\  ( X (,) Y ) 
C_  RR )  -> 
( E. z  e.  ( F " ( X (,) Y ) ) y  <  z  <->  E. x  e.  ( X (,) Y
) y  <  ( F `  x )
) )
4928, 29, 48sylancl 644 . . . . . . . . . . 11  |-  ( ph  ->  ( E. z  e.  ( F " ( X (,) Y ) ) y  <  z  <->  E. x  e.  ( X (,) Y
) y  <  ( F `  x )
) )
5049adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  RR+ )  ->  ( E. z  e.  ( F " ( X (,) Y
) ) y  < 
z  <->  E. x  e.  ( X (,) Y ) y  <  ( F `
 x ) ) )
5146, 50bitrd 245 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  RR+ )  ->  ( y  <  sup ( ( F
" ( X (,) Y ) ) , 
RR* ,  <  )  <->  E. x  e.  ( X (,) Y
) y  <  ( F `  x )
) )
52 itg2gt0cn.cn . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( F  |`  ( X (,) Y ) )  e.  ( ( X (,) Y ) -cn-> CC ) )
5352ad3antrrr 711 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( ( F  |`  ( X (,) Y
) ) `  x
) )  ->  ( F  |`  ( X (,) Y ) )  e.  ( ( X (,) Y ) -cn-> CC ) )
54 simplr 732 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( ( F  |`  ( X (,) Y
) ) `  x
) )  ->  x  e.  ( X (,) Y
) )
55 fssres 5569 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F : RR --> ( 0 [,)  +oo )  /\  ( X (,) Y )  C_  RR )  ->  ( F  |`  ( X (,) Y
) ) : ( X (,) Y ) --> ( 0 [,)  +oo ) )
5629, 55mpan2 653 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F : RR --> ( 0 [,)  +oo )  ->  ( F  |`  ( X (,) Y ) ) : ( X (,) Y
) --> ( 0 [,) 
+oo ) )
57 elrege0 10963 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( 0 [,) 
+oo )  <->  ( x  e.  RR  /\  0  <_  x ) )
5857simplbi 447 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  ( 0 [,) 
+oo )  ->  x  e.  RR )
5958ssriv 3312 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 0 [,)  +oo )  C_  RR
60 fss 5558 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( F  |`  ( X (,) Y ) ) : ( X (,) Y ) --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  RR )  ->  ( F  |`  ( X (,) Y
) ) : ( X (,) Y ) --> RR )
6159, 60mpan2 653 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F  |`  ( X (,) Y ) ) : ( X (,) Y
) --> ( 0 [,) 
+oo )  ->  ( F  |`  ( X (,) Y ) ) : ( X (,) Y
) --> RR )
624, 56, 613syl 19 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( F  |`  ( X (,) Y ) ) : ( X (,) Y ) --> RR )
6362adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  y  e.  RR+ )  ->  ( F  |`  ( X (,) Y
) ) : ( X (,) Y ) --> RR )
6463ffvelrnda 5829 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  ->  (
( F  |`  ( X (,) Y ) ) `
 x )  e.  RR )
65 rpre 10574 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  RR+  ->  y  e.  RR )
6665ad2antlr 708 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  ->  y  e.  RR )
6764, 66resubcld 9421 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  ->  (
( ( F  |`  ( X (,) Y ) ) `  x )  -  y )  e.  RR )
6867adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( ( F  |`  ( X (,) Y
) ) `  x
) )  ->  (
( ( F  |`  ( X (,) Y ) ) `  x )  -  y )  e.  RR )
6966, 64posdifd 9569 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  ->  (
y  <  ( ( F  |`  ( X (,) Y ) ) `  x )  <->  0  <  ( ( ( F  |`  ( X (,) Y ) ) `  x )  -  y ) ) )
7069biimpa 471 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( ( F  |`  ( X (,) Y
) ) `  x
) )  ->  0  <  ( ( ( F  |`  ( X (,) Y
) ) `  x
)  -  y ) )
7168, 70elrpd 10602 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( ( F  |`  ( X (,) Y
) ) `  x
) )  ->  (
( ( F  |`  ( X (,) Y ) ) `  x )  -  y )  e.  RR+ )
72 cncfi 18877 . . . . . . . . . . . . . . . 16  |-  ( ( ( F  |`  ( X (,) Y ) )  e.  ( ( X (,) Y ) -cn-> CC )  /\  x  e.  ( X (,) Y
)  /\  ( (
( F  |`  ( X (,) Y ) ) `
 x )  -  y )  e.  RR+ )  ->  E. z  e.  RR+  A. u  e.  ( X (,) Y ) ( ( abs `  (
u  -  x ) )  <  z  -> 
( abs `  (
( ( F  |`  ( X (,) Y ) ) `  u )  -  ( ( F  |`  ( X (,) Y
) ) `  x
) ) )  < 
( ( ( F  |`  ( X (,) Y
) ) `  x
)  -  y ) ) )
7353, 54, 71, 72syl3anc 1184 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( ( F  |`  ( X (,) Y
) ) `  x
) )  ->  E. z  e.  RR+  A. u  e.  ( X (,) Y
) ( ( abs `  ( u  -  x
) )  <  z  ->  ( abs `  (
( ( F  |`  ( X (,) Y ) ) `  u )  -  ( ( F  |`  ( X (,) Y
) ) `  x
) ) )  < 
( ( ( F  |`  ( X (,) Y
) ) `  x
)  -  y ) ) )
7473ex 424 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  ->  (
y  <  ( ( F  |`  ( X (,) Y ) ) `  x )  ->  E. z  e.  RR+  A. u  e.  ( X (,) Y
) ( ( abs `  ( u  -  x
) )  <  z  ->  ( abs `  (
( ( F  |`  ( X (,) Y ) ) `  u )  -  ( ( F  |`  ( X (,) Y
) ) `  x
) ) )  < 
( ( ( F  |`  ( X (,) Y
) ) `  x
)  -  y ) ) ) )
75 fvres 5704 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( X (,) Y )  ->  (
( F  |`  ( X (,) Y ) ) `
 x )  =  ( F `  x
) )
7675breq2d 4184 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( X (,) Y )  ->  (
y  <  ( ( F  |`  ( X (,) Y ) ) `  x )  <->  y  <  ( F `  x ) ) )
7776adantl 453 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  ->  (
y  <  ( ( F  |`  ( X (,) Y ) ) `  x )  <->  y  <  ( F `  x ) ) )
78 fvres 5704 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  e.  ( X (,) Y )  ->  (
( F  |`  ( X (,) Y ) ) `
 u )  =  ( F `  u
) )
7978adantl 453 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  u  e.  ( X (,) Y ) )  -> 
( ( F  |`  ( X (,) Y ) ) `  u )  =  ( F `  u ) )
8075ad2antlr 708 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  u  e.  ( X (,) Y ) )  -> 
( ( F  |`  ( X (,) Y ) ) `  x )  =  ( F `  x ) )
8179, 80oveq12d 6058 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  u  e.  ( X (,) Y ) )  -> 
( ( ( F  |`  ( X (,) Y
) ) `  u
)  -  ( ( F  |`  ( X (,) Y ) ) `  x ) )  =  ( ( F `  u )  -  ( F `  x )
) )
8281fveq2d 5691 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  u  e.  ( X (,) Y ) )  -> 
( abs `  (
( ( F  |`  ( X (,) Y ) ) `  u )  -  ( ( F  |`  ( X (,) Y
) ) `  x
) ) )  =  ( abs `  (
( F `  u
)  -  ( F `
 x ) ) ) )
8375oveq1d 6055 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( X (,) Y )  ->  (
( ( F  |`  ( X (,) Y ) ) `  x )  -  y )  =  ( ( F `  x )  -  y
) )
8483ad2antlr 708 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  u  e.  ( X (,) Y ) )  -> 
( ( ( F  |`  ( X (,) Y
) ) `  x
)  -  y )  =  ( ( F `
 x )  -  y ) )
8582, 84breq12d 4185 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  u  e.  ( X (,) Y ) )  -> 
( ( abs `  (
( ( F  |`  ( X (,) Y ) ) `  u )  -  ( ( F  |`  ( X (,) Y
) ) `  x
) ) )  < 
( ( ( F  |`  ( X (,) Y
) ) `  x
)  -  y )  <-> 
( abs `  (
( F `  u
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )
8685imbi2d 308 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  u  e.  ( X (,) Y ) )  -> 
( ( ( abs `  ( u  -  x
) )  <  z  ->  ( abs `  (
( ( F  |`  ( X (,) Y ) ) `  u )  -  ( ( F  |`  ( X (,) Y
) ) `  x
) ) )  < 
( ( ( F  |`  ( X (,) Y
) ) `  x
)  -  y ) )  <->  ( ( abs `  ( u  -  x
) )  <  z  ->  ( abs `  (
( F `  u
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) ) )
8786ralbidva 2682 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  ->  ( A. u  e.  ( X (,) Y ) ( ( abs `  (
u  -  x ) )  <  z  -> 
( abs `  (
( ( F  |`  ( X (,) Y ) ) `  u )  -  ( ( F  |`  ( X (,) Y
) ) `  x
) ) )  < 
( ( ( F  |`  ( X (,) Y
) ) `  x
)  -  y ) )  <->  A. u  e.  ( X (,) Y ) ( ( abs `  (
u  -  x ) )  <  z  -> 
( abs `  (
( F `  u
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) ) )
8887rexbidv 2687 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  ->  ( E. z  e.  RR+  A. u  e.  ( X (,) Y
) ( ( abs `  ( u  -  x
) )  <  z  ->  ( abs `  (
( ( F  |`  ( X (,) Y ) ) `  u )  -  ( ( F  |`  ( X (,) Y
) ) `  x
) ) )  < 
( ( ( F  |`  ( X (,) Y
) ) `  x
)  -  y ) )  <->  E. z  e.  RR+  A. u  e.  ( X (,) Y ) ( ( abs `  (
u  -  x ) )  <  z  -> 
( abs `  (
( F `  u
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) ) )
8974, 77, 883imtr3d 259 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  ->  (
y  <  ( F `  x )  ->  E. z  e.  RR+  A. u  e.  ( X (,) Y
) ( ( abs `  ( u  -  x
) )  <  z  ->  ( abs `  (
( F `  u
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) ) )
9089imp 419 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x ) )  ->  E. z  e.  RR+  A. u  e.  ( X (,) Y
) ( ( abs `  ( u  -  x
) )  <  z  ->  ( abs `  (
( F `  u
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )
911a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  A. u  e.  ( X (,) Y ) ( ( abs `  ( u  -  x ) )  <  z  ->  ( abs `  ( ( F `
 u )  -  ( F `  x ) ) )  <  (
( F `  x
)  -  y ) ) )  ->  0  e.  RR* )
92 ioorp 10944 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0 (,)  +oo )  =  RR+
93 ioossicc 10952 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0 (,)  +oo )  C_  (
0 [,]  +oo )
9492, 93eqsstr3i 3339 . . . . . . . . . . . . . . . . . . . . 21  |-  RR+  C_  (
0 [,]  +oo )
9594sseli 3304 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  RR+  ->  y  e.  ( 0 [,]  +oo ) )
96 0le0 10037 . . . . . . . . . . . . . . . . . . . . 21  |-  0  <_  0
97 elxrge0 10964 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 0  e.  ( 0 [,] 
+oo )  <->  ( 0  e.  RR*  /\  0  <_  0 ) )
981, 96, 97mpbir2an 887 . . . . . . . . . . . . . . . . . . . 20  |-  0  e.  ( 0 [,]  +oo )
99 ifcl 3735 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( y  e.  ( 0 [,]  +oo )  /\  0  e.  ( 0 [,]  +oo ) )  ->  if ( w  e.  (
( X (,) Y
)  i^i  ( (
x  -  z ) (,) ( z  +  x ) ) ) ,  y ,  0 )  e.  ( 0 [,]  +oo ) )
10095, 98, 99sylancl 644 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  RR+  ->  if ( w  e.  ( ( X (,) Y )  i^i  ( ( x  -  z ) (,) ( z  +  x
) ) ) ,  y ,  0 )  e.  ( 0 [,] 
+oo ) )
101100adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  RR+  /\  w  e.  RR )  ->  if ( w  e.  (
( X (,) Y
)  i^i  ( (
x  -  z ) (,) ( z  +  x ) ) ) ,  y ,  0 )  e.  ( 0 [,]  +oo ) )
102 eqid 2404 . . . . . . . . . . . . . . . . . 18  |-  ( w  e.  RR  |->  if ( w  e.  ( ( X (,) Y )  i^i  ( ( x  -  z ) (,) ( z  +  x
) ) ) ,  y ,  0 ) )  =  ( w  e.  RR  |->  if ( w  e.  ( ( X (,) Y )  i^i  ( ( x  -  z ) (,) ( z  +  x
) ) ) ,  y ,  0 ) )
103101, 102fmptd 5852 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  RR+  ->  ( w  e.  RR  |->  if ( w  e.  ( ( X (,) Y )  i^i  ( ( x  -  z ) (,) ( z  +  x
) ) ) ,  y ,  0 ) ) : RR --> ( 0 [,]  +oo ) )
104 itg2cl 19577 . . . . . . . . . . . . . . . . 17  |-  ( ( w  e.  RR  |->  if ( w  e.  ( ( X (,) Y
)  i^i  ( (
x  -  z ) (,) ( z  +  x ) ) ) ,  y ,  0 ) ) : RR --> ( 0 [,]  +oo )  ->  ( S.2 `  (
w  e.  RR  |->  if ( w  e.  ( ( X (,) Y
)  i^i  ( (
x  -  z ) (,) ( z  +  x ) ) ) ,  y ,  0 ) ) )  e. 
RR* )
105103, 104syl 16 . . . . . . . . . . . . . . . 16  |-  ( y  e.  RR+  ->  ( S.2 `  ( w  e.  RR  |->  if ( w  e.  ( ( X (,) Y
)  i^i  ( (
x  -  z ) (,) ( z  +  x ) ) ) ,  y ,  0 ) ) )  e. 
RR* )
106105ad5antlr 716 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  A. u  e.  ( X (,) Y ) ( ( abs `  ( u  -  x ) )  <  z  ->  ( abs `  ( ( F `
 u )  -  ( F `  x ) ) )  <  (
( F `  x
)  -  y ) ) )  ->  ( S.2 `  ( w  e.  RR  |->  if ( w  e.  ( ( X (,) Y )  i^i  ( ( x  -  z ) (,) (
z  +  x ) ) ) ,  y ,  0 ) ) )  e.  RR* )
107 ifcl 3735 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( y  e.  ( 0 [,]  +oo )  /\  0  e.  ( 0 [,]  +oo ) )  ->  if ( w  e.  { v  e.  ( X (,) Y )  |  y  <_  ( F `  v ) } , 
y ,  0 )  e.  ( 0 [,] 
+oo ) )
10895, 98, 107sylancl 644 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  RR+  ->  if ( w  e.  { v  e.  ( X (,) Y )  |  y  <_  ( F `  v ) } , 
y ,  0 )  e.  ( 0 [,] 
+oo ) )
109108adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  RR+  /\  w  e.  RR )  ->  if ( w  e.  { v  e.  ( X (,) Y )  |  y  <_  ( F `  v ) } , 
y ,  0 )  e.  ( 0 [,] 
+oo ) )
110 eqid 2404 . . . . . . . . . . . . . . . . . 18  |-  ( w  e.  RR  |->  if ( w  e.  { v  e.  ( X (,) Y )  |  y  <_  ( F `  v ) } , 
y ,  0 ) )  =  ( w  e.  RR  |->  if ( w  e.  { v  e.  ( X (,) Y )  |  y  <_  ( F `  v ) } , 
y ,  0 ) )
111109, 110fmptd 5852 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  RR+  ->  ( w  e.  RR  |->  if ( w  e.  { v  e.  ( X (,) Y )  |  y  <_  ( F `  v ) } , 
y ,  0 ) ) : RR --> ( 0 [,]  +oo ) )
112 itg2cl 19577 . . . . . . . . . . . . . . . . 17  |-  ( ( w  e.  RR  |->  if ( w  e.  {
v  e.  ( X (,) Y )  |  y  <_  ( F `  v ) } , 
y ,  0 ) ) : RR --> ( 0 [,]  +oo )  ->  ( S.2 `  ( w  e.  RR  |->  if ( w  e.  { v  e.  ( X (,) Y
)  |  y  <_ 
( F `  v
) } ,  y ,  0 ) ) )  e.  RR* )
113111, 112syl 16 . . . . . . . . . . . . . . . 16  |-  ( y  e.  RR+  ->  ( S.2 `  ( w  e.  RR  |->  if ( w  e.  {
v  e.  ( X (,) Y )  |  y  <_  ( F `  v ) } , 
y ,  0 ) ) )  e.  RR* )
114113ad5antlr 716 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  A. u  e.  ( X (,) Y ) ( ( abs `  ( u  -  x ) )  <  z  ->  ( abs `  ( ( F `
 u )  -  ( F `  x ) ) )  <  (
( F `  x
)  -  y ) ) )  ->  ( S.2 `  ( w  e.  RR  |->  if ( w  e.  { v  e.  ( X (,) Y
)  |  y  <_ 
( F `  v
) } ,  y ,  0 ) ) )  e.  RR* )
11565ad4antlr 714 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  y  e.  RR )
116 ioombl 19412 . . . . . . . . . . . . . . . . . . . . 21  |-  ( if ( X  <_  (
x  -  z ) ,  ( x  -  z ) ,  X
) (,) if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) )  e.  dom  vol
117 mblvol 19379 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( if ( X  <_ 
( x  -  z
) ,  ( x  -  z ) ,  X ) (,) if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) )  e.  dom  vol  ->  ( vol `  ( if ( X  <_  (
x  -  z ) ,  ( x  -  z ) ,  X
) (,) if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) ) )  =  ( vol
* `  ( if ( X  <_  ( x  -  z ) ,  ( x  -  z
) ,  X ) (,) if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) ) ) )
118116, 117ax-mp 8 . . . . . . . . . . . . . . . . . . . 20  |-  ( vol `  ( if ( X  <_  ( x  -  z ) ,  ( x  -  z ) ,  X ) (,)
if ( Y  <_ 
( z  +  x
) ,  Y , 
( z  +  x
) ) ) )  =  ( vol * `  ( if ( X  <_  ( x  -  z ) ,  ( x  -  z ) ,  X ) (,)
if ( Y  <_ 
( z  +  x
) ,  Y , 
( z  +  x
) ) ) )
119 elioore 10902 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( X (,) Y )  ->  x  e.  RR )
120119ad3antlr 712 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  x  e.  RR )
121 rpre 10574 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  e.  RR+  ->  z  e.  RR )
122121adantl 453 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  z  e.  RR )
123120, 122resubcld 9421 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  ( x  -  z )  e.  RR )
124123adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  X  <_  ( x  -  z
) )  ->  (
x  -  z )  e.  RR )
125123rexrd 9090 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  ( x  -  z )  e. 
RR* )
126125adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  -.  X  <_  ( x  -  z ) )  -> 
( x  -  z
)  e.  RR* )
12717simpld 446 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  X  e.  RR* )
128127ad5antr 715 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  -.  X  <_  ( x  -  z ) )  ->  X  e.  RR* )
12917simprd 450 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  Y  e.  RR* )
130129ad5antr 715 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  -.  X  <_  ( x  -  z ) )  ->  Y  e.  RR* )
131127ad4antr 713 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  X  e.  RR* )
132 xrltnle 9100 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( x  -  z
)  e.  RR*  /\  X  e.  RR* )  ->  (
( x  -  z
)  <  X  <->  -.  X  <_  ( x  -  z
) ) )
133125, 131, 132syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  ( (
x  -  z )  <  X  <->  -.  X  <_  ( x  -  z
) ) )
134133biimpar 472 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  -.  X  <_  ( x  -  z ) )  -> 
( x  -  z
)  <  X )
13512ad5antr 715 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  -.  X  <_  ( x  -  z ) )  ->  X  <  Y )
136 xrre2 10714 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( x  -  z )  e.  RR*  /\  X  e.  RR*  /\  Y  e.  RR* )  /\  (
( x  -  z
)  <  X  /\  X  <  Y ) )  ->  X  e.  RR )
137126, 128, 130, 134, 135, 136syl32anc 1192 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  -.  X  <_  ( x  -  z ) )  ->  X  e.  RR )
138124, 137ifclda 3726 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  if ( X  <_  ( x  -  z ) ,  ( x  -  z ) ,  X )  e.  RR )
139129ad5antr 715 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  Y  <_  ( z  +  x
) )  ->  Y  e.  RR* )
140122, 120readdcld 9071 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  ( z  +  x )  e.  RR )
141140adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  Y  <_  ( z  +  x
) )  ->  (
z  +  x )  e.  RR )
142 mnfxr 10670 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  -oo  e.  RR*
143142a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  -oo  e.  RR* )
144 mnfle 10685 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( X  e.  RR*  ->  -oo  <_  X )
145127, 144syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  -oo  <_  X )
146143, 127, 129, 145, 12xrlelttrd 10706 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  -oo  <  Y )
147146ad5antr 715 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  Y  <_  ( z  +  x
) )  ->  -oo  <  Y )
148 simpr 448 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  Y  <_  ( z  +  x
) )  ->  Y  <_  ( z  +  x
) )
149 xrre 10713 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( Y  e.  RR*  /\  ( z  +  x
)  e.  RR )  /\  (  -oo  <  Y  /\  Y  <_  (
z  +  x ) ) )  ->  Y  e.  RR )
150139, 141, 147, 148, 149syl22anc 1185 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  Y  <_  ( z  +  x
) )  ->  Y  e.  RR )
151140adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  -.  Y  <_  ( z  +  x ) )  -> 
( z  +  x
)  e.  RR )
152150, 151ifclda 3726 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) )  e.  RR )
153120rexrd 9090 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  x  e.  RR* )
154129ad4antr 713 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  Y  e.  RR* )
155 rpgt0 10579 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  e.  RR+  ->  0  < 
z )
156155adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  0  <  z )
157122, 120ltsubposd 9568 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  ( 0  <  z  <->  ( x  -  z )  < 
x ) )
158156, 157mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  ( x  -  z )  < 
x )
159 eliooord 10926 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  ( X (,) Y )  ->  ( X  <  x  /\  x  <  Y ) )
160159simprd 450 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( X (,) Y )  ->  x  <  Y )
161160ad3antlr 712 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  x  <  Y )
162125, 153, 154, 158, 161xrlttrd 10705 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  ( x  -  z )  < 
Y )
163122, 120ltaddpos2d 9567 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  ( 0  <  z  <->  x  <  ( z  +  x ) ) )
164156, 163mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  x  <  ( z  +  x ) )
165123, 120, 140, 158, 164lttrd 9187 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  ( x  -  z )  < 
( z  +  x
) )
166 breq2 4176 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( Y  =  if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) )  -> 
( ( x  -  z )  <  Y  <->  ( x  -  z )  <  if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) ) )
167 breq2 4176 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( z  +  x )  =  if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) )  -> 
( ( x  -  z )  <  (
z  +  x )  <-> 
( x  -  z
)  <  if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) ) )
168166, 167ifboth 3730 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( x  -  z
)  <  Y  /\  ( x  -  z
)  <  ( z  +  x ) )  -> 
( x  -  z
)  <  if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) )
169162, 165, 168syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  ( x  -  z )  < 
if ( Y  <_ 
( z  +  x
) ,  Y , 
( z  +  x
) ) )
17012ad4antr 713 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  X  <  Y )
171140rexrd 9090 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  ( z  +  x )  e.  RR* )
172159simpld 446 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( X (,) Y )  ->  X  <  x )
173172ad3antlr 712 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  X  <  x )
174131, 153, 171, 173, 164xrlttrd 10705 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  X  <  ( z  +  x ) )
175 breq2 4176 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( Y  =  if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) )  -> 
( X  <  Y  <->  X  <  if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) ) )
176 breq2 4176 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( z  +  x )  =  if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) )  -> 
( X  <  (
z  +  x )  <-> 
X  <  if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) ) )
177175, 176ifboth 3730 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( X  <  Y  /\  X  <  ( z  +  x ) )  ->  X  <  if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) )
178170, 174, 177syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  X  <  if ( Y  <_  (
z  +  x ) ,  Y ,  ( z  +  x ) ) )
179 breq1 4175 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  -  z )  =  if ( X  <_  ( x  -  z ) ,  ( x  -  z ) ,  X )  -> 
( ( x  -  z )  <  if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) )  <-> 
if ( X  <_ 
( x  -  z
) ,  ( x  -  z ) ,  X )  <  if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) ) )
180 breq1 4175 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( X  =  if ( X  <_  ( x  -  z ) ,  ( x  -  z ) ,  X )  -> 
( X  <  if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) )  <-> 
if ( X  <_ 
( x  -  z
) ,  ( x  -  z ) ,  X )  <  if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) ) )
181179, 180ifboth 3730 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( x  -  z
)  <  if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) )  /\  X  <  if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) )  ->  if ( X  <_  ( x  -  z ) ,  ( x  -  z ) ,  X )  < 
if ( Y  <_ 
( z  +  x
) ,  Y , 
( z  +  x
) ) )
182169, 178, 181syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  if ( X  <_  ( x  -  z ) ,  ( x  -  z ) ,  X )  < 
if ( Y  <_ 
( z  +  x
) ,  Y , 
( z  +  x
) ) )
183138, 152, 182ltled 9177 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  if ( X  <_  ( x  -  z ) ,  ( x  -  z ) ,  X )  <_  if ( Y  <_  (
z  +  x ) ,  Y ,  ( z  +  x ) ) )
184 ovolioo 19415 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( if ( X  <_ 
( x  -  z
) ,  ( x  -  z ) ,  X )  e.  RR  /\  if ( Y  <_ 
( z  +  x
) ,  Y , 
( z  +  x
) )  e.  RR  /\  if ( X  <_ 
( x  -  z
) ,  ( x  -  z ) ,  X )  <_  if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) )  ->  ( vol * `
 ( if ( X  <_  ( x  -  z ) ,  ( x  -  z
) ,  X ) (,) if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) ) )  =  ( if ( Y  <_  (
z  +  x ) ,  Y ,  ( z  +  x ) )  -  if ( X  <_  ( x  -  z ) ,  ( x  -  z
) ,  X ) ) )
185138, 152, 183, 184syl3anc 1184 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  ( vol * `
 ( if ( X  <_  ( x  -  z ) ,  ( x  -  z
) ,  X ) (,) if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) ) )  =  ( if ( Y  <_  (
z  +  x ) ,  Y ,  ( z  +  x ) )  -  if ( X  <_  ( x  -  z ) ,  ( x  -  z
) ,  X ) ) )
186118, 185syl5eq 2448 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  ( vol `  ( if ( X  <_  ( x  -  z ) ,  ( x  -  z ) ,  X ) (,)
if ( Y  <_ 
( z  +  x
) ,  Y , 
( z  +  x
) ) ) )  =  ( if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) )  -  if ( X  <_  (
x  -  z ) ,  ( x  -  z ) ,  X
) ) )
187152, 138resubcld 9421 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  ( if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) )  -  if ( X  <_  ( x  -  z ) ,  ( x  -  z ) ,  X ) )  e.  RR )
188186, 187eqeltrd 2478 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  ( vol `  ( if ( X  <_  ( x  -  z ) ,  ( x  -  z ) ,  X ) (,)
if ( Y  <_ 
( z  +  x
) ,  Y , 
( z  +  x
) ) ) )  e.  RR )
189 rpgt0 10579 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  RR+  ->  0  < 
y )
190189ad4antlr 714 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  0  <  y )
191138, 152posdifd 9569 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  ( if ( X  <_  ( x  -  z ) ,  ( x  -  z
) ,  X )  <  if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) )  <->  0  <  ( if ( Y  <_ 
( z  +  x
) ,  Y , 
( z  +  x
) )  -  if ( X  <_  ( x  -  z ) ,  ( x  -  z
) ,  X ) ) ) )
192182, 191mpbid 202 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  0  <  ( if ( Y  <_ 
( z  +  x
) ,  Y , 
( z  +  x
) )  -  if ( X  <_  ( x  -  z ) ,  ( x  -  z
) ,  X ) ) )
193192, 186breqtrrd 4198 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  0  <  ( vol `  ( if ( X  <_  (
x  -  z ) ,  ( x  -  z ) ,  X
) (,) if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) ) ) )
194115, 188, 190, 193mulgt0d 9181 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  0  <  ( y  x.  ( vol `  ( if ( X  <_  ( x  -  z ) ,  ( x  -  z ) ,  X ) (,)
if ( Y  <_ 
( z  +  x
) ,  Y , 
( z  +  x
) ) ) ) ) )
195 iooin 10906 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( X  e.  RR*  /\  Y  e.  RR* )  /\  ( ( x  -  z )  e.  RR*  /\  ( z  +  x
)  e.  RR* )
)  ->  ( ( X (,) Y )  i^i  ( ( x  -  z ) (,) (
z  +  x ) ) )  =  ( if ( X  <_ 
( x  -  z
) ,  ( x  -  z ) ,  X ) (,) if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) ) )
196131, 154, 125, 171, 195syl22anc 1185 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  ( ( X (,) Y )  i^i  ( ( x  -  z ) (,) (
z  +  x ) ) )  =  ( if ( X  <_ 
( x  -  z
) ,  ( x  -  z ) ,  X ) (,) if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) ) )
197196eleq2d 2471 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  ( w  e.  ( ( X (,) Y )  i^i  (
( x  -  z
) (,) ( z  +  x ) ) )  <->  w  e.  ( if ( X  <_  (
x  -  z ) ,  ( x  -  z ) ,  X
) (,) if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) ) ) )
198197ifbid 3717 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  if (
w  e.  ( ( X (,) Y )  i^i  ( ( x  -  z ) (,) ( z  +  x
) ) ) ,  y ,  0 )  =  if ( w  e.  ( if ( X  <_  ( x  -  z ) ,  ( x  -  z
) ,  X ) (,) if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) ) ,  y ,  0 ) )
199198mpteq2dv 4256 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  ( w  e.  RR  |->  if ( w  e.  ( ( X (,) Y )  i^i  ( ( x  -  z ) (,) (
z  +  x ) ) ) ,  y ,  0 ) )  =  ( w  e.  RR  |->  if ( w  e.  ( if ( X  <_  ( x  -  z ) ,  ( x  -  z
) ,  X ) (,) if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) ) ,  y ,  0 ) ) )
200199fveq2d 5691 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  ( S.2 `  ( w  e.  RR  |->  if ( w  e.  ( ( X (,) Y
)  i^i  ( (
x  -  z ) (,) ( z  +  x ) ) ) ,  y ,  0 ) ) )  =  ( S.2 `  (
w  e.  RR  |->  if ( w  e.  ( if ( X  <_ 
( x  -  z
) ,  ( x  -  z ) ,  X ) (,) if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) ) ,  y ,  0 ) ) ) )
201116a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  ( if ( X  <_  ( x  -  z ) ,  ( x  -  z
) ,  X ) (,) if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) )  e.  dom  vol )
202 rpge0 10580 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  RR+  ->  0  <_ 
y )
203 elrege0 10963 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( 0 [,) 
+oo )  <->  ( y  e.  RR  /\  0  <_ 
y ) )
20465, 202, 203sylanbrc 646 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  RR+  ->  y  e.  ( 0 [,)  +oo ) )
205204ad4antlr 714 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  y  e.  ( 0 [,)  +oo ) )
206 itg2const 19585 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( if ( X  <_  ( x  -  z ) ,  ( x  -  z ) ,  X ) (,)
if ( Y  <_ 
( z  +  x
) ,  Y , 
( z  +  x
) ) )  e. 
dom  vol  /\  ( vol `  ( if ( X  <_  ( x  -  z ) ,  ( x  -  z ) ,  X ) (,)
if ( Y  <_ 
( z  +  x
) ,  Y , 
( z  +  x
) ) ) )  e.  RR  /\  y  e.  ( 0 [,)  +oo ) )  ->  ( S.2 `  ( w  e.  RR  |->  if ( w  e.  ( if ( X  <_  ( x  -  z ) ,  ( x  -  z
) ,  X ) (,) if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) ) ,  y ,  0 ) ) )  =  ( y  x.  ( vol `  ( if ( X  <_  ( x  -  z ) ,  ( x  -  z
) ,  X ) (,) if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) ) ) ) )
207201, 188, 205, 206syl3anc 1184 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  ( S.2 `  ( w  e.  RR  |->  if ( w  e.  ( if ( X  <_ 
( x  -  z
) ,  ( x  -  z ) ,  X ) (,) if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) ) ,  y ,  0 ) ) )  =  ( y  x.  ( vol `  ( if ( X  <_  (
x  -  z ) ,  ( x  -  z ) ,  X
) (,) if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) ) ) ) )
208200, 207eqtrd 2436 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  ( S.2 `  ( w  e.  RR  |->  if ( w  e.  ( ( X (,) Y
)  i^i  ( (
x  -  z ) (,) ( z  +  x ) ) ) ,  y ,  0 ) ) )  =  ( y  x.  ( vol `  ( if ( X  <_  ( x  -  z ) ,  ( x  -  z
) ,  X ) (,) if ( Y  <_  ( z  +  x ) ,  Y ,  ( z  +  x ) ) ) ) ) )
209194, 208breqtrrd 4198 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  0  <  ( S.2 `  ( w  e.  RR  |->  if ( w  e.  ( ( X (,) Y )  i^i  ( ( x  -  z ) (,) ( z  +  x
) ) ) ,  y ,  0 ) ) ) )
210209adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  A. u  e.  ( X (,) Y ) ( ( abs `  ( u  -  x ) )  <  z  ->  ( abs `  ( ( F `
 u )  -  ( F `  x ) ) )  <  (
( F `  x
)  -  y ) ) )  ->  0  <  ( S.2 `  (
w  e.  RR  |->  if ( w  e.  ( ( X (,) Y
)  i^i  ( (
x  -  z ) (,) ( z  +  x ) ) ) ,  y ,  0 ) ) ) )
211103ad5antlr 716 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  A. u  e.  ( X (,) Y ) ( ( abs `  ( u  -  x ) )  <  z  ->  ( abs `  ( ( F `
 u )  -  ( F `  x ) ) )  <  (
( F `  x
)  -  y ) ) )  ->  (
w  e.  RR  |->  if ( w  e.  ( ( X (,) Y
)  i^i  ( (
x  -  z ) (,) ( z  +  x ) ) ) ,  y ,  0 ) ) : RR --> ( 0 [,]  +oo ) )
212111ad5antlr 716 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  A. u  e.  ( X (,) Y ) ( ( abs `  ( u  -  x ) )  <  z  ->  ( abs `  ( ( F `
 u )  -  ( F `  x ) ) )  <  (
( F `  x
)  -  y ) ) )  ->  (
w  e.  RR  |->  if ( w  e.  {
v  e.  ( X (,) Y )  |  y  <_  ( F `  v ) } , 
y ,  0 ) ) : RR --> ( 0 [,]  +oo ) )
213 oveq1 6047 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( u  =  w  ->  (
u  -  x )  =  ( w  -  x ) )
214213fveq2d 5691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( u  =  w  ->  ( abs `  ( u  -  x ) )  =  ( abs `  (
w  -  x ) ) )
215214breq1d 4182 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( u  =  w  ->  (
( abs `  (
u  -  x ) )  <  z  <->  ( abs `  ( w  -  x
) )  <  z
) )
216 fveq2 5687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( u  =  w  ->  ( F `  u )  =  ( F `  w ) )
217216oveq1d 6055 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( u  =  w  ->  (
( F `  u
)  -  ( F `
 x ) )  =  ( ( F `
 w )  -  ( F `  x ) ) )
218217fveq2d 5691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( u  =  w  ->  ( abs `  ( ( F `
 u )  -  ( F `  x ) ) )  =  ( abs `  ( ( F `  w )  -  ( F `  x ) ) ) )
219218breq1d 4182 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( u  =  w  ->  (
( abs `  (
( F `  u
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y )  <->  ( abs `  ( ( F `  w )  -  ( F `  x )
) )  <  (
( F `  x
)  -  y ) ) )
220215, 219imbi12d 312 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( u  =  w  ->  (
( ( abs `  (
u  -  x ) )  <  z  -> 
( abs `  (
( F `  u
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) )  <-> 
( ( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) ) )
221220rspccva 3011 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A. u  e.  ( X (,) Y ) ( ( abs `  (
u  -  x ) )  <  z  -> 
( abs `  (
( F `  u
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) )  /\  w  e.  ( X (,) Y ) )  ->  ( ( abs `  ( w  -  x ) )  < 
z  ->  ( abs `  ( ( F `  w )  -  ( F `  x )
) )  <  (
( F `  x
)  -  y ) ) )
222 breq1 4175 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  if ( w  e.  ( ( x  -  z ) (,) ( z  +  x
) ) ,  y ,  0 )  -> 
( y  <_  if ( y  <_  ( F `  w ) ,  y ,  0 )  <->  if ( w  e.  ( ( x  -  z ) (,) (
z  +  x ) ) ,  y ,  0 )  <_  if ( y  <_  ( F `  w ) ,  y ,  0 ) ) )
223 breq1 4175 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 0  =  if ( w  e.  ( ( x  -  z ) (,) ( z  +  x
) ) ,  y ,  0 )  -> 
( 0  <_  if ( y  <_  ( F `  w ) ,  y ,  0 )  <->  if ( w  e.  ( ( x  -  z ) (,) (
z  +  x ) ) ,  y ,  0 )  <_  if ( y  <_  ( F `  w ) ,  y ,  0 ) ) )
22465leidd 9549 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  e.  RR+  ->  y  <_ 
y )
225224ad6antlr 718 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  /\  w  e.  ( ( x  -  z ) (,) (
z  +  x ) ) )  ->  y  <_  y )
226119ad4antlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  ->  x  e.  RR )
227121ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  ->  z  e.  RR )
228226, 227resubcld 9421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  ->  ( x  -  z )  e.  RR )
229228rexrd 9090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  ->  ( x  -  z )  e. 
RR* )
230227, 226readdcld 9071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  ->  ( z  +  x )  e.  RR )
231230rexrd 9090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  ->  ( z  +  x )  e.  RR* )
232 elioo2 10913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( x  -  z
)  e.  RR*  /\  (
z  +  x )  e.  RR* )  ->  (
w  e.  ( ( x  -  z ) (,) ( z  +  x ) )  <->  ( w  e.  RR  /\  ( x  -  z )  < 
w  /\  w  <  ( z  +  x ) ) ) )
233229, 231, 232syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  ->  ( w  e.  ( ( x  -  z ) (,) (
z  +  x ) )  <->  ( w  e.  RR  /\  ( x  -  z )  < 
w  /\  w  <  ( z  +  x ) ) ) )
234 3anass 940 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( w  e.  RR  /\  ( x  -  z
)  <  w  /\  w  <  ( z  +  x ) )  <->  ( w  e.  RR  /\  ( ( x  -  z )  <  w  /\  w  <  ( z  +  x
) ) ) )
235233, 234syl6bb 253 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  ->  ( w  e.  ( ( x  -  z ) (,) (
z  +  x ) )  <->  ( w  e.  RR  /\  ( ( x  -  z )  <  w  /\  w  <  ( z  +  x
) ) ) ) )
236 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  /\  w  e.  RR )  ->  w  e.  RR )
237119ad5antlr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  /\  w  e.  RR )  ->  x  e.  RR )
238236, 237resubcld 9421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  /\  w  e.  RR )  ->  (
w  -  x )  e.  RR )
239121ad3antlr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  /\  w  e.  RR )  ->  z  e.  RR )
240238, 239absltd 12187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  /\  w  e.  RR )  ->  (
( abs `  (
w  -  x ) )  <  z  <->  ( -u z  <  ( w  -  x
)  /\  ( w  -  x )  <  z
) ) )
241239renegcld 9420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  /\  w  e.  RR )  ->  -u z  e.  RR )
242237, 241, 236ltaddsub2d 9583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  /\  w  e.  RR )  ->  (
( x  +  -u z )  <  w  <->  -u z  <  ( w  -  x ) ) )
243237recnd 9070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  /\  w  e.  RR )  ->  x  e.  CC )
244239recnd 9070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  /\  w  e.  RR )  ->  z  e.  CC )
245243, 244negsubd 9373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  /\  w  e.  RR )  ->  (
x  +  -u z
)  =  ( x  -  z ) )
246245breq1d 4182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  /\  w  e.  RR )  ->  (
( x  +  -u z )  <  w  <->  ( x  -  z )  <  w ) )
247242, 246bitr3d 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  /\  w  e.  RR )  ->  ( -u z  <  ( w  -  x )  <->  ( x  -  z )  < 
w ) )
248236, 237, 239ltsubaddd 9578 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  /\  w  e.  RR )  ->  (
( w  -  x
)  <  z  <->  w  <  ( z  +  x ) ) )
249247, 248anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  /\  w  e.  RR )  ->  (
( -u z  <  (
w  -  x )  /\  ( w  -  x )  <  z
)  <->  ( ( x  -  z )  < 
w  /\  w  <  ( z  +  x ) ) ) )
250240, 249bitrd 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  /\  w  e.  RR )  ->  (
( abs `  (
w  -  x ) )  <  z  <->  ( (
x  -  z )  <  w  /\  w  <  ( z  +  x
) ) ) )
251250pm5.32da 623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  ->  ( (
w  e.  RR  /\  ( abs `  ( w  -  x ) )  <  z )  <->  ( w  e.  RR  /\  ( ( x  -  z )  <  w  /\  w  <  ( z  +  x
) ) ) ) )
252235, 251bitr4d 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  ->  ( w  e.  ( ( x  -  z ) (,) (
z  +  x ) )  <->  ( w  e.  RR  /\  ( abs `  ( w  -  x
) )  <  z
) ) )
253252biimpa 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  (
( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  /\  w  e.  ( ( x  -  z ) (,) (
z  +  x ) ) )  ->  (
w  e.  RR  /\  ( abs `  ( w  -  x ) )  <  z ) )
254 pm3.35 571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( abs `  (
w  -  x ) )  <  z  /\  ( ( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) ) )  ->  ( abs `  ( ( F `  w )  -  ( F `  x )
) )  <  (
( F `  x
)  -  y ) )
255254ancoms 440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) )  /\  ( abs `  (
w  -  x ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) )
25665ad6antlr 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  w  e.  RR )  /\  ( abs `  ( ( F `
 w )  -  ( F `  x ) ) )  <  (
( F `  x
)  -  y ) )  ->  y  e.  RR )
2574ad4antr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y ) )  /\  y  <  ( F `  x )
)  /\  z  e.  RR+ )  ->  F : RR
--> ( 0 [,)  +oo ) )
258257ffvelrnda 5829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  w  e.  RR )  ->  ( F `  w )  e.  ( 0 [,)  +oo ) )
25959, 258sseldi 3306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  w  e.  RR )  ->  ( F `  w )  e.  RR )
260259adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  w  e.  RR )  /\  ( abs `  ( ( F `
 w )  -  ( F `  x ) ) )  <  (
( F `  x
)  -  y ) )  ->  ( F `  w )  e.  RR )
2614adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  y  e.  RR+ )  ->  F : RR
--> ( 0 [,)  +oo ) )
262261ffvelrnda 5829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  RR )  ->  ( F `  x )  e.  ( 0 [,)  +oo ) )
26359, 262sseldi 3306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  RR )  ->  ( F `  x )  e.  RR )
264119, 263sylan2 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  ->  ( F `  x )  e.  RR )
265264ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  w  e.  RR )  ->  ( F `  x )  e.  RR )
266259, 265resubcld 9421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  w  e.  RR )  ->  (
( F `  w
)  -  ( F `
 x ) )  e.  RR )
267264, 66resubcld 9421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  ->  (
( F `  x
)  -  y )  e.  RR )
268267ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  w  e.  RR )  ->  (
( F `  x
)  -  y )  e.  RR )
269266, 268absltd 12187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  w  e.  RR )  ->  (
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y )  <->  ( -u (
( F `  x
)  -  y )  <  ( ( F `
 w )  -  ( F `  x ) )  /\  ( ( F `  w )  -  ( F `  x ) )  < 
( ( F `  x )  -  y
) ) ) )
270264recnd 9070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  ->  ( F `  x )  e.  CC )
271 rpcn 10576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( y  e.  RR+  ->  y  e.  CC )
272271ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  ->  y  e.  CC )
273270, 272negsubdi2d 9383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  ->  -u (
( F `  x
)  -  y )  =  ( y  -  ( F `  x ) ) )
274273ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  w  e.  RR )  ->  -u (
( F `  x
)  -  y )  =  ( y  -  ( F `  x ) ) )
275274breq1d 4182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  w  e.  RR )  ->  ( -u ( ( F `  x )  -  y
)  <  ( ( F `  w )  -  ( F `  x ) )  <->  ( y  -  ( F `  x ) )  < 
( ( F `  w )  -  ( F `  x )
) ) )
276275anbi1d 686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  w  e.  RR )  ->  (
( -u ( ( F `
 x )  -  y )  <  (
( F `  w
)  -  ( F `
 x ) )  /\  ( ( F `
 w )  -  ( F `  x ) )  <  ( ( F `  x )  -  y ) )  <-> 
( ( y  -  ( F `  x ) )  <  ( ( F `  w )  -  ( F `  x ) )  /\  ( ( F `  w )  -  ( F `  x )
)  <  ( ( F `  x )  -  y ) ) ) )
277269, 276bitrd 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  w  e.  RR )  ->  (
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y )  <->  ( (
y  -  ( F `
 x ) )  <  ( ( F `
 w )  -  ( F `  x ) )  /\  ( ( F `  w )  -  ( F `  x ) )  < 
( ( F `  x )  -  y
) ) ) )
278277simprbda 607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  w  e.  RR )  /\  ( abs `  ( ( F `
 w )  -  ( F `  x ) ) )  <  (
( F `  x
)  -  y ) )  ->  ( y  -  ( F `  x ) )  < 
( ( F `  w )  -  ( F `  x )
) )
279264ad4antr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  w  e.  RR )  /\  ( abs `  ( ( F `
 w )  -  ( F `  x ) ) )  <  (
( F `  x
)  -  y ) )  ->  ( F `  x )  e.  RR )
280256, 260, 279ltsub1d 9591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  w  e.  RR )  /\  ( abs `  ( ( F `
 w )  -  ( F `  x ) ) )  <  (
( F `  x
)  -  y ) )  ->  ( y  <  ( F `  w
)  <->  ( y  -  ( F `  x ) )  <  ( ( F `  w )  -  ( F `  x ) ) ) )
281278, 280mpbird 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  w  e.  RR )  /\  ( abs `  ( ( F `
 w )  -  ( F `  x ) ) )  <  (
( F `  x
)  -  y ) )  ->  y  <  ( F `  w ) )
282256, 260, 281ltled 9177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  w  e.  RR )  /\  ( abs `  ( ( F `
 w )  -  ( F `  x ) ) )  <  (
( F `  x
)  -  y ) )  ->  y  <_  ( F `  w ) )
283255, 282sylan2 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  ( X (,) Y
) )  /\  y  <  ( F `  x
) )  /\  z  e.  RR+ )  /\  w  e.  RR )  /\  (
( ( abs `  (
w  -  x ) )  <  z  -> 
( abs `  (
( F `  w
)  -  ( F `
 x ) ) )  <  ( ( F `  x )  -  y ) )  /\  ( abs `  (
w  -  x ) )  <  z ) )  ->  y  <_  ( F `  w ) )
284283an4s 800 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  x  e.  (