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

Theorem dvlip 19356
Description: A function with derivative bounded by  M is Lipschitz continuous with Lipchitz 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 5541 . . . . . . . 8  |-  ( a  =  Y  ->  ( F `  a )  =  ( F `  Y ) )
21oveq2d 5890 . . . . . . 7  |-  ( a  =  Y  ->  (
( F `  b
)  -  ( F `
 a ) )  =  ( ( F `
 b )  -  ( F `  Y ) ) )
32fveq2d 5545 . . . . . 6  |-  ( a  =  Y  ->  ( abs `  ( ( F `
 b )  -  ( F `  a ) ) )  =  ( abs `  ( ( F `  b )  -  ( F `  Y ) ) ) )
4 oveq2 5882 . . . . . . . 8  |-  ( a  =  Y  ->  (
b  -  a )  =  ( b  -  Y ) )
54fveq2d 5545 . . . . . . 7  |-  ( a  =  Y  ->  ( abs `  ( b  -  a ) )  =  ( abs `  (
b  -  Y ) ) )
65oveq2d 5890 . . . . . 6  |-  ( a  =  Y  ->  ( M  x.  ( abs `  ( b  -  a
) ) )  =  ( M  x.  ( abs `  ( b  -  Y ) ) ) )
73, 6breq12d 4052 . . . . 5  |-  ( a  =  Y  ->  (
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  <_  ( M  x.  ( abs `  (
b  -  a ) ) )  <->  ( abs `  ( ( F `  b )  -  ( F `  Y )
) )  <_  ( M  x.  ( abs `  ( b  -  Y
) ) ) ) )
87imbi2d 307 . . . 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 5541 . . . . . . . 8  |-  ( b  =  X  ->  ( F `  b )  =  ( F `  X ) )
109oveq1d 5889 . . . . . . 7  |-  ( b  =  X  ->  (
( F `  b
)  -  ( F `
 Y ) )  =  ( ( F `
 X )  -  ( F `  Y ) ) )
1110fveq2d 5545 . . . . . 6  |-  ( b  =  X  ->  ( abs `  ( ( F `
 b )  -  ( F `  Y ) ) )  =  ( abs `  ( ( F `  X )  -  ( F `  Y ) ) ) )
12 oveq1 5881 . . . . . . . 8  |-  ( b  =  X  ->  (
b  -  Y )  =  ( X  -  Y ) )
1312fveq2d 5545 . . . . . . 7  |-  ( b  =  X  ->  ( abs `  ( b  -  Y ) )  =  ( abs `  ( X  -  Y )
) )
1413oveq2d 5890 . . . . . 6  |-  ( b  =  X  ->  ( M  x.  ( abs `  ( b  -  Y
) ) )  =  ( M  x.  ( abs `  ( X  -  Y ) ) ) )
1511, 14breq12d 4052 . . . . 5  |-  ( b  =  X  ->  (
( abs `  (
( F `  b
)  -  ( F `
 Y ) ) )  <_  ( M  x.  ( abs `  (
b  -  Y ) ) )  <->  ( abs `  ( ( F `  X )  -  ( F `  Y )
) )  <_  ( M  x.  ( abs `  ( X  -  Y
) ) ) ) )
1615imbi2d 307 . . . 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 5541 . . . . . . . . . 10  |-  ( y  =  b  ->  ( F `  y )  =  ( F `  b ) )
18 fveq2 5541 . . . . . . . . . 10  |-  ( x  =  a  ->  ( F `  x )  =  ( F `  a ) )
1917, 18oveqan12d 5893 . . . . . . . . 9  |-  ( ( y  =  b  /\  x  =  a )  ->  ( ( F `  y )  -  ( F `  x )
)  =  ( ( F `  b )  -  ( F `  a ) ) )
2019fveq2d 5545 . . . . . . . 8  |-  ( ( y  =  b  /\  x  =  a )  ->  ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  =  ( abs `  ( ( F `  b )  -  ( F `  a )
) ) )
21 oveq12 5883 . . . . . . . . . 10  |-  ( ( y  =  b  /\  x  =  a )  ->  ( y  -  x
)  =  ( b  -  a ) )
2221fveq2d 5545 . . . . . . . . 9  |-  ( ( y  =  b  /\  x  =  a )  ->  ( abs `  (
y  -  x ) )  =  ( abs `  ( b  -  a
) ) )
2322oveq2d 5890 . . . . . . . 8  |-  ( ( y  =  b  /\  x  =  a )  ->  ( M  x.  ( abs `  ( y  -  x ) ) )  =  ( M  x.  ( abs `  ( b  -  a ) ) ) )
2420, 23breq12d 4052 . . . . . . 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 439 . . . . . 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 5541 . . . . . . . . . 10  |-  ( y  =  a  ->  ( F `  y )  =  ( F `  a ) )
27 fveq2 5541 . . . . . . . . . 10  |-  ( x  =  b  ->  ( F `  x )  =  ( F `  b ) )
2826, 27oveqan12d 5893 . . . . . . . . 9  |-  ( ( y  =  a  /\  x  =  b )  ->  ( ( F `  y )  -  ( F `  x )
)  =  ( ( F `  a )  -  ( F `  b ) ) )
2928fveq2d 5545 . . . . . . . 8  |-  ( ( y  =  a  /\  x  =  b )  ->  ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  =  ( abs `  ( ( F `  a )  -  ( F `  b )
) ) )
30 oveq12 5883 . . . . . . . . . 10  |-  ( ( y  =  a  /\  x  =  b )  ->  ( y  -  x
)  =  ( a  -  b ) )
3130fveq2d 5545 . . . . . . . . 9  |-  ( ( y  =  a  /\  x  =  b )  ->  ( abs `  (
y  -  x ) )  =  ( abs `  ( a  -  b
) ) )
3231oveq2d 5890 . . . . . . . 8  |-  ( ( y  =  a  /\  x  =  b )  ->  ( M  x.  ( abs `  ( y  -  x ) ) )  =  ( M  x.  ( abs `  ( a  -  b ) ) ) )
3329, 32breq12d 4052 . . . . . . 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 439 . . . . . 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 10747 . . . . . . 7  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A [,] B
)  C_  RR )
3835, 36, 37syl2anc 642 . . . . . 6  |-  ( ph  ->  ( A [,] B
)  C_  RR )
39 dvlip.f . . . . . . . . . . 11  |-  ( ph  ->  F  e.  ( ( A [,] B )
-cn-> CC ) )
40 cncff 18413 . . . . . . . . . . 11  |-  ( F  e.  ( ( A [,] B ) -cn-> CC )  ->  F :
( A [,] B
) --> CC )
4139, 40syl 15 . . . . . . . . . 10  |-  ( ph  ->  F : ( A [,] B ) --> CC )
42 ffvelrn 5679 . . . . . . . . . . 11  |-  ( ( F : ( A [,] B ) --> CC 
/\  a  e.  ( A [,] B ) )  ->  ( F `  a )  e.  CC )
43 ffvelrn 5679 . . . . . . . . . . 11  |-  ( ( F : ( A [,] B ) --> CC 
/\  b  e.  ( A [,] B ) )  ->  ( F `  b )  e.  CC )
4442, 43anim12dan 810 . . . . . . . . . 10  |-  ( ( F : ( A [,] B ) --> CC 
/\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  (
( F `  a
)  e.  CC  /\  ( F `  b )  e.  CC ) )
4541, 44sylan 457 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  (
( F `  a
)  e.  CC  /\  ( F `  b )  e.  CC ) )
4645simprd 449 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( F `  b )  e.  CC )
4745simpld 445 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( F `  a )  e.  CC )
4846, 47abssubd 11951 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( abs `  ( ( F `
 b )  -  ( F `  a ) ) )  =  ( abs `  ( ( F `  a )  -  ( F `  b ) ) ) )
49 ax-resscn 8810 . . . . . . . . . . . 12  |-  RR  C_  CC
5038, 49syl6ss 3204 . . . . . . . . . . 11  |-  ( ph  ->  ( A [,] B
)  C_  CC )
5150sselda 3193 . . . . . . . . . 10  |-  ( (
ph  /\  b  e.  ( A [,] B ) )  ->  b  e.  CC )
5251adantrl 696 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  b  e.  CC )
5350sselda 3193 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  ( A [,] B ) )  ->  a  e.  CC )
5453adantrr 697 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  a  e.  CC )
5552, 54abssubd 11951 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( abs `  ( b  -  a ) )  =  ( abs `  (
a  -  b ) ) )
5655oveq2d 5890 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( M  x.  ( abs `  ( b  -  a
) ) )  =  ( M  x.  ( abs `  ( a  -  b ) ) ) )
5748, 56breq12d 4052 . . . . . 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 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  F : ( A [,] B ) --> CC )
59 simpr2 962 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  ( A [,] B
) )
6058, 59, 43syl2anc 642 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( F `  b )  e.  CC )
61 simpr1 961 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  ( A [,] B
) )
6258, 61, 42syl2anc 642 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( F `  a )  e.  CC )
63 subeq0 9089 . . . . . . . . . . . . 13  |-  ( ( ( F `  b
)  e.  CC  /\  ( F `  a )  e.  CC )  -> 
( ( ( F `
 b )  -  ( F `  a ) )  =  0  <->  ( F `  b )  =  ( F `  a ) ) )
6460, 62, 63syl2anc 642 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( ( F `  b )  -  ( F `  a )
)  =  0  <->  ( F `  b )  =  ( F `  a ) ) )
6564biimpar 471 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =  ( F `  a ) )  -> 
( ( F `  b )  -  ( F `  a )
)  =  0 )
6665fveq2d 5545 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =  ( F `  a ) )  -> 
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  =  ( abs `  0 ) )
67 abs0 11786 . . . . . . . . . 10  |-  ( abs `  0 )  =  0
6866, 67syl6eq 2344 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =  ( F `  a ) )  -> 
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  =  0 )
6938adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( A [,] B )  C_  RR )
7069, 61sseldd 3194 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  RR )
7170rexrd 8897 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  RR* )
7269, 59sseldd 3194 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  RR )
7372rexrd 8897 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  RR* )
74 ioon0 10698 . . . . . . . . . . . . 13  |-  ( ( a  e.  RR*  /\  b  e.  RR* )  ->  (
( a (,) b
)  =/=  (/)  <->  a  <  b ) )
7571, 73, 74syl2anc 642 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( a (,) b
)  =/=  (/)  <->  a  <  b ) )
76 dvlip.m . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  e.  RR )
7776ad2antrr 706 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  ->  M  e.  RR )
7872, 70resubcld 9227 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
b  -  a )  e.  RR )
7978adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
( b  -  a
)  e.  RR )
8035adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  A  e.  RR )
8180rexrd 8897 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  A  e.  RR* )
8236adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  B  e.  RR )
83 elicc2 10731 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( a  e.  ( A [,] B )  <-> 
( a  e.  RR  /\  A  <_  a  /\  a  <_  B ) ) )
8480, 82, 83syl2anc 642 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a  e.  ( A [,] B )  <->  ( a  e.  RR  /\  A  <_ 
a  /\  a  <_  B ) ) )
8561, 84mpbid 201 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a  e.  RR  /\  A  <_  a  /\  a  <_  B ) )
8685simp2d 968 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  A  <_  a )
87 iooss1 10707 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  RR*  /\  A  <_  a )  ->  (
a (,) b ) 
C_  ( A (,) b ) )
8881, 86, 87syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a (,) b ) 
C_  ( A (,) b ) )
8982rexrd 8897 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  B  e.  RR* )
90 elicc2 10731 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( b  e.  ( A [,] B )  <-> 
( b  e.  RR  /\  A  <_  b  /\  b  <_  B ) ) )
9180, 82, 90syl2anc 642 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
b  e.  ( A [,] B )  <->  ( b  e.  RR  /\  A  <_ 
b  /\  b  <_  B ) ) )
9259, 91mpbid 201 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
b  e.  RR  /\  A  <_  b  /\  b  <_  B ) )
9392simp3d 969 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  <_  B )
94 iooss2 10708 . . . . . . . . . . . . . . . . . 18  |-  ( ( B  e.  RR*  /\  b  <_  B )  ->  ( A (,) b )  C_  ( A (,) B ) )
9589, 93, 94syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( A (,) b )  C_  ( A (,) B ) )
9688, 95sstrd 3202 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a (,) b ) 
C_  ( A (,) B ) )
97 ssn0 3500 . . . . . . . . . . . . . . . 16  |-  ( ( ( a (,) b
)  C_  ( A (,) B )  /\  (
a (,) b )  =/=  (/) )  ->  ( A (,) B )  =/=  (/) )
9896, 97sylan 457 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
( A (,) B
)  =/=  (/) )
99 n0 3477 . . . . . . . . . . . . . . . . 17  |-  ( ( A (,) B )  =/=  (/)  <->  E. x  x  e.  ( A (,) B
) )
100 0re 8854 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  RR
101100a1i 10 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  0  e.  RR )
102 dvf 19273 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( RR 
_D  F ) : dom  ( RR  _D  F ) --> CC
103 dvlip.d . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
104103feq2d 5396 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( RR  _D  F ) : dom  ( RR  _D  F
) --> CC  <->  ( RR  _D  F ) : ( A (,) B ) --> CC ) )
105102, 104mpbii 202 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( RR  _D  F
) : ( A (,) B ) --> CC )
106 ffvelrn 5679 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( RR  _D  F
) : ( A (,) B ) --> CC 
/\  x  e.  ( A (,) B ) )  ->  ( ( RR  _D  F ) `  x )  e.  CC )
107105, 106sylan 457 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( ( RR  _D  F ) `  x )  e.  CC )
108107abscld 11934 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( abs `  ( ( RR  _D  F ) `  x
) )  e.  RR )
10976adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  M  e.  RR )
110107absge0d 11942 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  0  <_  ( abs `  ( ( RR  _D  F ) `
 x ) ) )
