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

Theorem dvlip 21307
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 5679 . . . . . . . 8  |-  ( a  =  Y  ->  ( F `  a )  =  ( F `  Y ) )
21oveq2d 6096 . . . . . . 7  |-  ( a  =  Y  ->  (
( F `  b
)  -  ( F `
 a ) )  =  ( ( F `
 b )  -  ( F `  Y ) ) )
32fveq2d 5683 . . . . . 6  |-  ( a  =  Y  ->  ( abs `  ( ( F `
 b )  -  ( F `  a ) ) )  =  ( abs `  ( ( F `  b )  -  ( F `  Y ) ) ) )
4 oveq2 6088 . . . . . . . 8  |-  ( a  =  Y  ->  (
b  -  a )  =  ( b  -  Y ) )
54fveq2d 5683 . . . . . . 7  |-  ( a  =  Y  ->  ( abs `  ( b  -  a ) )  =  ( abs `  (
b  -  Y ) ) )
65oveq2d 6096 . . . . . 6  |-  ( a  =  Y  ->  ( M  x.  ( abs `  ( b  -  a
) ) )  =  ( M  x.  ( abs `  ( b  -  Y ) ) ) )
73, 6breq12d 4293 . . . . 5  |-  ( a  =  Y  ->  (
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  <_  ( M  x.  ( abs `  (
b  -  a ) ) )  <->  ( abs `  ( ( F `  b )  -  ( F `  Y )
) )  <_  ( M  x.  ( abs `  ( b  -  Y
) ) ) ) )
87imbi2d 316 . . . 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 5679 . . . . . . . 8  |-  ( b  =  X  ->  ( F `  b )  =  ( F `  X ) )
109oveq1d 6095 . . . . . . 7  |-  ( b  =  X  ->  (
( F `  b
)  -  ( F `
 Y ) )  =  ( ( F `
 X )  -  ( F `  Y ) ) )
1110fveq2d 5683 . . . . . 6  |-  ( b  =  X  ->  ( abs `  ( ( F `
 b )  -  ( F `  Y ) ) )  =  ( abs `  ( ( F `  X )  -  ( F `  Y ) ) ) )
12 oveq1 6087 . . . . . . . 8  |-  ( b  =  X  ->  (
b  -  Y )  =  ( X  -  Y ) )
1312fveq2d 5683 . . . . . . 7  |-  ( b  =  X  ->  ( abs `  ( b  -  Y ) )  =  ( abs `  ( X  -  Y )
) )
1413oveq2d 6096 . . . . . 6  |-  ( b  =  X  ->  ( M  x.  ( abs `  ( b  -  Y
) ) )  =  ( M  x.  ( abs `  ( X  -  Y ) ) ) )
1511, 14breq12d 4293 . . . . 5  |-  ( b  =  X  ->  (
( abs `  (
( F `  b
)  -  ( F `
 Y ) ) )  <_  ( M  x.  ( abs `  (
b  -  Y ) ) )  <->  ( abs `  ( ( F `  X )  -  ( F `  Y )
) )  <_  ( M  x.  ( abs `  ( X  -  Y
) ) ) ) )
1615imbi2d 316 . . . 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 5679 . . . . . . . . . 10  |-  ( y  =  b  ->  ( F `  y )  =  ( F `  b ) )
18 fveq2 5679 . . . . . . . . . 10  |-  ( x  =  a  ->  ( F `  x )  =  ( F `  a ) )
1917, 18oveqan12d 6099 . . . . . . . . 9  |-  ( ( y  =  b  /\  x  =  a )  ->  ( ( F `  y )  -  ( F `  x )
)  =  ( ( F `  b )  -  ( F `  a ) ) )
2019fveq2d 5683 . . . . . . . 8  |-  ( ( y  =  b  /\  x  =  a )  ->  ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  =  ( abs `  ( ( F `  b )  -  ( F `  a )
) ) )
21 oveq12 6089 . . . . . . . . . 10  |-  ( ( y  =  b  /\  x  =  a )  ->  ( y  -  x
)  =  ( b  -  a ) )
2221fveq2d 5683 . . . . . . . . 9  |-  ( ( y  =  b  /\  x  =  a )  ->  ( abs `  (
y  -  x ) )  =  ( abs `  ( b  -  a
) ) )
2322oveq2d 6096 . . . . . . . 8  |-  ( ( y  =  b  /\  x  =  a )  ->  ( M  x.  ( abs `  ( y  -  x ) ) )  =  ( M  x.  ( abs `  ( b  -  a ) ) ) )
2420, 23breq12d 4293 . . . . . . 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 450 . . . . . 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 5679 . . . . . . . . . 10  |-  ( y  =  a  ->  ( F `  y )  =  ( F `  a ) )
27 fveq2 5679 . . . . . . . . . 10  |-  ( x  =  b  ->  ( F `  x )  =  ( F `  b ) )
2826, 27oveqan12d 6099 . . . . . . . . 9  |-  ( ( y  =  a  /\  x  =  b )  ->  ( ( F `  y )  -  ( F `  x )
)  =  ( ( F `  a )  -  ( F `  b ) ) )
2928fveq2d 5683 . . . . . . . 8  |-  ( ( y  =  a  /\  x  =  b )  ->  ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  =  ( abs `  ( ( F `  a )  -  ( F `  b )
) ) )
30 oveq12 6089 . . . . . . . . . 10  |-  ( ( y  =  a  /\  x  =  b )  ->  ( y  -  x
)  =  ( a  -  b ) )
3130fveq2d 5683 . . . . . . . . 9  |-  ( ( y  =  a  /\  x  =  b )  ->  ( abs `  (
y  -  x ) )  =  ( abs `  ( a  -  b
) ) )
3231oveq2d 6096 . . . . . . . 8  |-  ( ( y  =  a  /\  x  =  b )  ->  ( M  x.  ( abs `  ( y  -  x ) ) )  =  ( M  x.  ( abs `  ( a  -  b ) ) ) )
3329, 32breq12d 4293 . . . . . . 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 450 . . . . . 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 11365 . . . . . . 7  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A [,] B
)  C_  RR )
3835, 36, 37syl2anc 654 . . . . . 6  |-  ( ph  ->  ( A [,] B
)  C_  RR )
39 dvlip.f . . . . . . . . . . 11  |-  ( ph  ->  F  e.  ( ( A [,] B )
-cn-> CC ) )
40 cncff 20311 . . . . . . . . . . 11  |-  ( F  e.  ( ( A [,] B ) -cn-> CC )  ->  F :
( A [,] B
) --> CC )
4139, 40syl 16 . . . . . . . . . 10  |-  ( ph  ->  F : ( A [,] B ) --> CC )
42 ffvelrn 5829 . . . . . . . . . . 11  |-  ( ( F : ( A [,] B ) --> CC 
/\  a  e.  ( A [,] B ) )  ->  ( F `  a )  e.  CC )
43 ffvelrn 5829 . . . . . . . . . . 11  |-  ( ( F : ( A [,] B ) --> CC 
/\  b  e.  ( A [,] B ) )  ->  ( F `  b )  e.  CC )
4442, 43anim12dan 826 . . . . . . . . . 10  |-  ( ( F : ( A [,] B ) --> CC 
/\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  (
( F `  a
)  e.  CC  /\  ( F `  b )  e.  CC ) )
4541, 44sylan 468 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  (
( F `  a
)  e.  CC  /\  ( F `  b )  e.  CC ) )
4645simprd 460 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( F `  b )  e.  CC )
4745simpld 456 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( F `  a )  e.  CC )
4846, 47abssubd 12923 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( abs `  ( ( F `
 b )  -  ( F `  a ) ) )  =  ( abs `  ( ( F `  a )  -  ( F `  b ) ) ) )
49 ax-resscn 9327 . . . . . . . . . . . 12  |-  RR  C_  CC
5038, 49syl6ss 3356 . . . . . . . . . . 11  |-  ( ph  ->  ( A [,] B
)  C_  CC )
5150sselda 3344 . . . . . . . . . 10  |-  ( (
ph  /\  b  e.  ( A [,] B ) )  ->  b  e.  CC )
5251adantrl 708 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  b  e.  CC )
5350sselda 3344 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  ( A [,] B ) )  ->  a  e.  CC )
5453adantrr 709 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  a  e.  CC )
5552, 54abssubd 12923 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( abs `  ( b  -  a ) )  =  ( abs `  (
a  -  b ) ) )
5655oveq2d 6096 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( M  x.  ( abs `  ( b  -  a
) ) )  =  ( M  x.  ( abs `  ( a  -  b ) ) ) )
5748, 56breq12d 4293 . . . . . 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 462 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  F : ( A [,] B ) --> CC )
59 simpr2 988 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  ( A [,] B
) )
6058, 59ffvelrnd 5832 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( F `  b )  e.  CC )
61 simpr1 987 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  ( A [,] B
) )
6258, 61ffvelrnd 5832 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( F `  a )  e.  CC )
6360, 62subeq0ad 9717 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( ( F `  b )  -  ( F `  a )
)  =  0  <->  ( F `  b )  =  ( F `  a ) ) )
6463biimpar 482 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =  ( F `  a ) )  -> 
( ( F `  b )  -  ( F `  a )
)  =  0 )
6564abs00bd 12764 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =  ( F `  a ) )  -> 
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  =  0 )
6638adantr 462 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( A [,] B )  C_  RR )
6766, 61sseldd 3345 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  RR )
6867rexrd 9421 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  RR* )
6966, 59sseldd 3345 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  RR )
7069rexrd 9421 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  RR* )
71 ioon0 11314 . . . . . . . . . . . . 13  |-  ( ( a  e.  RR*  /\  b  e.  RR* )  ->  (
( a (,) b
)  =/=  (/)  <->  a  <  b ) )
7268, 70, 71syl2anc 654 . . . . . . . . . . . 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 718 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  ->  M  e.  RR )
7569, 67resubcld 9764 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
b  -  a )  e.  RR )
7675adantr 462 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
( b  -  a
)  e.  RR )
7735adantr 462 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  A  e.  RR )
7877rexrd 9421 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  A  e.  RR* )
7936adantr 462 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  B  e.  RR )
80 elicc2 11348 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( a  e.  ( A [,] B )  <-> 
( a  e.  RR  /\  A  <_  a  /\  a  <_  B ) ) )
8177, 79, 80syl2anc 654 . . . . . . . . . . . . . . . . . . . 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 994 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  A  <_  a )
84 iooss1 11323 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  RR*  /\  A  <_  a )  ->  (
a (,) b ) 
C_  ( A (,) b ) )
8578, 83, 84syl2anc 654 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a (,) b ) 
C_  ( A (,) b ) )
8679rexrd 9421 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  B  e.  RR* )
87 elicc2 11348 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( b  e.  ( A [,] B )  <-> 
( b  e.  RR  /\  A  <_  b  /\  b  <_  B ) ) )
8877, 79, 87syl2anc 654 . . . . . . . . . . . . . . . . . . . 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 995 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  <_  B )
91 iooss2 11324 . . . . . . . . . . . . . . . . . 18  |-  ( ( B  e.  RR*  /\  b  <_  B )  ->  ( A (,) b )  C_  ( A (,) B ) )
9286, 90, 91syl2anc 654 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( A (,) b )  C_  ( A (,) B ) )
9385, 92sstrd 3354 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a (,) b ) 
C_  ( A (,) B ) )
94 ssn0 3658 . . . . . . . . . . . . . . . 16  |-  ( ( ( a (,) b
)  C_  ( A (,) B )  /\  (
a (,) b )  =/=  (/) )  ->  ( A (,) B )  =/=  (/) )
9593, 94sylan 468 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
( A (,) B
)  =/=  (/) )
96 n0 3634 . . . . . . . . . . . . . . . . 17  |-  ( ( A (,) B )  =/=  (/)  <->  E. x  x  e.  ( A (,) B
) )
97 0red 9375 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  0  e.  RR )
98 dvf 21224 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( RR 
_D  F ) : dom  ( RR  _D  F ) --> CC
99 dvlip.d . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
10099feq2d 5535 . . . . . . . . . . . . . . . . . . . . . . . 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 5831 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( ( RR  _D  F ) `  x )  e.  CC )
103102abscld 12906 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( abs `  ( ( RR  _D  F ) `  x
) )  e.  RR )
10473adantr 462 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  M  e.  RR )
105102absge0d 12914 . . . . . . . . . . . . . . . . . . . . 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 9516 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  0  <_  M )
108107ex 434 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( x  e.  ( A (,) B )  ->  0  <_  M
) )
109108exlimdv 1689 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( E. x  x  e.  ( A (,) B )  ->  0  <_  M ) )
110109imp 429 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  E. x  x  e.  ( A (,) B ) )  -> 
0  <_  M )
11196, 110sylan2b 472 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( A (,) B )  =/=  (/) )  -> 
0  <_  M )
112111adantlr 707 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( A (,) B )  =/=  (/) )  ->  0  <_  M )
11395, 112syldan 467 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
0  <_  M )
114 simpr3 989 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  <_  b )
11569, 67subge0d 9917 . . . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
0  <_  ( b  -  a ) )
11874, 76, 113, 117mulge0d 9904 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
0  <_  ( M  x.  ( b  -  a
) ) )
119118ex 434 . . . . . . . . . . . 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 9400 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  CC )
12267recnd 9400 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  CC )
123121, 122subeq0ad 9717 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( b  -  a
)  =  0  <->  b  =  a ) )
124 equcom 1731 . . . . . . . . . . . . 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 9374 . . . . . . . . . . . . . 14  |-  0  e.  RR
12773adantr 462 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  M  e.  RR )
128127recnd 9400 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  M  e.  CC )
129128mul01d 9556 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( M  x.  0 )  =  0 )
130129eqcomd 2438 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  0  =  ( M  x.  0 ) )
131 eqle 9465 . . . . . . . . . . . . . 14  |-  ( ( 0  e.  RR  /\  0  =  ( M  x.  0 ) )  -> 
0  <_  ( M  x.  0 ) )
132126, 130, 131sylancr 656 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  0  <_  ( M  x.  0 ) )
133 oveq2 6088 . . . . . . . . . . . . . 14  |-  ( ( b  -  a )  =  0  ->  ( M  x.  ( b  -  a ) )  =  ( M  x.  0 ) )
134133breq2d 4292 . . . . . . . . . . . . 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 9505 . . . . . . . . . . . 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 381 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  0  <_  ( M  x.  (
b  -  a ) ) )
140139adantr 462 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =  ( F `  a ) )  -> 
0  <_  ( M  x.  ( b  -  a
) ) )
14165, 140eqbrtrd 4300 . . . . . . . 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 9707 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( F `  b
)  -  ( F `
 a ) )  e.  CC )
143142adantr 462 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( F `  b )  -  ( F `  a )
)  e.  CC )
144143abscld 12906 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  e.  RR )
145144recnd 9400 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  e.  CC )
14675adantr 462 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( b  -  a
)  e.  RR )
147146recnd 9400 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( b  -  a
)  e.  CC )
148138ord 377 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( -.  a  <  b  -> 
a  =  b ) )
149 fveq2 5679 . . . . . . . . . . . . . . . . 17  |-  ( a  =  b  ->  ( F `  a )  =  ( F `  b ) )
150149eqcomd 2438 . . . . . . . . . . . . . . . 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 2668 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( F `  b
)  =/=  ( F `
 a )  -> 
a  <  b )
)
153152imp 429 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
a  <  b )
15467adantr 462 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
a  e.  RR )
15569adantr 462 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
b  e.  RR )
156154, 155posdifd 9914 . . . . . . . . . . . . 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 9892 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( b  -  a
)  =/=  0 )
159145, 147, 158divrec2d 10099 . . . . . . . . . 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 11354 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B ) )  -> 
( a [,] b
)  C_  ( A [,] B ) )
16161, 59, 160syl2anc 654 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a [,] b ) 
C_  ( A [,] B ) )
162161adantr 462 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a [,] b
)  C_  ( A [,] B ) )
163162sselda 3344 . . . . . . . . . . . . . . . . 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 718 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  ->  F : ( A [,] B ) --> CC )
165164ffvelrnda 5831 . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . 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 718 . . . . . . . . . . . . . . . 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 2633 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( ( F `  b )  -  ( F `  a )
)  =/=  0  <->  ( F `  b )  =/=  ( F `  a
) ) )
169168biimpar 482 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( F `  b )  -  ( F `  a )
)  =/=  0 )
170169adantr 462 . . . . . . . . . . . . . . . 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 10095 . . . . . . . . . . . . . . 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 5733 . . . . . . . . . . . . . . . 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 2434 . . . . . . . . . . . . . . . 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 6087 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( F `  y )  ->  (
x  /  ( ( F `  b )  -  ( F `  a ) ) )  =  ( ( F `
 y )  / 
( ( F `  b )  -  ( F `  a )
) ) )
175166, 172, 173, 174fmptco 5863 . . . . . . . . . . . . . . 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 12585 . . . . . . . . . . . . . . . . 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 5732 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  ->  Re  =  ( x  e.  CC  |->  ( Re `  x ) ) )
179 fveq2 5679 . . . . . . . . . . . . . . 15  |-  ( x  =  ( ( F `
 y )  / 
( ( F `  b )  -  ( F `  a )
) )  ->  (
Re `  x )  =  ( Re `  ( ( F `  y )  /  (
( F `  b
)  -  ( F `
 a ) ) ) ) )
