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

Theorem dvcvx 19367
Description: A real function with strictly increasing derivative is strictly convex. (Contributed by Mario Carneiro, 20-Jun-2015.)
Hypotheses
Ref Expression
dvcvx.a  |-  ( ph  ->  A  e.  RR )
dvcvx.b  |-  ( ph  ->  B  e.  RR )
dvcvx.l  |-  ( ph  ->  A  <  B )
dvcvx.f  |-  ( ph  ->  F  e.  ( ( A [,] B )
-cn-> RR ) )
dvcvx.d  |-  ( ph  ->  ( RR  _D  F
)  Isom  <  ,  <  ( ( A (,) B
) ,  W ) )
dvcvx.t  |-  ( ph  ->  T  e.  ( 0 (,) 1 ) )
dvcvx.c  |-  C  =  ( ( T  x.  A )  +  ( ( 1  -  T
)  x.  B ) )
Assertion
Ref Expression
dvcvx  |-  ( ph  ->  ( F `  C
)  <  ( ( T  x.  ( F `  A ) )  +  ( ( 1  -  T )  x.  ( F `  B )
) ) )

Proof of Theorem dvcvx
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvcvx.a . . 3  |-  ( ph  ->  A  e.  RR )
2 dvcvx.c . . . 4  |-  C  =  ( ( T  x.  A )  +  ( ( 1  -  T
)  x.  B ) )
3 dvcvx.t . . . . . . 7  |-  ( ph  ->  T  e.  ( 0 (,) 1 ) )
4 elioore 10686 . . . . . . 7  |-  ( T  e.  ( 0 (,) 1 )  ->  T  e.  RR )
53, 4syl 15 . . . . . 6  |-  ( ph  ->  T  e.  RR )
65, 1remulcld 8863 . . . . 5  |-  ( ph  ->  ( T  x.  A
)  e.  RR )
7 1re 8837 . . . . . . 7  |-  1  e.  RR
8 resubcl 9111 . . . . . . 7  |-  ( ( 1  e.  RR  /\  T  e.  RR )  ->  ( 1  -  T
)  e.  RR )
97, 5, 8sylancr 644 . . . . . 6  |-  ( ph  ->  ( 1  -  T
)  e.  RR )
10 dvcvx.b . . . . . 6  |-  ( ph  ->  B  e.  RR )
119, 10remulcld 8863 . . . . 5  |-  ( ph  ->  ( ( 1  -  T )  x.  B
)  e.  RR )
126, 11readdcld 8862 . . . 4  |-  ( ph  ->  ( ( T  x.  A )  +  ( ( 1  -  T
)  x.  B ) )  e.  RR )
132, 12syl5eqel 2367 . . 3  |-  ( ph  ->  C  e.  RR )
14 ax-1cn 8795 . . . . . . . . 9  |-  1  e.  CC
1514a1i 10 . . . . . . . 8  |-  ( ph  ->  1  e.  CC )
165recnd 8861 . . . . . . . 8  |-  ( ph  ->  T  e.  CC )
171recnd 8861 . . . . . . . 8  |-  ( ph  ->  A  e.  CC )
1815, 16, 17subdird 9236 . . . . . . 7  |-  ( ph  ->  ( ( 1  -  T )  x.  A
)  =  ( ( 1  x.  A )  -  ( T  x.  A ) ) )
1917mulid2d 8853 . . . . . . . 8  |-  ( ph  ->  ( 1  x.  A
)  =  A )
2019oveq1d 5873 . . . . . . 7  |-  ( ph  ->  ( ( 1  x.  A )  -  ( T  x.  A )
)  =  ( A  -  ( T  x.  A ) ) )
2118, 20eqtrd 2315 . . . . . 6  |-  ( ph  ->  ( ( 1  -  T )  x.  A
)  =  ( A  -  ( T  x.  A ) ) )
22 dvcvx.l . . . . . . 7  |-  ( ph  ->  A  <  B )
23 eliooord 10710 . . . . . . . . . . 11  |-  ( T  e.  ( 0 (,) 1 )  ->  (
0  <  T  /\  T  <  1 ) )
243, 23syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( 0  <  T  /\  T  <  1
) )
2524simprd 449 . . . . . . . . 9  |-  ( ph  ->  T  <  1 )
26 posdif 9267 . . . . . . . . . 10  |-  ( ( T  e.  RR  /\  1  e.  RR )  ->  ( T  <  1  <->  0  <  ( 1  -  T ) ) )
275, 7, 26sylancl 643 . . . . . . . . 9  |-  ( ph  ->  ( T  <  1  <->  0  <  ( 1  -  T ) ) )
2825, 27mpbid 201 . . . . . . . 8  |-  ( ph  ->  0  <  ( 1  -  T ) )
29 ltmul2 9607 . . . . . . . 8  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  (
( 1  -  T
)  e.  RR  /\  0  <  ( 1  -  T ) ) )  ->  ( A  < 
B  <->  ( ( 1  -  T )  x.  A )  <  (
( 1  -  T
)  x.  B ) ) )
301, 10, 9, 28, 29syl112anc 1186 . . . . . . 7  |-  ( ph  ->  ( A  <  B  <->  ( ( 1  -  T
)  x.  A )  <  ( ( 1  -  T )  x.  B ) ) )
3122, 30mpbid 201 . . . . . 6  |-  ( ph  ->  ( ( 1  -  T )  x.  A
)  <  ( (
1  -  T )  x.  B ) )
3221, 31eqbrtrrd 4045 . . . . 5  |-  ( ph  ->  ( A  -  ( T  x.  A )
)  <  ( (
1  -  T )  x.  B ) )
331, 6, 11ltsubadd2d 9370 . . . . 5  |-  ( ph  ->  ( ( A  -  ( T  x.  A
) )  <  (
( 1  -  T
)  x.  B )  <-> 
A  <  ( ( T  x.  A )  +  ( ( 1  -  T )  x.  B ) ) ) )
3432, 33mpbid 201 . . . 4  |-  ( ph  ->  A  <  ( ( T  x.  A )  +  ( ( 1  -  T )  x.  B ) ) )
3534, 2syl6breqr 4063 . . 3  |-  ( ph  ->  A  <  C )
361leidd 9339 . . . . 5  |-  ( ph  ->  A  <_  A )
3710recnd 8861 . . . . . . . . . . 11  |-  ( ph  ->  B  e.  CC )
3815, 16, 37subdird 9236 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1  -  T )  x.  B
)  =  ( ( 1  x.  B )  -  ( T  x.  B ) ) )
3937mulid2d 8853 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  x.  B
)  =  B )
4039oveq1d 5873 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1  x.  B )  -  ( T  x.  B )
)  =  ( B  -  ( T  x.  B ) ) )
4138, 40eqtrd 2315 . . . . . . . . 9  |-  ( ph  ->  ( ( 1  -  T )  x.  B
)  =  ( B  -  ( T  x.  B ) ) )
425, 10remulcld 8863 . . . . . . . . . 10  |-  ( ph  ->  ( T  x.  B
)  e.  RR )
4324simpld 445 . . . . . . . . . . . 12  |-  ( ph  ->  0  <  T )
44 ltmul2 9607 . . . . . . . . . . . 12  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  ( T  e.  RR  /\  0  <  T ) )  -> 
( A  <  B  <->  ( T  x.  A )  <  ( T  x.  B ) ) )
451, 10, 5, 43, 44syl112anc 1186 . . . . . . . . . . 11  |-  ( ph  ->  ( A  <  B  <->  ( T  x.  A )  <  ( T  x.  B ) ) )
4622, 45mpbid 201 . . . . . . . . . 10  |-  ( ph  ->  ( T  x.  A
)  <  ( T  x.  B ) )
476, 42, 10, 46ltsub2dd 9385 . . . . . . . . 9  |-  ( ph  ->  ( B  -  ( T  x.  B )
)  <  ( B  -  ( T  x.  A ) ) )
4841, 47eqbrtrd 4043 . . . . . . . 8  |-  ( ph  ->  ( ( 1  -  T )  x.  B
)  <  ( B  -  ( T  x.  A ) ) )
49 ltaddsub2 9249 . . . . . . . . 9  |-  ( ( ( T  x.  A
)  e.  RR  /\  ( ( 1  -  T )  x.  B
)  e.  RR  /\  B  e.  RR )  ->  ( ( ( T  x.  A )  +  ( ( 1  -  T )  x.  B
) )  <  B  <->  ( ( 1  -  T
)  x.  B )  <  ( B  -  ( T  x.  A
) ) ) )
506, 11, 10, 49syl3anc 1182 . . . . . . . 8  |-  ( ph  ->  ( ( ( T  x.  A )  +  ( ( 1  -  T )  x.  B
) )  <  B  <->  ( ( 1  -  T
)  x.  B )  <  ( B  -  ( T  x.  A
) ) ) )
5148, 50mpbird 223 . . . . . . 7  |-  ( ph  ->  ( ( T  x.  A )  +  ( ( 1  -  T
)  x.  B ) )  <  B )
522, 51syl5eqbr 4056 . . . . . 6  |-  ( ph  ->  C  <  B )
5313, 10, 52ltled 8967 . . . . 5  |-  ( ph  ->  C  <_  B )
54 iccss 10718 . . . . 5  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( A  <_  A  /\  C  <_  B
) )  ->  ( A [,] C )  C_  ( A [,] B ) )
551, 10, 36, 53, 54syl22anc 1183 . . . 4  |-  ( ph  ->  ( A [,] C
)  C_  ( A [,] B ) )
56 dvcvx.f . . . 4  |-  ( ph  ->  F  e.  ( ( A [,] B )
-cn-> RR ) )
57 rescncf 18401 . . . 4  |-  ( ( A [,] C ) 
C_  ( A [,] B )  ->  ( F  e.  ( ( A [,] B ) -cn-> RR )  ->  ( F  |`  ( A [,] C
) )  e.  ( ( A [,] C
) -cn-> RR ) ) )
5855, 56, 57sylc 56 . . 3  |-  ( ph  ->  ( F  |`  ( A [,] C ) )  e.  ( ( A [,] C ) -cn-> RR ) )
59 ax-resscn 8794 . . . . . . . 8  |-  RR  C_  CC
6059a1i 10 . . . . . . 7  |-  ( ph  ->  RR  C_  CC )
61 cncff 18397 . . . . . . . . 9  |-  ( F  e.  ( ( A [,] B ) -cn-> RR )  ->  F :
( A [,] B
) --> RR )
6256, 61syl 15 . . . . . . . 8  |-  ( ph  ->  F : ( A [,] B ) --> RR )
63 fss 5397 . . . . . . . 8  |-  ( ( F : ( A [,] B ) --> RR 
/\  RR  C_  CC )  ->  F : ( A [,] B ) --> CC )
6462, 59, 63sylancl 643 . . . . . . 7  |-  ( ph  ->  F : ( A [,] B ) --> CC )
65 iccssre 10731 . . . . . . . 8  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A [,] B
)  C_  RR )
661, 10, 65syl2anc 642 . . . . . . 7  |-  ( ph  ->  ( A [,] B
)  C_  RR )
67 iccssre 10731 . . . . . . . 8  |-  ( ( A  e.  RR  /\  C  e.  RR )  ->  ( A [,] C
)  C_  RR )
681, 13, 67syl2anc 642 . . . . . . 7  |-  ( ph  ->  ( A [,] C
)  C_  RR )
69 eqid 2283 . . . . . . . 8  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
7069tgioo2 18309 . . . . . . . 8  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
7169, 70dvres 19261 . . . . . . 7  |-  ( ( ( RR  C_  CC  /\  F : ( A [,] B ) --> CC )  /\  ( ( A [,] B ) 
C_  RR  /\  ( A [,] C )  C_  RR ) )  ->  ( RR  _D  ( F  |`  ( A [,] C ) ) )  =  ( ( RR  _D  F
)  |`  ( ( int `  ( topGen `  ran  (,) )
) `  ( A [,] C ) ) ) )
7260, 64, 66, 68, 71syl22anc 1183 . . . . . 6  |-  ( ph  ->  ( RR  _D  ( F  |`  ( A [,] C ) ) )  =  ( ( RR 
_D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] C ) ) ) )
73 iccntr 18326 . . . . . . . 8  |-  ( ( A  e.  RR  /\  C  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] C ) )  =  ( A (,) C
) )
741, 13, 73syl2anc 642 . . . . . . 7  |-  ( ph  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] C ) )  =  ( A (,) C
) )
7574reseq2d 4955 . . . . . 6  |-  ( ph  ->  ( ( RR  _D  F )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( A [,] C ) ) )  =  ( ( RR 
_D  F )  |`  ( A (,) C ) ) )
7672, 75eqtrd 2315 . . . . 5  |-  ( ph  ->  ( RR  _D  ( F  |`  ( A [,] C ) ) )  =  ( ( RR 
_D  F )  |`  ( A (,) C ) ) )
7776dmeqd 4881 . . . 4  |-  ( ph  ->  dom  ( RR  _D  ( F  |`  ( A [,] C ) ) )  =  dom  (
( RR  _D  F
)  |`  ( A (,) C ) ) )
78 dmres 4976 . . . . 5  |-  dom  (
( RR  _D  F
)  |`  ( A (,) C ) )  =  ( ( A (,) C )  i^i  dom  ( RR  _D  F
) )
7910rexrd 8881 . . . . . . . 8  |-  ( ph  ->  B  e.  RR* )
80 iooss2 10692 . . . . . . . 8  |-  ( ( B  e.  RR*  /\  C  <_  B )  ->  ( A (,) C )  C_  ( A (,) B ) )
8179, 53, 80syl2anc 642 . . . . . . 7  |-  ( ph  ->  ( A (,) C
)  C_  ( A (,) B ) )
82 dvcvx.d . . . . . . . 8  |-  ( ph  ->  ( RR  _D  F
)  Isom  <  ,  <  ( ( A (,) B
) ,  W ) )
83 isof1o 5822 . . . . . . . 8  |-  ( ( RR  _D  F ) 
Isom  <  ,  <  (
( A (,) B
) ,  W )  ->  ( RR  _D  F ) : ( A (,) B ) -1-1-onto-> W )
84 f1odm 5476 . . . . . . . 8  |-  ( ( RR  _D  F ) : ( A (,) B ) -1-1-onto-> W  ->  dom  ( RR 
_D  F )  =  ( A (,) B
) )
8582, 83, 843syl 18 . . . . . . 7  |-  ( ph  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
8681, 85sseqtr4d 3215 . . . . . 6  |-  ( ph  ->  ( A (,) C
)  C_  dom  ( RR 
_D  F ) )
87 df-ss 3166 . . . . . 6  |-  ( ( A (,) C ) 
C_  dom  ( RR  _D  F )  <->  ( ( A (,) C )  i^i 
dom  ( RR  _D  F ) )  =  ( A (,) C
) )
8886, 87sylib 188 . . . . 5  |-  ( ph  ->  ( ( A (,) C )  i^i  dom  ( RR  _D  F
) )  =  ( A (,) C ) )
8978, 88syl5eq 2327 . . . 4  |-  ( ph  ->  dom  ( ( RR 
_D  F )  |`  ( A (,) C ) )  =  ( A (,) C ) )
9077, 89eqtrd 2315 . . 3  |-  ( ph  ->  dom  ( RR  _D  ( F  |`  ( A [,] C ) ) )  =  ( A (,) C ) )
911, 13, 35, 58, 90mvth 19339 . 2  |-  ( ph  ->  E. x  e.  ( A (,) C ) ( ( RR  _D  ( F  |`  ( A [,] C ) ) ) `  x )  =  ( ( ( ( F  |`  ( A [,] C ) ) `
 C )  -  ( ( F  |`  ( A [,] C ) ) `  A ) )  /  ( C  -  A ) ) )
921, 13, 35ltled 8967 . . . . 5  |-  ( ph  ->  A  <_  C )
9310leidd 9339 . . . . 5  |-  ( ph  ->  B  <_  B )
94 iccss 10718 . . . . 5  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( A  <_  C  /\  B  <_  B
) )  ->  ( C [,] B )  C_  ( A [,] B ) )
951, 10, 92, 93, 94syl22anc 1183 . . . 4  |-  ( ph  ->  ( C [,] B
)  C_  ( A [,] B ) )
96 rescncf 18401 . . . 4  |-  ( ( C [,] B ) 
C_  ( A [,] B )  ->  ( F  e.  ( ( A [,] B ) -cn-> RR )  ->  ( F  |`  ( C [,] B
) )  e.  ( ( C [,] B
) -cn-> RR ) ) )
9795, 56, 96sylc 56 . . 3  |-  ( ph  ->  ( F  |`  ( C [,] B ) )  e.  ( ( C [,] B ) -cn-> RR ) )
98 iccssre 10731 . . . . . . . 8  |-  ( ( C  e.  RR  /\  B  e.  RR )  ->  ( C [,] B
)  C_  RR )
9913, 10, 98syl2anc 642 . . . . . . 7  |-  ( ph  ->  ( C [,] B
)  C_  RR )
10069, 70dvres 19261 . . . . . . 7  |-  ( ( ( RR  C_  CC  /\  F : ( A [,] B ) --> CC )  /\  ( ( A [,] B ) 
C_  RR  /\  ( C [,] B )  C_  RR ) )  ->  ( RR  _D  ( F  |`  ( C [,] B ) ) )  =  ( ( RR  _D  F
)  |`  ( ( int `  ( topGen `  ran  (,) )
) `  ( C [,] B ) ) ) )
10160, 64, 66, 99, 100syl22anc 1183 . . . . . 6  |-  ( ph  ->  ( RR  _D  ( F  |`  ( C [,] B ) ) )  =  ( ( RR 
_D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( C [,] B ) ) ) )
102 iccntr 18326 . . . . . . . 8  |-  ( ( C  e.  RR  /\  B  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( C [,] B ) )  =  ( C (,) B
) )
10313, 10, 102syl2anc 642 . . . . . . 7  |-  ( ph  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( C [,] B ) )  =  ( C (,) B
) )
104103reseq2d 4955 . . . . . 6  |-  ( ph  ->  ( ( RR  _D  F )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( C [,] B ) ) )  =  ( ( RR 
_D  F )  |`  ( C (,) B ) ) )
105101, 104eqtrd 2315 . . . . 5  |-  ( ph  ->  ( RR  _D  ( F  |`  ( C [,] B ) ) )  =  ( ( RR 
_D  F )  |`  ( C (,) B ) ) )
106105dmeqd 4881 . . . 4  |-  ( ph  ->  dom  ( RR  _D  ( F  |`  ( C [,] B ) ) )  =  dom  (
( RR  _D  F
)  |`  ( C (,) B ) ) )
107 dmres 4976 . . . . 5  |-  dom  (
( RR  _D  F
)  |`  ( C (,) B ) )  =  ( ( C (,) B )  i^i  dom  ( RR  _D  F
) )
1081rexrd 8881 . . . . . . . 8  |-  ( ph  ->  A  e.  RR* )
109 iooss1 10691 . . . . . . . 8  |-  ( ( A  e.  RR*  /\  A  <_  C )  ->  ( C (,) B )  C_  ( A (,) B ) )
110108, 92, 109syl2anc 642 . . . . . . 7  |-  ( ph  ->  ( C (,) B
)  C_  ( A (,) B ) )
111110, 85sseqtr4d 3215 . . . . . 6  |-  ( ph  ->  ( C (,) B
)  C_  dom  ( RR 
_D  F ) )
112 df-ss 3166 . . . . . 6  |-  ( ( C (,) B ) 
C_  dom  ( RR  _D  F )  <->  ( ( C (,) B )  i^i 
dom  ( RR  _D  F ) )  =  ( C (,) B
) )
113111, 112sylib 188 . . . . 5  |-  ( ph  ->  ( ( C (,) B )  i^i  dom  ( RR  _D  F
) )  =  ( C (,) B ) )
114107, 113syl5eq 2327 . . . 4  |-  ( ph  ->  dom  ( ( RR 
_D  F )  |`  ( C (,) B ) )  =  ( C (,) B ) )
115106, 114eqtrd 2315 . . 3  |-  ( ph  ->  dom  ( RR  _D  ( F  |`  ( C [,] B ) ) )  =  ( C (,) B ) )
11613, 10, 52, 97, 115mvth 19339 . 2  |-  ( ph  ->  E. y  e.  ( C (,) B ) ( ( RR  _D  ( F  |`  ( C [,] B ) ) ) `  y )  =  ( ( ( ( F  |`  ( C [,] B ) ) `
 B )  -  ( ( F  |`  ( C [,] B ) ) `  C ) )  /  ( B  -  C ) ) )
117 reeanv 2707 . . 3  |-  ( E. x  e.  ( A (,) C ) E. y  e.  ( C (,) B ) ( ( ( RR  _D  ( F  |`  ( A [,] C ) ) ) `  x )  =  ( ( ( ( F  |`  ( A [,] C ) ) `
 C )  -  ( ( F  |`  ( A [,] C ) ) `  A ) )  /  ( C  -  A ) )  /\  ( ( RR 
_D  ( F  |`  ( C [,] B ) ) ) `  y
)  =  ( ( ( ( F  |`  ( C [,] B ) ) `  B )  -  ( ( F  |`  ( C [,] B
) ) `  C
) )  /  ( B  -  C )
) )  <->  ( E. x  e.  ( A (,) C ) ( ( RR  _D  ( F  |`  ( A [,] C
) ) ) `  x )  =  ( ( ( ( F  |`  ( A [,] C
) ) `  C
)  -  ( ( F  |`  ( A [,] C ) ) `  A ) )  / 
( C  -  A
) )  /\  E. y  e.  ( C (,) B ) ( ( RR  _D  ( F  |`  ( C [,] B
) ) ) `  y )  =  ( ( ( ( F  |`  ( C [,] B
) ) `  B
)  -  ( ( F  |`  ( C [,] B ) ) `  C ) )  / 
( B  -  C
) ) ) )
11876fveq1d 5527 . . . . . . . 8  |-  ( ph  ->  ( ( RR  _D  ( F  |`  ( A [,] C ) ) ) `  x )  =  ( ( ( RR  _D  F )  |`  ( A (,) C
) ) `  x
) )
119 fvres 5542 . . . . . . . . 9  |-  ( x  e.  ( A (,) C )  ->  (
( ( RR  _D  F )  |`  ( A (,) C ) ) `
 x )  =  ( ( RR  _D  F ) `  x
) )
120119adantr 451 . . . . . . . 8  |-  ( ( x  e.  ( A (,) C )  /\  y  e.  ( C (,) B ) )  -> 
( ( ( RR 
_D  F )  |`  ( A (,) C ) ) `  x )  =  ( ( RR 
_D  F ) `  x ) )
121118, 120sylan9eq 2335 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( A (,) C
)  /\  y  e.  ( C (,) B ) ) )  ->  (
( RR  _D  ( F  |`  ( A [,] C ) ) ) `
 x )  =  ( ( RR  _D  F ) `  x
) )
12213rexrd 8881 . . . . . . . . . . . 12  |-  ( ph  ->  C  e.  RR* )
123 ubicc2 10753 . . . . . . . . . . . 12  |-  ( ( A  e.  RR*  /\  C  e.  RR*  /\  A  <_  C )  ->  C  e.  ( A [,] C
) )
124108, 122, 92, 123syl3anc 1182 . . . . . . . . . . 11  |-  ( ph  ->  C  e.  ( A [,] C ) )
125 fvres 5542 . . . . . . . . . . 11  |-  ( C  e.  ( A [,] C )  ->  (
( F  |`  ( A [,] C ) ) `
 C )  =  ( F `  C
) )
126124, 125syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( ( F  |`  ( A [,] C ) ) `  C )  =  ( F `  C ) )
127 lbicc2 10752 . . . . . . . . . . . 12  |-  ( ( A  e.  RR*  /\  C  e.  RR*  /\  A  <_  C )  ->  A  e.  ( A [,] C
) )
128108, 122, 92, 127syl3anc 1182 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  ( A [,] C ) )
129 fvres 5542 . . . . . . . . . . 11  |-  ( A  e.  ( A [,] C )  ->  (
( F  |`  ( A [,] C ) ) `
 A )  =  ( F `  A
) )
130128, 129syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( ( F  |`  ( A [,] C ) ) `  A )  =  ( F `  A ) )
131126, 130oveq12d 5876 . . . . . . . . 9  |-  ( ph  ->  ( ( ( F  |`  ( A [,] C
) ) `  C
)  -  ( ( F  |`  ( A [,] C ) ) `  A ) )  =  ( ( F `  C )  -  ( F `  A )
) )
132131oveq1d 5873 . . . . . . . 8  |-  ( ph  ->  ( ( ( ( F  |`  ( A [,] C ) ) `  C )  -  (
( F  |`  ( A [,] C ) ) `
 A ) )  /  ( C  -  A ) )  =  ( ( ( F `
 C )  -  ( F `  A ) )  /  ( C  -  A ) ) )
133132adantr 451 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( A (,) C
)  /\  y  e.  ( C (,) B ) ) )  ->  (
( ( ( F  |`  ( A [,] C
) ) `  C
)  -  ( ( F  |`  ( A [,] C ) ) `  A ) )  / 
( C  -  A
) )  =  ( ( ( F `  C )  -  ( F `  A )
)  /  ( C  -  A ) ) )
134121, 133eqeq12d 2297 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( A (,) C
)  /\  y  e.  ( C (,) B ) ) )  ->  (
( ( RR  _D  ( F  |`  ( A [,] C ) ) ) `  x )  =  ( ( ( ( F  |`  ( A [,] C ) ) `
 C )  -  ( ( F  |`  ( A [,] C ) ) `  A ) )  /  ( C  -  A ) )  <-> 
( ( RR  _D  F ) `  x
)  =  ( ( ( F `  C
)  -  ( F `
 A ) )  /  ( C  -  A ) ) ) )
135105fveq1d 5527 . . . . . . . 8  |-  ( ph  ->  ( ( RR  _D  ( F  |`  ( C [,] B ) ) ) `  y )  =  ( ( ( RR  _D  F )  |`  ( C (,) B
) ) `  y
) )
136 fvres 5542 . . . . . . . . 9  |-  ( y  e.  ( C (,) B )  ->  (
( ( RR  _D  F )  |`  ( C (,) B ) ) `
 y )  =  ( ( RR  _D  F ) `  y
) )
137136adantl 452 . . . . . . . 8  |-  ( ( x  e.  ( A (,) C )  /\  y  e.  ( C (,) B ) )  -> 
( ( ( RR 
_D  F )  |`  ( C (,) B ) ) `  y )  =  ( ( RR 
_D  F ) `  y ) )
138135, 137sylan9eq 2335 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( A (,) C
)  /\  y  e.  ( C (,) B ) ) )  ->  (
( RR  _D  ( F  |`  ( C [,] B ) ) ) `
 y )  =  ( ( RR  _D  F ) `  y
) )
139 ubicc2 10753 . . . . . . . . . . . 12  |-  ( ( C  e.  RR*  /\  B  e.  RR*  /\  C  <_  B )  ->  B  e.  ( C [,] B
) )
140122, 79, 53, 139syl3anc 1182 . . . . . . . . . . 11  |-  ( ph  ->  B  e.  ( C [,] B ) )
141 fvres 5542 . . . . . . . . . . 11  |-  ( B  e.  ( C [,] B )  ->  (
( F  |`  ( C [,] B ) ) `
 B )  =  ( F `  B
) )
142140, 141syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( ( F  |`  ( C [,] B ) ) `  B )  =  ( F `  B ) )
143 lbicc2 10752 . . . . . . . . . . . 12  |-  ( ( C  e.  RR*  /\  B  e.  RR*  /\  C  <_  B )  ->  C  e.  ( C [,] B
) )
144122, 79, 53, 143syl3anc 1182 . . . . . . . . . . 11  |-  ( ph  ->  C  e.  ( C [,] B ) )
145 fvres 5542 . . . . . . . . . . 11  |-  ( C  e.  ( C [,] B )  ->  (
( F  |`  ( C [,] B ) ) `
 C )  =  ( F `  C
) )
146144, 145syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( ( F  |`  ( C [,] B ) ) `  C )  =  ( F `  C ) )
147142, 146oveq12d 5876 . . . . . . . . 9  |-  ( ph  ->  ( ( ( F  |`  ( C [,] B
) ) `  B
)  -  ( ( F  |`  ( C [,] B ) ) `  C ) )  =  ( ( F `  B )  -  ( F `  C )
) )
148147oveq1d 5873 . . . . . . . 8  |-  ( ph  ->  ( ( ( ( F  |`  ( C [,] B ) ) `  B )  -  (
( F  |`  ( C [,] B ) ) `
 C ) )  /  ( B  -  C ) )  =  ( ( ( F `
 B )  -  ( F `  C ) )  /  ( B  -  C ) ) )
149148adantr 451 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( A (,) C
)  /\  y  e.  ( C (,) B ) ) )  ->  (
( ( ( F  |`  ( C [,] B
) ) `  B
)  -  ( ( F  |`  ( C [,] B ) ) `  C ) )  / 
( B  -  C
) )  =  ( ( ( F `  B )  -  ( F `  C )
)  /  ( B  -  C ) ) )
150138, 149eqeq12d 2297 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( A (,) C
)  /\  y  e.  ( C (,) B ) ) )  ->  (
( ( RR  _D  ( F  |`  ( C [,] B ) ) ) `  y )  =  ( ( ( ( F  |`  ( C [,] B ) ) `
 B )  -  ( ( F  |`  ( C [,] B ) ) `  C ) )  /  ( B  -  C ) )  <-> 
( ( RR  _D  F ) `  y
)  =  ( ( ( F `  B
)  -  ( F `
 C ) )  /  ( B  -  C ) ) ) )
151134, 150anbi12d 691 . . . . 5  |-  ( (
ph  /\  ( x  e.  ( A (,) C
)  /\  y  e.  ( C (,) B ) ) )  ->  (
( ( ( RR 
_D  ( F  |`  ( A [,] C ) ) ) `  x
)  =  ( ( ( ( F  |`  ( A [,] C ) ) `  C )  -  ( ( F  |`  ( A [,] C
) ) `  A
) )  /  ( C  -  A )
)  /\  ( ( RR  _D  ( F  |`  ( C [,] B ) ) ) `  y
)  =  ( ( ( ( F  |`  ( C [,] B ) ) `  B )  -  ( ( F  |`  ( C [,] B
) ) `  C
) )  /  ( B  -  C )
) )  <->  ( (
( RR  _D  F
) `  x )  =  ( ( ( F `  C )  -  ( F `  A ) )  / 
( C  -  A
) )  /\  (
( RR  _D  F
) `  y )  =  ( ( ( F `  B )  -  ( F `  C ) )  / 
( B  -  C
) ) ) ) )
152 elioore 10686 . . . . . . . . . 10  |-  ( x  e.  ( A (,) C )  ->  x  e.  RR )
153152ad2antrl 708 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( A (,) C
)  /\  y  e.  ( C (,) B ) ) )  ->  x  e.  RR )
15413adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( A (,) C
)  /\  y  e.  ( C (,) B ) ) )  ->  C  e.  RR )
155 elioore 10686 . . . . . . . . . 10  |-  ( y  e.  ( C (,) B )  ->  y  e.  RR )
156155ad2antll 709 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( A (,) C
)  /\  y  e.  ( C (,) B ) ) )  ->  y  e.  RR )
157 eliooord 10710 . . . . . . . . . . 11  |-  ( x  e.  ( A (,) C )  ->  ( A  <  x  /\  x  <  C ) )
158157ad2antrl 708 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( A (,) C
)  /\  y  e.  ( C (,) B ) ) )  ->  ( A  <  x  /\  x  <  C ) )
159158simprd 449 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( A (,) C
)  /\  y  e.  ( C (,) B ) ) )  ->  x  <  C )
160 eliooord 10710 . . . . . . . . . . 11  |-  ( y  e.  ( C (,) B )  ->  ( C  <  y  /\  y  <  B ) )
161160ad2antll 709 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( A (,) C
)  /\  y  e.  ( C (,) B ) ) )  ->  ( C  <  y  /\  y  <  B ) )
162161simpld 445 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( A (,) C
)  /\  y  e.  ( C (,) B ) ) )  ->  C  <  y )
163153, 154, 156, 159, 162lttrd 8977 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( A (,) C
)  /\  y  e.  ( C (,) B ) ) )  ->  x  <  y )
16482adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( A (,) C
)  /\  y  e.  ( C (,) B ) ) )  ->  ( RR  _D  F )  Isom  <  ,  <  ( ( A (,) B ) ,  W ) )
16581sselda 3180 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( A (,) C ) )  ->  x  e.  ( A (,) B ) )
166165adantrr 697 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( A (,) C
)  /\  y  e.  ( C (,) B ) ) )  ->  x  e.  ( A (,) B
) )
167110sselda 3180 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( C (,) B ) )  ->  y  e.  ( A (,) B ) )
168167adantrl 696 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( A (,) C
)  /\  y  e.  ( C (,) B ) ) )  ->  y  e.  ( A (,) B
) )
169 isorel 5823 . . . . . . . . 9  |-  ( ( ( RR  _D  F
)  Isom  <  ,  <  ( ( A (,) B
) ,  W )  /\  ( x  e.  ( A (,) B
)  /\  y  e.  ( A (,) B ) ) )  ->  (
x  <  y  <->  ( ( RR  _D  F ) `  x )  <  (
( RR  _D  F
) `  y )
) )
170164, 166, 168, 169syl12anc 1180 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( A (,) C
)  /\  y  e.  ( C (,) B ) ) )  ->  (
x  <  y  <->  ( ( RR  _D  F ) `  x )  <  (
( RR  _D  F
) `  y )
) )
171163, 170mpbid 201 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( A (,) C
)  /\  y  e.  ( C (,) B ) ) )  ->  (
( RR  _D  F
) `  x )  <  ( ( RR  _D  F ) `  y
) )
172 breq12 4028 . . . . . . 7  |-  ( ( ( ( RR  _D  F ) `  x
)  =  ( ( ( F `  C
)  -  ( F `
 A ) )  /  ( C  -  A ) )  /\  ( ( RR  _D  F ) `  y
)  =  ( ( ( F `  B
)  -  ( F `
 C ) )  /  ( B  -  C ) ) )  ->  ( ( ( RR  _D  F ) `
 x )  < 