111 dvlip.l . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( abs `  ( ( RR  _D  F ) `  x
) )  <_  M
)
112101, 108, 109, 110, 111letrd 8989 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  0  <_  M )
113112ex 423 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( x  e.  ( A (,) B )  ->  0  <_  M
) )
114113exlimdv 1626 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( E. x  x  e.  ( A (,) B )  ->  0  <_  M ) )
115114imp 418 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  E. x  x  e.  ( A (,) B ) )  -> 
0  <_  M )
11699, 115sylan2b 461 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( A (,) B )  =/=  (/) )  -> 
0  <_  M )
117116adantlr 695 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( A (,) B )  =/=  (/) )  ->  0  <_  M )
11898, 117syldan 456 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
0  <_  M )
119 simpr3 963 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  <_  b )
12072, 70subge0d 9378 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
0  <_  ( b  -  a )  <->  a  <_  b ) )
121119, 120mpbird 223 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  0  <_  ( b  -  a
) )
122121adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
0  <_  ( b  -  a ) )
12377, 79, 118, 122mulge0d 9365 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
0  <_  ( M  x.  ( b  -  a
) ) )
124123ex 423 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( a (,) b
)  =/=  (/)  ->  0  <_  ( M  x.  (
b  -  a ) ) ) )
12575, 124sylbird 226 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a  <  b  ->  0  <_  ( M  x.  ( b  -  a
) ) ) )
12672recnd 8877 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  CC )
12770recnd 8877 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  CC )
128 subeq0 9089 . . . . . . . . . . . . . 14  |-  ( ( b  e.  CC  /\  a  e.  CC )  ->  ( ( b  -  a )  =  0  <-> 
b  =  a ) )
129126, 127, 128syl2anc 642 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( b  -  a
)  =  0  <->  b  =  a ) )
130 equcom 1665 . . . . . . . . . . . . 13  |-  ( b  =  a  <->  a  =  b )
131129, 130syl6bb 252 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( b  -  a
)  =  0  <->  a  =  b ) )
13276adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  M  e.  RR )
133132recnd 8877 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  M  e.  CC )
134133mul01d 9027 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( M  x.  0 )  =  0 )
135134eqcomd 2301 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  0  =  ( M  x.  0 ) )
136 eqle 8939 . . . . . . . . . . . . . 14  |-  ( ( 0  e.  RR  /\  0  =  ( M  x.  0 ) )  -> 
0  <_  ( M  x.  0 ) )
137100, 135, 136sylancr 644 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  0  <_  ( M  x.  0 ) )
138 oveq2 5882 . . . . . . . . . . . . . 14  |-  ( ( b  -  a )  =  0  ->  ( M  x.  ( b  -  a ) )  =  ( M  x.  0 ) )
139138breq2d 4051 . . . . . . . . . . . . 13  |-  ( ( b  -  a )  =  0  ->  (
0  <_  ( M  x.  ( b  -  a
) )  <->  0  <_  ( M  x.  0 ) ) )
140137, 139syl5ibrcom 213 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( b  -  a
)  =  0  -> 
0  <_  ( M  x.  ( b  -  a
) ) ) )
141131, 140sylbird 226 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a  =  b  -> 
0  <_  ( M  x.  ( b  -  a
) ) ) )
14270, 72leloed 8978 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a  <_  b  <->  ( a  <  b  \/  a  =  b ) ) )
143119, 142mpbid 201 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a  <  b  \/  a  =  b )
)
144125, 141, 143mpjaod 370 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  0  <_  ( M  x.  (
b  -  a ) ) )
145144adantr 451 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =  ( F `  a ) )  -> 
0  <_  ( M  x.  ( b  -  a
) ) )
14668, 145eqbrtrd 4059 . . . . . . . 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
) ) )
14760, 62subcld 9173 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( F `  b
)  -  ( F `
 a ) )  e.  CC )
148147adantr 451 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( F `  b )  -  ( F `  a )
)  e.  CC )
149148abscld 11934 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  e.  RR )
150149recnd 8877 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  e.  CC )
15178adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( b  -  a
)  e.  RR )
152151recnd 8877 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( b  -  a
)  e.  CC )
153143ord 366 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( -.  a  <  b  -> 
a  =  b ) )
154 fveq2 5541 . . . . . . . . . . . . . . . . 17  |-  ( a  =  b  ->  ( F `  a )  =  ( F `  b ) )
155154eqcomd 2301 . . . . . . . . . . . . . . . 16  |-  ( a  =  b  ->  ( F `  b )  =  ( F `  a ) )
156153, 155syl6 29 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( -.  a  <  b  -> 
( F `  b
)  =  ( F `
 a ) ) )
157156necon1ad 2526 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( F `  b
)  =/=  ( F `
 a )  -> 
a  <  b )
)
158157imp 418 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
a  <  b )
15970adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
a  e.  RR )
16072adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
b  e.  RR )
161159, 160posdifd 9375 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a  <  b  <->  0  <  ( b  -  a ) ) )
162158, 161mpbid 201 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
0  <  ( b  -  a ) )
163162gt0ne0d 9353 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( b  -  a
)  =/=  0 )
164150, 152, 163divrec2d 9556 . . . . . . . . . 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 ) ) ) ) )
165 iccss2 10736 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B ) )  -> 
( a [,] b
)  C_  ( A [,] B ) )
16661, 59, 165syl2anc 642 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a [,] b ) 
C_  ( A [,] B ) )
167166adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a [,] b
)  C_  ( A [,] B ) )
168167sselda 3193 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  y  e.  ( a [,] b
) )  ->  y  e.  ( A [,] B
) )
16941ad2antrr 706 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  ->  F : ( A [,] B ) --> CC )
170 ffvelrn 5679 . . . . . . . . . . . . . . . . . 18  |-  ( ( F : ( A [,] B ) --> CC 
/\  y  e.  ( A [,] B ) )  ->  ( F `  y )  e.  CC )
171169, 170sylan 457 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  y  e.  ( A [,] B
) )  ->  ( F `  y )  e.  CC )
172168, 171syldan 456 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  y  e.  ( a [,] b
) )  ->  ( F `  y )  e.  CC )
173147ad2antrr 706 . . . . . . . . . . . . . . . 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 )
17464necon3bid 2494 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( ( F `  b )  -  ( F `  a )
)  =/=  0  <->  ( F `  b )  =/=  ( F `  a
) ) )
175174biimpar 471 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( F `  b )  -  ( F `  a )
)  =/=  0 )
176175adantr 451 . . . . . . . . . . . . . . . 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 )
177172, 173, 176divcld 9552 . . . . . . . . . . . . . . 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 )
178169, 167feqresmpt 5592 . . . . . . . . . . . . . . . 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 ) ) )
179 eqidd 2297 . . . . . . . . . . . . . . . 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 ) ) ) ) )
180 oveq1 5881 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( F `  y )  ->  (
x  /  ( ( F `  b )  -  ( F `  a ) ) )  =  ( ( F `
 y )  / 
