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	mullidd	⊢ ( 𝜑 → ( 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	mullidd	⊢ ( 𝜑 → ( 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	eqtrid	⊢ ( 𝜑 → 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	eqtrid	⊢ ( 𝜑 → 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	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ℝ )
170	55 125	sseldd	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
171	61 170	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ℝ )
172	169 171	resubcld	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ )
173	29	gt0ne0d	⊢ ( 𝜑 → ( 1 − 𝑇 ) ≠ 0 )
174	172 13 173	redivcld	⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝐶 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 1 − 𝑇 ) ) ∈ ℝ )
175	93 136	sseldd	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
176	61 175	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ ℝ )
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	mullidd	⊢ ( 𝜑 → ( 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	eqtrid	⊢ ( 𝜑 → 𝐶 = ( ( ( 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	biimtrrid	⊢ ( 𝜑 → ( ( ∃ 𝑥 ∈ ( 𝐴 (,) 𝐶 ) ( ( ℝ D ( 𝐹 ↾ ( 𝐴 [,] 𝐶 ) ) ) ‘ 𝑥 ) = ( ( ( ( 𝐹 ↾ ( 𝐴 [,] 𝐶 ) ) ‘ 𝐶 ) − ( ( 𝐹 ↾ ( 𝐴 [,] 𝐶 ) ) ‘ 𝐴 ) ) / ( 𝐶 − 𝐴 ) ) ∧ ∃ 𝑦 ∈ ( 𝐶 (,) 𝐵 ) ( ( ℝ D ( 𝐹 ↾ ( 𝐶 [,] 𝐵 ) ) ) ‘ 𝑦 ) = ( ( ( ( 𝐹 ↾ ( 𝐶 [,] 𝐵 ) ) ‘ 𝐵 ) − ( ( 𝐹 ↾ ( 𝐶 [,] 𝐵 ) ) ‘ 𝐶 ) ) / ( 𝐵 − 𝐶 ) ) ) → ( 𝐹 ‘ 𝐶 ) < ( ( 𝑇 · ( 𝐹 ‘ 𝐴 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝐵 ) ) ) ) )
260	89 114 259	mp2and	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) < ( ( 𝑇 · ( 𝐹 ‘ 𝐴 ) ) + ( ( 1 − 𝑇 ) · ( 𝐹 ‘ 𝐵 ) ) ) )