MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvlip Structured version   Unicode version

Theorem dvlip 22563
Description: A function with derivative bounded by  M is Lipschitz continuous with Lipschitz constant equal to 
M. (Contributed by Mario Carneiro, 3-Mar-2015.)
Hypotheses
Ref Expression
dvlip.a  |-  ( ph  ->  A  e.  RR )
dvlip.b  |-  ( ph  ->  B  e.  RR )
dvlip.f  |-  ( ph  ->  F  e.  ( ( A [,] B )
-cn-> CC ) )
dvlip.d  |-  ( ph  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
dvlip.m  |-  ( ph  ->  M  e.  RR )
dvlip.l  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( abs `  ( ( RR  _D  F ) `  x
) )  <_  M
)
Assertion
Ref Expression
dvlip  |-  ( (
ph  /\  ( X  e.  ( A [,] B
)  /\  Y  e.  ( A [,] B ) ) )  ->  ( abs `  ( ( F `
 X )  -  ( F `  Y ) ) )  <_  ( M  x.  ( abs `  ( X  -  Y
) ) ) )
Distinct variable groups:    x, A    x, B    ph, x    x, F    x, M
Allowed substitution hints:    X( x)    Y( x)

Proof of Theorem dvlip
Dummy variables  a 
b  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 5848 . . . . . . . 8  |-  ( a  =  Y  ->  ( F `  a )  =  ( F `  Y ) )
21oveq2d 6286 . . . . . . 7  |-  ( a  =  Y  ->  (
( F `  b
)  -  ( F `
 a ) )  =  ( ( F `
 b )  -  ( F `  Y ) ) )
32fveq2d 5852 . . . . . 6  |-  ( a  =  Y  ->  ( abs `  ( ( F `
 b )  -  ( F `  a ) ) )  =  ( abs `  ( ( F `  b )  -  ( F `  Y ) ) ) )