( ( RR  _D  F ) `  y
)  <->  ( ( ( F `  C )  -  ( F `  A ) )  / 
( C  -  A
) )  <  (
( ( F `  B )  -  ( F `  C )
)  /  ( B  -  C ) ) ) )
173171, 172syl5ibcom 211 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( A (,) C
)  /\  y  e.  ( C (,) B ) ) )  ->  (
( ( ( RR 
_D  F ) `  x )  =  ( ( ( F `  C )  -  ( F `  A )
)  /  ( C  -  A ) )  /\  ( ( RR 
_D  F ) `  y )  =  ( ( ( F `  B )  -  ( F `  C )
)  /  ( B  -  C ) ) )  ->  ( (
( F `  C
)  -  ( F `
 A ) )  /  ( C  -  A ) )  < 
( ( ( F `
 B )  -  ( F `  C ) )  /  ( B  -  C ) ) ) )
17455, 124sseldd 3181 . . . . . . . . . . . 12  |-  ( ph  ->  C  e.  ( A [,] B ) )
175 ffvelrn 5663 . . . . . . . . . . . 12  |-  ( ( F : ( A [,] B ) --> RR 
/\  C  e.  ( A [,] B ) )  ->  ( F `  C )  e.  RR )
17662, 174, 175syl2anc 642 . . . . . . . . . . 11  |-  ( ph  ->  ( F `  C
)  e.  RR )
17755, 128sseldd 3181 . . . . . . . . . . . 12  |-  ( ph  ->  A  e.  ( A [,] B ) )
178 ffvelrn 5663 . . . . . . . . . . . 12  |-  ( ( F : ( A [,] B ) --> RR 
/\  A  e.  ( A [,] B ) )  ->  ( F `  A )  e.  RR )
17962, 177, 178syl2anc 642 . . . . . . . . . . 11  |-  ( ph  ->  ( F `  A
)  e.  RR )
180176, 179resubcld 9211 . . . . . . . . . 10  |-  ( ph  ->  ( ( F `  C )  -  ( F `  A )
)  e.  RR )
18128gt0ne0d 9337 . . . . . . . . . 10  |-  ( ph  ->  ( 1  -  T
)  =/=  0 )
182180, 9, 181redivcld 9588 . . . . . . . . 9  |-  ( ph  ->  ( ( ( F `
 C )  -  ( F `  A ) )  /  ( 1  -  T ) )  e.  RR )
18395, 140sseldd 3181 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  ( A [,] B ) )
184 ffvelrn 5663 . . . . . . . . . . . 12  |-  ( ( F : ( A [,] B ) --> RR 
/\  B  e.  ( A [,] B ) )  ->  ( F `  B )  e.  RR )
18562, 183, 184syl2anc 642 . . . . . . . . . . 11  |-  ( ph  ->  ( F `  B
)  e.  RR )
186185, 176resubcld 9211 . . . . . . . . . 10  |-  ( ph  ->  ( ( F `  B )  -  ( F `  C )
)  e.  RR )
18743gt0ne0d 9337 . . . . . . . . . 10  |-  ( ph  ->  T  =/=  0 )
188186, 5, 187redivcld 9588 . . . . . . . . 9  |-  ( ph  ->  ( ( ( F `
 B )  -  ( F `  C ) )  /  T )  e.  RR )
18910, 1resubcld 9211 . . . . . . . . 9  |-  ( ph  ->  ( B  -  A
)  e.  RR )
1901, 10posdifd 9359 . . . . . . . . . 10  |-  ( ph  ->  ( A  <  B  <->  0  <  ( B  -  A ) ) )
19122, 190mpbid 201 . . . . . . . . 9  |-  ( ph  ->  0  <  ( B  -  A ) )
192 ltdiv1 9620 . . . . . . . . 9  |-  ( ( ( ( ( F `
 C )  -  ( F `  A ) )  /  ( 1  -  T ) )  e.  RR  /\  (
( ( F `  B )  -  ( F `  C )
)  /  T )  e.  RR  /\  (
( B  -  A
)  e.  RR  /\  0  <  ( B  -  A ) ) )  ->  ( ( ( ( F `  C
)  -  ( F `
 A ) )  /  ( 1  -  T ) )  < 
( ( ( F `
 B )  -  ( F `  C ) )  /  T )  <-> 
( ( ( ( F `  C )  -  ( F `  A ) )  / 
( 1  -  T
) )  /  ( B  -  A )
)  <  ( (
( ( F `  B )  -  ( F `  C )
)  /  T )  /  ( B  -  A ) ) ) )
193182, 188, 189, 191, 192syl112anc 1186 . . . . . . . 8  |-  ( ph  ->  ( ( ( ( F `  C )  -  ( F `  A ) )  / 
( 1  -  T
) )  <  (
( ( F `  B )  -  ( F `  C )
)  /  T )  <-> 
( ( ( ( F `  C )  -  ( F `  A ) )  / 
( 1  -  T
) )  /  ( B  -  A )
)  <  ( (
( ( F `  B )  -  ( F `  C )
)  /  T )  /  ( B  -  A ) ) ) )
194180recnd 8861 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( F `  C )  -  ( F `  A )
)  e.  CC )
195194, 16mulcomd 8856 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( F `
 C )  -  ( F `  A ) )  x.  T )  =  ( T  x.  ( ( F `  C )  -  ( F `  A )
) ) )
196176recnd 8861 . . . . . . . . . . . 12  |-  ( ph  ->  ( F `  C
)  e.  CC )
197179recnd 8861 . . . . . . . . . . . 12  |-  ( ph  ->  ( F `  A
)  e.  CC )
19816, 196, 197subdid 9235 . . . . . . . . . . 11  |-  ( ph  ->  ( T  x.  (
( F `  C
)  -  ( F `
 A ) ) )  =  ( ( T  x.  ( F `
 C ) )  -  ( T  x.  ( F `  A ) ) ) )
199195, 198eqtrd 2315 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( F `
 C )  -  ( F `  A ) )  x.  T )  =  ( ( T  x.  ( F `  C ) )  -  ( T  x.  ( F `  A )
) ) )
200186recnd 8861 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( F `  B )  -  ( F `  C )
)  e.  CC )
2019recnd 8861 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  -  T
)  e.  CC )
202200, 201mulcomd 8856 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( F `
 B )  -  ( F `  C ) )  x.  ( 1  -  T ) )  =  ( ( 1  -  T )  x.  ( ( F `  B )  -  ( F `  C )
) ) )
203185recnd 8861 . . . . . . . . . . . 12  |-  ( ph  ->  ( F `  B
)  e.  CC )
204201, 203, 196subdid 9235 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 1  -  T )  x.  (
( F `  B
)  -  ( F `
 C ) ) )  =  ( ( ( 1  -  T
)  x.  ( F `
 B ) )  -  ( ( 1  -  T )  x.  ( F `  C
) ) ) )
205202, 204eqtrd 2315 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( F `
 B )  -  ( F `  C ) )  x.  ( 1  -  T ) )  =  ( ( ( 1  -  T )  x.  ( F `  B ) )  -  ( ( 1  -  T )  x.  ( F `  C )
) ) )
206199, 205breq12d 4036 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( F `  C )  -  ( F `  A ) )  x.  T )  <  (
( ( F `  B )  -  ( F `  C )
)  x.  ( 1  -  T ) )  <-> 
( ( T  x.  ( F `  C ) )  -  ( T  x.  ( F `  A ) ) )  <  ( ( ( 1  -  T )  x.  ( F `  B ) )  -  ( ( 1  -  T )  x.  ( F `  C )
) ) ) )
2075, 43jca 518 . . . . . . . . . 10  |-  ( ph  ->  ( T  e.  RR  /\  0  <  T ) )
2089, 28jca 518 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1  -  T )  e.  RR  /\  0  <  ( 1  -  T ) ) )
209 lt2mul2div 9632 . . . . . . . . . 10  |-  ( ( ( ( ( F `
 C )  -  ( F `  A ) )  e.  RR  /\  ( T  e.  RR  /\  0  <  T ) )  /\  ( ( ( F `  B
)  -  ( F `
 C ) )  e.  RR  /\  (
( 1  -  T
)  e.  RR  /\  0  <  ( 1  -  T ) ) ) )  ->  ( (
( ( F `  C )  -  ( F `  A )
)  x.  T )  <  ( ( ( F `  B )  -  ( F `  C ) )  x.  ( 1  -  T
) )  <->  ( (
( F `  C
)  -  ( F `
 A ) )  /  ( 1  -  T ) )  < 
( ( ( F `
 B )  -  ( F `  C ) )  /  T ) ) )
