Metamath Proof Explorer

Theorem dvcvx

Description: A real function with strictly increasing derivative is strictly convex. (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Hypotheses 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 dvcvx 
|- ( ph -> ( F ` C ) < ( ( T x. ( F ` A ) ) + ( ( 1 - T ) x. ( F ` B ) ) ) )

Proof

Step Hyp Ref Expression
1 dvcvx.a 
 |-  ( ph -> A e. RR )
2 dvcvx.b 
 |-  ( ph -> B e. RR )
3 dvcvx.l 
 |-  ( ph -> A < B )
4 dvcvx.f 
 |-  ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )
5 dvcvx.d 
 |-  ( ph -> ( RR _D F ) Isom < , < ( ( A (,) B ) , W ) )
6 dvcvx.t 
 |-  ( ph -> T e. ( 0 (,) 1 ) )
7 dvcvx.c 
 |-  C = ( ( T x. A ) + ( ( 1 - T ) x. B ) )
8 elioore 
 |-  ( T e. ( 0 (,) 1 ) -> T e. RR )
9 6 8 syl 
 |-  ( ph -> T e. RR )
10 9 1 remulcld 
 |-  ( ph -> ( T x. A ) e. RR )
11 1re 
 |-  1 e. RR
12 resubcl 
 |-  ( ( 1 e. RR /\ T e. RR ) -> ( 1 - T ) e. RR )
13 11 9 12 sylancr 
 |-  ( ph -> ( 1 - T ) e. RR )
14 13 2 remulcld 
 |-  ( ph -> ( ( 1 - T ) x. B ) e. RR )
15 10 14 readdcld 
 |-  ( ph -> ( ( T x. A ) + ( ( 1 - T ) x. B ) ) e. RR )
16 7 15 eqeltrid 
 |-  ( ph -> C e. RR )
17 1cnd 
 |-  ( ph -> 1 e. CC )
18 9 recnd 
 |-  ( ph -> T e. CC )
19 1 recnd 
 |-  ( ph -> A e. CC )
20 17 18 19 subdird 
 |-  ( ph -> ( ( 1 - T ) x. A ) = ( ( 1 x. A ) - ( T x. A ) ) )
21 19 mullidd 
 |-  ( ph -> ( 1 x. A ) = A )
22 21 oveq1d 
 |-  ( ph -> ( ( 1 x. A ) - ( T x. A ) ) = ( A - ( T x. A ) ) )
23 20 22 eqtrd 
 |-  ( ph -> ( ( 1 - T ) x. A ) = ( A - ( T x. A ) ) )
24 eliooord 
 |-  ( T e. ( 0 (,) 1 ) -> ( 0 < T /\ T < 1 ) )
25 6 24 syl 
 |-  ( ph -> ( 0 < T /\ T < 1 ) )
26 25 simprd 
 |-  ( ph -> T < 1 )
27 posdif 
 |-  ( ( T e. RR /\ 1 e. RR ) -> ( T < 1 <-> 0 < ( 1 - T ) ) )
28 9 11 27 sylancl 
 |-  ( ph -> ( T < 1 <-> 0 < ( 1 - T ) ) )
29 26 28 mpbid 
 |-  ( ph -> 0 < ( 1 - T ) )
30 ltmul2 
 |-  ( ( A e. RR /\ B e. RR /\ ( ( 1 - T ) e. RR /\ 0 < ( 1 - T ) ) ) -> ( A < B <-> ( ( 1 - T ) x. A ) < ( ( 1 - T ) x. B ) ) )
31 1 2 13 29 30 syl112anc 
 |-  ( ph -> ( A < B <-> ( ( 1 - T ) x. A ) < ( ( 1 - T ) x. B ) ) )
32 3 31 mpbid 
 |-  ( ph -> ( ( 1 - T ) x. A ) < ( ( 1 - T ) x. B ) )
33 23 32 eqbrtrrd 
 |-  ( ph -> ( A - ( T x. A ) ) < ( ( 1 - T ) x. B ) )
34 1 10 14 ltsubadd2d 
 |-  ( ph -> ( ( A - ( T x. A ) ) < ( ( 1 - T ) x. B ) <-> A < ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) )
35 33 34 mpbid 
 |-  ( ph -> A < ( ( T x. A ) + ( ( 1 - T ) x. B ) ) )
36 35 7 breqtrrdi 
 |-  ( ph -> A < C )
37 1 leidd 
 |-  ( ph -> A <_ A )
38 2 recnd 
 |-  ( ph -> B e. CC )
39 17 18 38 subdird 
 |-  ( ph -> ( ( 1 - T ) x. B ) = ( ( 1 x. B ) - ( T x. B ) ) )
40 38 mullidd 
 |-  ( ph -> ( 1 x. B ) = B )
41 40 oveq1d 
 |-  ( ph -> ( ( 1 x. B ) - ( T x. B ) ) = ( B - ( T x. B ) ) )
42 39 41 eqtrd 
 |-  ( ph -> ( ( 1 - T ) x. B ) = ( B - ( T x. B ) ) )
43 9 2 remulcld 
 |-  ( ph -> ( T x. B ) e. RR )
44 25 simpld 
 |-  ( ph -> 0 < T )
45 ltmul2 
 |-  ( ( A e. RR /\ B e. RR /\ ( T e. RR /\ 0 < T ) ) -> ( A < B <-> ( T x. A ) < ( T x. B ) ) )
46 1 2 9 44 45 syl112anc 
 |-  ( ph -> ( A < B <-> ( T x. A ) < ( T x. B ) ) )
47 3 46 mpbid 
 |-  ( ph -> ( T x. A ) < ( T x. B ) )
48 10 43 2 47 ltsub2dd 
 |-  ( ph -> ( B - ( T x. B ) ) < ( B - ( T x. A ) ) )
49 42 48 eqbrtrd 
 |-  ( ph -> ( ( 1 - T ) x. B ) < ( B - ( T x. A ) ) )
50 10 14 2 ltaddsub2d 
 |-  ( ph -> ( ( ( T x. A ) + ( ( 1 - T ) x. B ) ) < B <-> ( ( 1 - T ) x. B ) < ( B - ( T x. A ) ) ) )
51 49 50 mpbird 
 |-  ( ph -> ( ( T x. A ) + ( ( 1 - T ) x. B ) ) < B )
52 7 51 eqbrtrid 
 |-  ( ph -> C < B )
53 16 2 52 ltled 
 |-  ( ph -> C <_ B )
54 iccss 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( A <_ A /\ C <_ B ) ) -> ( A [,] C ) C_ ( A [,] B ) )
55 1 2 37 53 54 syl22anc 
 |-  ( ph -> ( A [,] C ) C_ ( A [,] B ) )
56 rescncf 
 |-  ( ( A [,] C ) C_ ( A [,] B ) -> ( F e. ( ( A [,] B ) -cn-> RR ) -> ( F |` ( A [,] C ) ) e. ( ( A [,] C ) -cn-> RR ) ) )