4 oveq2 6278 . . . . . . . 8  |-  ( a  =  Y  ->  (
b  -  a )  =  ( b  -  Y ) )
54fveq2d 5852 . . . . . . 7  |-  ( a  =  Y  ->  ( abs `  ( b  -  a ) )  =  ( abs `  (
b  -  Y ) ) )
65oveq2d 6286 . . . . . 6  |-  ( a  =  Y  ->  ( M  x.  ( abs `  ( b  -  a
) ) )  =  ( M  x.  ( abs `  ( b  -  Y ) ) ) )
73, 6breq12d 4452 . . . . 5  |-  ( a  =  Y  ->  (
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  <_  ( M  x.  ( abs `  (
b  -  a ) ) )  <->  ( abs `  ( ( F `  b )  -  ( F `  Y )
) )  <_  ( M  x.  ( abs `  ( b  -  Y
) ) ) ) )
87imbi2d 314 . . . 4  |-  ( a  =  Y  ->  (
( ph  ->  ( abs `  ( ( F `  b )  -  ( F `  a )
) )  <_  ( M  x.  ( abs `  ( b  -  a
) ) ) )  <-> 
( ph  ->  ( abs `  ( ( F `  b )  -  ( F `  Y )
) )  <_  ( M  x.  ( abs `  ( b  -  Y
) ) ) ) ) )
9 fveq2 5848 . . . . . . . 8  |-  ( b  =  X  ->  ( F `  b )  =  ( F `  X ) )
109oveq1d 6285 . . . . . . 7  |-  ( b  =  X  ->  (
( F `  b
)  -  ( F `
 Y ) )  =  ( ( F `
 X )  -  ( F `  Y ) ) )
1110fveq2d 5852 . . . . . 6  |-  ( b  =  X  ->  ( abs `  ( ( F `
 b )  -  ( F `  Y ) ) )  =  ( abs `  ( ( F `  X )  -  ( F `  Y ) ) ) )
12 oveq1 6277 . . . . . . . 8  |-  ( b  =  X  ->  (
b  -  Y )  =  ( X  -  Y ) )
1312fveq2d 5852 . . . . . . 7  |-  ( b  =  X  ->  ( abs `  ( b  -  Y ) )  =  ( abs `  ( X  -  Y )
) )
1413oveq2d 6286 . . . . . 6  |-  ( b  =  X  ->  ( M  x.  ( abs `  ( b  -  Y
) ) )  =  ( M  x.  ( abs `  ( X  -  Y ) ) ) )
1511, 14breq12d 4452 . . . . 5  |-  ( b  =  X  ->  (
( abs `  (
( F `  b
)  -  ( F `
 Y ) ) )  <_  ( M  x.  ( abs `  (
b  -  Y ) ) )  <->  ( abs `  ( ( F `  X )  -  ( F `  Y )
) )  <_  ( M  x.  ( abs `  ( X  -  Y
) ) ) ) )
1615imbi2d 314 . . . 4  |-  ( b  =  X  ->  (
( ph  ->  ( abs `  ( ( F `  b )  -  ( F `  Y )
) )  <_  ( M  x.  ( abs `  ( b  -  Y
) ) ) )  <-> 
( ph  ->  ( abs `  ( ( F `  X )  -  ( F `  Y )
) )  <_  ( M  x.  ( abs `  ( X  -  Y
) ) ) ) ) )
17 fveq2 5848 . . . . . . . . . 10  |-  ( y  =  b  ->  ( F `  y )  =  ( F `  b ) )
18 fveq2 5848 . . . . . . . . . 10  |-  ( x  =  a  ->  ( F `  x )  =  ( F `  a ) )
1917, 18oveqan12d 6289 . . . . . . . . 9  |-  ( ( y  =  b  /\  x  =  a )  ->  ( ( F `  y )  -  ( F `  x )
)  =  ( ( F `  b )  -  ( F `  a ) ) )
2019fveq2d 5852 . . . . . . . 8  |-  ( ( y  =  b  /\  x  =  a )  ->  ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  =  ( abs `  ( ( F `  b )  -  ( F `  a )
) ) )
21 oveq12 6279 . . . . . . . . . 10  |-  ( ( y  =  b  /\  x  =  a )  ->  ( y  -  x
)  =  ( b  -  a ) )
2221fveq2d 5852 . . . . . . . . 9  |-  ( ( y  =  b  /\  x  =  a )  ->  ( abs `  (
y  -  x ) )  =  ( abs `  ( b  -  a
) ) )
2322oveq2d 6286 . . . . . . . 8  |-  ( ( y  =  b  /\  x  =  a )  ->  ( M  x.  ( abs `  ( y  -  x ) ) )  =  ( M  x.  ( abs `  ( b  -  a ) ) ) )
2420, 23breq12d 4452 . . . . . . 7  |-  ( ( y  =  b  /\  x  =  a )  ->  ( ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  <_  ( M  x.  ( abs `  (
y  -  x ) ) )  <->  ( abs `  ( ( F `  b )  -  ( F `  a )
) )  <_  ( M  x.  ( abs `  ( b  -  a
) ) ) ) )
2524ancoms 451 . . . . . 6  |-  ( ( x  =  a  /\  y  =  b )  ->  ( ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  <_  ( M  x.  ( abs `  (
y  -  x ) ) )  <->  ( abs `  ( ( F `  b )  -  ( F `  a )
) )  <_  ( M  x.  ( abs `  ( b  -  a
) ) ) ) )
26 fveq2 5848 . . . . . . . . . 10  |-  ( y  =  a  ->  ( F `  y )  =  ( F `  a ) )
27 fveq2 5848 . . . . . . . . . 10  |-  ( x  =  b  ->  ( F `  x )  =  ( F `  b ) )
2826, 27oveqan12d 6289 . . . . . . . . 9  |-  ( ( y  =  a  /\  x  =  b )  ->  ( ( F `  y )  -  ( F `  x )
)  =  ( ( F `  a )  -  ( F `  b ) ) )
2928fveq2d 5852 . . . . . . . 8  |-  ( ( y  =  a  /\  x  =  b )  ->  ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  =  ( abs `  ( ( F `  a )  -  ( F `  b )
) ) )
30 oveq12 6279 . . . . . . . . . 10  |-  ( ( y  =  a  /\  x  =  b )  ->  ( y  -  x
)  =  ( a  -  b ) )
3130fveq2d 5852 . . . . . . . . 9  |-  ( ( y  =  a  /\  x  =  b )  ->  ( abs `  (
y  -  x ) )  =  ( abs `  ( a  -  b
) ) )
3231oveq2d 6286 . . . . . . . 8  |-  ( ( y  =  a  /\  x  =  b )  ->  ( M  x.  ( abs `  ( y  -  x ) ) )  =  ( M  x.  ( abs `  ( a  -  b ) ) ) )
3329, 32breq12d 4452 . . . . . . 7  |-  ( ( y  =  a  /\  x  =  b )  ->  ( ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  <_  ( M  x.  ( abs `  (
y  -  x ) ) )  <->  ( abs `  ( ( F `  a )  -  ( F `  b )
) )  <_  ( M  x.  ( abs `  ( a  -  b
) ) ) ) )
3433ancoms 451 . . . . . 6  |-  ( ( x  =  b  /\  y  =  a )  ->  ( ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  <_  ( M  x.  ( abs `  (
y  -  x ) ) )  <->  ( abs `  ( ( F `  a )  -  ( F `  b )
) )  <_  ( M  x.  ( abs `  ( a  -  b
) ) ) ) )
35 dvlip.a . . . . . . 7  |-  ( ph  ->  A  e.  RR )
36 dvlip.b . . . . . . 7  |-  ( ph  ->  B  e.  RR )
37 iccssre 11609 . . . . . . 7  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A [,] B
)  C_  RR )
3835, 36, 37syl2anc 659 . . . . . 6  |-  ( ph  ->  ( A [,] B
)  C_  RR )
39 dvlip.f . . . . . . . . . . 11  |-  ( ph  ->  F  e.  ( ( A [,] B )
-cn-> CC ) )
40 cncff 21566 . . . . . . . . . . 11  |-  ( F  e.  ( ( A [,] B ) -cn-> CC )  ->  F :
( A [,] B
) --> CC )
4139, 40syl 16 . . . . . . . . . 10  |-  ( ph  ->  F : ( A [,] B ) --> CC )
42 ffvelrn 6005 . . . . . . . . . . 11  |-  ( ( F : ( A [,] B ) --> CC 
/\  a  e.  ( A [,] B ) )  ->  ( F `  a )  e.  CC )
43 ffvelrn 6005 . . . . . . . . . . 11  |-  ( ( F : ( A [,] B ) --> CC 
/\  b  e.  ( A [,] B ) )  ->  ( F `  b )  e.  CC )
4442, 43anim12dan 835 . . . . . . . . . 10  |-  ( ( F : ( A [,] B ) --> CC 
/\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  (
( F `  a
)  e.  CC  /\  ( F `  b )  e.  CC ) )
4541, 44sylan 469 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  (
( F `  a
)  e.  CC  /\  ( F `  b )  e.  CC ) )
4645simprd 461 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( F `  b )  e.  CC )
4745simpld 457 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( F `  a )  e.  CC )
4846, 47abssubd 13369 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( abs `  ( ( F `
 b )  -  ( F `  a ) ) )  =  ( abs `  ( ( F `  a )  -  ( F `  b ) ) ) )
49 ax-resscn 9538 . . . . . . . . . . . 12  |-  RR  C_  CC
5038, 49syl6ss 3501 . . . . . . . . . . 11  |-  ( ph  ->  ( A [,] B
)  C_  CC )
5150sselda 3489 . . . . . . . . . 10  |-  ( (
ph  /\  b  e.  ( A [,] B ) )  ->  b  e.  CC )
5251adantrl 713 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  b  e.  CC )
5350sselda 3489 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  ( A [,] B ) )  ->  a  e.  CC )
5453adantrr 714 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  a  e.  CC )
5552, 54abssubd 13369 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( abs `  ( b  -  a ) )  =  ( abs `  (
a  -  b ) ) )
5655oveq2d 6286 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( M  x.  ( abs `  ( b  -  a
) ) )  =  ( M  x.  ( abs `  ( a  -  b ) ) ) )
5748, 56breq12d 4452 . . . . . 6  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  (
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  <_  ( M  x.  ( abs `  (
b  -  a ) ) )  <->  ( abs `  ( ( F `  a )  -  ( F `  b )
) )  <_  ( M  x.  ( abs `  ( a  -  b
) ) ) ) )
5841adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  F : ( A [,] B ) --> CC )
59 simpr2 1001 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  ( A [,] B
) )
6058, 59ffvelrnd 6008 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( F `  b )  e.  CC )
61 simpr1 1000 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  ( A [,] B
) )
6258, 61ffvelrnd 6008 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( F `  a )  e.  CC )
6360, 62subeq0ad 9932 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( ( F `  b )  -  ( F `  a )
)  =  0  <->  ( F `  b )  =  ( F `  a ) ) )
6463biimpar 483 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =  ( F `  a ) )  -> 
( ( F `  b )  -  ( F `  a )
)  =  0 )
6564abs00bd 13209 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =  ( F `  a ) )  -> 
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  =  0 )
6638adantr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( A [,] B )  C_  RR )
6766, 61sseldd 3490 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  RR )
6867rexrd 9632 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  RR* )
6966, 59sseldd 3490 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  RR )
7069rexrd 9632 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  RR* )
71 ioon0 11558 . . . . . . . . . . . . 13  |-  ( ( a  e.  RR*  /\  b  e.  RR* )  ->  (
( a (,) b
)  =/=  (/)  <->  a  <  b ) )
7268, 70, 71syl2anc 659 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( a (,) b
)  =/=  (/)  <->  a  <  b ) )
73 dvlip.m . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  e.  RR )
7473ad2antrr 723 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  ->  M  e.  RR )
7569, 67resubcld 9983 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
b  -  a )  e.  RR )
7675adantr 463 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
( b  -  a
)  e.  RR )
7735adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  A  e.  RR )
7877rexrd 9632 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  A  e.  RR* )
7936adantr 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  B  e.  RR )
80 elicc2 11592 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( a  e.  ( A [,] B )  <-> 
( a  e.  RR  /\  A  <_  a  /\  a  <_  B ) ) )
8177, 79, 80syl2anc 659 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a  e.  ( A [,] B )  <->  ( a  e.  RR  /\  A  <_ 
a  /\  a  <_  B ) ) )
8261, 81mpbid 210 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a  e.  RR  /\  A  <_  a  /\  a  <_  B ) )
8382simp2d 1007 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  A  <_  a )
84 iooss1 11567 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  RR*  /\  A  <_  a )  ->  (
a (,) b ) 
C_  ( A (,) b ) )
8578, 83, 84syl2anc 659 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a (,) b ) 
C_  ( A (,) b ) )
8679rexrd 9632 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  B  e.  RR* )
87 elicc2 11592 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( b  e.  ( A [,] B )  <-> 
( b  e.  RR  /\  A  <_  b  /\  b  <_  B ) ) )
8877, 79, 87syl2anc 659 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
b  e.  ( A [,] B )  <->  ( b  e.  RR  /\  A  <_ 
b  /\  b  <_  B ) ) )
8959, 88mpbid 210 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
b  e.  RR  /\  A  <_  b  /\  b  <_  B ) )
9089simp3d 1008 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  <_  B )
91 iooss2 11568 . . . . . . . . . . . . . . . . . 18  |-  ( ( B  e.  RR*  /\  b  <_  B )  ->  ( A (,) b )  C_  ( A (,) B ) )
9286, 90, 91syl2anc 659 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( A (,) b )  C_  ( A (,) B ) )
9385, 92sstrd 3499 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a (,) b ) 
C_  ( A (,) B ) )
94 ssn0 3817 . . . . . . . . . . . . . . . 16  |-  ( ( ( a (,) b
)  C_  ( A (,) B )  /\  (
a (,) b )  =/=  (/) )  ->  ( A (,) B )  =/=  (/) )
9593, 94sylan 469 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
( A (,) B
)  =/=  (/) )
96 n0 3793 . . . . . . . . . . . . . . . . 17  |-  ( ( A (,) B )  =/=  (/)  <->  E. x  x  e.  ( A (,) B
) )
97 0red 9586 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  0  e.  RR )
98 dvf 22480 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( RR 
_D  F ) : dom  ( RR  _D  F ) --> CC
99 dvlip.d . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
10099feq2d 5700 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( RR  _D  F ) : dom  ( RR  _D  F
) --> CC  <->  ( RR  _D  F ) : ( A (,) B ) --> CC ) )
10198, 100mpbii 211 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( RR  _D  F
) : ( A (,) B ) --> CC )
102101ffvelrnda 6007 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( ( RR  _D  F ) `  x )  e.  CC )
103102abscld 13352 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( abs `  ( ( RR  _D  F ) `  x
) )  e.  RR )
10473adantr 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  M  e.  RR )
105102absge0d 13360 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  0  <_  ( abs `  ( ( RR  _D  F ) `
 x ) ) )
106 dvlip.l . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( abs `  ( ( RR  _D  F ) `  x
) )  <_  M
)
10797, 103, 104, 105, 106letrd 9728 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  0  <_  M )
108107ex 432 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( x  e.  ( A (,) B )  ->  0  <_  M
) )
109108exlimdv 1729 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( E. x  x  e.  ( A (,) B )  ->  0  <_  M ) )
110109imp 427 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  E. x  x  e.  ( A (,) B ) )  -> 
0  <_  M )
11196, 110sylan2b 473 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( A (,) B )  =/=  (/) )  -> 
0  <_  M )
112111adantlr 712 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( A (,) B )  =/=  (/) )  ->  0  <_  M )
11395, 112syldan 468 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
0  <_  M )
114 simpr3 1002 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  <_  b )
11569, 67subge0d 10138 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
0  <_  ( b  -  a )  <->  a  <_  b ) )
116114, 115mpbird 232 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  0  <_  ( b  -  a
) )
117116adantr 463 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
0  <_  ( b  -  a ) )
11874, 76, 113, 117mulge0d 10125 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
0  <_  ( M  x.  ( b  -  a
) ) )
119118ex 432 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( a (,) b
)  =/=  (/)  ->  0  <_  ( M  x.  (
b  -  a ) ) ) )
12072, 119sylbird 235 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a  <  b  ->  0  <_  ( M  x.  ( b  -  a
) ) ) )
12169recnd 9611 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  CC )
12267recnd 9611 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  CC )
123121, 122subeq0ad 9932 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( b  -  a
)  =  0  <->  b  =  a ) )
124 equcom 1799 . . . . . . . . . . . . 13  |-  ( b  =  a  <->  a  =  b )
125123, 124syl6bb 261 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( b  -  a
)  =  0  <->  a  =  b ) )
126 0re 9585 . . . . . . . . . . . . . 14  |-  0  e.  RR
12773adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  M  e.  RR )
128127recnd 9611 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  M  e.  CC )
129128mul01d 9768 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( M  x.  0 )  =  0 )
130129eqcomd 2462 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  0  =  ( M  x.  0 ) )
131 eqle 9676 . . . . . . . . . . . . . 14  |-  ( ( 0  e.  RR  /\  0  =  ( M  x.  0 ) )  -> 
0  <_  ( M  x.  0 ) )
132126, 130, 131sylancr 661 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  0  <_  ( M  x.  0 ) )
133 oveq2 6278 . . . . . . . . . . . . . 14  |-  ( ( b  -  a )  =  0  ->  ( M  x.  ( b  -  a ) )  =  ( M  x.  0 ) )
134133breq2d 4451 . . . . . . . . . . . . 13  |-  ( ( b  -  a )  =  0  ->  (
0  <_  ( M  x.  ( b  -  a
) )  <->  0  <_  ( M  x.  0 ) ) )
135132, 134syl5ibrcom 222 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( b  -  a
)  =  0  -> 
0  <_  ( M  x.  ( b  -  a
) ) ) )
136125, 135sylbird 235 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a  =  b  -> 
0  <_  ( M  x.  ( b  -  a
) ) ) )
13767, 69leloed 9717 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a  <_  b  <->  ( a  <  b  \/  a  =  b ) ) )
138114, 137mpbid 210 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a  <  b  \/  a  =  b )
)
139120, 136, 138mpjaod 379 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  0  <_  ( M  x.  (
b  -  a ) ) )
140139adantr 463 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =  ( F `  a ) )  -> 
0  <_  ( M  x.  ( b  -  a
) ) )
14165, 140eqbrtrd 4459 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =  ( F `  a ) )  -> 
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  <_  ( M  x.  ( b  -  a
) ) )
14260, 62subcld 9922 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( F `  b
)  -  ( F `
 a ) )  e.  CC )
143142adantr 463 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( F `  b )  -  ( F `  a )
)  e.  CC )
144143abscld 13352 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  e.  RR )
145144recnd 9611 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  e.  CC )
14675adantr 463 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( b  -  a
)  e.  RR )
147146recnd 9611 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( b  -  a
)  e.  CC )
148138ord 375 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( -.  a  <  b  -> 
a  =  b ) )
149 fveq2 5848 . . . . . . . . . . . . . . . . 17  |-  ( a  =  b  ->  ( F `  a )  =  ( F `  b ) )
150149eqcomd 2462 . . . . . . . . . . . . . . . 16  |-  ( a  =  b  ->  ( F `  b )  =  ( F `  a ) )
151148, 150syl6 33 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( -.  a  <  b  -> 
( F `  b
)  =  ( F `
 a ) ) )
152151necon1ad 2670 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( F `  b
)  =/=  ( F `
 a )  -> 
a  <  b )
)
153152imp 427 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
a  <  b )
15467adantr 463 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
a  e.  RR )
15569adantr 463 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
b  e.  RR )
156154, 155posdifd 10135 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a  <  b  <->  0  <  ( b  -  a ) ) )
157153, 156mpbid 210 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
0  <  ( b  -  a ) )
158157gt0ne0d 10113 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( b  -  a
)  =/=  0 )
159145, 147, 158divrec2d 10320 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  /  ( b  -  a ) )  =  ( ( 1  /  ( b  -  a ) )  x.  ( abs `  (
( F `  b
)  -  ( F `
 a ) ) ) ) )