210180, 207, 186, 208, 209syl22anc 1183 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( F `  C )  -  ( F `  A ) )  x.  T )  <  (
( ( F `  B )  -  ( F `  C )
)  x.  ( 1  -  T ) )  <-> 
( ( ( F `
 C )  -  ( F `  A ) )  /  ( 1  -  T ) )  <  ( ( ( F `  B )  -  ( F `  C ) )  /  T ) ) )
2115, 176remulcld 8863 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( T  x.  ( F `  C )
)  e.  RR )
212211recnd 8861 . . . . . . . . . . . . 13  |-  ( ph  ->  ( T  x.  ( F `  C )
)  e.  CC )
2139, 176remulcld 8863 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1  -  T )  x.  ( F `  C )
)  e.  RR )
214213recnd 8861 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 1  -  T )  x.  ( F `  C )
)  e.  CC )
2155, 179remulcld 8863 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( T  x.  ( F `  A )
)  e.  RR )
216215recnd 8861 . . . . . . . . . . . . 13  |-  ( ph  ->  ( T  x.  ( F `  A )
)  e.  CC )
217212, 214, 216addsubd 9178 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( T  x.  ( F `  C ) )  +  ( ( 1  -  T )  x.  ( F `  C )
) )  -  ( T  x.  ( F `  A ) ) )  =  ( ( ( T  x.  ( F `
 C ) )  -  ( T  x.  ( F `  A ) ) )  +  ( ( 1  -  T
)  x.  ( F `
 C ) ) ) )