57 55 4 56 sylc 
 |-  ( ph -> ( F |` ( A [,] C ) ) e. ( ( A [,] C ) -cn-> RR ) )
58 ax-resscn 
 |-  RR C_ CC
59 58 a1i 
 |-  ( ph -> RR C_ CC )
60 cncff 
 |-  ( F e. ( ( A [,] B ) -cn-> RR ) -> F : ( A [,] B ) --> RR )
61 4 60 syl 
 |-  ( ph -> F : ( A [,] B ) --> RR )
62 fss 
 |-  ( ( F : ( A [,] B ) --> RR /\ RR C_ CC ) -> F : ( A [,] B ) --> CC )
63 61 58 62 sylancl 
 |-  ( ph -> F : ( A [,] B ) --> CC )
64 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
65 1 2 64 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
66 iccssre 
 |-  ( ( A e. RR /\ C e. RR ) -> ( A [,] C ) C_ RR )
67 1 16 66 syl2anc 
 |-  ( ph -> ( A [,] C ) C_ RR )
68 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
69 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
70 68 69 dvres 
 |-  ( ( ( 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 ) ) ) )
71 59 63 65 67 70 syl22anc 
 |-  ( ph -> ( RR _D ( F |` ( A [,] C ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] C ) ) ) )
72 iccntr 
 |-  ( ( A e. RR /\ C e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] C ) ) = ( A (,) C ) )
73 1 16 72 syl2anc 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] C ) ) = ( A (,) C ) )
74 73 reseq2d 
 |-  ( ph -> ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] C ) ) ) = ( ( RR _D F ) |` ( A (,) C ) ) )
75 71 74 eqtrd 
 |-  ( ph -> ( RR _D ( F |` ( A [,] C ) ) ) = ( ( RR _D F ) |` ( A (,) C ) ) )
76 75 dmeqd 
 |-  ( ph -> dom ( RR _D ( F |` ( A [,] C ) ) ) = dom ( ( RR _D F ) |` ( A (,) C ) ) )
77 dmres 
 |-  dom ( ( RR _D F ) |` ( A (,) C ) ) = ( ( A (,) C ) i^i dom ( RR _D F ) )
78 2 rexrd 
 |-  ( ph -> B e. RR* )