160 iccss2 11598 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B ) )  -> 
( a [,] b
)  C_  ( A [,] B ) )
16161, 59, 160syl2anc 659 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a [,] b ) 
C_  ( A [,] B ) )
162161adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a [,] b
)  C_  ( A [,] B ) )
163162sselda 3489 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  y  e.  ( a [,] b
) )  ->  y  e.  ( A [,] B
) )
16441ad2antrr 723 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  ->  F : ( A [,] B ) --> CC )
165164ffvelrnda 6007 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  y  e.  ( A [,] B
) )  ->  ( F `  y )  e.  CC )
166163, 165syldan 468 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  y  e.  ( a [,] b
) )  ->  ( F `  y )  e.  CC )
167142ad2antrr 723 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  y  e.  ( a [,] b
) )  ->  (
( F `  b
)  -  ( F `
 a ) )  e.  CC )
16863necon3bid 2712 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( ( F `  b )  -  ( F `  a )
)  =/=  0  <->  ( F `  b )  =/=  ( F `  a
) ) )
169168biimpar 483 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( F `  b )  -  ( F `  a )
)  =/=  0 )
170169adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  y  e.  ( a [,] b
) )  ->  (
( F `  b
)  -  ( F `
 a ) )  =/=  0 )
171166, 167, 170divcld 10316 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  y  e.  ( a [,] b
) )  ->  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) )  e.  CC )
172164, 162feqresmpt 5902 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( F  |`  (
a [,] b ) )  =  ( y  e.  ( a [,] b )  |->  ( F `
 y ) ) )
