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

Theorem dvlip 19869
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 5720 . . . . . . . 8  |-  ( a  =  Y  ->  ( F `  a )  =  ( F `  Y ) )
21oveq2d 6089 . . . . . . 7  |-  ( a  =  Y  ->  (
( F `  b
)  -  ( F `
 a ) )  =  ( ( F `
 b )  -  ( F `  Y ) ) )
32fveq2d 5724 . . . . . 6  |-  ( a  =  Y  ->  ( abs `  ( ( F `
 b )  -  ( F `  a ) ) )  =  ( abs `  ( ( F `  b )  -  ( F `  Y ) ) ) )
4 oveq2 6081 . . . . . . . 8  |-  ( a  =  Y  ->  (
b  -  a )  =  ( b  -  Y ) )
54fveq2d 5724 . . . . . . 7  |-  ( a  =  Y  ->  ( abs `  ( b  -  a ) )  =  ( abs `  (
b  -  Y ) ) )
65oveq2d 6089 . . . . . 6  |-  ( a  =  Y  ->  ( M  x.  ( abs `  ( b  -  a
) ) )  =  ( M  x.  ( abs `  ( b  -  Y ) ) ) )
73, 6breq12d 4217 . . . . 5  |-  ( a  =  Y  ->  (
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  <_  ( M  x.  ( abs `  (
b  -  a ) ) )  <->  ( abs `  ( ( F `  b )  -  ( F `  Y )
) )  <_  ( M  x.  ( abs `  ( b  -  Y
) ) ) ) )
87imbi2d 308 . . . 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 5720 . . . . . . . 8  |-  ( b  =  X  ->  ( F `  b )  =  ( F `  X ) )
109oveq1d 6088 . . . . . . 7  |-  ( b  =  X  ->  (
( F `  b
)  -  ( F `
 Y ) )  =  ( ( F `
 X )  -  ( F `  Y ) ) )
1110fveq2d 5724 . . . . . 6  |-  ( b  =  X  ->  ( abs `  ( ( F `
 b )  -  ( F `  Y ) ) )  =  ( abs `  ( ( F `  X )  -  ( F `  Y ) ) ) )
12 oveq1 6080 . . . . . . . 8  |-  ( b  =  X  ->  (
b  -  Y )  =  ( X  -  Y ) )
1312fveq2d 5724 . . . . . . 7  |-  ( b  =  X  ->  ( abs `  ( b  -  Y ) )  =  ( abs `  ( X  -  Y )
) )
1413oveq2d 6089 . . . . . 6  |-  ( b  =  X  ->  ( M  x.  ( abs `  ( b  -  Y
) ) )  =  ( M  x.  ( abs `  ( X  -  Y ) ) ) )
1511, 14breq12d 4217 . . . . 5  |-  ( b  =  X  ->  (
( abs `  (
( F `  b
)  -  ( F `
 Y ) ) )  <_  ( M  x.  ( abs `  (
b  -  Y ) ) )  <->  ( abs `  ( ( F `  X )  -  ( F `  Y )
) )  <_  ( M  x.  ( abs `  ( X  -  Y
) ) ) ) )
1615imbi2d 308 . . . 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 5720 . . . . . . . . . 10  |-  ( y  =  b  ->  ( F `  y )  =  ( F `  b ) )
18 fveq2 5720 . . . . . . . . . 10  |-  ( x  =  a  ->  ( F `  x )  =  ( F `  a ) )
1917, 18oveqan12d 6092 . . . . . . . . 9  |-  ( ( y  =  b  /\  x  =  a )  ->  ( ( F `  y )  -  ( F `  x )
)  =  ( ( F `  b )  -  ( F `  a ) ) )
2019fveq2d 5724 . . . . . . . 8  |-  ( ( y  =  b  /\  x  =  a )  ->  ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  =  ( abs `  ( ( F `  b )  -  ( F `  a )
) ) )
21 oveq12 6082 . . . . . . . . . 10  |-  ( ( y  =  b  /\  x  =  a )  ->  ( y  -  x
)  =  ( b  -  a ) )
2221fveq2d 5724 . . . . . . . . 9  |-  ( ( y  =  b  /\  x  =  a )  ->  ( abs `  (
y  -  x ) )  =  ( abs `  ( b  -  a
) ) )
2322oveq2d 6089 . . . . . . . 8  |-  ( ( y  =  b  /\  x  =  a )  ->  ( M  x.  ( abs `  ( y  -  x ) ) )  =  ( M  x.  ( abs `  ( b  -  a ) ) ) )
2420, 23breq12d 4217 . . . . . . 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 440 . . . . . 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 5720 . . . . . . . . . 10  |-  ( y  =  a  ->  ( F `  y )  =  ( F `  a ) )
27 fveq2 5720 . . . . . . . . . 10  |-  ( x  =  b  ->  ( F `  x )  =  ( F `  b ) )
2826, 27oveqan12d 6092 . . . . . . . . 9  |-  ( ( y  =  a  /\  x  =  b )  ->  ( ( F `  y )  -  ( F `  x )
)  =  ( ( F `  a )  -  ( F `  b ) ) )
2928fveq2d 5724 . . . . . . . 8  |-  ( ( y  =  a  /\  x  =  b )  ->  ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  =  ( abs `  ( ( F `  a )  -  ( F `  b )
) ) )
30 oveq12 6082 . . . . . . . . . 10  |-  ( ( y  =  a  /\  x  =  b )  ->  ( y  -  x
)  =  ( a  -  b ) )
3130fveq2d 5724 . . . . . . . . 9  |-  ( ( y  =  a  /\  x  =  b )  ->  ( abs `  (
y  -  x ) )  =  ( abs `  ( a  -  b
) ) )
3231oveq2d 6089 . . . . . . . 8  |-  ( ( y  =  a  /\  x  =  b )  ->  ( M  x.  ( abs `  ( y  -  x ) ) )  =  ( M  x.  ( abs `  ( a  -  b ) ) ) )
3329, 32breq12d 4217 . . . . . . 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 440 . . . . . 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 10984 . . . . . . 7  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A [,] B
)  C_  RR )
3835, 36, 37syl2anc 643 . . . . . 6  |-  ( ph  ->  ( A [,] B
)  C_  RR )
39 dvlip.f . . . . . . . . . . 11  |-  ( ph  ->  F  e.  ( ( A [,] B )
-cn-> CC ) )
40 cncff 18915 . . . . . . . . . . 11  |-  ( F  e.  ( ( A [,] B ) -cn-> CC )  ->  F :
( A [,] B
) --> CC )
4139, 40syl 16 . . . . . . . . . 10  |-  ( ph  ->  F : ( A [,] B ) --> CC )
42 ffvelrn 5860 . . . . . . . . . . 11  |-  ( ( F : ( A [,] B ) --> CC 
/\  a  e.  ( A [,] B ) )  ->  ( F `  a )  e.  CC )
43 ffvelrn 5860 . . . . . . . . . . 11  |-  ( ( F : ( A [,] B ) --> CC 
/\  b  e.  ( A [,] B ) )  ->  ( F `  b )  e.  CC )
4442, 43anim12dan 811 . . . . . . . . . 10  |-  ( ( F : ( A [,] B ) --> CC 
/\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  (
( F `  a
)  e.  CC  /\  ( F `  b )  e.  CC ) )
4541, 44sylan 458 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  (
( F `  a
)  e.  CC  /\  ( F `  b )  e.  CC ) )
4645simprd 450 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( F `  b )  e.  CC )
4745simpld 446 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( F `  a )  e.  CC )
4846, 47abssubd 12247 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( abs `  ( ( F `
 b )  -  ( F `  a ) ) )  =  ( abs `  ( ( F `  a )  -  ( F `  b ) ) ) )
49 ax-resscn 9039 . . . . . . . . . . . 12  |-  RR  C_  CC
5038, 49syl6ss 3352 . . . . . . . . . . 11  |-  ( ph  ->  ( A [,] B
)  C_  CC )
5150sselda 3340 . . . . . . . . . 10  |-  ( (
ph  /\  b  e.  ( A [,] B ) )  ->  b  e.  CC )
5251adantrl 697 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  b  e.  CC )
5350sselda 3340 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  ( A [,] B ) )  ->  a  e.  CC )
5453adantrr 698 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  a  e.  CC )
5552, 54abssubd 12247 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( abs `  ( b  -  a ) )  =  ( abs `  (
a  -  b ) ) )
5655oveq2d 6089 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B ) ) )  ->  ( M  x.  ( abs `  ( b  -  a
) ) )  =  ( M  x.  ( abs `  ( a  -  b ) ) ) )
5748, 56breq12d 4217 . . . . . 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 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  F : ( A [,] B ) --> CC )
59 simpr2 964 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  ( A [,] B
) )
6058, 59ffvelrnd 5863 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( F `  b )  e.  CC )
61 simpr1 963 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  ( A [,] B
) )
6258, 61ffvelrnd 5863 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( F `  a )  e.  CC )
6360, 62subeq0ad 9413 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( ( F `  b )  -  ( F `  a )
)  =  0  <->  ( F `  b )  =  ( F `  a ) ) )
6463biimpar 472 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =  ( F `  a ) )  -> 
( ( F `  b )  -  ( F `  a )
)  =  0 )
6564abs00bd 12088 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =  ( F `  a ) )  -> 
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  =  0 )
6638adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( A [,] B )  C_  RR )
6766, 61sseldd 3341 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  RR )
6867rexrd 9126 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  RR* )
6966, 59sseldd 3341 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  RR )
7069rexrd 9126 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  RR* )
71 ioon0 10934 . . . . . . . . . . . . 13  |-  ( ( a  e.  RR*  /\  b  e.  RR* )  ->  (
( a (,) b
)  =/=  (/)  <->  a  <  b ) )
7268, 70, 71syl2anc 643 . . . . . . . . . . . 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 707 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  ->  M  e.  RR )
7569, 67resubcld 9457 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
b  -  a )  e.  RR )
7675adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
( b  -  a
)  e.  RR )
7735adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  A  e.  RR )
7877rexrd 9126 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  A  e.  RR* )
7936adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  B  e.  RR )
80 elicc2 10967 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( a  e.  ( A [,] B )  <-> 
( a  e.  RR  /\  A  <_  a  /\  a  <_  B ) ) )
8177, 79, 80syl2anc 643 . . . . . . . . . . . . . . . . . . . 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 202 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a  e.  RR  /\  A  <_  a  /\  a  <_  B ) )
8382simp2d 970 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  A  <_  a )
84 iooss1 10943 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  RR*  /\  A  <_  a )  ->  (
a (,) b ) 
C_  ( A (,) b ) )
8578, 83, 84syl2anc 643 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a (,) b ) 
C_  ( A (,) b ) )
8679rexrd 9126 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  B  e.  RR* )
87 elicc2 10967 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( b  e.  ( A [,] B )  <-> 
( b  e.  RR  /\  A  <_  b  /\  b  <_  B ) ) )
8877, 79, 87syl2anc 643 . . . . . . . . . . . . . . . . . . . 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 202 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
b  e.  RR  /\  A  <_  b  /\  b  <_  B ) )
9089simp3d 971 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  <_  B )
91 iooss2 10944 . . . . . . . . . . . . . . . . . 18  |-  ( ( B  e.  RR*  /\  b  <_  B )  ->  ( A (,) b )  C_  ( A (,) B ) )
9286, 90, 91syl2anc 643 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( A (,) b )  C_  ( A (,) B ) )
9385, 92sstrd 3350 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a (,) b ) 
C_  ( A (,) B ) )
94 ssn0 3652 . . . . . . . . . . . . . . . 16  |-  ( ( ( a (,) b
)  C_  ( A (,) B )  /\  (
a (,) b )  =/=  (/) )  ->  ( A (,) B )  =/=  (/) )
9593, 94sylan 458 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
( A (,) B
)  =/=  (/) )
96 n0 3629 . . . . . . . . . . . . . . . . 17  |-  ( ( A (,) B )  =/=  (/)  <->  E. x  x  e.  ( A (,) B
) )
97 0re 9083 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  RR
9897a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  0  e.  RR )
99 dvf 19786 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( RR 
_D  F ) : dom  ( RR  _D  F ) --> CC
100 dvlip.d . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
101100feq2d 5573 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( RR  _D  F ) : dom  ( RR  _D  F
) --> CC  <->  ( RR  _D  F ) : ( A (,) B ) --> CC ) )
10299, 101mpbii 203 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( RR  _D  F
) : ( A (,) B ) --> CC )
103102ffvelrnda 5862 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( ( RR  _D  F ) `  x )  e.  CC )
104103abscld 12230 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( abs `  ( ( RR  _D  F ) `  x
) )  e.  RR )
10573adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  M  e.  RR )
106103absge0d 12238 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  0  <_  ( abs `  ( ( RR  _D  F ) `
 x ) ) )