79 iooss2 
 |-  ( ( B e. RR* /\ C <_ B ) -> ( A (,) C ) C_ ( A (,) B ) )
80 78 53 79 syl2anc 
 |-  ( ph -> ( A (,) C ) C_ ( A (,) B ) )
81 isof1o 
 |-  ( ( RR _D F ) Isom < , < ( ( A (,) B ) , W ) -> ( RR _D F ) : ( A (,) B ) -1-1-onto-> W )
82 f1odm 
 |-  ( ( RR _D F ) : ( A (,) B ) -1-1-onto-> W -> dom ( RR _D F ) = ( A (,) B ) )
83 5 81 82 3syl 
 |-  ( ph -> dom ( RR _D F ) = ( A (,) B ) )
84 80 83 sseqtrrd 
 |-  ( ph -> ( A (,) C ) C_ dom ( RR _D F ) )
85 dfss2 
 |-  ( ( A (,) C ) C_ dom ( RR _D F ) <-> ( ( A (,) C ) i^i dom ( RR _D F ) ) = ( A (,) C ) )
86 84 85 sylib 
 |-  ( ph -> ( ( A (,) C ) i^i dom ( RR _D F ) ) = ( A (,) C ) )
87 77 86 eqtrid 
 |-  ( ph -> dom ( ( RR _D F ) |` ( A (,) C ) ) = ( A (,) C ) )
88 76 87 eqtrd 
 |-  ( ph -> dom ( RR _D ( F |` ( A [,] C ) ) ) = ( A (,) C ) )
89 1 16 36 57 88 mvth 
 |-  ( ph -> E. x e. ( A (,) C ) ( ( RR _D ( F |` ( A [,] C ) ) ) ` x ) = ( ( ( ( F |` ( A [,] C ) ) ` C ) - ( ( F |` ( A [,] C ) ) ` A ) ) / ( C - A ) ) )
90 1 16 36 ltled 
 |-  ( ph -> A <_ C )
91 2 leidd 
 |-  ( ph -> B <_ B )
92 iccss 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( A <_ C /\ B <_ B ) ) -> ( C [,] B ) C_ ( A [,] B ) )
93 1 2 90 91 92 syl22anc 
 |-  ( ph -> ( C [,] B ) C_ ( A [,] B ) )
94 rescncf 
 |-  ( ( C [,] B ) C_ ( A [,] B ) -> ( F e. ( ( A [,] B ) -cn-> RR ) -> ( F |` ( C [,] B ) ) e. ( ( C [,] B ) -cn-> RR ) ) )
95 93 4 94 sylc 
 |-  ( ph -> ( F |` ( C [,] B ) ) e. ( ( C [,] B ) -cn-> RR ) )
96 iccssre 
 |-  ( ( C e. RR /\ B e. RR ) -> ( C [,] B ) C_ RR )
97 16 2 96 syl2anc 
 |-  ( ph -> ( C [,] B ) C_ RR )
98 68 69 dvres 
 |-  ( ( ( 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 ) ) ) )
99 59 63 65 97 98 syl22anc 
 |-  ( ph -> ( RR _D ( F |` ( C [,] B ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( C [,] B ) ) ) )
100 iccntr 
 |-  ( ( C e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( C [,] B ) ) = ( C (,) B ) )
101 16 2 100 syl2anc 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( C [,] B ) ) = ( C (,) B ) )
102 101 reseq2d 
 |-  ( ph -> ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( C [,] B ) ) ) = ( ( RR _D F ) |` ( C (,) B ) ) )
103 99 102 eqtrd 
 |-  ( ph -> ( RR _D ( F |` ( C [,] B ) ) ) = ( ( RR _D F ) |` ( C (,) B ) ) )
104 103 dmeqd 
 |-  ( ph -> dom ( RR _D ( F |` ( C [,] B ) ) ) = dom ( ( RR _D F ) |` ( C (,) B ) ) )
105 dmres 
 |-  dom ( ( RR _D F ) |` ( C (,) B ) ) = ( ( C (,) B ) i^i dom ( RR _D F ) )
106 1 rexrd 
 |-  ( ph -> A e. RR* )
107 iooss1 
 |-  ( ( A e. RR* /\ A <_ C ) -> ( C (,) B ) C_ ( A (,) B ) )
108 106 90 107 syl2anc 
 |-  ( ph -> ( C (,) B ) C_ ( A (,) B ) )
109 108 83 sseqtrrd 
 |-  ( ph -> ( C (,) B ) C_ dom ( RR _D F ) )
110 dfss2 
 |-  ( ( C (,) B ) C_ dom ( RR _D F ) <-> ( ( C (,) B ) i^i dom ( RR _D F ) ) = ( C (,) B ) )
111 109 110 sylib 
 |-  ( ph -> ( ( C (,) B ) i^i dom ( RR _D F ) ) = ( C (,) B ) )
112 105 111 eqtrid 
 |-  ( ph -> dom ( ( RR _D F ) |` ( C (,) B ) ) = ( C (,) B ) )
113 104 112 eqtrd 
 |-  ( ph -> dom ( RR _D ( F |` ( C [,] B ) ) ) = ( C (,) B ) )
114 16 2 52 95 113 mvth 
 |-  ( ph -> E. y e. ( C (,) B ) ( ( RR _D ( F |` ( C [,] B ) ) ) ` y ) = ( ( ( ( F |` ( C [,] B ) ) ` B ) - ( ( F |` ( C [,] B ) ) ` C ) ) / ( B - C ) ) )
115 reeanv 
 |-  ( 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 ) ) ) )
116 75 fveq1d 
 |-  ( ph -> ( ( RR _D ( F |` ( A [,] C ) ) ) ` x ) = ( ( ( RR _D F ) |` ( A (,) C ) ) ` x ) )
117 fvres 
 |-  ( x e. ( A (,) C ) -> ( ( ( RR _D F ) |` ( A (,) C ) ) ` x ) = ( ( RR _D F ) ` x ) )