173 eqidd 2455 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( x  e.  CC  |->  ( x  /  (
( F `  b
)  -  ( F `
 a ) ) ) )  =  ( x  e.  CC  |->  ( x  /  ( ( F `  b )  -  ( F `  a ) ) ) ) )
174 oveq1 6277 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( F `  y )  ->  (
x  /  ( ( F `  b )  -  ( F `  a ) ) )  =  ( ( F `
 y )  / 
( ( F `  b )  -  ( F `  a )
) ) )
175166, 172, 173, 174fmptco 6040 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( x  e.  CC  |->  ( x  / 
( ( F `  b )  -  ( F `  a )
) ) )  o.  ( F  |`  (
a [,] b ) ) )  =  ( y  e.  ( a [,] b )  |->  ( ( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) )
176 ref 13030 . . . . . . . . . . . . . . . . 17  |-  Re : CC
--> RR
177176a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  ->  Re : CC --> RR )
178177feqmptd 5901 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  ->  Re  =  ( x  e.  CC  |->  ( Re `  x ) ) )
179 fveq2 5848 . . . . . . . . . . . . . . 15  |-  ( x  =  ( ( F `
 y )  / 
( ( F `  b )  -  ( F `  a )
) )  ->  (
Re `  x )  =  ( Re `  ( ( F `  y )  /  (
( F `  b
)  -  ( F `
 a ) ) ) ) )