218 pncan3 9059 . . . . . . . . . . . . . . . 16  |-  ( ( T  e.  CC  /\  1  e.  CC )  ->  ( T  +  ( 1  -  T ) )  =  1 )
21916, 14, 218sylancl 643 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( T  +  ( 1  -  T ) )  =  1 )
220219oveq1d 5873 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( T  +  ( 1  -  T
) )  x.  ( F `  C )
)  =  ( 1  x.  ( F `  C ) ) )
22116, 201, 196adddird 8860 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( T  +  ( 1  -  T
) )  x.  ( F `  C )
)  =  ( ( T  x.  ( F `
 C ) )  +  ( ( 1  -  T )  x.  ( F `  C
) ) ) )
222196mulid2d 8853 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1  x.  ( F `  C )
)  =  ( F `
 C ) )
223220, 221, 2223eqtr3d 2323 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( T  x.  ( F `  C ) )  +  ( ( 1  -  T )  x.  ( F `  C ) ) )  =  ( F `  C ) )
224223oveq1d 5873 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( T  x.  ( F `  C ) )  +  ( ( 1  -  T )  x.  ( F `  C )
) )  -  ( T  x.  ( F `  A ) ) )  =  ( ( F `
 C )  -  ( T  x.  ( F `  A )
) ) )
225217, 224eqtr3d 2317 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( T  x.  ( F `  C ) )  -  ( T  x.  ( F `  A )
) )  +  ( ( 1  -  T
)  x.  ( F `
 C ) ) )  =  ( ( F `  C )  -  ( T  x.  ( F `  A ) ) ) )