118 117 adantr 
 |-  ( ( x e. ( A (,) C ) /\ y e. ( C (,) B ) ) -> ( ( ( RR _D F ) |` ( A (,) C ) ) ` x ) = ( ( RR _D F ) ` x ) )
119 116 118 sylan9eq 
 |-  ( ( ph /\ ( x e. ( A (,) C ) /\ y e. ( C (,) B ) ) ) -> ( ( RR _D ( F |` ( A [,] C ) ) ) ` x ) = ( ( RR _D F ) ` x ) )
120 16 rexrd 
 |-  ( ph -> C e. RR* )
121 ubicc2 
 |-  ( ( A e. RR* /\ C e. RR* /\ A <_ C ) -> C e. ( A [,] C ) )
122 106 120 90 121 syl3anc 
 |-  ( ph -> C e. ( A [,] C ) )
123 122 fvresd 
 |-  ( ph -> ( ( F |` ( A [,] C ) ) ` C ) = ( F ` C ) )
124 lbicc2 
 |-  ( ( A e. RR* /\ C e. RR* /\ A <_ C ) -> A e. ( A [,] C ) )
125 106 120 90 124 syl3anc 
 |-  ( ph -> A e. ( A [,] C ) )
126 125 fvresd 
 |-  ( ph -> ( ( F |` ( A [,] C ) ) ` A ) = ( F ` A ) )