107 dvlip.l . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( abs `  ( ( RR  _D  F ) `  x
) )  <_  M
)
10898, 104, 105, 106, 107letrd 9219 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  0  <_  M )
109108ex 424 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( x  e.  ( A (,) B )  ->  0  <_  M
) )
110109exlimdv 1646 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( E. x  x  e.  ( A (,) B )  ->  0  <_  M ) )
111110imp 419 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  E. x  x  e.  ( A (,) B ) )  -> 
0  <_  M )
11296, 111sylan2b 462 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( A (,) B )  =/=  (/) )  -> 
0  <_  M )
113112adantlr 696 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( A (,) B )  =/=  (/) )  ->  0  <_  M )
11495, 113syldan 457 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
0  <_  M )
115 simpr3 965 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  <_  b )
11669, 67subge0d 9608 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
0  <_  ( b  -  a )  <->  a  <_  b ) )
117115, 116mpbird 224 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  0  <_  ( b  -  a
) )
118117adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
0  <_  ( b  -  a ) )
11974, 76, 114, 118mulge0d 9595 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( a (,) b
)  =/=  (/) )  -> 
0  <_  ( M  x.  ( b  -  a
) ) )
120119ex 424 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( a (,) b
)  =/=  (/)  ->  0  <_  ( M  x.  (
b  -  a ) ) ) )
12172, 120sylbird 227 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a  <  b  ->  0  <_  ( M  x.  ( b  -  a
) ) ) )
12269recnd 9106 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  CC )
12367recnd 9106 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  CC )
124122, 123subeq0ad 9413 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( b  -  a
)  =  0  <->  b  =  a ) )
125 equcom 1692 . . . . . . . . . . . . 13  |-  ( b  =  a  <->  a  =  b )
126124, 125syl6bb 253 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( b  -  a
)  =  0  <->  a  =  b ) )
12773adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  M  e.  RR )
128127recnd 9106 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  M  e.  CC )
129128mul01d 9257 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( M  x.  0 )  =  0 )
130129eqcomd 2440 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  0  =  ( M  x.  0 ) )
131 eqle 9168 . . . . . . . . . . . . . 14  |-  ( ( 0  e.  RR  /\  0  =  ( M  x.  0 ) )  -> 
0  <_  ( M  x.  0 ) )
13297, 130, 131sylancr 645 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  0  <_  ( M  x.  0 ) )
133 oveq2 6081 . . . . . . . . . . . . . 14  |-  ( ( b  -  a )  =  0  ->  ( M  x.  ( b  -  a ) )  =  ( M  x.  0 ) )
134133breq2d 4216 . . . . . . . . . . . . 13  |-  ( ( b  -  a )  =  0  ->  (
0  <_  ( M  x.  ( b  -  a
) )  <->  0  <_  ( M  x.  0 ) ) )
135132, 134syl5ibrcom 214 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( b  -  a
)  =  0  -> 
0  <_  ( M  x.  ( b  -  a
) ) ) )
136126, 135sylbird 227 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a  =  b  -> 
0  <_  ( M  x.  ( b  -  a
) ) ) )
13767, 69leloed 9208 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a  <_  b  <->  ( a  <  b  \/  a  =  b ) ) )
138115, 137mpbid 202 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a  <  b  \/  a  =  b )
)
139121, 136, 138mpjaod 371 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  0  <_  ( M  x.  (
b  -  a ) ) )
140139adantr 452 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =  ( F `  a ) )  -> 
0  <_  ( M  x.  ( b  -  a
) ) )
14165, 140eqbrtrd 4224 . . . . . . . 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 9403 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( F `  b
)  -  ( F `
 a ) )  e.  CC )
143142adantr 452 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( F `  b )  -  ( F `  a )
)  e.  CC )
144143abscld 12230 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  e.  RR )
145144recnd 9106 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  e.  CC )
14675adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( b  -  a
)  e.  RR )
147146recnd 9106 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( b  -  a
)  e.  CC )
148138ord 367 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( -.  a  <  b  -> 
a  =  b ) )
149 fveq2 5720 . . . . . . . . . . . . . . . . 17  |-  ( a  =  b  ->  ( F `  a )  =  ( F `  b ) )
150149eqcomd 2440 . . . . . . . . . . . . . . . 16  |-  ( a  =  b  ->  ( F `  b )  =  ( F `  a ) )
151148, 150syl6 31 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( -.  a  <  b  -> 
( F `  b
)  =  ( F `
 a ) ) )
152151necon1ad 2665 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( F `  b
)  =/=  ( F `
 a )  -> 
a  <  b )
)
153152imp 419 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
a  <  b )
15467adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
a  e.  RR )
15569adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
b  e.  RR )
156154, 155posdifd 9605 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a  <  b  <->  0  <  ( b  -  a ) ) )
157153, 156mpbid 202 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
0  <  ( b  -  a ) )
158157gt0ne0d 9583 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( b  -  a
)  =/=  0 )
159145, 147, 158divrec2d 9786 . . . . . . . . . 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 10973 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B ) )  -> 
( a [,] b
)  C_  ( A [,] B ) )
16161, 59, 160syl2anc 643 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
a [,] b ) 
C_  ( A [,] B ) )
162161adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a [,] b
)  C_  ( A [,] B ) )
163162sselda 3340 . . . . . . . . . . . . . . . . 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 707 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  ->  F : ( A [,] B ) --> CC )
165164ffvelrnda 5862 . . . . . . . . . . . . . . . . 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 457 . . . . . . . . . . . . . . . 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 707 . . . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( F `  b )  -  ( F `  a )
)  =/=  0 )
170169adantr 452 . . . . . . . . . . . . . . . 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 9782 . . . . . . . . . . . . . . 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 5772 . . . . . . . . . . . . . . . 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 2436 . . . . . . . . . . . . . . . 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 6080 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( F `  y )  ->  (
x  /  ( ( F `  b )  -  ( F `  a ) ) )  =  ( ( F `
 y )  / 
( ( F `  b )  -  ( F `  a )
) ) )
175166, 172, 173, 174fmptco 5893 . . . . . . . . . . . . . . 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 11909 . . . . . . . . . . . . . . . . 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 5771 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  ->  Re  =  ( x  e.  CC  |->  ( Re `  x ) ) )
179 fveq2 5720 . . . . . . . . . . . . . . 15  |-  ( x  =  ( ( F `
 y )  / 
( ( F `  b )  -  ( F `  a )
) )  ->  (
Re `  x )  =  ( Re `  ( ( F `  y )  /  (
( F `  b
)  -  ( F `
 a ) ) ) ) )