180171, 175, 178, 179fmptco 5863 . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  F  e.  ( ( A [,] B ) -cn-> CC ) )
182 rescncf 20315 . . . . . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . 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 2433 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  CC  |->  ( x  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  =  ( x  e.  CC  |->  ( x  /  (
( F `  b
)  -  ( F `
 a ) ) ) )
186185divccncf 20324 . . . . . . . . . . . . . . . . 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 654 . . . . . . . . . . . . . . . 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 20325 . . . . . . . . . . . . . . 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 20320 . . . . . . . . . . . . . . . 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 20325 . . . . . . . . . . . . . 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 2508 . . . . . . . . . . . . 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 11365 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  e.  RR  /\  b  e.  RR )  ->  ( a [,] b
)  C_  RR )
195154, 155, 194syl2anc 654 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a [,] b
)  C_  RR )
196171recld 12667 . . . . . . . . . . . . . . . . . 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 9400 . . . . . . . . . . . . . . . . 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 2433 . . . . . . . . . . . . . . . . . 18  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
199198tgioo2 20222 . . . . . . . . . . . . . . . . 17  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
200 iccntr 20240 . . . . . . . . . . . . . . . . . . 19  |-  ( ( a  e.  RR  /\  b  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( a [,] b ) )  =  ( a (,) b
) )
20167, 69, 200syl2anc 654 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( int `  ( topGen `
 ran  (,) )
) `  ( a [,] b ) )  =  ( a (,) b
) )
202201adantr 462 . . . . . . . . . . . . . . . . 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 21287 . . . . . . . . . . . . . . . 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 11369 . . . . . . . . . . . . . . . . . . 19  |-  ( a (,) b )  C_  ( a [,] b
)
205204sseli 3340 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( a (,) b )  ->  y  e.  ( a [,] b
) )
206205, 171sylan2 471 . . . . . . . . . . . . . . . . 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 6105 . . . . . . . . . . . . . . . . . 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 9362 . . . . . . . . . . . . . . . . . . 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 471 . . . . . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a (,) b
)  C_  ( A (,) B ) )
213212sselda 3344 . . . . . . . . . . . . . . . . . . 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 718 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( RR  _D  F
) : ( A (,) B ) --> CC )
215214ffvelrnda 5831 . . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . . 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 718 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( A [,] B
)  C_  RR )
218 ioossre 11345 . . . . . . . . . . . . . . . . . . . . . 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 21228 . . . . . . . . . . . . . . . . . . . . 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 1212 . . . . . . . . . . . . . . . . . . . 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 20182 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( topGen ` 
ran  (,) )  e.  Top
223 iooretop 20187 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a (,) b )  e.  ( topGen `  ran  (,) )
224 isopn3i 18528 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( a (,) b )  e.  ( topGen `  ran  (,) )
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  (
a (,) b ) )  =  ( a (,) b ) )
225222, 223, 224mp2an 665 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( a (,) b
) )  =  ( a (,) b )
226225reseq2i 5094 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( a (,) b ) ) )  =  ( ( RR 
_D  F )  |`  ( a (,) b
) )
227221, 226syl6eq 2481 . . . . . . . . . . . . . . . . . . 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 3355 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a (,) b
)  C_  ( A [,] B ) )
229164, 228feqresmpt 5733 . . . . . . . . . . . . . . . . . . . 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 6096 . . . . . . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( RR  _D  F ) : ( A (,) B
) --> CC )
232 fssres 5566 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( RR  _D  F
) : ( A (,) B ) --> CC 
/\  ( a (,) b )  C_  ( A (,) B ) )  ->  ( ( RR 
_D  F )  |`  ( a (,) b
) ) : ( a (,) b ) --> CC )
233231, 93, 232syl2anc 654 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( RR  _D  F
)  |`  ( a (,) b ) ) : ( a (,) b
) --> CC )
234233feqmptd 5732 . . . . . . . . . . . . . . . . . . . . 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
) ) )
235234adantr 462 . . . . . . . . . . . . . . . . . . . 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 ) ) )
236 fvres 5692 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( a (,) b )  ->  (
( ( RR  _D  F )  |`  (
a (,) b ) ) `  y )  =  ( ( RR 
_D  F ) `  y ) )
237236mpteq2ia 4362 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( a (,) b )  |->  ( ( ( RR  _D  F
)  |`  ( a (,) b ) ) `  y ) )  =  ( y  e.  ( a (,) b ) 
|->  ( ( RR  _D  F ) `  y
) )
238235, 237syl6eq 2481 . . . . . . . . . . . . . . . . . . 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 ) ) )
239227, 230, 2383eqtr3d 2473 . . . . . . . . . . . . . . . . . 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 )
) )
240210, 211, 216, 239, 143, 169dvmptdivc 21281 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
241206, 208, 240dvmptre 21285 . . . . . . . . . . . . . . . 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 )
) ) ) ) )
242203, 241eqtrd 2465 . . . . . . . . . . . . . . 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 )
) ) ) ) )
243242dmeqd 5029 . . . . . . . . . . . . . 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 ) ) ) ) ) )
244 dmmptg 5323 . . . . . . . . . . . . . . 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
) )
245 fvex 5689 . . . . . . . . . . . . . . . 16  |-  ( Re
`  ( ( ( RR  _D  F ) `
 y )  / 
( ( F `  b )  -  ( F `  a )
) ) )  e. 
_V
246245a1i 11 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( a (,) b )  ->  (
Re `  ( (
( RR  _D  F
) `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  e. 
_V )
247244, 246mprg 2775 . . . . . . . . . . . . . 14  |-  dom  (
y  e.  ( a (,) b )  |->  ( Re `  ( ( ( RR  _D  F
) `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) ) )  =  ( a (,) b )
248243, 247syl6eq 2481 . . . . . . . . . . . . 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 ) )
249154, 155, 153, 192, 248mvth 21306 . . . . . . . . . . . 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
) ) )
250242fveq1d 5681 . . . . . . . . . . . . . . 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
) )
251 fveq2 5679 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  x  ->  (
( RR  _D  F
) `  y )  =  ( ( RR 
_D  F ) `  x ) )
252251oveq1d 6095 . . . . . . . . . . . . . . . . 17  |-  ( y  =  x  ->  (
( ( RR  _D  F ) `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) )  =  ( ( ( RR  _D  F ) `
 x )  / 
( ( F `  b )  -  ( F `  a )
) ) )
253252fveq2d 5683 . . . . . . . . . . . . . . . 16  |-  ( y  =  x  ->  (
Re `  ( (
( RR  _D  F
) `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  =  ( Re `  (
( ( RR  _D  F ) `  x
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) )
254 eqid 2433 . . . . . . . . . . . . . . . 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 ) ) ) ) )
255 fvex 5689 . . . . . . . . . . . . . . . 16  |-  ( Re
`  ( ( ( RR  _D  F ) `
 x )  / 
( ( F `  b )  -  ( F `  a )
) ) )  e. 
_V
256253, 254, 255fvmpt 5762 . . . . . . . . . . . . . . 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 )
) ) ) )
257250, 256sylan9eq 2485 . . . . . . . . . . . . . 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 ) ) ) ) )
258 ubicc2 11389 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  RR*  /\  b  e.  RR*  /\  a  <_ 
b )  ->  b  e.  ( a [,] b
) )
25968, 70, 114, 258syl3anc 1211 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  ( a [,] b
) )
260259ad2antrr 718 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  b  e.  ( a [,] b
) )
26117oveq1d 6095 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  b  ->  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) )  =  ( ( F `
 b )  / 
( ( F `  b )  -  ( F `  a )
) ) )
262261fveq2d 5683 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  b  ->  (
Re `  ( ( F `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  =  ( Re `  (
( F `  b
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) )
263 eqid 2433 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( a [,] b )  |->  ( Re
`  ( ( F `
 y )  / 
( ( F `  b )  -  ( F `  a )
) ) ) )  =  ( y  e.  ( a [,] b
)  |->  ( Re `  ( ( F `  y )  /  (
( F `  b
)  -  ( F `
 a ) ) ) ) )
264 fvex 5689 . . . . . . . . . . . . . . . . . . 19  |-  ( Re
`  ( ( F `
 b )  / 
( ( F `  b )  -  ( F `  a )
) ) )  e. 
_V
265262, 263, 264fvmpt 5762 . . . . . . . . . . . . . . . . . 18  |-  ( b  e.  ( a [,] b )  ->  (
( y  e.  ( a [,] b ) 
|->  ( Re `  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) ) `  b
)  =  ( Re
`  ( ( F `
 b )  / 
( ( F `  b )  -  ( F `  a )
) ) ) )
266260, 265syl 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 )
) ) ) )
267 lbicc2 11388 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  RR*  /\  b  e.  RR*  /\  a  <_ 
b )  ->  a  e.  ( a [,] b
) )
26868, 70, 114, 267syl3anc 1211 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  ( a [,] b
) )
269268ad2antrr 718 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  a  e.  ( a [,] b
) )
27026oveq1d 6095 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  a  ->  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) )  =  ( ( F `
 a )  / 
( ( F `  b )  -  ( F `  a )
) ) )
271270fveq2d 5683 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  a  ->  (
Re `  ( ( F `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  =  ( Re `  (
( F `  a
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) )
272 fvex 5689 . . . . . . . . . . . . . . . . . . 19  |-  ( Re
`  ( ( F `
 a )  / 
( ( F `  b )  -  ( F `  a )
) ) )  e. 
_V
273271, 263, 272fvmpt 5762 . . . . . . . . . . . . . . . . . 18  |-  ( a  e.  ( a [,] b )  ->  (
( y  e.  ( a [,] b ) 
|->  ( Re `  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) ) `  a
)  =  ( Re
`  ( ( F `
 a )  / 
( ( F `  b )  -  ( F `  a )
) ) ) )
274269, 273syl 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 )
) ) ) )
275266, 274oveq12d 6098 . . . . . . . . . . . . . . . 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 )
) ) ) ) )
27660adantr 462 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( F `  b
)  e.  CC )
277276, 143, 169divcld 10095 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( F `  b )  /  (
( F `  b
)  -  ( F `
 a ) ) )  e.  CC )
27862adantr 462 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( F `  a
)  e.  CC )
279278, 143, 169divcld 10095 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( F `  a )  /  (
( F `  b
)  -  ( F `
 a ) ) )  e.  CC )
280277, 279resubd 12689 . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
281276, 278, 143, 169divsubdird 10134 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
282143, 169dividd 10093 . . . . . . . . . . . . . . . . . . . . 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 )
283281, 282eqtr3d 2467 . . . . . . . . . . . . . . . . . . . 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 )
284283fveq2d 5683 . . . . . . . . . . . . . . . . . . 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 ) )
285 re1 12627 . . . . . . . . . . . . . . . . . . 19  |-  ( Re
`  1 )  =  1
286284, 285syl6eq 2481 . . . . . . . . . . . . . . . . . 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 )
287280, 286eqtr3d 2467 . . . . . . . . . . . . . . . . 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 )
288287adantr 462 . . . . . . . . . . . . . . . 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 )
289275, 288eqtrd 2465 . . . . . . . . . . . . . . 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 )
290289oveq1d 6095 . . . . . . . . . . . . . 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 ) ) )
291257, 290eqeq12d 2447 . . . . . . . . . . . . 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 ) ) ) )
292291rexbidva 2722 . . . . . . . . . . . 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 ) ) ) )
293249, 292mpbid 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 ) ) )
294212sselda 3344 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  x  e.  ( A (,) B
) )
295214ffvelrnda 5831 . . . . . . . . . . . . . . . . . 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 )
296294, 295syldan 467 . . . . . . . . . . . . . . . . 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 )
297142ad2antrr 718 . . . . . . . . . . . . . . . . 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 )
298169adantr 462 . . . . . . . . . . . . . . . . 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 )
299296, 297, 298divcld 10095 . . . . . . . . . . . . . . . 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 )
300299recld 12667 . . . . . . . . . . . . . . 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 )
301144adantr 462 . . . . . . . . . . . . . . 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 )
302300, 301remulcld 9402 . . . . . . . . . . . . . 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 )
303296abscld 12906 . . . . . . . . . . . . . 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 )
304127ad2antrr 718 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  M  e.  RR )
305299abscld 12906 . . . . . . . . . . . . . . . 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 )
306143absge0d 12914 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
0  <_  ( abs `  ( ( F `  b )  -  ( F `  a )
) ) )
307306adantr 462 . . . . . . . . . . . . . . . 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 ) ) ) )
308299releabsd 12921 . . . . . . . . . . . . . . . 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 ) ) ) ) )
309300, 305, 301, 307, 308lemul1ad 10260 . . . . . . . . . . . . . . 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
) <