180171, 175, 178, 179fmptco 6040 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( Re  o.  (
( x  e.  CC  |->  ( x  /  (
( F `  b
)  -  ( F `
 a ) ) ) )  o.  ( F  |`  ( a [,] b ) ) ) )  =  ( y  e.  ( a [,] b )  |->  ( Re
`  ( ( F `
 y )  / 
( ( F `  b )  -  ( F `  a )
) ) ) ) )
18139adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  F  e.  ( ( A [,] B ) -cn-> CC ) )
182 rescncf 21570 . . . . . . . . . . . . . . . . . 18  |-  ( ( a [,] b ) 
C_  ( A [,] B )  ->  ( F  e.  ( ( A [,] B ) -cn-> CC )  ->  ( F  |`  ( a [,] b
) )  e.  ( ( a [,] b
) -cn-> CC ) ) )
183161, 181, 182sylc 60 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( F  |`  ( a [,] b ) )  e.  ( ( a [,] b ) -cn-> CC ) )
184183adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( F  |`  (
a [,] b ) )  e.  ( ( a [,] b )
-cn-> CC ) )
185 eqid 2454 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  CC  |->  ( x  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  =  ( x  e.  CC  |->  ( x  /  (
( F `  b
)  -  ( F `
 a ) ) ) )
186185divccncf 21579 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( F `  b )  -  ( F `  a )
)  e.  CC  /\  ( ( F `  b )  -  ( F `  a )
)  =/=  0 )  ->  ( x  e.  CC  |->  ( x  / 
( ( F `  b )  -  ( F `  a )
) ) )  e.  ( CC -cn-> CC ) )
187143, 169, 186syl2anc 659 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( x  e.  CC  |->  ( x  /  (
( F `  b
)  -  ( F `
 a ) ) ) )  e.  ( CC -cn-> CC ) )
188184, 187cncfco 21580 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( x  e.  CC  |->  ( x  / 
( ( F `  b )  -  ( F `  a )
) ) )  o.  ( F  |`  (
a [,] b ) ) )  e.  ( ( a [,] b
) -cn-> CC ) )
189 recncf 21575 . . . . . . . . . . . . . . . 16  |-  Re  e.  ( CC -cn-> RR )
190189a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  ->  Re  e.  ( CC -cn-> RR ) )
191188, 190cncfco 21580 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( Re  o.  (
( x  e.  CC  |->  ( x  /  (
( F `  b
)  -  ( F `
 a ) ) ) )  o.  ( F  |`  ( a [,] b ) ) ) )  e.  ( ( a [,] b )
-cn-> RR ) )
192180, 191eqeltrrd 2543 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( y  e.  ( a [,] b ) 
|->  ( Re `  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) )  e.  ( ( a [,] b
) -cn-> RR ) )
19349a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  ->  RR  C_  CC )
194 iccssre 11609 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  e.  RR  /\  b  e.  RR )  ->  ( a [,] b
)  C_  RR )
195154, 155, 194syl2anc 659 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a [,] b
)  C_  RR )
196171recld 13112 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  y  e.  ( a [,] b
) )  ->  (
Re `  ( ( F `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  e.  RR )
197196recnd 9611 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  y  e.  ( a [,] b
) )  ->  (
Re `  ( ( F `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  e.  CC )
198 eqid 2454 . . . . . . . . . . . . . . . . . 18  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
199198tgioo2 21477 . . . . . . . . . . . . . . . . 17  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
200 iccntr 21495 . . . . . . . . . . . . . . . . . . 19  |-  ( ( a  e.  RR  /\  b  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( a [,] b ) )  =  ( a (,) b
) )
20167, 69, 200syl2anc 659 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( int `  ( topGen `
 ran  (,) )
) `  ( a [,] b ) )  =  ( a (,) b
) )
202201adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( int `  ( topGen `
 ran  (,) )
) `  ( a [,] b ) )  =  ( a (,) b
) )
203193, 195, 197, 199, 198, 202dvmptntr 22543 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( RR  _D  (
y  e.  ( a [,] b )  |->  ( Re `  ( ( F `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) ) ) )  =  ( RR 
_D  ( y  e.  ( a (,) b
)  |->  ( Re `  ( ( F `  y )  /  (
( F `  b
)  -  ( F `
 a ) ) ) ) ) ) )
204 ioossicc 11613 . . . . . . . . . . . . . . . . . . 19  |-  ( a (,) b )  C_  ( a [,] b
)
205204sseli 3485 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( a (,) b )  ->  y  e.  ( a [,] b
) )
206205, 171sylan2 472 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  y  e.  ( a (,) b
) )  ->  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) )  e.  CC )
207 ovex 6298 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( RR  _D  F
) `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) )  e.  _V
208207a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  y  e.  ( a (,) b
) )  ->  (
( ( RR  _D  F ) `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) )  e.  _V )
209 reelprrecn 9573 . . . . . . . . . . . . . . . . . . 19  |-  RR  e.  { RR ,  CC }
210209a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  ->  RR  e.  { RR ,  CC } )
211205, 166sylan2 472 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  y  e.  ( a (,) b
) )  ->  ( F `  y )  e.  CC )
21293adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a (,) b
)  C_  ( A (,) B ) )
213212sselda 3489 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  y  e.  ( a (,) b
) )  ->  y  e.  ( A (,) B
) )
214101ad2antrr 723 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( RR  _D  F
) : ( A (,) B ) --> CC )
215214ffvelrnda 6007 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  y  e.  ( A (,) B
) )  ->  (
( RR  _D  F
) `  y )  e.  CC )
216213, 215syldan 468 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  y  e.  ( a (,) b
) )  ->  (
( RR  _D  F
) `  y )  e.  CC )
21738ad2antrr 723 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( A [,] B
)  C_  RR )
218 ioossre 11589 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a (,) b )  C_  RR
219218a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a (,) b
)  C_  RR )
220198, 199dvres 22484 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( RR  C_  CC  /\  F : ( A [,] B ) --> CC )  /\  ( ( A [,] B ) 
C_  RR  /\  (
a (,) b ) 
C_  RR ) )  ->  ( RR  _D  ( F  |`  ( a (,) b ) ) )  =  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( a (,) b ) ) ) )
221193, 164, 217, 219, 220syl22anc 1227 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( RR  _D  ( F  |`  ( a (,) b ) ) )  =  ( ( RR 
_D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( a (,) b ) ) ) )
222 retop 21437 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( topGen ` 
ran  (,) )  e.  Top
223 iooretop 21442 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a (,) b )  e.  ( topGen `  ran  (,) )
224 isopn3i 19753 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( a (,) b )  e.  ( topGen `  ran  (,) )
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  (
a (,) b ) )  =  ( a (,) b ) )
225222, 223, 224mp2an 670 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( a (,) b
) )  =  ( a (,) b )
226225reseq2i 5259 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( a (,) b ) ) )  =  ( ( RR 
_D  F )  |`  ( a (,) b
) )
227221, 226syl6eq 2511 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( RR  _D  ( F  |`  ( a (,) b ) ) )  =  ( ( RR 
_D  F )  |`  ( a (,) b
) ) )
228204, 162syl5ss 3500 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a (,) b
)  C_  ( A [,] B ) )
229164, 228feqresmpt 5902 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( F  |`  (
a (,) b ) )  =  ( y  e.  ( a (,) b )  |->  ( F `
 y ) ) )