226225breq1d 4033 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( T  x.  ( F `
 C ) )  -  ( T  x.  ( F `  A ) ) )  +  ( ( 1  -  T
)  x.  ( F `
 C ) ) )  <  ( ( 1  -  T )  x.  ( F `  B ) )  <->  ( ( F `  C )  -  ( T  x.  ( F `  A ) ) )  <  (
( 1  -  T
)  x.  ( F `
 B ) ) ) )
227211, 215resubcld 9211 . . . . . . . . . . 11  |-  ( ph  ->  ( ( T  x.  ( F `  C ) )  -  ( T  x.  ( F `  A ) ) )  e.  RR )
2289, 185remulcld 8863 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 1  -  T )  x.  ( F `  B )
)  e.  RR )
229227, 213, 228ltaddsubd 9372 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( T  x.  ( F `
 C ) )  -  ( T  x.  ( F `  A ) ) )  +  ( ( 1  -  T
)  x.  ( F `
 C ) ) )  <  ( ( 1  -  T )  x.  ( F `  B ) )  <->  ( ( T  x.  ( F `  C ) )  -  ( T  x.  ( F `  A )
) )  <  (
( ( 1  -  T )  x.  ( F `  B )
)  -  ( ( 1  -  T )  x.  ( F `  C ) ) ) ) )
230176, 215, 228ltsubadd2d 9370 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( F `
 C )  -  ( T  x.  ( F `  A )
) )  <  (
( 1  -  T
)  x.  ( F `
 B ) )  <-> 
( F `  C
)  <  ( ( T  x.  ( F `  A ) )  +  ( ( 1  -  T )  x.  ( F `  B )
) ) ) )
231226, 229, 2303bitr3d 274 . . . . . . . . 9  |-  ( ph  ->  ( ( ( T  x.  ( F `  C ) )  -  ( T  x.  ( F `  A )
) )  <  (
( ( 1  -  T )  x.  ( F `  B )
)  -  ( ( 1  -  T )  x.  ( F `  C ) ) )  <-> 
( F `  C
)  <  ( ( T  x.  ( F `  A ) )  +  ( ( 1  -  T )  x.  ( F `  B )
) ) ) )
232206, 210, 2313bitr3d 274 . . . . . . . 8  |-  ( ph  ->  ( ( ( ( F `  C )  -  ( F `  A ) )  / 
( 1  -  T
) )  <  (
( ( F `  B )  -  ( F `  C )
)  /  T )  <-> 
( F `  C
)  <  ( ( T  x.  ( F `  A ) )  +  ( ( 1  -  T )  x.  ( F `  B )
) ) ) )
233189recnd 8861 . . . . . . . . . . 11  |-  ( ph  ->  ( B  -  A
)  e.  CC )
234191gt0ne0d 9337 . . . . . . . . . . 11  |-  ( ph  ->  ( B  -  A
)  =/=  0 )
235194, 201, 233, 181, 234divdiv1d 9567 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( F `  C )  -  ( F `  A ) )  / 
( 1  -  T
) )  /  ( B  -  A )
)  =  ( ( ( F `  C
)  -  ( F `
 A ) )  /  ( ( 1  -  T )  x.  ( B  -  A
) ) ) )
23621oveq2d 5874 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( 1  -  T )  x.  B )  -  (
( 1  -  T
)  x.  A ) )  =  ( ( ( 1  -  T
)  x.  B )  -  ( A  -  ( T  x.  A
) ) ) )
23711recnd 8861 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1  -  T )  x.  B
)  e.  CC )
2386recnd 8861 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( T  x.  A
)  e.  CC )
239237, 17, 238subsub3d 9187 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( 1  -  T )  x.  B )  -  ( A  -  ( T  x.  A ) ) )  =  ( ( ( ( 1  -  T
)  x.  B )  +  ( T  x.  A ) )  -  A ) )
240236, 239eqtrd 2315 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( 1  -  T )  x.  B )  -  (
( 1  -  T
)  x.  A ) )  =  ( ( ( ( 1  -  T )  x.  B
)  +  ( T  x.  A ) )  -  A ) )
241201, 37, 17subdid 9235 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1  -  T )  x.  ( B  -  A )
)  =  ( ( ( 1  -  T
)  x.  B )  -  ( ( 1  -  T )  x.  A ) ) )
242238, 237addcomd 9014 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( T  x.  A )  +  ( ( 1  -  T
)  x.  B ) )  =  ( ( ( 1  -  T
)  x.  B )  +  ( T  x.  A ) ) )
2432, 242syl5eq 2327 . . . . . . . . . . . . 13  |-  ( ph  ->  C  =  ( ( ( 1  -  T
)  x.  B )  +  ( T  x.  A ) ) )
244243oveq1d 5873 . . . . . . . . . . . 12  |-  ( ph  ->  ( C  -  A
)  =  ( ( ( ( 1  -  T )  x.  B
)  +  ( T  x.  A ) )  -  A ) )
245240, 241, 2443eqtr4d 2325 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 1  -  T )  x.  ( B  -  A )
)  =  ( C  -  A ) )
246245oveq2d 5874 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( F `
 C )  -  ( F `  A ) )  /  ( ( 1  -  T )  x.  ( B  -  A ) ) )  =  ( ( ( F `  C )  -  ( F `  A ) )  / 
( C  -  A
) ) )
247235, 246eqtrd 2315 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( F `  C )  -  ( F `  A ) )  / 
( 1  -  T
) )  /  ( B  -  A )
)  =  ( ( ( F `  C
)  -  ( F `
 A ) )  /  ( C  -  A ) ) )
