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

Theorem dvlip 22887
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 5825 . . . . . . . 8  |-  ( a  =  Y  ->  ( F `  a )  =  ( F `  Y ) )
21oveq2d 6265 . . . . . . 7  |-  ( a  =  Y  ->  (
( F `  b
)  -  ( F `
 a ) )  =  ( ( F `
 b )  -  ( F `  Y ) ) )
32fveq2d 5829 . . . . . 6  |-  ( a  =  Y  ->  ( abs `  ( ( F `
 b )  -  ( F `  a ) ) )  =  ( abs `  ( ( F `  b )  -  ( F `  Y ) ) ) )
4 oveq2 6257 . . . . . . . 8  |-  ( a  =  Y  ->  (
b  -  a )  =  ( b  -  Y ) )
54fveq2d 5829 . . . . . . 7  |-  ( a  =  Y  ->  ( abs `  ( b  -  a ) )  =  ( abs `  (
b  -  Y ) ) )
65oveq2d 6265 . . . . . 6  |-  ( a  =  Y  ->  ( M  x.  ( abs `  ( b  -  a
) ) )  =  ( M  x.  ( abs `  ( b  -  Y ) ) ) )
73, 6breq12d 4379 . . . . 5  |-  ( a  =  Y  ->  (
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  <_  ( M  x.  ( abs `  (
b  -  a ) ) )  <->  ( abs `  ( ( F `  b )  -  ( F `  Y )
) )  <_  ( M  x.  ( abs `  ( b  -  Y
) ) ) ) )
87imbi2d 317 . . . 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 5825 . . . . . . . 8  |-  ( b  =  X  ->  ( F `  b )  =  ( F `  X ) )
109oveq1d 6264 . . . . . . 7  |-  ( b  =  X  ->  (
( F `  b
)  -  ( F `
 Y ) )  =  ( ( F `
 X )  -  ( F `  Y ) ) )
1110fveq2d 5829 . . . . . 6  |-  ( b  =  X  ->  ( abs `  ( ( F `
 b )  -  ( F `  Y ) ) )  =  ( abs `  ( ( F `  X )  -  ( F `  Y ) ) ) )
12 oveq1 6256 . . . . . . . 8  |-  ( b  =  X  ->  (
b  -  Y )  =  ( X  -  Y ) )
1312fveq2d 5829 . . . . . . 7  |-  ( b  =  X  ->  ( abs `  ( b  -  Y ) )  =  ( abs `  ( X  -  Y )
) )
1413oveq2d 6265 . . . . . 6  |-  ( b  =  X  ->  ( M  x.  ( abs `  ( b  -  Y
) ) )  =  ( M  x.  ( abs `  ( X  -  Y ) ) ) )
1511, 14breq12d 4379 . . . . 5  |-  ( b  =  X  ->  (
( abs `  (
( F `  b
)  -  ( F `
 Y ) ) )  <_  ( M  x.  ( abs `  (
b  -  Y ) ) )  <->  ( abs `  ( ( F `  X )  -  ( F `  Y )
) )  <_  ( M  x.  ( abs `  ( X  -  Y
) ) ) ) )
1615imbi2d 317 . . . 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 5825 . . . . . . . . . 10  |-  ( y  =  b  ->  ( F `  y )  =  ( F `  b ) )
18 fveq2 5825 . . . . . . . . . 10  |-  ( x  =  a  ->  ( F `  x )  =  ( F `  a ) )
1917, 18oveqan12d 6268 . . . . . . . . 9  |-  ( ( y  =  b  /\  x  =  a )  ->  ( ( F `  y )  -  ( F `  x )
)  =  ( ( F `  b )  -  ( F `  a ) ) )
2019fveq2d 5829 . . . . . . . 8  |-  ( ( y  =  b  /\  x  =  a )  ->  ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  =  ( abs `  ( ( F `  b )  -  ( F `  a )
) ) )
21 oveq12 6258 . . . . . . . . . 10  |-  ( ( y  =  b  /\  x  =  a )  ->  ( y  -  x
)  =  ( b  -  a ) )
2221fveq2d 5829 . . . . . . . . 9  |-  ( ( y  =  b  /\  x  =  a )  ->  ( abs `  (
y  -  x ) )  =  ( abs `  ( b  -  a
) ) )
2322oveq2d 6265 . . . . . . . 8  |-  ( ( y  =  b  /\  x  =  a )  ->  ( M  x.  ( abs `  ( y  -  x ) ) )  =  ( M  x.  ( abs `  ( b  -  a ) ) ) )
2420, 23breq12d 4379 . . . . . . 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 454 . . . . . 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 5825 . . . . . . . . . 10  |-  ( y  =  a  ->  ( F `  y )  =  ( F `  a ) )
27 fveq2 5825 . . . . . . . . . 10  |-  ( x  =  b  ->  ( F `  x )  =  ( F `  b ) )
2826, 27oveqan12d 6268 . . . . . . . . 9  |-  ( ( y  =  a  /\  x  =  b )  ->  ( ( F `  y )  -  ( F `  x )
)  =  ( ( F `  a )  -  ( F `  b ) ) )
2928fveq2d 5829 . . . . . . . 8  |-  ( ( y  =  a  /\  x  =  b )  ->  ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  =  ( abs `  ( ( F `  a )  -  ( F `  b )
) ) )
30 oveq12 6258 . . . . . . . . . 10  |-  ( ( y  =  a  /\  x  =  b )  ->  ( y  -  x
)  =  ( a  -  b ) )
3130fveq2d 5829 . . . . . . . . 9  |-  ( ( y  =  a  /\  x  =  b )  ->  ( abs `  (
y  -  x ) )  =  ( abs `  ( a  -  b
) ) )
3231oveq2d 6265 . . . . . . . 8  |-  ( ( y  =  a  /\  x  =  b )  ->  ( M  x.  ( abs `  ( y  -  x ) ) )  =  ( M  x.  ( abs `  ( a  -  b ) ) ) )
3329, 32breq12d 4379 . . . . . . 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 454 . . . . . 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 11667 . . . . . . 7  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A [,] B
)  C_  RR )
3835, 36, 37syl2anc 665 . . . . . 6  |-  ( ph  ->  ( A [,] B
)  C_  RR )
39 dvlip.f . . . . . . . . . . 11  |-  ( ph  ->  F  e.  ( ( A [,] B )
-cn-> CC ) )
40 cncff 21867 . . . . . . . . . . 11  |-  ( F  e.  ( ( A [,] B ) -cn-> CC )  ->  F :
( A [,] B
) --> CC )
4139, 40syl 17 . . . . . . . . . 10  |-  ( ph  ->  F : ( A [,] B ) --> CC )
42 ffvelrn 5979 . . . . . . . . . . 11  |-  ( ( F : ( A [,] B ) --> CC 
/\  a  e.  ( A [,] B ) )  ->  ( F `  a )  e.  CC )
43 ffvelrn 5979 . . . . . . . . . . 11  |-  ( ( F : ( A [,] B ) --> CC 
/\  b  e.  ( A [,] B ) )  ->  ( F `  b )  e.  CC )
4442, 43anim12dan 845 . . . . . . . . . 10  |-  ( ( F : ( A [,] B ) --> CC 
/\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  (
( F `  a
)  e.  CC  /\  ( F `  b )  e.  CC ) )
4541, 44sylan 473 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  (
( F `  a
)  e.  CC  /\  ( F `  b )  e.  CC ) )
4645simprd 464 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( F `  b )  e.  CC )
4745simpld 460 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( F `  a )  e.  CC )
4846, 47abssubd 13458 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( abs `  ( ( F `
 b )  -  ( F `  a ) ) )  =  ( abs `  ( ( F `  a )  -  ( F `  b ) ) ) )
49 ax-resscn 9547 . . . . . . . . . . . 12  |-  RR  C_  CC
5038, 49syl6ss 3419 . . . . . . . . . . 11  |-  ( ph  ->  ( A [,] B
)  C_  CC )
5150sselda 3407 . . . . . . . . . 10  |-  ( (
ph  /\  b  e.  ( A [,] B ) )  ->  b  e.  CC )
5251adantrl 720 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  b  e.  CC )
5350sselda 3407 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  ( A [,] B ) )  ->  a  e.  CC )
5453adantrr 721 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  a  e.  CC )
5552, 54abssubd 13458 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( abs `  ( b  -  a ) )  =  ( abs `  (
a  -  b ) ) )
5655oveq2d 6265 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( M  x.  ( abs `  ( b  -  a
) ) )  =  ( M  x.  ( abs `  ( a  -  b ) ) ) )
5748, 56breq12d 4379 . . . . . 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 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  F : ( A [,] B ) --> CC )
59 simpr2 1012 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  ( A [,] B
) )
6058, 59ffvelrnd 5982 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( F `  b )  e.  CC )
61 simpr1 1011 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  ( A [,] B
) )
6258, 61ffvelrnd 5982 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( F `  a )  e.  CC )
6360, 62subeq0ad 9947 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( ( F `  b )  -  ( F `  a )
)  =  0  <->  ( F `  b )  =  ( F `  a ) ) )
6463biimpar 487 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =  ( F `  a ) )  -> 
( ( F `  b )  -  ( F `  a )
)  =  0 )
6564abs00bd 13298 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =  ( F `  a ) )  -> 
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  =  0 )
6638adantr 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( A [,] B )  C_  RR )
6766, 61sseldd 3408 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  RR )
6867rexrd 9641 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  RR* )
6966, 59sseldd 3408 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  RR )
7069rexrd 9641 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  RR* )
71 ioon0 11613 . . . . . . . . . . . . 13  |-  ( ( a  e.  RR*  /\  b  e.  RR* )  ->  (
( a (,) b
)  =/=  (/)  <->  a  <  b ) )
7268, 70, 71syl2anc 665 . . . . . . . . . . . 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 730 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  ->  M  e.  RR )
7569, 67resubcld 9998 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
b  -  a )  e.  RR )
7675adantr 466 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
( b  -  a
)  e.  RR )
7735adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  A  e.  RR )
7877rexrd 9641 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  A  e.  RR* )
7936adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  B  e.  RR )
80 elicc2 11650 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( a  e.  ( A [,] B )  <-> 
( a  e.  RR  /\  A  <_  a  /\  a  <_  B ) ) )
8177, 79, 80syl2anc 665 . . . . . . . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a  e.  RR  /\  A  <_  a  /\  a  <_  B ) )
8382simp2d 1018 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  A  <_  a )
84 iooss1 11622 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  RR*  /\  A  <_  a )  ->  (
a (,) b ) 
C_  ( A (,) b ) )
8578, 83, 84syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a (,) b ) 
C_  ( A (,) b ) )
8679rexrd 9641 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  B  e.  RR* )
87 elicc2 11650 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( b  e.  ( A [,] B )  <-> 
( b  e.  RR  /\  A  <_  b  /\  b  <_  B ) ) )
8877, 79, 87syl2anc 665 . . . . . . . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
b  e.  RR  /\  A  <_  b  /\  b  <_  B ) )
9089simp3d 1019 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  <_  B )
91 iooss2 11623 . . . . . . . . . . . . . . . . . 18  |-  ( ( B  e.  RR*  /\  b  <_  B )  ->  ( A (,) b )  C_  ( A (,) B ) )
9286, 90, 91syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( A (,) b )  C_  ( A (,) B ) )
9385, 92sstrd 3417 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a (,) b ) 
C_  ( A (,) B ) )
94 ssn0 3740 . . . . . . . . . . . . . . . 16  |-  ( ( ( a (,) b
)  C_  ( A (,) B )  /\  (
a (,) b )  =/=  (/) )  ->  ( A (,) B )  =/=  (/) )
9593, 94sylan 473 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
( A (,) B
)  =/=  (/) )
96 n0 3714 . . . . . . . . . . . . . . . . 17  |-  ( ( A (,) B )  =/=  (/)  <->  E. x  x  e.  ( A (,) B
) )
97 0red 9595 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  0  e.  RR )
98 dvf 22804 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( RR 
_D  F ) : dom  ( RR  _D  F ) --> CC
99 dvlip.d . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
10099feq2d 5676 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( RR  _D  F ) : dom  ( RR  _D  F
) --> CC  <->  ( RR  _D  F ) : ( A (,) B ) --> CC ) )
10198, 100mpbii 214 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( RR  _D  F
) : ( A (,) B ) --> CC )
102101ffvelrnda 5981 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( ( RR  _D  F ) `  x )  e.  CC )
103102abscld 13441 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( abs `  ( ( RR  _D  F ) `  x
) )  e.  RR )
10473adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  M  e.  RR )
105102absge0d 13449 . . . . . . . . . . . . . . . . . . . . 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 9743 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  0  <_  M )
108107ex 435 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( x  e.  ( A (,) B )  ->  0  <_  M
) )
109108exlimdv 1772 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( E. x  x  e.  ( A (,) B )  ->  0  <_  M ) )
110109imp 430 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  E. x  x  e.  ( A (,) B ) )  -> 
0  <_  M )
11196, 110sylan2b 477 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( A (,) B )  =/=  (/) )  -> 
0  <_  M )
112111adantlr 719 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( A (,) B )  =/=  (/) )  ->  0  <_  M )
11395, 112syldan 472 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
0  <_  M )
114 simpr3 1013 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  <_  b )
11569, 67subge0d 10154 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
0  <_  ( b  -  a )  <->  a  <_  b ) )
116114, 115mpbird 235 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  0  <_  ( b  -  a
) )
117116adantr 466 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
0  <_  ( b  -  a ) )
11874, 76, 113, 117mulge0d 10141 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
0  <_  ( M  x.  ( b  -  a
) ) )
119118ex 435 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( a (,) b
)  =/=  (/)  ->  0  <_  ( M  x.  (
b  -  a ) ) ) )
12072, 119sylbird 238 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a  <  b  ->  0  <_  ( M  x.  ( b  -  a
) ) ) )
12169recnd 9620 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  CC )
12267recnd 9620 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  CC )
123121, 122subeq0ad 9947 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( b  -  a
)  =  0  <->  b  =  a ) )
124 equcom 1848 . . . . . . . . . . . . 13  |-  ( b  =  a  <->  a  =  b )
125123, 124syl6bb 264 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( b  -  a
)  =  0  <->  a  =  b ) )
126 0re 9594 . . . . . . . . . . . . . 14  |-  0  e.  RR
12773adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  M  e.  RR )
128127recnd 9620 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  M  e.  CC )
129128mul01d 9783 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( M  x.  0 )  =  0 )
130129eqcomd 2434 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  0  =  ( M  x.  0 ) )
131 eqle 9687 . . . . . . . . . . . . . 14  |-  ( ( 0  e.  RR  /\  0  =  ( M  x.  0 ) )  -> 
0  <_  ( M  x.  0 ) )
132126, 130, 131sylancr 667 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  0  <_  ( M  x.  0 ) )
133 oveq2 6257 . . . . . . . . . . . . . 14  |-  ( ( b  -  a )  =  0  ->  ( M  x.  ( b  -  a ) )  =  ( M  x.  0 ) )
134133breq2d 4378 . . . . . . . . . . . . 13  |-  ( ( b  -  a )  =  0  ->  (
0  <_  ( M  x.  ( b  -  a
) )  <->  0  <_  ( M  x.  0 ) ) )
135132, 134syl5ibrcom 225 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( b  -  a
)  =  0  -> 
0  <_  ( M  x.  ( b  -  a
) ) ) )
136125, 135sylbird 238 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a  =  b  -> 
0  <_  ( M  x.  ( b  -  a
) ) ) )
13767, 69leloed 9729 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a  <_  b  <->  ( a  <  b  \/  a  =  b ) ) )
138114, 137mpbid 213 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a  <  b  \/  a  =  b )
)
139120, 136, 138mpjaod 382 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  0  <_  ( M  x.  (
b  -  a ) ) )
140139adantr 466 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =  ( F `  a ) )  -> 
0  <_  ( M  x.  ( b  -  a
) ) )
14165, 140eqbrtrd 4387 . . . . . . . 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 9937 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( F `  b
)  -  ( F `
 a ) )  e.  CC )
143142adantr 466 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( F `  b )  -  ( F `  a )
)  e.  CC )
144143abscld 13441 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  e.  RR )
145144recnd 9620 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  e.  CC )
14675adantr 466 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( b  -  a
)  e.  RR )
147146recnd 9620 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( b  -  a
)  e.  CC )
148138ord 378 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( -.  a  <  b  -> 
a  =  b ) )
149 fveq2 5825 . . . . . . . . . . . . . . . . 17  |-  ( a  =  b  ->  ( F `  a )  =  ( F `  b ) )
150149eqcomd 2434 . . . . . . . . . . . . . . . 16  |-  ( a  =  b  ->  ( F `  b )  =  ( F `  a ) )
151148, 150syl6 34 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( -.  a  <  b  -> 
( F `  b
)  =  ( F `
 a ) ) )
152151necon1ad 2618 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( F `  b
)  =/=  ( F `
 a )  -> 
a  <  b )
)
153152imp 430 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
a  <  b )
15467adantr 466 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
a  e.  RR )
15569adantr 466 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
b  e.  RR )
156154, 155posdifd 10151 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a  <  b  <->  0  <  ( b  -  a ) ) )
157153, 156mpbid 213 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
0  <  ( b  -  a ) )
158157gt0ne0d 10129 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( b  -  a
)  =/=  0 )
159145, 147, 158divrec2d 10338 . . . . . . . . . 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 11656 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B ) )  -> 
( a [,] b
)  C_  ( A [,] B ) )
16161, 59, 160syl2anc 665 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a [,] b ) 
C_  ( A [,] B ) )
162161adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a [,] b
)  C_  ( A [,] B ) )
163162sselda 3407 . . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  ->  F : ( A [,] B ) --> CC )
165164ffvelrnda 5981 . . . . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . 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 2645 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( ( F `  b )  -  ( F `  a )
)  =/=  0  <->  ( F `  b )  =/=  ( F `  a
) ) )
169168biimpar 487 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( F `  b )  -  ( F `  a )
)  =/=  0 )
170169adantr 466 . . . . . . . . . . . . . . . 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 10334 . . . . . . . . . . . . . . 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 5879 . . . . . . . . . . . . . . . 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 2429 . . . . . . . . . . . . . . . 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 6256 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( F `  y )  ->  (
x  /  ( ( F `  b )  -  ( F `  a ) ) )  =  ( ( F `
 y )  / 
( ( F `  b )  -  ( F `  a )
) ) )
175166, 172, 173, 174fmptco 6015 . . . . . . . . . . . . . . 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 13119 . . . . . . . . . . . . . . . . 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 5878 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  ->  Re  =  ( x  e.  CC  |->  ( Re `  x ) ) )
179 fveq2 5825 . . . . . . . . . . . . . . 15  |-  ( x  =  ( ( F `
 y )  / 
( ( F `  b )  -  ( F `  a )
) )  ->  (
Re `  x )  =  ( Re `  ( ( F `  y )  /  (
( F `  b
)  -  ( F `
 a ) ) ) ) )