127 123 126 oveq12d 
 |-  ( ph -> ( ( ( F |` ( A [,] C ) ) ` C ) - ( ( F |` ( A [,] C ) ) ` A ) ) = ( ( F ` C ) - ( F ` A ) ) )
128 127 oveq1d 
 |-  ( ph -> ( ( ( ( F |` ( A [,] C ) ) ` C ) - ( ( F |` ( A [,] C ) ) ` A ) ) / ( C - A ) ) = ( ( ( F ` C ) - ( F ` A ) ) / ( C - A ) ) )
129 128 adantr 
 |-  ( ( 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 ) ) )
130 119 129 eqeq12d 
 |-  ( ( 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 ) ) ) )
131 103 fveq1d 
 |-  ( ph -> ( ( RR _D ( F |` ( C [,] B ) ) ) ` y ) = ( ( ( RR _D F ) |` ( C (,) B ) ) ` y ) )
132 fvres 
 |-  ( y e. ( C (,) B ) -> ( ( ( RR _D F ) |` ( C (,) B ) ) ` y ) = ( ( RR _D F ) ` y ) )
133 132 adantl 
 |-  ( ( x e. ( A (,) C ) /\ y e. ( C (,) B ) ) -> ( ( ( RR _D F ) |` ( C (,) B ) ) ` y ) = ( ( RR _D F ) ` y ) )
134 131 133 sylan9eq 
 |-  ( ( ph /\ ( x e. ( A (,) C ) /\ y e. ( C (,) B ) ) ) -> ( ( RR _D ( F |` ( C [,] B ) ) ) ` y ) = ( ( RR _D F ) ` y ) )
135 ubicc2 
 |-  ( ( C e. RR* /\ B e. RR* /\ C <_ B ) -> B e. ( C [,] B ) )
136 120 78 53 135 syl3anc 
 |-  ( ph -> B e. ( C [,] B ) )
137 136 fvresd 
 |-  ( ph -> ( ( F |` ( C [,] B ) ) ` B ) = ( F ` B ) )
138 lbicc2 
 |-  ( ( C e. RR* /\ B e. RR* /\ C <_ B ) -> C e. ( C [,] B ) )
139 120 78 53 138 syl3anc 
 |-  ( ph -> C e. ( C [,] B ) )
140 139 fvresd 
 |-  ( ph -> ( ( F |` ( C [,] B ) ) ` C ) = ( F ` C ) )
141 137 140 oveq12d 
 |-  ( ph -> ( ( ( F |` ( C [,] B ) ) ` B ) - ( ( F |` ( C [,] B ) ) ` C ) ) = ( ( F ` B ) - ( F ` C ) ) )
142 141 oveq1d 
 |-  ( ph -> ( ( ( ( F |` ( C [,] B ) ) ` B ) - ( ( F |` ( C [,] B ) ) ` C ) ) / ( B - C ) ) = ( ( ( F ` B ) - ( F ` C ) ) / ( B - C ) ) )
143 142 adantr 
 |-  ( ( 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 ) ) )
144 134 143 eqeq12d 
 |-  ( ( 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 ) ) ) )
145 130 144 anbi12d 
 |-  ( ( 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 ) ) ) ) )
146 elioore 
 |-  ( x e. ( A (,) C ) -> x e. RR )
147 146 ad2antrl 
 |-  ( ( ph /\ ( x e. ( A (,) C ) /\ y e. ( C (,) B ) ) ) -> x e. RR )
148 16 adantr 
 |-  ( ( ph /\ ( x e. ( A (,) C ) /\ y e. ( C (,) B ) ) ) -> C e. RR )
149 elioore 
 |-  ( y e. ( C (,) B ) -> y e. RR )
150 149 ad2antll 
 |-  ( ( ph /\ ( x e. ( A (,) C ) /\ y e. ( C (,) B ) ) ) -> y e. RR )
151 eliooord 
 |-  ( x e. ( A (,) C ) -> ( A < x /\ x < C ) )
152 151 ad2antrl 
 |-  ( ( ph /\ ( x e. ( A (,) C ) /\ y e. ( C (,) B ) ) ) -> ( A < x /\ x < C ) )
153 152 simprd 
 |-  ( ( ph /\ ( x e. ( A (,) C ) /\ y e. ( C (,) B ) ) ) -> x < C )
154 eliooord 
 |-  ( y e. ( C (,) B ) -> ( C < y /\ y < B ) )
155 154 ad2antll 
 |-  ( ( ph /\ ( x e. ( A (,) C ) /\ y e. ( C (,) B ) ) ) -> ( C < y /\ y < B ) )
156 155 simpld 
 |-  ( ( ph /\ ( x e. ( A (,) C ) /\ y e. ( C (,) B ) ) ) -> C < y )
157 147 148 150 153 156 lttrd 
 |-  ( ( ph /\ ( x e. ( A (,) C ) /\ y e. ( C (,) B ) ) ) -> x < y )
158 5 adantr 
 |-  ( ( ph /\ ( x e. ( A (,) C ) /\ y e. ( C (,) B ) ) ) -> ( RR _D F ) Isom < , < ( ( A (,) B ) , W ) )
159 80 sselda 
 |-  ( ( ph /\ x e. ( A (,) C ) ) -> x e. ( A (,) B ) )
160 159 adantrr 
 |-  ( ( ph /\ ( x e. ( A (,) C ) /\ y e. ( C (,) B ) ) ) -> x e. ( A (,) B ) )
161 108 sselda 
 |-  ( ( ph /\ y e. ( C (,) B ) ) -> y e. ( A (,) B ) )
162 161 adantrl 
 |-  ( ( ph /\ ( x e. ( A (,) C ) /\ y e. ( C (,) B ) ) ) -> y e. ( A (,) B ) )
163 isorel 
 |-  ( ( ( 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 ) ) )
164 158 160 162 163 syl12anc 
 |-  ( ( ph /\ ( x e. ( A (,) C ) /\ y e. ( C (,) B ) ) ) -> ( x < y <-> ( ( RR _D F ) ` x ) < ( ( RR _D F ) ` y ) ) )
165 157 164 mpbid 
 |-  ( ( ph /\ ( x e. ( A (,) C ) /\ y e. ( C (,) B ) ) ) -> ( ( RR _D F ) ` x ) < ( ( RR _D F ) ` y ) )
166 breq12 
 |-  ( ( ( ( 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 ) ) ) )
167 165 166 syl5ibcom 
 |-  ( ( 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 ) ) ) )
168 55 122 sseldd 
 |-  ( ph -> C e. ( A [,] B ) )
169 61 168 ffvelcdmd 
 |-  ( ph -> ( F ` C ) e. RR )
170 55 125 sseldd 
 |-  ( ph -> A e. ( A [,] B ) )
171 61 170 ffvelcdmd 
 |-  ( ph -> ( F ` A ) e. RR )
172 169 171 resubcld 
 |-  ( ph -> ( ( F ` C ) - ( F ` A ) ) e. RR )
173 29 gt0ne0d 
 |-  ( ph -> ( 1 - T ) =/= 0 )
174 172 13 173 redivcld 
 |-  ( ph -> ( ( ( F ` C ) - ( F ` A ) ) / ( 1 - T ) ) e. RR )
175 93 136 sseldd 
 |-  ( ph -> B e. ( A [,] B ) )
176 61 175 ffvelcdmd 
 |-  ( ph -> ( F ` B ) e. RR )
177 176 169 resubcld 
 |-  ( ph -> ( ( F ` B ) - ( F ` C ) ) e. RR )
178 44 gt0ne0d 
 |-  ( ph -> T =/= 0 )
179 177 9 178 redivcld 
 |-  ( ph -> ( ( ( F ` B ) - ( F ` C ) ) / T ) e. RR )
180 2 1 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
181 1 2 posdifd 
 |-  ( ph -> ( A < B <-> 0 < ( B - A ) ) )
182 3 181 mpbid 
 |-  ( ph -> 0 < ( B - A ) )
183 ltdiv1 
 |-  ( ( ( ( ( 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 ) ) ) )
184 174 179 180 182 183 syl112anc 
 |-  ( 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 ) ) ) )