180171, 175, 178, 179fmptco 5893 . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  F  e.  ( ( A [,] B ) -cn-> CC ) )
182 rescncf 18919 . . . . . . . . . . . . . . . . . 18  |-  ( ( a [,] b ) 
C_  ( A [,] B )  ->  ( F  e.  ( ( A [,] B ) -cn-> CC )  ->  ( F  |`  ( a [,] b
) )  e.  ( ( a [,] b
) -cn-> CC ) ) )
183161, 181, 182sylc 58 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( F  |`  ( a [,] b ) )  e.  ( ( a [,] b ) -cn-> CC ) )
184183adantr 452 . . . . . . . . . . . . . . . 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 2435 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  CC  |->  ( x  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  =  ( x  e.  CC  |->  ( x  /  (
( F `  b
)  -  ( F `
 a ) ) ) )
186185divccncf 18928 . . . . . . . . . . . . . . . . 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 643 . . . . . . . . . . . . . . . 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 18929 . . . . . . . . . . . . . . 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 18924 . . . . . . . . . . . . . . . 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 18929 . . . . . . . . . . . . . 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 2510 . . . . . . . . . . . . 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 10984 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  e.  RR  /\  b  e.  RR )  ->  ( a [,] b
)  C_  RR )
195154, 155, 194syl2anc 643 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a [,] b
)  C_  RR )
196171recld 11991 . . . . . . . . . . . . . . . . . 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 9106 . . . . . . . . . . . . . . . . 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 2435 . . . . . . . . . . . . . . . . . 18  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
199198tgioo2 18826 . . . . . . . . . . . . . . . . 17  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
200 iccntr 18844 . . . . . . . . . . . . . . . . . . 19  |-  ( ( a  e.  RR  /\  b  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( a [,] b ) )  =  ( a (,) b
) )
20167, 69, 200syl2anc 643 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( int `  ( topGen `
 ran  (,) )
) `  ( a [,] b ) )  =  ( a (,) b
) )
202201adantr 452 . . . . . . . . . . . . . . . . 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 19849 . . . . . . . . . . . . . . . 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 10988 . . . . . . . . . . . . . . . . . . 19  |-  ( a (,) b )  C_  ( a [,] b
)
205204sseli 3336 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( a (,) b )  ->  y  e.  ( a [,] b
) )
206205, 171sylan2 461 . . . . . . . . . . . . . . . . 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 6098 . . . . . . . . . . . . . . . . . 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 reex 9073 . . . . . . . . . . . . . . . . . . . 20  |-  RR  e.  _V
210209prid1 3904 . . . . . . . . . . . . . . . . . . 19  |-  RR  e.  { RR ,  CC }
211210a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  ->  RR  e.  { RR ,  CC } )
212205, 166sylan2 461 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  y  e.  ( a (,) b
) )  ->  ( F `  y )  e.  CC )
21393adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a (,) b
)  C_  ( A (,) B ) )
214213sselda 3340 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  y  e.  ( a (,) b
) )  ->  y  e.  ( A (,) B
) )
215102ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( RR  _D  F
) : ( A (,) B ) --> CC )
216215ffvelrnda 5862 . . . . . . . . . . . . . . . . . . 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 )
217214, 216syldan 457 . . . . . . . . . . . . . . . . . 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 )
21838ad2antrr 707 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( A [,] B
)  C_  RR )
219 ioossre 10964 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a (,) b )  C_  RR
220219a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a (,) b
)  C_  RR )
221198, 199dvres 19790 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
222193, 164, 218, 220, 221syl22anc 1185 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
223 retop 18787 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( topGen ` 
ran  (,) )  e.  Top
224 iooretop 18792 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a (,) b )  e.  ( topGen `  ran  (,) )
225 isopn3i 17138 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( a (,) b )  e.  ( topGen `  ran  (,) )
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  (
a (,) b ) )  =  ( a (,) b ) )
226223, 224, 225mp2an 654 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( a (,) b
) )  =  ( a (,) b )
227226reseq2i 5135 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( a (,) b ) ) )  =  ( ( RR 
_D  F )  |`  ( a (,) b
) )
228222, 227syl6eq 2483 . . . . . . . . . . . . . . . . . . 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
) ) )
229204, 162syl5ss 3351 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( a (,) b
)  C_  ( A [,] B ) )
230164, 229feqresmpt 5772 . . . . . . . . . . . . . . . . . . . 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 ) ) )
231230oveq2d 6089 . . . . . . . . . . . . . . . . . . 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
) ) ) )
232102adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  ( RR  _D  F ) : ( A (,) B
) --> CC )
233 fssres 5602 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( RR  _D  F
) : ( A (,) B ) --> CC 
/\  ( a (,) b )  C_  ( A (,) B ) )  ->  ( ( RR 
_D  F )  |`  ( a (,) b
) ) : ( a (,) b ) --> CC )
234232, 93, 233syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  (
( RR  _D  F
)  |`  ( a (,) b ) ) : ( a (,) b
) --> CC )
235234feqmptd 5771 . . . . . . . . . . . . . . . . . . . . 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
) ) )
236235adantr 452 . . . . . . . . . . . . . . . . . . . 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 ) ) )
237 fvres 5737 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( a (,) b )  ->  (
( ( RR  _D  F )  |`  (
a (,) b ) ) `  y )  =  ( ( RR 
_D  F ) `  y ) )
238237mpteq2ia 4283 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( a (,) b )  |->  ( ( ( RR  _D  F
)  |`  ( a (,) b ) ) `  y ) )  =  ( y  e.  ( a (,) b ) 
|->  ( ( RR  _D  F ) `  y
) )
239236, 238syl6eq 2483 . . . . . . . . . . . . . . . . . . 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 ) ) )
240228, 231, 2393eqtr3d 2475 . . . . . . . . . . . . . . . . . 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 )
) )
241211, 212, 217, 240, 143, 169dvmptdivc 19843 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
242206, 208, 241dvmptre 19847 . . . . . . . . . . . . . . . 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 )
) ) ) ) )
243203, 242eqtrd 2467 . . . . . . . . . . . . . . 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 )
) ) ) ) )
244243dmeqd 5064 . . . . . . . . . . . . . 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 ) ) ) ) ) )
245 dmmptg 5359 . . . . . . . . . . . . . . 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
) )
246 fvex 5734 . . . . . . . . . . . . . . . 16  |-  ( Re
`  ( ( ( RR  _D  F ) `
 y )  / 
