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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
dvcvx.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
dvcvx.l ⊢ ( 𝜑 → 𝐴 < 𝐵 )
dvcvx.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
dvcvx.d ⊢ ( 𝜑 → ( ℝ D 𝐹 ) Isom < , < ( ( 𝐴 (,) 𝐵 ) , 𝑊 ) )
dvcvx.t ⊢ ( 𝜑 → 𝑇 ∈ ( 0 (,) 1 ) )
dvcvx.c ⊢ 𝐶 = ( ( 𝑇 · 𝐴 ) + ( ( 1 − 𝑇 ) · 𝐵 ) )
Assertion dvcvx ( 𝜑 → ( 𝐹 ‘ 𝐶 ) < ( ( 𝑇 · ( 𝐹 ‘ 𝐴 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝐵 ) ) ) )

Proof

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