185 172 recnd 
 |-  ( ph -> ( ( F ` C ) - ( F ` A ) ) e. CC )
186 185 18 mulcomd 
 |-  ( ph -> ( ( ( F ` C ) - ( F ` A ) ) x. T ) = ( T x. ( ( F ` C ) - ( F ` A ) ) ) )
187 169 recnd 
 |-  ( ph -> ( F ` C ) e. CC )
188 171 recnd 
 |-  ( ph -> ( F ` A ) e. CC )
189 18 187 188 subdid 
 |-  ( ph -> ( T x. ( ( F ` C ) - ( F ` A ) ) ) = ( ( T x. ( F ` C ) ) - ( T x. ( F ` A ) ) ) )
190 186 189 eqtrd 
 |-  ( ph -> ( ( ( F ` C ) - ( F ` A ) ) x. T ) = ( ( T x. ( F ` C ) ) - ( T x. ( F ` A ) ) ) )
191 177 recnd 
 |-  ( ph -> ( ( F ` B ) - ( F ` C ) ) e. CC )
192 13 recnd 
 |-  ( ph -> ( 1 - T ) e. CC )
193 191 192 mulcomd 
 |-  ( ph -> ( ( ( F ` B ) - ( F ` C ) ) x. ( 1 - T ) ) = ( ( 1 - T ) x. ( ( F ` B ) - ( F ` C ) ) ) )
194 176 recnd 
 |-  ( ph -> ( F ` B ) e. CC )
195 192 194 187 subdid 
 |-  ( ph -> ( ( 1 - T ) x. ( ( F ` B ) - ( F ` C ) ) ) = ( ( ( 1 - T ) x. ( F ` B ) ) - ( ( 1 - T ) x. ( F ` C ) ) ) )
196 193 195 eqtrd 
 |-  ( ph -> ( ( ( F ` B ) - ( F ` C ) ) x. ( 1 - T ) ) = ( ( ( 1 - T ) x. ( F ` B ) ) - ( ( 1 - T ) x. ( F ` C ) ) ) )
197 190 196 breq12d 
 |-  ( 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 ) ) ) ) )
198 9 44 jca 
 |-  ( ph -> ( T e. RR /\ 0 < T ) )
199 13 29 jca 
 |-  ( ph -> ( ( 1 - T ) e. RR /\ 0 < ( 1 - T ) ) )
200 lt2mul2div 
 |-  ( ( ( ( ( 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 ) ) )
201 172 198 177 199 200 syl22anc 
 |-  ( 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 ) ) )
202 9 169 remulcld 
 |-  ( ph -> ( T x. ( F ` C ) ) e. RR )
203 202 recnd 
 |-  ( ph -> ( T x. ( F ` C ) ) e. CC )
204 13 169 remulcld 
 |-  ( ph -> ( ( 1 - T ) x. ( F ` C ) ) e. RR )
205 204 recnd 
 |-  ( ph -> ( ( 1 - T ) x. ( F ` C ) ) e. CC )
206 9 171 remulcld 
 |-  ( ph -> ( T x. ( F ` A ) ) e. RR )