( ( F `  b )  -  ( F `  a )
) ) )
181172, 178, 179, 180fmptco 5707 . . . . . . . . . . . . . . 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 ) ) ) ) )
182 ref 11613 . . . . . . . . . . . . . . . . 17  |-  Re : CC
--> RR
183182a1i 10 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  ->  Re : CC --> RR )
184183feqmptd 5591 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  ->  Re  =  ( x  e.  CC  |->  ( Re `  x ) ) )
185 fveq2 5541 . . . . . . . . . . . . . . 15  |-  ( x  =  ( ( F `
 y )  / 
( ( F `  b )  -  ( F `  a )
) )  ->  (
Re `  x )  =  ( Re `  ( ( F `  y )  /  (
( F `  b
)  -  ( F `
 a ) ) ) ) )
186177, 181, 184, 185fmptco 5707 . . . . . . . . . . . . . 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 )
) ) ) ) )
18739adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  F  e.  ( ( A [,] B ) -cn-> CC ) )
188 rescncf 18417 . . . . . . . . . . . . . . . . . 18  |-  ( ( a [,] b ) 
C_  ( A [,] B )  ->  ( F  e.  ( ( A [,] B ) -cn-> CC )  ->  ( F  |`  ( a [,] b
) )  e.  ( ( a [,] b
) -cn-> CC ) ) )
189166, 187, 188sylc 56 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( F  |`  ( a [,] b ) )  e.  ( ( a [,] b ) -cn-> CC ) )
190189adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( F  |`  (
a [,] b ) )  e.  ( ( a [,] b )
-cn-> CC ) )
191 eqid 2296 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  CC  |->  ( x  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  =  ( x  e.  CC  |->  ( x  /  (
( F `  b
)  -  ( F `
 a ) ) ) )
192191divccncf 18426 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( F `  b )  -  ( F `  a )
)  e.  CC  /\  ( ( F `  b )  -  ( F `  a )
)  =/=  0 )  ->  ( x  e.  CC  |->  ( x  / 
( ( F `  b )  -  ( F `  a )
) ) )  e.  ( CC -cn-> CC ) )
193148, 175, 192syl2anc 642 . . . . . . . . . . . . . . . 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 ) )
194190, 193cncfco 18427 . . . . . . . . . . . . . . 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 ) )
195 recncf 18422 . . . . . . . . . . . . . . . 16  |-  Re  e.  ( CC -cn-> RR )
196195a1i 10 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  ->  Re  e.  ( CC -cn-> RR ) )
197194, 196cncfco 18427 . . . . . . . . . . . . . 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 ) )
198186, 197eqeltrrd 2371 . . . . . . . . . . . . 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 ) )
19949a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  ->  RR  C_  CC )
200 iccssre 10747 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  e.  RR  /\  b  e.  RR )  ->  ( a [,] b
)  C_  RR )
201159, 160, 200syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a [,] b
)  C_  RR )
202177recld 11695 . . . . . . . . . . . . . . . . . 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 )
203202recnd 8877 . . . . . . . . . . . . . . . . 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 )
204 eqid 2296 . . . . . . . . . . . . . . . . . 18  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
205204tgioo2 18325 . . . . . . . . . . . . . . . . 17  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
206 iccntr 18342 . . . . . . . . . . . . . . . . . . 19  |-  ( ( a  e.  RR  /\  b  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( a [,] b ) )  =  ( a (,) b
) )
20770, 72, 206syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( int `  ( topGen `
 ran  (,) )
) `  ( a [,] b ) )  =  ( a (,) b
) )
208207adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( int `  ( topGen `
 ran  (,) )
) `  ( a [,] b ) )  =  ( a (,) b
) )
209199, 201, 203, 205, 204, 208dvmptntr 19336 . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
210 ioossicc 10751 . . . . . . . . . . . . . . . . . . 19  |-  ( a (,) b )  C_  ( a [,] b
)
211210sseli 3189 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( a (,) b )  ->  y  e.  ( a [,] b
) )
212211, 177sylan2 460 . . . . . . . . . . . . . . . . 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 )
213 ovex 5899 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( RR  _D  F
) `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) )  e.  _V
214213a1i 10 . . . . . . . . . . . . . . . . 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 )
215 reex 8844 . . . . . . . . . . . . . . . . . . . 20  |-  RR  e.  _V
216215prid1 3747 . . . . . . . . . . . . . . . . . . 19  |-  RR  e.  { RR ,  CC }
217216a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  ->  RR  e.  { RR ,  CC } )
218211, 172sylan2 460 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  y  e.  ( a (,) b
) )  ->  ( F `  y )  e.  CC )
21996adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a (,) b
)  C_  ( A (,) B ) )
220219sselda 3193 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  y  e.  ( a (,) b
) )  ->  y  e.  ( A (,) B
) )
221105ad2antrr 706 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( RR  _D  F
) : ( A (,) B ) --> CC )
222 ffvelrn 5679 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( RR  _D  F
) : ( A (,) B ) --> CC 
/\  y  e.  ( A (,) B ) )  ->  ( ( RR  _D  F ) `  y )  e.  CC )
223221, 222sylan 457 . . . . . . . . . . . . . . . . . . 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 )
224220, 223syldan 456 . . . . . . . . . . . . . . . . . 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 )
22538ad2antrr 706 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( A [,] B
)  C_  RR )
226 ioossre 10728 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a (,) b )  C_  RR
227226a1i 10 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a (,) b
)  C_  RR )
228204, 205dvres 19277 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
229199, 169, 225, 227, 228syl22anc 1183 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
230 retop 18286 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( topGen ` 
ran  (,) )  e.  Top
231 iooretop 18291 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a (,) b )  e.  ( topGen `  ran  (,) )
232 isopn3i 16835 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( a (,) b )  e.  ( topGen `  ran  (,) )
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  (
a (,) b ) )  =  ( a (,) b ) )
233230, 231, 232mp2an 653 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( a (,) b
) )  =  ( a (,) b )
234233reseq2i 4968 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( a (,) b ) ) )  =  ( ( RR 
_D  F )  |`  ( a (,) b
) )
235229, 234syl6eq 2344 . . . . . . . . . . . . . . . . . . 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
) ) )
236210, 167syl5ss 3203 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a (,) b
)  C_  ( A [,] B ) )
237169, 236feqresmpt 5592 . . . . . . . . . . . . . . . . . . . 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 ) ) )
238237oveq2d 5890 . . . . . . . . . . . . . . . . . . 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
) ) ) )
239105adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( RR  _D  F ) : ( A (,) B
) --> CC )
240 fssres 5424 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( RR  _D  F
) : ( A (,) B ) --> CC 
/\  ( a (,) b )  C_  ( A (,) B ) )  ->  ( ( RR 
_D  F )  |`  ( a (,) b
) ) : ( a (,) b ) --> CC )
241239, 96, 240syl2anc 642 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( RR  _D  F
)  |`  ( a (,) b ) ) : ( a (,) b
) --> CC )
242241feqmptd 5591 . . . . . . . . . . . . . . . . . . . . 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
) ) )
243242adantr 451 . . . . . . . . . . . . . . . . . . . 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 ) ) )
244 fvres 5558 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( a (,) b )  ->  (
( ( RR  _D  F )  |`  (
a (,) b ) ) `  y )  =  ( ( RR 
_D  F ) `  y ) )
245244mpteq2ia 4118 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( a (,) b )  |->  ( ( ( RR  _D  F
)  |`  ( a (,) b ) ) `  y ) )  =  ( y  e.  ( a (,) b ) 
|->  ( ( RR  _D  F ) `  y
) )
246243, 245syl6eq 2344 . . . . . . . . . . . . . . . . . . 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 ) ) )
247235, 238, 2463eqtr3d 2336 . . . . . . . . . . . . . . . . . 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 )
) )
248217, 218, 224, 247, 148, 175dvmptdivc 19330 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
249212, 214, 248dvmptre 19334 . . . . . . . . . . . . . . . 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 )
) ) ) ) )
250209, 249eqtrd 2328 . . . . . . . . . . . . . . 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 )
) ) ) ) )
251250dmeqd 4897 . . . . . . . . . . . . . 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 ) ) ) ) ) )
252 dmmptg 5186 . . . . . . . . . . . . . . 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
) )
253 fvex 5555 . . . . . . . . . . . . . . . 16  |-  ( Re
`  ( ( ( RR  _D  F ) `
 y )  / 
( ( F `  b )  -  ( F `  a )
) ) )  e. 
_V
254253a1i 10 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( a (,) b )  ->  (
Re `  ( (
( RR  _D  F
) `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  e. 
_V )
255252, 254mprg 2625 . . . . . . . . . . . . . 14  |-  dom  (
y  e.  ( a (,) b )  |->  ( Re `  ( ( ( RR  _D  F
) `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) ) )  =  ( a (,) b )
256251, 255syl6eq 2344 . . . . . . . . . . . . 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 ) )
257159, 160, 158, 198, 256mvth 19355 . . . . . . . . . . . 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
) ) )
258250fveq1d 5543 . . . . . . . . . . . . . . 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
) )
259 fveq2 5541 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  x  ->  (
( RR  _D  F
) `  y )  =  ( ( RR 
_D  F ) `  x ) )
260259oveq1d 5889 . . . . . . . . . . . . . . . . 17  |-  ( y  =  x  ->  (
( ( RR  _D  F ) `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) )  =  ( ( ( RR  _D  F ) `
 x )  / 
( ( F `  b )  -  ( F `  a )
) ) )
261260fveq2d 5545 . . . . . . . . . . . . . . . 16  |-  ( y  =  x  ->  (
Re `  ( (
( RR  _D  F
) `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  =  ( Re `  (
( ( RR  _D  F ) `  x
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) )
262 eqid 2296 . . . . . . . . . . . . . . . 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 ) ) ) ) )
263 fvex 5555 . . . . . . . . . . . . . . . 16  |-  ( Re
`  ( ( ( RR  _D  F ) `
 x )  / 
( ( F `  b )  -  ( F `  a )
) ) )  e. 
_V
264261, 262, 263fvmpt 5618 . . . . . . . . . . . . . . 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 )
) ) ) )
265258, 264sylan9eq 2348 . . . . . . . . . . . . . 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 ) ) ) ) )
266 ubicc2 10769 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  RR*  /\  b  e.  RR*  /\  a  <_ 
b )  ->  b  e.  ( a [,] b
) )
26771, 73, 119, 266syl3anc 1182 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  ( a [,] b
) )
268267ad2antrr 706 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  b  e.  ( a [,] b
) )
26917oveq1d 5889 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  b  ->  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) )  =  ( ( F `
 b )  / 
( ( F `  b )  -  ( F `  a )
) ) )
270269fveq2d 5545 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  b  ->  (
Re `  ( ( F `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  =  ( Re `  (
( F `  b
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) )
271 eqid 2296 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( a [,] b )  |->  ( Re
`  ( ( F `
 y )  / 
( ( F `  b )  -  ( F `  a )
) ) ) )  =  ( y  e.  ( a [,] b
)  |->  ( Re `  ( ( F `  y )  /  (
( F `  b
)  -  ( F `
 a ) ) ) ) )
272 fvex 5555 . . . . . . . . . . . . . . . . . . 19  |-  ( Re
`  ( ( F `
 b )  / 
( ( F `  b )  -  ( F `  a )
) ) )  e. 
_V
273270, 271, 272fvmpt 5618 . . . . . . . . . . . . . . . . . 18  |-  ( b  e.  ( a [,] b )  ->  (
( y  e.  ( a [,] b ) 
|->  ( Re `  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) ) `  b
)  =  ( Re
`  ( ( F `
 b )  / 
( ( F `  b )  -  ( F `  a )
) ) ) )
274268, 273syl 15 . . . . . . . . . . . . . . . . 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 )
) ) ) )
275 lbicc2 10768 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  RR*  /\  b  e.  RR*  /\  a  <_ 
b )  ->  a  e.  ( a [,] b
) )
27671, 73, 119, 275syl3anc 1182 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  ( a [,] b
) )
277276ad2antrr 706 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  a  e.  ( a [,] b
) )
27826oveq1d 5889 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  a  ->  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) )  =  ( ( F `
 a )  / 
( ( F `  b )  -  ( F `  a )
) ) )
279278fveq2d 5545 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  a  ->  (
Re `  ( ( F `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  =  ( Re `  (
( F `  a
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) )
280 fvex 5555 . . . . . . . . . . . . . . . . . . 19  |-  ( Re
`  ( ( F `
 a )  / 
( ( F `  b )  -  ( F `  a )
) ) )  e. 
_V
281279, 271, 280fvmpt 5618 . . . . . . . . . . . . . . . . . 18  |-  ( a  e.  ( a [,] b )  ->  (
( y  e.  ( a [,] b ) 
|->  ( Re `  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) ) `  a
)  =  ( Re
`  ( ( F `
 a )  / 
( ( F `  b )  -  ( F `  a )
) ) ) )
282277, 281syl 15 . . . . . . . . . . . . . . . . 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 )
) ) ) )
283274, 282oveq12d 5892 . . . . . . . . . . . . . . . 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 )
) ) ) ) )
28460adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( F `  b
)  e.  CC )
285284, 148, 175divcld 9552 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( F `  b )  /  (
( F `  b
)  -  ( F `
 a ) ) )  e.  CC )
28662adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( F `  a
)  e.  CC )
287286, 148, 175divcld 9552 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( F `  a )  /  (
( F `  b
)  -  ( F `
 a ) ) )  e.  CC )
288285, 287resubd 11717 . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
289284, 286, 148, 175divsubdird 9591 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
290148, 175dividd 9550 . . . . . . . . . . . . . . . . . . . . 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 )
291289, 290eqtr3d 2330 . . . . . . . . . . . . . . . . . . . 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 )
292291fveq2d 5545 . . . . . . . . . . . . . . . . . . 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 ) )
293 re1 11655 . . . . . . . . . . . . . . . . . . 19  |-  ( Re
`  1 )  =  1
294292, 293syl6eq 2344 . . . . . . . . . . . . . . . . . 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 )
295288, 294eqtr3d 2330 . . . . . . . . . . . . . . . . 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 )
296295adantr 451 . . . . . . . . . . . . . . . 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 )
297283, 296eqtrd 2328 . . . . . . . . . . . . . . 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 )
298297oveq1d 5889 . . . . . . . . . . . . . 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 ) ) )
299265, 298eqeq12d 2310 . . . . . . . . . . . . 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 ) ) ) )
300299rexbidva 2573 . . . . . . . . . . . 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 ) ) ) )
301257, 300mpbid 201 . . . . . . . . . . 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 ) ) )
302219sselda 3193 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  x  e.  ( A (,) B
) )
303221, 106sylan 457 . . . . . . . . . . . . . . . . . 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 )
304302, 303syldan 456 . . . . . . . . . . . . . . . . 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 )
305147ad2antrr 706 . . . . . . . . . . . . . . . . 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 )
306175adantr 451 . . . . . . . . . . . . . . . . 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 )
307304, 305, 306divcld 9552 . . . . . . . . . . . . . . . 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 )
308307recld 11695 . . . . . . . . . . . . . . 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 )
309149adantr 451 . . . . . . . . . . . . . . 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 )
310308, 309remulcld 8879 . . . . . . . . . . . . . 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 )
311304abscld 11934 . . . . . . . . . . . . . 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 )
312132ad2antrr 706 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,)