248200, 16, 233, 187, 234divdiv1d 9567 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( F `  B )  -  ( F `  C ) )  /  T )  /  ( B  -  A )
)  =  ( ( ( F `  B
)  -  ( F `
 C ) )  /  ( T  x.  ( B  -  A
) ) ) )
24937, 237, 238subsub4d 9188 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( B  -  ( ( 1  -  T )  x.  B
) )  -  ( T  x.  A )
)  =  ( B  -  ( ( ( 1  -  T )  x.  B )  +  ( T  x.  A
) ) ) )
25041oveq2d 5874 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( B  -  (
( 1  -  T
)  x.  B ) )  =  ( B  -  ( B  -  ( T  x.  B
) ) ) )
25142recnd 8861 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( T  x.  B
)  e.  CC )
25237, 251nncand 9162 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( B  -  ( B  -  ( T  x.  B ) ) )  =  ( T  x.  B ) )
253250, 252eqtrd 2315 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( B  -  (
( 1  -  T
)  x.  B ) )  =  ( T  x.  B ) )
254253oveq1d 5873 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( B  -  ( ( 1  -  T )  x.  B
) )  -  ( T  x.  A )
)  =  ( ( T  x.  B )  -  ( T  x.  A ) ) )
255249, 254eqtr3d 2317 . . . . . . . . . . . 12  |-  ( ph  ->  ( B  -  (
( ( 1  -  T )  x.  B
)  +  ( T  x.  A ) ) )  =  ( ( T  x.  B )  -  ( T  x.  A ) ) )
256243oveq2d 5874 . . . . . . . . . . . 12  |-  ( ph  ->  ( B  -  C
)  =  ( B  -  ( ( ( 1  -  T )  x.  B )  +  ( T  x.  A
) ) ) )
25716, 37, 17subdid 9235 . . . . . . . . . . . 12  |-  ( ph  ->  ( T  x.  ( B  -  A )
)  =  ( ( T  x.  B )  -  ( T  x.  A ) ) )
258255, 256, 2573eqtr4d 2325 . . . . . . . . . . 11  |-  ( ph  ->  ( B  -  C
)  =  ( T  x.  ( B  -  A ) ) )
259258oveq2d 5874 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( F `
 B )  -  ( F `  C ) )  /  ( B  -  C ) )  =  ( ( ( F `  B )  -  ( F `  C ) )  / 
( T  x.  ( B  -  A )
) ) )
260248, 259eqtr4d 2318 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( F `  B )  -  ( F `  C ) )  /  T )  /  ( B  -  A )
)  =  ( ( ( F `  B
)  -  ( F `
 C ) )  /  ( B  -  C ) ) )