230229oveq2d 6286 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( RR  _D  ( F  |`  ( a (,) b ) ) )  =  ( RR  _D  ( y  e.  ( a (,) b ) 
|->  ( F `  y
) ) ) )
231101adantr 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( RR  _D  F ) : ( A (,) B
) --> CC )
232231, 93fssresd 5734 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( RR  _D  F
)  |`  ( a (,) b ) ) : ( a (,) b
) --> CC )
233232feqmptd 5901 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( RR  _D  F
)  |`  ( a (,) b ) )  =  ( y  e.  ( a (,) b ) 
|->  ( ( ( RR 
_D  F )  |`  ( a (,) b
) ) `  y
) ) )
234233adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( RR  _D  F )  |`  (
a (,) b ) )  =  ( y  e.  ( a (,) b )  |->  ( ( ( RR  _D  F
)  |`  ( a (,) b ) ) `  y ) ) )
235 fvres 5862 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( a (,) b )  ->  (
( ( RR  _D  F )  |`  (
a (,) b ) ) `  y )  =  ( ( RR 
_D  F ) `  y ) )
236235mpteq2ia 4521 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( a (,) b )  |->  ( ( ( RR  _D  F
)  |`  ( a (,) b ) ) `  y ) )  =  ( y  e.  ( a (,) b ) 
|->  ( ( RR  _D  F ) `  y
) )
237234, 236syl6eq 2511 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( RR  _D  F )  |`  (
a (,) b ) )  =  ( y  e.  ( a (,) b )  |->  ( ( RR  _D  F ) `
 y ) ) )
238227, 230, 2373eqtr3d 2503 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( RR  _D  (
y  e.  ( a (,) b )  |->  ( F `  y ) ) )  =  ( y  e.  ( a (,) b )  |->  ( ( RR  _D  F
) `  y )
) )
239210, 211, 216, 238, 143, 169dvmptdivc 22537 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( RR  _D  (
y  e.  ( a (,) b )  |->  ( ( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) )  =  ( y  e.  ( a (,) b )  |->  ( ( ( RR  _D  F ) `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) )
240206, 208, 239dvmptre 22541 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( RR  _D  (
y  e.  ( a (,) b )  |->  ( Re `  ( ( F `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) ) ) )  =  ( y  e.  ( a (,) b )  |->  ( Re
`  ( ( ( RR  _D  F ) `
 y )  / 
( ( F `  b )  -  ( F `  a )
) ) ) ) )
241203, 240eqtrd 2495 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( RR  _D  (
y  e.  ( a [,] b )  |->  ( Re `  ( ( F `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) ) ) )  =  ( y  e.  ( a (,) b )  |->  ( Re
`  ( ( ( RR  _D  F ) `
 y )  / 
( ( F `  b )  -  ( F `  a )
) ) ) ) )
242241dmeqd 5194 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  ->  dom  ( RR  _D  (
y  e.  ( a [,] b )  |->  ( Re `  ( ( F `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) ) ) )  =  dom  (
y  e.  ( a (,) b )  |->  ( Re `  ( ( ( RR  _D  F
) `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) ) ) )
243 dmmptg 5487 . . . . . . . . . . . . . . 15  |-  ( A. y  e.  ( a (,) b ) ( Re
`  ( ( ( RR  _D  F ) `
 y )  / 
( ( F `  b )  -  ( F `  a )
) ) )  e. 
_V  ->  dom  ( y  e.  ( a (,) b
)  |->  ( Re `  ( ( ( RR 
_D  F ) `  y )  /  (
( F `  b
)  -  ( F `
 a ) ) ) ) )  =  ( a (,) b
) )
244 fvex 5858 . . . . . . . . . . . . . . . 16  |-  ( Re
`  ( ( ( RR  _D  F ) `
 y )  / 