180171, 175, 178, 179fmptco 6015 . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  F  e.  ( ( A [,] B ) -cn-> CC ) )
182 rescncf 21871 . . . . . . . . . . . . . . . . . 18  |-  ( ( a [,] b ) 
C_  ( A [,] B )  ->  ( F  e.  ( ( A [,] B ) -cn-> CC )  ->  ( F  |`  ( a [,] b
) )  e.  ( ( a [,] b
) -cn-> CC ) ) )
183161, 181, 182sylc 62 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( F  |`  ( a [,] b ) )  e.  ( ( a [,] b ) -cn-> CC ) )
184183adantr 466 . . . . . . . . . . . . . . . 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 2428 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  CC  |->  ( x  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  =  ( x  e.  CC  |->  ( x  /  (
( F `  b
)  -  ( F `
 a ) ) ) )
186185divccncf 21880 . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . 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 21881 . . . . . . . . . . . . . . 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 21876 . . . . . . . . . . . . . . . 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 21881 . . . . . . . . . . . . . 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 2507 . . . . . . . . . . . . 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 11667 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  e.  RR  /\  b  e.  RR )  ->  ( a [,] b
)  C_  RR )
195154, 155, 194syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a [,] b
)  C_  RR )
196171recld 13201 . . . . . . . . . . . . . . . . . 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 9620 . . . . . . . . . . . . . . . . 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 2428 . . . . . . . . . . . . . . . . . 18  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
199198tgioo2 21763 . . . . . . . . . . . . . . . . 17  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
200 iccntr 21781 . . . . . . . . . . . . . . . . . . 19  |-  ( ( a  e.  RR  /\  b  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( a [,] b ) )  =  ( a (,) b
) )
20167, 69, 200syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( int `  ( topGen `
 ran  (,) )
) `  ( a [,] b ) )  =  ( a (,) b
) )
202201adantr 466 . . . . . . . . . . . . . . . . 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 22867 . . . . . . . . . . . . . . . 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 11671 . . . . . . . . . . . . . . . . . . 19  |-  ( a (,) b )  C_  ( a [,] b
)
205204sseli 3403 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( a (,) b )  ->  y  e.  ( a [,] b
) )
206205, 171sylan2 476 . . . . . . . . . . . . . . . . 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 6277 . . . . . . . . . . . . . . . . . 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 9582 . . . . . . . . . . . . . . . . . . 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 476 . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a (,) b
)  C_  ( A (,) B ) )
213212sselda 3407 . . . . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( RR  _D  F
) : ( A (,) B ) --> CC )
215214ffvelrnda 5981 . . . . . . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( A [,] B
)  C_  RR )
218 ioossre 11647 . . . . . . . . . . . . . . . . . . . . . 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 22808 . . . . . . . . . . . . . . . . . . . . 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 1265 . . . . . . . . . . . . . . . . . . . 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 21724 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( topGen ` 
ran  (,) )  e.  Top
223 iooretop 21728 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a (,) b )  e.  ( topGen `  ran  (,) )
224 isopn3i 20040 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( a (,) b )  e.  ( topGen `  ran  (,) )
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  (
a (,) b ) )  =  ( a (,) b ) )
225222, 223, 224mp2an 676 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( a (,) b
) )  =  ( a (,) b )
226225reseq2i 5064 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( a (,) b ) ) )  =  ( ( RR 
_D  F )  |`  ( a (,) b
) )
227221, 226syl6eq 2478 . . . . . . . . . . . . . . . . . . 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 3418 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a (,) b
)  C_  ( A [,] B ) )
229164, 228feqresmpt 5879 . . . . . . . . . . . . . . . . . . . 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 6265 . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( RR  _D  F ) : ( A (,) B
) --> CC )
232231, 93fssresd 5710 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( RR  _D  F
)  |`  ( a (,) b ) ) : ( a (,) b
) --> CC )
233232feqmptd 5878 . . . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . 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 5839 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( a (,) b )  ->  (
( ( RR  _D  F )  |`  (
a (,) b ) ) `  y )  =  ( ( RR 
_D  F ) `  y ) )
236235mpteq2ia 4449 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( a (,) b )  |->  ( ( ( RR  _D  F
)  |`  ( a (,) b ) ) `  y ) )  =  ( y  e.  ( a (,) b ) 
|->  ( ( RR  _D  F ) `  y
) )
237234, 236syl6eq 2478 . . . . . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . . . . . . 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 22861 . . . . . . . . . . . . . . . . 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 22865 . . . . . . . . . . . . . . . 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 2462 . . . . . . . . . . . . . . 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 4999 . . . . . . . . . . . . . 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 5294 . . . . . . . . . . . . . . 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 5835 . . . . . . . . . . . . . . . 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 2728 . . . . . . . . . . . . . 14  |-  dom  (
y  e.  ( a (,) b )  |->  ( Re `  ( ( ( RR  _D  F
) `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) ) )  =  ( a (,) b )
247242, 246syl6eq 2478 . . . . . . . . . . . . 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 22886 . . . . . . . . . . . 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 5827 . . . . . . . . . . . . . . 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 5825 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  x  ->  (
( RR  _D  F
) `  y )  =  ( ( RR 
_D  F ) `  x ) )
251250oveq1d 6264 . . . . . . . . . . . . . . . . 17  |-  ( y  =  x  ->  (
( ( RR  _D  F ) `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) )  =  ( ( ( RR  _D  F ) `
 x )  / 
( ( F `  b )  -  ( F `  a )
) ) )
252251fveq2d 5829 . . . . . . . . . . . . . . . 16  |-  ( y  =  x  ->  (
Re `  ( (
( RR  _D  F
) `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  =  ( Re `  (
( ( RR  _D  F ) `  x
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) )
253 eqid 2428 . . . . . . . . . . . . . . . 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 5835 . . . . . . . . . . . . . . . 16  |-  ( Re
`  ( ( ( RR  _D  F ) `
 x )  / 
( ( F `  b )  -  ( F `  a )
) ) )  e. 
_V
255252, 253, 254fvmpt 5908 . . . . . . . . . . . . . . 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 2482 . . . . . . . . . . . . . 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 11700 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  RR*  /\  b  e.  RR*  /\  a  <_ 
b )  ->  b  e.  ( a [,] b
) )
25868, 70, 114, 257syl3anc 1264 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  ( a [,] b
) )
259258ad2antrr 730 . . . . . . . . . . . . . . . . . 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 6264 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  b  ->  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) )  =  ( ( F `
 b )  / 
( ( F `  b )  -  ( F `  a )
) ) )
261260fveq2d 5829 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  b  ->  (
Re `  ( ( F `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  =  ( Re `  (
( F `  b
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) )
262 eqid 2428 . . . . . . . . . . . . . . . . . . 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 5835 . . . . . . . . . . . . . . . . . . 19  |-  ( Re
`  ( ( F `
 b )  / 
( ( F `  b )  -  ( F `  a )
) ) )  e. 
_V
264261, 262, 263fvmpt 5908 . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . 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 11699 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  RR*  /\  b  e.  RR*  /\  a  <_ 
b )  ->  a  e.  ( a [,] b
) )
26768, 70, 114, 266syl3anc 1264 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  ( a [,] b
) )
268267ad2antrr 730 . . . . . . . . . . . . . . . . . 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 6264 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  a  ->  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) )  =  ( ( F `
 a )  / 
( ( F `  b )  -  ( F `  a )
) ) )
270269fveq2d 5829 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  a  ->  (
Re `  ( ( F `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  =  ( Re `  (
( F `  a
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) )
271 fvex 5835 . . . . . . . . . . . . . . . . . . 19  |-  ( Re
`  ( ( F `
 a )  / 
( ( F `  b )  -  ( F `  a )
) ) )  e. 
_V
272270, 262, 271fvmpt 5908 . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . 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 6267 . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( F `  b
)  e.  CC )
276275, 143, 169divcld 10334 . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( F `  a
)  e.  CC )
278277, 143, 169divcld 10334 . . . . . . . . . . . . . . . . . . 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 13223 . . . . . . . . . . . . . . . . . 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 10373 . . . . . . . . . . . . . . . . . . . . 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 10332 . . . . . . . . . . . . . . . . . . . . 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 2464 . . . . . . . . . . . . . . . . . . . 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 5829 . . . . . . . . . . . . . . . . . . 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 13161 . . . . . . . . . . . . . . . . . . 19  |-  ( Re
`  1 )  =  1
285283, 284syl6eq 2478 . . . . . . . . . . . . . . . . . 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 2464 . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . 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 2462 . . . . . . . . . . . . . . 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 6264 . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . 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 2875 . . . . . . . . . . . 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 213 . . . . . . . . . . 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 3407 . . . . . . . . . . . . . . . . . 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 5981 . . . . . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . 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 10334 . . . . . . . . . . . . . . . 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 13201 . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . 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 9622 . . . . . . . . . . . . . 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 13441 . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  M  e.  RR )
304298abscld 13441 . . . . . . . . . . . . . . . 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 13449 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
0  <_  ( abs `  ( ( F `  b )  -  ( F `  a )
) ) )
306305adantr 466 . . . . . . . . . . . . . . . 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 13456 . . . . . . . . . . . . . . . 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 10497 . . . . . . . . . . . . . . 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 )  -