261247, 260breq12d 4036 . . . . . . . 8  |-  ( ph  ->  ( ( ( ( ( F `  C
)  -  ( F `
 A ) )  /  ( 1  -  T ) )  / 
( B  -  A
) )  <  (
( ( ( F `
 B )  -  ( F `  C ) )  /  T )  /  ( B  -  A ) )  <->  ( (
( F `  C
)  -  ( F `
 A ) )  /  ( C  -  A ) )  < 
( ( ( F `
 B )  -  ( F `  C ) )  /  ( B  -  C ) ) ) )
262193, 232, 2613bitr3rd 275 . . . . . . 7  |-  ( ph  ->  ( ( ( ( F `  C )  -  ( F `  A ) )  / 
( C  -  A
) )  <  (
( ( F `  B )  -  ( F `  C )
)  /  ( B  -  C ) )  <-> 
( F `  C
)  <  ( ( T  x.  ( F `  A ) )  +  ( ( 1  -  T )  x.  ( F `  B )
) ) ) )
263262adantr 451 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( A (,) C
)  /\  y  e.  ( C (,) B ) ) )  ->  (
( ( ( F `
 C )  -  ( F `  A ) )  /  ( C  -  A ) )  <  ( ( ( F `  B )  -  ( F `  C ) )  / 
( B  -  C
) )  <->  ( F `  C )  <  (
( T  x.  ( F `  A )
)  +  ( ( 1  -  T )  x.  ( F `  B ) ) ) ) )
264173, 263sylibd 205 . . . . 5  |-  ( (
ph  /\  ( x  e.  ( A (,) C
)  /\  y  e.  ( C (,) B ) ) )  ->  (
( ( ( RR 
_D  F ) `  x )  =  ( ( ( F `  C )  -  ( F `  A )
)  /  ( C  -  A ) )  /\  ( ( RR 
_D  F ) `  y )  =  ( ( ( F `  B )  -  ( F `  C )
)  /  ( B  -  C ) ) )  ->  ( F `  C )  <  (
( T  x.  ( F `  A )
)  +  ( ( 1  -  T )  x.  ( F `  B ) ) ) ) )
265151, 264sylbid 206 . . . 4  |-  ( (
ph  /\  ( x  e.  ( A (,) C
)  /\  y  e.  ( C (,) B ) ) )  ->  (
( ( ( RR 
_D  ( F  |`  ( A [,] C ) ) ) `  x
)  =  ( ( ( ( F  |`  ( A [,] C ) ) `  C )  -  ( ( F  |`  ( A [,] C
) ) `  A
) )  /  ( C  -  A )
)  /\  ( ( RR  _D  ( F  |`  ( C [,] B ) ) ) `  y
)  =  ( ( ( ( F  |`  ( C [,] B ) ) `  B )  -  ( ( F  |`  ( C [,] B
) ) `  C
) )  /  ( B  -  C )
) )  ->  ( F `  C )  <  ( ( T  x.  ( F `  A ) )  +  ( ( 1  -  T )  x.  ( F `  B ) ) ) ) )
266265rexlimdvva 2674 . . 3  |-  ( ph  ->  ( E. x  e.  ( A (,) C
) E. y  e.  ( C (,) B
) ( ( ( RR  _D  ( F  |`  ( A [,] C
) ) ) `  x )  =  ( ( ( ( F  |`  ( A [,] C
) ) `  C
)  -  ( ( F  |`  ( A [,] C ) ) `  A ) )  / 
( C  -  A
) )  /\  (
( RR  _D  ( F  |`  ( C [,] B ) ) ) `
 y )  =  ( ( ( ( F  |`  ( C [,] B ) ) `  B )  -  (
( F  |`  ( C [,] B ) ) `
 C ) )  /  ( B  -  C ) ) )  ->  ( F `  C )  <  (
( T  x.  ( F `  A )
)  +  ( ( 1  -  T )  x.  ( F `  B ) ) ) ) )
267117, 266syl5bir 209 . 2  |-  ( ph  ->  ( ( E. x  e.  ( A (,) C
) ( ( RR 
_D  ( F  |`  ( A [,] C ) ) ) `  x
)  =  ( ( ( ( F  |`  ( A [,] C ) ) `  C )  -  ( ( F  |`  ( A [,] C
) ) `  A
) )  /  ( C  -  A )
)  /\  E. y  e.  ( C (,) B
) ( ( RR 
_D  ( F  |`  ( C [,] B ) ) ) `  y
)  =  ( ( ( ( F  |`  ( C [,] B ) ) `  B )  -  ( ( F  |`  ( C [,] B
) ) `  C
) )  /  ( B  -  C )
) )  ->  ( F `  C )  <  ( ( T  x.  ( F `  A ) )  +  ( ( 1  -  T )  x.  ( F `  B ) ) ) ) )
26891, 116, 267mp2and 660 1  |-  ( ph  ->  ( F `  C
)  <  ( ( T  x.  ( F `  A ) )  +  ( ( 1  -  T )  x.  ( F `  B )
) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1623    e. wcel 1684   E.wrex 2544    i^i cin 3151    C_ wss 3152   class class class wbr 4023   dom cdm 4689   ran crn 4690    |` cres 4691   -->wf 5251   -1-1-onto->wf1o 5254   ` cfv 5255    Isom wiso 5256  (class class class)co 5858   CCcc 8735   RRcr 8736   0cc0 8737   1c1 8738    + caddc 8740    x. cmul 8742   RR*cxr 8866    < clt 8867    <_ cle 8868    - cmin 9037    / cdiv 9423   (,)cioo 10656   [,]cicc 10659   TopOpenctopn 13326   topGenctg 13342  ℂfldccnfld 16377   intcnt 16754   -cn->ccncf 18380    _D cdv 19213
This theorem is referenced by:  efcvx  19825  logccv  20010
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-inf2 7342  ax-cnex 8793  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-mulcom 8801  ax-addass 8802  ax-mulass 8803  ax-distr 8804  ax-i2m1 8805  ax-1ne0 8806  ax-1rid 8807  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812  ax-pre-ltadd 8813  ax-pre-mulgt0 8814  ax-pre-sup 8815  ax-addf 8816  ax-mulf 8817
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-iin 3908  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-se 4353  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-isom 5264  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-of 6078  df-1st 6122  df-2nd 6123  df-riota 6304  df-recs 6388  df-rdg 6423  df-1o 6479  df-2o 6480  df-oadd 6483  df-er 6660  df-map 6774  df-pm 6775  df-ixp 6818  df-en 6864  df-dom 6865  df-sdom 6866  df-fin 6867  df-fi 7165  df-sup 7194  df-oi 7225  df-card 7572  df-cda 7794  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873  df-sub 9039  df-neg 9040  df-div 9424  df-nn 9747  df-2 9804  df-3 9805  df-4 9806  df-5 9807  df-6 9808  df-7 9809  df-8 9810  df-9 9811  df-10 9812  df-n0 9966  df-z 10025  df-dec 10125  df-uz 10231  df-q 10317  df-rp 10355  df-xneg 10452  df-xadd 10453  df-xmul 10454  df-ioo 10660  df-ico 10662  df-icc 10663  df-fz 10783  df-fzo 10871  df-seq 11047  df-exp 11105  df-hash 11338  df-cj 11584  df-re 11585  df-im 11586  df-sqr 11720  df-abs 11721  df-struct 13150  df-ndx 13151  df-slot 13152  df-base 13153  df-sets 13154  df-ress 13155  df-plusg 13221  df-mulr 13222  df-starv 13223  df-sca 13224  df-vsca 13225  df-tset 13227  df-ple 13228  df-ds 13230  df-hom 13232  df-cco 13233  df-rest 13327  df-topn 13328  df-topgen 13344  df-pt 13345  df-prds 13348  df-xrs 13403  df-0g 13404  df-gsum 13405  df-qtop 13410  df-imas 13411  df-xps 13413  df-mre 13488  df-mrc 13489  df-acs 13491  df-mnd 14367  df-submnd 14416  df-mulg 14492  df-cntz 14793  df-cmn 15091  df-xmet 16373  df-met 16374  df-bl 16375  df-mopn 16376  df-cnfld 16378  df-top 16636  df-bases 16638  df-topon 16639  df-topsp 16640  df-cld 16756  df-ntr 16757  df-cls 16758  df-nei 16835  df-lp 16868  df-perf 16869  df-cn 16957  df-cnp 16958  df-haus 17043  df-cmp 17114  df-tx 17257  df-hmeo 17446  df-fbas 17520  df-fg 17521  df-fil 17541  df-fm 17633  df-flim 17634  df-flf 17635  df-xms 17885  df-ms 17886  df-tms 17887  df-cncf 18382  df-limc 19216  df-dv 19217
  Copyright terms: Public domain W3C validator