dvcvx

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

	Ref	Expression
Hypotheses	dvcvx.a	$⊢ φ \to A \in ℝ$
	dvcvx.b	$⊢ φ \to B \in ℝ$
	dvcvx.l	$⊢ φ \to A < B$
	dvcvx.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℝ$
	dvcvx.d	$⊢ φ \to F_{ℝ}^{'} {Isom}_{<, <} ((A, B), W)$
	dvcvx.t	$⊢ φ \to T \in (0, 1)$
	dvcvx.c	$⊢ C = T A + (1 - T) B$
Assertion	dvcvx	$⊢ φ \to F (C) < T F (A) + (1 - T) F (B)$

Proof

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

Metamath Proof Explorer

Theorem dvcvx

Proof