( ( F `  b )  -  ( F `  a )
) ) )  e. 
_V
245244a1i 11 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( a (,) b )  ->  (
Re `  ( (
( RR  _D  F
) `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  e. 
_V )
246243, 245mprg 2817 . . . . . . . . . . . . . 14  |-  dom  (
y  e.  ( a (,) b )  |->  ( Re `  ( ( ( RR  _D  F
) `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) ) )  =  ( a (,) b )
247242, 246syl6eq 2511 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  ->  dom  ( RR  _D  (
y  e.  ( a [,] b )  |->  ( Re `  ( ( F `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) ) ) )  =  ( a (,) b ) )
248154, 155, 153, 192, 247mvth 22562 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  ->  E. x  e.  (
a (,) b ) ( ( RR  _D  ( y  e.  ( a [,] b ) 
|->  ( Re `  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) ) ) `  x )  =  ( ( ( ( y  e.  ( a [,] b )  |->  ( Re
`  ( ( F `
 y )  / 
( ( F `  b )  -  ( F `  a )
) ) ) ) `
 b )  -  ( ( y  e.  ( a [,] b
)  |->  ( Re `  ( ( F `  y )  /  (
( F `  b
)  -  ( F `
 a ) ) ) ) ) `  a ) )  / 
( b  -  a
) ) )
249241fveq1d 5850 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( RR  _D  ( y  e.  ( a [,] b ) 
|->  ( Re `  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) ) ) `  x )  =  ( ( y  e.  ( a (,) b ) 
|->  ( Re `  (
( ( RR  _D  F ) `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) ) `  x
) )
250 fveq2 5848 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  x  ->  (
( RR  _D  F
) `  y )  =  ( ( RR 
_D  F ) `  x ) )
251250oveq1d 6285 . . . . . . . . . . . . . . . . 17  |-  ( y  =  x  ->  (
( ( RR  _D  F ) `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) )  =  ( ( ( RR  _D  F ) `
 x )  / 
( ( F `  b )  -  ( F `  a )
) ) )
252251fveq2d 5852 . . . . . . . . . . . . . . . 16  |-  ( y  =  x  ->  (
Re `  ( (
( RR  _D  F
) `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  =  ( Re `  (
( ( RR  _D  F ) `  x
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) )
253 eqid 2454 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( a (,) b )  |->  ( Re
`  ( ( ( RR  _D  F ) `
 y )  / 
( ( F `  b )  -  ( F `  a )
) ) ) )  =  ( y  e.  ( a (,) b
)  |->  ( Re `  ( ( ( RR 
_D  F ) `  y )  /  (
( F `  b
)  -  ( F `
 a ) ) ) ) )
254 fvex 5858 . . . . . . . . . . . . . . . 16  |-  ( Re
`  ( ( ( RR  _D  F ) `
 x )  / 
( ( F `  b )  -  ( F `  a )
) ) )  e. 
_V
255252, 253, 254fvmpt 5931 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( a (,) b )  ->  (
( y  e.  ( a (,) b ) 
|->  ( Re `  (
( ( RR  _D  F ) `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) ) `  x
)  =  ( Re
`  ( ( ( RR  _D  F ) `
 x )  / 
( ( F `  b )  -  ( F `  a )
) ) ) )
256249, 255sylan9eq 2515 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  (
( RR  _D  (
y  e.  ( a [,] b )  |->  ( Re `  ( ( F `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) ) ) ) `  x )  =  ( Re `  ( ( ( RR 
_D  F ) `  x )  /  (
( F `  b
)  -  ( F `
 a ) ) ) ) )
257 ubicc2 11640 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  RR*  /\  b  e.  RR*  /\  a  <_ 
b )  ->  b  e.  ( a [,] b
) )
25868, 70, 114, 257syl3anc 1226 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  ( a [,] b
) )
259258ad2antrr 723 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  b  e.  ( a [,] b
) )
26017oveq1d 6285 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  b  ->  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) )  =  ( ( F `
 b )  / 
( ( F `  b )  -  ( F `  a )
) ) )
261260fveq2d 5852 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  b  ->  (
Re `  ( ( F `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  =  ( Re `  (
( F `  b
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) )
262 eqid 2454 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( a [,] b )  |->  ( Re
`  ( ( F `
 y )  / 
( ( F `  b )  -  ( F `  a )
) ) ) )  =  ( y  e.  ( a [,] b
)  |->  ( Re `  ( ( F `  y )  /  (
( F `  b
)  -  ( F `
 a ) ) ) ) )
263 fvex 5858 . . . . . . . . . . . . . . . . . . 19  |-  ( Re
`  ( ( F `
 b )  / 
( ( F `  b )  -  ( F `  a )
) ) )  e. 
_V
264261, 262, 263fvmpt 5931 . . . . . . . . . . . . . . . . . 18  |-  ( b  e.  ( a [,] b )  ->  (
( y  e.  ( a [,] b ) 
|->  ( Re `  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) ) `  b
)  =  ( Re
`  ( ( F `
 b )  / 
( ( F `  b )  -  ( F `  a )
) ) ) )
265259, 264syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  (
( y  e.  ( a [,] b ) 
|->  ( Re `  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) ) `  b
)  =  ( Re
`  ( ( F `
 b )  / 
( ( F `  b )  -  ( F `  a )
) ) ) )
266 lbicc2 11639 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  RR*  /\  b  e.  RR*  /\  a  <_ 
b )  ->  a  e.  ( a [,] b
) )
26768, 70, 114, 266syl3anc 1226 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  ( a [,] b
) )
268267ad2antrr 723 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  a  e.  ( a [,] b
) )
26926oveq1d 6285 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  a  ->  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) )  =  ( ( F `
 a )  / 
( ( F `  b )  -  ( F `  a )
) ) )
270269fveq2d 5852 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  a  ->  (
Re `  ( ( F `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  =  ( Re `  (
( F `  a
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) )
271 fvex 5858 . . . . . . . . . . . . . . . . . . 19  |-  ( Re
`  ( ( F `
 a )  / 
( ( F `  b )  -  ( F `  a )
) ) )  e. 
_V
272270, 262, 271fvmpt 5931 . . . . . . . . . . . . . . . . . 18  |-  ( a  e.  ( a [,] b )  ->  (
( y  e.  ( a [,] b ) 
|->  ( Re `  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) ) `  a
)  =  ( Re
`  ( ( F `
 a )  / 
( ( F `  b )  -  ( F `  a )
) ) ) )
273268, 272syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  (
( y  e.  ( a [,] b ) 
|->  ( Re `  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) ) `  a
)  =  ( Re
`  ( ( F `
 a )  / 
( ( F `  b )  -  ( F `  a )
) ) ) )
274265, 273oveq12d 6288 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  (
( ( y  e.  ( a [,] b
)  |->  ( Re `  ( ( F `  y )  /  (
( F `  b
)  -  ( F `
 a ) ) ) ) ) `  b )  -  (
( y  e.  ( a [,] b ) 
|->  ( Re `  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) ) `  a
) )  =  ( ( Re `  (
( F `  b
)  /  ( ( F `  b )  -  ( F `  a ) ) ) )  -  ( Re
`  ( ( F `
 a )  / 
( ( F `  b )  -  ( F `  a )
) ) ) ) )
27560adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( F `  b
)  e.  CC )
276275, 143, 169divcld 10316 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( F `  b )  /  (
( F `  b
)  -  ( F `
 a ) ) )  e.  CC )
27762adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( F `  a
)  e.  CC )
278277, 143, 169divcld 10316 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( F `  a )  /  (
( F `  b
)  -  ( F `
 a ) ) )  e.  CC )
279276, 278resubd 13134 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( Re `  (
( ( F `  b )  /  (
( F `  b
)  -  ( F `
 a ) ) )  -  ( ( F `  a )  /  ( ( F `
 b )  -  ( F `  a ) ) ) ) )  =  ( ( Re
`  ( ( F `
 b )  / 
( ( F `  b )  -  ( F `  a )
) ) )  -  ( Re `  ( ( F `  a )  /  ( ( F `
 b )  -  ( F `  a ) ) ) ) ) )
280275, 277, 143, 169divsubdird 10355 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( ( F `
 b )  -  ( F `  a ) )  /  ( ( F `  b )  -  ( F `  a ) ) )  =  ( ( ( F `  b )  /  ( ( F `
 b )  -  ( F `  a ) ) )  -  (
( F `  a
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) )
281143, 169dividd 10314 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( ( F `
 b )  -  ( F `  a ) )  /  ( ( F `  b )  -  ( F `  a ) ) )  =  1 )
282280, 281eqtr3d 2497 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( ( F `
 b )  / 
( ( F `  b )  -  ( F `  a )
) )  -  (
( F `  a
)  /  ( ( F `  b )  -  ( F `  a ) ) ) )  =  1 )
283282fveq2d 5852 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( Re `  (
( ( F `  b )  /  (
( F `  b
)  -  ( F `
 a ) ) )  -  ( ( F `  a )  /  ( ( F `
 b )  -  ( F `  a ) ) ) ) )  =  ( Re ` 
1 ) )
284 re1 13072 . . . . . . . . . . . . . . . . . . 19  |-  ( Re
`  1 )  =  1
285283, 284syl6eq 2511 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( Re `  (
( ( F `  b )  /  (
( F `  b
)  -  ( F `
 a ) ) )  -  ( ( F `  a )  /  ( ( F `
 b )  -  ( F `  a ) ) ) ) )  =  1 )
286279, 285eqtr3d 2497 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( Re `  ( ( F `  b )  /  (
( F `  b
)  -  ( F `
 a ) ) ) )  -  (
Re `  ( ( F `  a )  /  ( ( F `
 b )  -  ( F `  a ) ) ) ) )  =  1 )
287286adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  (
( Re `  (
( F `  b
)  /  ( ( F `  b )  -  ( F `  a ) ) ) )  -  ( Re
`  ( ( F `
 a )  / 
( ( F `  b )  -  ( F `  a )
) ) ) )  =  1 )
288274, 287eqtrd 2495 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  (
( ( y  e.  ( a [,] b
)  |->  ( Re `  ( ( F `  y )  /  (
( F `  b
)  -  ( F `
 a ) ) ) ) ) `  b )  -  (
( y  e.  ( a [,] b ) 
|->  ( Re `  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) ) `  a
) )  =  1 )
289288oveq1d 6285 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  (
( ( ( y  e.  ( a [,] b )  |->  ( Re
`  ( ( F `
 y )  / 
( ( F `  b )  -  ( F `  a )
) ) ) ) `
 b )  -  ( ( y  e.  ( a [,] b
)  |->  ( Re `  ( ( F `  y )  /  (
( F `  b
)  -  ( F `
 a ) ) ) ) ) `  a ) )  / 
( b  -  a
) )  =  ( 1  /  ( b  -  a ) ) )
290256, 289eqeq12d 2476 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  (
( ( RR  _D  ( y  e.  ( a [,] b ) 
|->  ( Re `  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) ) ) `  x )  =  ( ( ( ( y  e.  ( a [,] b )  |->  ( Re
`  ( ( F `
 y )  / 
( ( F `  b )  -  ( F `  a )
) ) ) ) `
 b )  -  ( ( y  e.  ( a [,] b
)  |->  ( Re `  ( ( F `  y )  /  (
( F `  b
)  -  ( F `
 a ) ) ) ) ) `  a ) )  / 
( b  -  a
) )  <->  ( Re `  ( ( ( RR 
_D  F ) `  x )  /  (
( F `  b
)  -  ( F `
 a ) ) ) )  =  ( 1  /  ( b  -  a ) ) ) )
291290rexbidva 2962 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( E. x  e.  ( a (,) b
) ( ( RR 
_D  ( y  e.  ( a [,] b
)  |->  ( Re `  ( ( F `  y )  /  (
( F `  b
)  -  ( F `
 a ) ) ) ) ) ) `
 x )  =  ( ( ( ( y  e.  ( a [,] b )  |->  ( Re `  ( ( F `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) ) ) `
 b )  -  ( ( y  e.  ( a [,] b
)  |->  ( Re `  ( ( F `  y )  /  (
( F `  b
)  -  ( F `
 a ) ) ) ) ) `  a ) )  / 
( b  -  a
) )  <->  E. x  e.  ( a (,) b
) ( Re `  ( ( ( RR 
_D  F ) `  x )  /  (
( F `  b
)  -  ( F `
 a ) ) ) )  =  ( 1  /  ( b  -  a ) ) ) )
292248, 291mpbid 210 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  ->  E. x  e.  (
a (,) b ) ( Re `  (
( ( RR  _D  F ) `  x
)  /  ( ( F `  b )  -  ( F `  a ) ) ) )  =  ( 1  /  ( b  -  a ) ) )
293212sselda 3489 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  x  e.  ( A (,) B
) )
294214ffvelrnda 6007 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( A (,) B
) )  ->  (
( RR  _D  F
) `  x )  e.  CC )
295293, 294syldan 468 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  (
( RR  _D  F
) `  x )  e.  CC )
296142ad2antrr 723 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  (
( F `  b
)  -  ( F `
 a ) )  e.  CC )
297169adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  (
( F `  b
)  -  ( F `
 a ) )  =/=  0 )
298295, 296, 297divcld 10316 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  (
( ( RR  _D  F ) `  x
)  /  ( ( F `  b )  -  ( F `  a ) ) )  e.  CC )
299298recld 13112 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  (
Re `  ( (
( RR  _D  F
) `  x )  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  e.  RR )
300144adantr 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  ( abs `  ( ( F `
 b )  -  ( F `  a ) ) )  e.  RR )
301299, 300remulcld 9613 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  (
( Re `  (
( ( RR  _D  F ) `  x
)  /  ( ( F `  b )  -  ( F `  a ) ) ) )  x.  ( abs `  ( ( F `  b )  -  ( F `  a )
) ) )  e.  RR )
302295abscld 13352 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  ( abs `  ( ( RR 
_D  F ) `  x ) )  e.  RR )
303127ad2antrr 723 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  M  e.  RR )
304298abscld 13352 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  ( abs `  ( ( ( RR  _D  F ) `
 x )  / 
( ( F `  b )  -  ( F `  a )
) ) )  e.  RR )
305143absge0d 13360 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
0  <_  ( abs `  ( ( F `  b )  -  ( F `  a )
) ) )
306305adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  0  <_  ( abs `  (
( F `  b
)  -  ( F `
 a ) ) ) )
307298releabsd 13367 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  (
Re `  ( (
( RR  _D  F
) `  x )  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  <_ 
( abs `  (
( ( RR  _D  F ) `  x
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) )
308299, 304, 300, 306, 307lemul1ad 10480 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  (
( Re `  (
( ( RR  _D  F ) `  x
)  /  ( ( F `  b )  -  ( F `  a ) ) ) )  x.  ( abs `  ( ( F `  b )  -  ( F `  a )
) ) )  <_ 
( ( abs `  (
( ( RR  _D  F ) `  x
)  /  ( ( F `  b )  -