207 206 recnd 
 |-  ( ph -> ( T x. ( F ` A ) ) e. CC )
208 203 205 207 addsubd 
 |-  ( 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 ) ) ) )
209 ax-1cn 
 |-  1 e. CC
210 pncan3 
 |-  ( ( T e. CC /\ 1 e. CC ) -> ( T + ( 1 - T ) ) = 1 )
211 18 209 210 sylancl 
 |-  ( ph -> ( T + ( 1 - T ) ) = 1 )
212 211 oveq1d 
 |-  ( ph -> ( ( T + ( 1 - T ) ) x. ( F ` C ) ) = ( 1 x. ( F ` C ) ) )
213 18 192 187 adddird 
 |-  ( ph -> ( ( T + ( 1 - T ) ) x. ( F ` C ) ) = ( ( T x. ( F ` C ) ) + ( ( 1 - T ) x. ( F ` C ) ) ) )
214 187 mullidd 
 |-  ( ph -> ( 1 x. ( F ` C ) ) = ( F ` C ) )
215 212 213 214 3eqtr3d 
 |-  ( ph -> ( ( T x. ( F ` C ) ) + ( ( 1 - T ) x. ( F ` C ) ) ) = ( F ` C ) )
216 215 oveq1d 
 |-  ( ph -> ( ( ( T x. ( F ` C ) ) + ( ( 1 - T ) x. ( F ` C ) ) ) - ( T x. ( F ` A ) ) ) = ( ( F ` C ) - ( T x. ( F ` A ) ) ) )
217 208 216 eqtr3d 
 |-  ( ph -> ( ( ( T x. ( F ` C ) ) - ( T x. ( F ` A ) ) ) + ( ( 1 - T ) x. ( F ` C ) ) ) = ( ( F ` C ) - ( T x. ( F ` A ) ) ) )
218 217 breq1d 
 |-  ( 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 ) ) ) )
219 202 206 resubcld 
 |-  ( ph -> ( ( T x. ( F ` C ) ) - ( T x. ( F ` A ) ) ) e. RR )
220 13 176 remulcld 
 |-  ( ph -> ( ( 1 - T ) x. ( F ` B ) ) e. RR )
221 219 204 220 ltaddsubd 
 |-  ( 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 ) ) ) ) )
222 169 206 220 ltsubadd2d 
 |-  ( ph -> ( ( ( F ` C ) - ( T x. ( F ` A ) ) ) < ( ( 1 - T ) x. ( F ` B ) ) <-> ( F ` C ) < ( ( T x. ( F ` A ) ) + ( ( 1 - T ) x. ( F ` B ) ) ) ) )
223 218 221 222 3bitr3d 
 |-  ( 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 ) ) ) ) )