( ( F `  b )  -  ( F `  a )
) ) )  e. 
_V
247246a1i 11 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( a (,) b )  ->  (
Re `  ( (
( RR  _D  F
) `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  e. 
_V )
248245, 247mprg 2767 . . . . . . . . . . . . . 14  |-  dom  (
y  e.  ( a (,) b )  |->  ( Re `  ( ( ( RR  _D  F
) `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) ) )  =  ( a (,) b )
249244, 248syl6eq 2483 . . . . . . . . . . . . 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 ) )
250154, 155, 153, 192, 249mvth 19868 . . . . . . . . . . . 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
) ) )
251243fveq1d 5722 . . . . . . . . . . . . . . 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
) )
252 fveq2 5720 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  x  ->  (
( RR  _D  F
) `  y )  =  ( ( RR 
_D  F ) `  x ) )
253252oveq1d 6088 . . . . . . . . . . . . . . . . 17  |-  ( y  =  x  ->  (
( ( RR  _D  F ) `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) )  =  ( ( ( RR  _D  F ) `
 x )  / 
( ( F `  b )  -  ( F `  a )
) ) )
254253fveq2d 5724 . . . . . . . . . . . . . . . 16  |-  ( y  =  x  ->  (
Re `  ( (
( RR  _D  F
) `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  =  ( Re `  (
( ( RR  _D  F ) `  x
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) )
255 eqid 2435 . . . . . . . . . . . . . . . 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 ) ) ) ) )
256 fvex 5734 . . . . . . . . . . . . . . . 16  |-  ( Re
`  ( ( ( RR  _D  F ) `
 x )  / 