224 197 201 223 3bitr3d 
 |-  ( ph -> ( ( ( ( F ` C ) - ( F ` A ) ) / ( 1 - T ) ) < ( ( ( F ` B ) - ( F ` C ) ) / T ) <-> ( F ` C ) < ( ( T x. ( F ` A ) ) + ( ( 1 - T ) x. ( F ` B ) ) ) ) )
225 180 recnd 
 |-  ( ph -> ( B - A ) e. CC )
226 182 gt0ne0d 
 |-  ( ph -> ( B - A ) =/= 0 )
227 185 192 225 173 226 divdiv1d 
 |-  ( ph -> ( ( ( ( F ` C ) - ( F ` A ) ) / ( 1 - T ) ) / ( B - A ) ) = ( ( ( F ` C ) - ( F ` A ) ) / ( ( 1 - T ) x. ( B - A ) ) ) )
228 23 oveq2d 
 |-  ( ph -> ( ( ( 1 - T ) x. B ) - ( ( 1 - T ) x. A ) ) = ( ( ( 1 - T ) x. B ) - ( A - ( T x. A ) ) ) )
229 14 recnd 
 |-  ( ph -> ( ( 1 - T ) x. B ) e. CC )
230 10 recnd 
 |-  ( ph -> ( T x. A ) e. CC )
231 229 19 230 subsub3d 
 |-  ( ph -> ( ( ( 1 - T ) x. B ) - ( A - ( T x. A ) ) ) = ( ( ( ( 1 - T ) x. B ) + ( T x. A ) ) - A ) )
232 228 231 eqtrd 
 |-  ( ph -> ( ( ( 1 - T ) x. B ) - ( ( 1 - T ) x. A ) ) = ( ( ( ( 1 - T ) x. B ) + ( T x. A ) ) - A ) )
233 192 38 19 subdid 
 |-  ( ph -> ( ( 1 - T ) x. ( B - A ) ) = ( ( ( 1 - T ) x. B ) - ( ( 1 - T ) x. A ) ) )
234 230 229 addcomd 
 |-  ( ph -> ( ( T x. A ) + ( ( 1 - T ) x. B ) ) = ( ( ( 1 - T ) x. B ) + ( T x. A ) ) )
235 7 234 eqtrid 
 |-  ( ph -> C = ( ( ( 1 - T ) x. B ) + ( T x. A ) ) )
236 235 oveq1d 
 |-  ( ph -> ( C - A ) = ( ( ( ( 1 - T ) x. B ) + ( T x. A ) ) - A ) )
237 232 233 236 3eqtr4d 
 |-  ( ph -> ( ( 1 - T ) x. ( B - A ) ) = ( C - A ) )
238 237 oveq2d 
 |-  ( ph -> ( ( ( F ` C ) - ( F ` A ) ) / ( ( 1 - T ) x. ( B - A ) ) ) = ( ( ( F ` C ) - ( F ` A ) ) / ( C - A ) ) )
239 227 238 eqtrd 
 |-  ( ph -> ( ( ( ( F ` C ) - ( F ` A ) ) / ( 1 - T ) ) / ( B - A ) ) = ( ( ( F ` C ) - ( F ` A ) ) / ( C - A ) ) )
240 191 18 225 178 226 divdiv1d 
 |-  ( ph -> ( ( ( ( F ` B ) - ( F ` C ) ) / T ) / ( B - A ) ) = ( ( ( F ` B ) - ( F ` C ) ) / ( T x. ( B - A ) ) ) )
241 38 229 230 subsub4d 
 |-  ( ph -> ( ( B - ( ( 1 - T ) x. B ) ) - ( T x. A ) ) = ( B - ( ( ( 1 - T ) x. B ) + ( T x. A ) ) ) )
242 42 oveq2d 
 |-  ( ph -> ( B - ( ( 1 - T ) x. B ) ) = ( B - ( B - ( T x. B ) ) ) )
243 43 recnd 
 |-  ( ph -> ( T x. B ) e. CC )
244 38 243 nncand 
 |-  ( ph -> ( B - ( B - ( T x. B ) ) ) = ( T x. B ) )
245 242 244 eqtrd 
 |-  ( ph -> ( B - ( ( 1 - T ) x. B ) ) = ( T x. B ) )
246 245 oveq1d 
 |-  ( ph -> ( ( B - ( ( 1 - T ) x. B ) ) - ( T x. A ) ) = ( ( T x. B ) - ( T x. A ) ) )
247 241 246 eqtr3d 
 |-  ( ph -> ( B - ( ( ( 1 - T ) x. B ) + ( T x. A ) ) ) = ( ( T x. B ) - ( T x. A ) ) )
248 235 oveq2d 
 |-  ( ph -> ( B - C ) = ( B - ( ( ( 1 - T ) x. B ) + ( T x. A ) ) ) )
249 18 38 19 subdid 
 |-  ( ph -> ( T x. ( B - A ) ) = ( ( T x. B ) - ( T x. A ) ) )
250 247 248 249 3eqtr4d 
 |-  ( ph -> ( B - C ) = ( T x. ( B - A ) ) )
251 250 oveq2d 
 |-  ( ph -> ( ( ( F ` B ) - ( F ` C ) ) / ( B - C ) ) = ( ( ( F ` B ) - ( F ` C ) ) / ( T x. ( B - A ) ) ) )
252 240 251 eqtr4d 
 |-  ( ph -> ( ( ( ( F ` B ) - ( F ` C ) ) / T ) / ( B - A ) ) = ( ( ( F ` B ) - ( F ` C ) ) / ( B - C ) ) )
253 239 252 breq12d 
 |-  ( 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 ) ) ) )
254 184 224 253 3bitr3rd 
 |-  ( ph -> ( ( ( ( F ` C ) - ( F ` A ) ) / ( C - A ) ) < ( ( ( F ` B ) - ( F ` C ) ) / ( B - C ) ) <-> ( F ` C ) < ( ( T x. ( F ` A ) ) + ( ( 1 - T ) x. ( F ` B ) ) ) ) )
255 254 adantr 
 |-  ( ( 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 ) ) ) ) )
256 167 255 sylibd 
 |-  ( ( 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 ) ) ) ) )
257 145 256 sylbid 
 |-  ( ( 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 ) ) ) ) )
258 257 rexlimdvva 
 |-  ( 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 ) ) ) ) )
259 115 258 biimtrrid 
 |-  ( 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 ) ) ) ) )
260 89 114 259 mp2and 
 |-  ( ph -> ( F ` C ) < ( ( T x. ( F ` A ) ) + ( ( 1 - T ) x. ( F ` B ) ) ) )