( ( F `  b )  -  ( F `  a )
) ) )  e. 
_V
257254, 255, 256fvmpt 5798 . . . . . . . . . . . . . . 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 )
) ) ) )
258251, 257sylan9eq 2487 . . . . . . . . . . . . . 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 ) ) ) ) )
259 ubicc2 11006 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  RR*  /\  b  e.  RR*  /\  a  <_ 
b )  ->  b  e.  ( a [,] b
) )
26068, 70, 115, 259syl3anc 1184 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  b  e.  ( a [,] b
) )
261260ad2antrr 707 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  b  e.  ( a [,] b
) )
26217oveq1d 6088 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  b  ->  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) )  =  ( ( F `
 b )  / 
( ( F `  b )  -  ( F `  a )
) ) )
263262fveq2d 5724 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  b  ->  (
Re `  ( ( F `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  =  ( Re `  (
( F `  b
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) )
264 eqid 2435 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( a [,] b )  |->  ( Re
`  ( ( F `
 y )  / 
( ( F `  b )  -  ( F `  a )
) ) ) )  =  ( y  e.  ( a [,] b
)  |->  ( Re `  ( ( F `  y )  /  (
( F `  b
)  -  ( F `
 a ) ) ) ) )
265 fvex 5734 . . . . . . . . . . . . . . . . . . 19  |-  ( Re
`  ( ( F `
 b )  / 
( ( F `  b )  -  ( F `  a )
) ) )  e. 
_V
266263, 264, 265fvmpt 5798 . . . . . . . . . . . . . . . . . 18  |-  ( b  e.  ( a [,] b )  ->  (
( y  e.  ( a [,] b ) 
|->  ( Re `  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) ) `  b
)  =  ( Re
`  ( ( F `
 b )  / 
( ( F `  b )  -  ( F `  a )
) ) ) )
267261, 266syl 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 )
) ) ) )
268 lbicc2 11005 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  RR*  /\  b  e.  RR*  /\  a  <_ 
b )  ->  a  e.  ( a [,] b
) )
26968, 70, 115, 268syl3anc 1184 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( A [,] B
)  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  ->  a  e.  ( a [,] b
) )
270269ad2antrr 707 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  a  e.  ( a [,] b
) )
27126oveq1d 6088 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  a  ->  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) )  =  ( ( F `
 a )  / 
( ( F `  b )  -  ( F `  a )
) ) )
272271fveq2d 5724 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  a  ->  (
Re `  ( ( F `  y )  /  ( ( F `
 b )  -  ( F `  a ) ) ) )  =  ( Re `  (
( F `  a
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) )
273 fvex 5734 . . . . . . . . . . . . . . . . . . 19  |-  ( Re
`  ( ( F `
 a )  / 
( ( F `  b )  -  ( F `  a )
) ) )  e. 
_V
274272, 264, 273fvmpt 5798 . . . . . . . . . . . . . . . . . 18  |-  ( a  e.  ( a [,] b )  ->  (
( y  e.  ( a [,] b ) 
|->  ( Re `  (
( F `  y
)  /  ( ( F `  b )  -  ( F `  a ) ) ) ) ) `  a
)  =  ( Re
`  ( ( F `
 a )  / 
( ( F `  b )  -  ( F `  a )
) ) ) )
275270, 274syl 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 )
) ) ) )
276267, 275oveq12d 6091 . . . . . . . . . . . . . . . 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 )
) ) ) ) )
27760adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( F `  b
)  e.  CC )
278277, 143, 169divcld 9782 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( F `  b )  /  (
( F `  b
)  -  ( F `
 a ) ) )  e.  CC )
27962adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( F `  a
)  e.  CC )
280279, 143, 169divcld 9782 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
( ( F `  a )  /  (
( F `  b
)  -  ( F `
 a ) ) )  e.  CC )
281278, 280resubd 12013 . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
282277, 279, 143, 169divsubdird 9821 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
283143, 169dividd 9780 . . . . . . . . . . . . . . . . . . . . 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 )
284282, 283eqtr3d 2469 . . . . . . . . . . . . . . . . . . . 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 )
285284fveq2d 5724 . . . . . . . . . . . . . . . . . . 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 ) )
286 re1 11951 . . . . . . . . . . . . . . . . . . 19  |-  ( Re
`  1 )  =  1
287285, 286syl6eq 2483 . . . . . . . . . . . . . . . . . 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 )
288281, 287eqtr3d 2469 . . . . . . . . . . . . . . . . 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 )
289288adantr 452 . . . . . . . . . . . . . . . 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 )
290276, 289eqtrd 2467 . . . . . . . . . . . . . . 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 )
291290oveq1d 6088 . . . . . . . . . . . . . 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 ) ) )
292258, 291eqeq12d 2449 . . . . . . . . . . . . 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 ) ) ) )
293292rexbidva 2714 . . . . . . . . . . . 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 ) ) ) )
294250, 293mpbid 202 . . . . . . . . . . 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 ) ) )
295213sselda 3340 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  x  e.  ( A (,) B
) )
296215ffvelrnda 5862 . . . . . . . . . . . . . . . . . 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 )
297295, 296syldan 457 . . . . . . . . . . . . . . . . 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 )
298142ad2antrr 707 . . . . . . . . . . . . . . . . 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 )
299169adantr 452 . . . . . . . . . . . . . . . . 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 )
300297, 298, 299divcld 9782 . . . . . . . . . . . . . . . 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 )
301300recld 11991 . . . . . . . . . . . . . . 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 )
302144adantr 452 . . . . . . . . . . . . . . 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 )
303301, 302remulcld 9108 . . . . . . . . . . . . . 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 )
304297abscld 12230 . . . . . . . . . . . . . 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 )
305127ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  M  e.  RR )
306300abscld 12230 . . . . . . . . . . . . . . . 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 )
307143absge0d 12238 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b ) )  /\  ( F `  b )  =/=  ( F `  a ) )  -> 
0  <_  ( abs `  ( ( F `  b )  -  ( F `  a )
) ) )
308307adantr 452 . . . . . . . . . . . . . . . 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 ) ) ) )
309300releabsd 12245 . . . . . . . . . . . . . . . 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 ) ) ) ) )
310301, 306, 302, 308, 309lemul1ad 9942 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( a  e.  ( A [,] B )  /\  b  e.  ( A [,] B )  /\  a  <_  b
) )  /\  ( F `  b )  =/=  ( F `  a
) )  /\  x  e.  ( a (,) b
) )  ->  (
( Re