scvxcvx

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

	Ref	Expression
Hypotheses	scvxcvx.1	$⊢ φ \to D \subseteq ℝ$
	scvxcvx.2	$⊢ φ \to F : D ⟶ ℝ$
	scvxcvx.3	$⊢ (φ \land (a \in D \land b \in D)) \to [a, b] \subseteq D$
	scvxcvx.4	$⊢ (φ \land (x \in D \land y \in D \land x < y) \land t \in (0, 1)) \to F (t x + (1 - t) y) < t F (x) + (1 - t) F (y)$
Assertion	scvxcvx	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to F (T X + (1 - T) Y) \leq T F (X) + (1 - T) F (Y)$

Proof

Step	Hyp	Ref	Expression
1		scvxcvx.1	$⊢ φ \to D \subseteq ℝ$
2		scvxcvx.2	$⊢ φ \to F : D ⟶ ℝ$
3		scvxcvx.3	$⊢ (φ \land (a \in D \land b \in D)) \to [a, b] \subseteq D$
4		scvxcvx.4	$⊢ (φ \land (x \in D \land y \in D \land x < y) \land t \in (0, 1)) \to F (t x + (1 - t) y) < t F (x) + (1 - t) F (y)$
5	1	adantr	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to D \subseteq ℝ$
6		simpr1	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to X \in D$
7	5 6	sseldd	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to X \in ℝ$
8	7	adantr	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land T \in (0, 1)) \to X \in ℝ$
9		simpr2	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to Y \in D$
10	5 9	sseldd	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to Y \in ℝ$
11	10	adantr	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land T \in (0, 1)) \to Y \in ℝ$
12	8 11	lttri4d	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land T \in (0, 1)) \to (X < Y \lor X = Y \lor Y < X)$
13		oveq1	$⊢ t = T \to t X = T X$
14		oveq2	$⊢ t = T \to 1 - t = 1 - T$
15	14	oveq1d	$⊢ t = T \to (1 - t) Y = (1 - T) Y$
16	13 15	oveq12d	$⊢ t = T \to t X + (1 - t) Y = T X + (1 - T) Y$
17	16	fveq2d	$⊢ t = T \to F (t X + (1 - t) Y) = F (T X + (1 - T) Y)$
18		oveq1	$⊢ t = T \to t F (X) = T F (X)$
19	14	oveq1d	$⊢ t = T \to (1 - t) F (Y) = (1 - T) F (Y)$
20	18 19	oveq12d	$⊢ t = T \to t F (X) + (1 - t) F (Y) = T F (X) + (1 - T) F (Y)$
21	17 20	breq12d	$⊢ t = T \to (F (t X + (1 - t) Y) < t F (X) + (1 - t) F (Y) \leftrightarrow F (T X + (1 - T) Y) < T F (X) + (1 - T) F (Y))$
22	6	adantr	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land (T \in (0, 1) \land X < Y)) \to X \in D$
23	9	adantr	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land (T \in (0, 1) \land X < Y)) \to Y \in D$
24	22 23	jca	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land (T \in (0, 1) \land X < Y)) \to (X \in D \land Y \in D)$
25		simprr	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land (T \in (0, 1) \land X < Y)) \to X < Y$
26		simpll	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land (T \in (0, 1) \land X < Y)) \to φ$
27		breq1	$⊢ x = X \to (x < y \leftrightarrow X < y)$
28		oveq2	$⊢ x = X \to t x = t X$
29	28	fvoveq1d	$⊢ x = X \to F (t x + (1 - t) y) = F (t X + (1 - t) y)$
30		fveq2	$⊢ x = X \to F (x) = F (X)$
31	30	oveq2d	$⊢ x = X \to t F (x) = t F (X)$
32	31	oveq1d	$⊢ x = X \to t F (x) + (1 - t) F (y) = t F (X) + (1 - t) F (y)$
33	29 32	breq12d	$⊢ x = X \to (F (t x + (1 - t) y) < t F (x) + (1 - t) F (y) \leftrightarrow F (t X + (1 - t) y) < t F (X) + (1 - t) F (y))$
34	33	ralbidv	$⊢ x = X \to (\forall t \in (0, 1) F (t x + (1 - t) y) < t F (x) + (1 - t) F (y) \leftrightarrow \forall t \in (0, 1) F (t X + (1 - t) y) < t F (X) + (1 - t) F (y))$
35	34	imbi2d	$⊢ x = X \to ((φ \to \forall t \in (0, 1) F (t x + (1 - t) y) < t F (x) + (1 - t) F (y)) \leftrightarrow (φ \to \forall t \in (0, 1) F (t X + (1 - t) y) < t F (X) + (1 - t) F (y)))$
36	27 35	imbi12d	$⊢ x = X \to ((x < y \to (φ \to \forall t \in (0, 1) F (t x + (1 - t) y) < t F (x) + (1 - t) F (y))) \leftrightarrow (X < y \to (φ \to \forall t \in (0, 1) F (t X + (1 - t) y) < t F (X) + (1 - t) F (y))))$
37		breq2	$⊢ y = Y \to (X < y \leftrightarrow X < Y)$
38		oveq2	$⊢ y = Y \to (1 - t) y = (1 - t) Y$
39	38	oveq2d	$⊢ y = Y \to t X + (1 - t) y = t X + (1 - t) Y$
40	39	fveq2d	$⊢ y = Y \to F (t X + (1 - t) y) = F (t X + (1 - t) Y)$
41		fveq2	$⊢ y = Y \to F (y) = F (Y)$
42	41	oveq2d	$⊢ y = Y \to (1 - t) F (y) = (1 - t) F (Y)$
43	42	oveq2d	$⊢ y = Y \to t F (X) + (1 - t) F (y) = t F (X) + (1 - t) F (Y)$
44	40 43	breq12d	$⊢ y = Y \to (F (t X + (1 - t) y) < t F (X) + (1 - t) F (y) \leftrightarrow F (t X + (1 - t) Y) < t F (X) + (1 - t) F (Y))$
45	44	ralbidv	$⊢ y = Y \to (\forall t \in (0, 1) F (t X + (1 - t) y) < t F (X) + (1 - t) F (y) \leftrightarrow \forall t \in (0, 1) F (t X + (1 - t) Y) < t F (X) + (1 - t) F (Y))$
46	45	imbi2d	$⊢ y = Y \to ((φ \to \forall t \in (0, 1) F (t X + (1 - t) y) < t F (X) + (1 - t) F (y)) \leftrightarrow (φ \to \forall t \in (0, 1) F (t X + (1 - t) Y) < t F (X) + (1 - t) F (Y)))$
47	37 46	imbi12d	$⊢ y = Y \to ((X < y \to (φ \to \forall t \in (0, 1) F (t X + (1 - t) y) < t F (X) + (1 - t) F (y))) \leftrightarrow (X < Y \to (φ \to \forall t \in (0, 1) F (t X + (1 - t) Y) < t F (X) + (1 - t) F (Y))))$
48	4	3expia	$⊢ (φ \land (x \in D \land y \in D \land x < y)) \to (t \in (0, 1) \to F (t x + (1 - t) y) < t F (x) + (1 - t) F (y))$
49	48	ralrimiv	$⊢ (φ \land (x \in D \land y \in D \land x < y)) \to \forall t \in (0, 1) F (t x + (1 - t) y) < t F (x) + (1 - t) F (y)$
50	49	expcom	$⊢ (x \in D \land y \in D \land x < y) \to (φ \to \forall t \in (0, 1) F (t x + (1 - t) y) < t F (x) + (1 - t) F (y))$
51	50	3expia	$⊢ (x \in D \land y \in D) \to (x < y \to (φ \to \forall t \in (0, 1) F (t x + (1 - t) y) < t F (x) + (1 - t) F (y)))$
52	36 47 51	vtocl2ga	$⊢ (X \in D \land Y \in D) \to (X < Y \to (φ \to \forall t \in (0, 1) F (t X + (1 - t) Y) < t F (X) + (1 - t) F (Y)))$
53	24 25 26 52	syl3c	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land (T \in (0, 1) \land X < Y)) \to \forall t \in (0, 1) F (t X + (1 - t) Y) < t F (X) + (1 - t) F (Y)$
54		simprl	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land (T \in (0, 1) \land X < Y)) \to T \in (0, 1)$
55	21 53 54	rspcdva	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land (T \in (0, 1) \land X < Y)) \to F (T X + (1 - T) Y) < T F (X) + (1 - T) F (Y)$
56	55	orcd	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land (T \in (0, 1) \land X < Y)) \to (F (T X + (1 - T) Y) < T F (X) + (1 - T) F (Y) \lor F (T X + (1 - T) Y) = T F (X) + (1 - T) F (Y))$
57	56	expr	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land T \in (0, 1)) \to (X < Y \to (F (T X + (1 - T) Y) < T F (X) + (1 - T) F (Y) \lor F (T X + (1 - T) Y) = T F (X) + (1 - T) F (Y)))$
58		unitssre	$⊢ [0, 1] \subseteq ℝ$
59		simpr3	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to T \in [0, 1]$
60	58 59	sseldi	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to T \in ℝ$
61	60	recnd	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to T \in ℂ$
62		ax-1cn	$⊢ 1 \in ℂ$
63		pncan3	$⊢ (T \in ℂ \land 1 \in ℂ) \to T + 1 - T = 1$
64	61 62 63	sylancl	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to T + 1 - T = 1$
65	64	oveq1d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to (T + 1 - T) Y = 1 Y$
66		subcl	$⊢ (1 \in ℂ \land T \in ℂ) \to 1 - T \in ℂ$
67	62 61 66	sylancr	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to 1 - T \in ℂ$
68	10	recnd	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to Y \in ℂ$
69	61 67 68	adddird	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to (T + 1 - T) Y = T Y + (1 - T) Y$
70	68	mulid2d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to 1 Y = Y$
71	65 69 70	3eqtr3d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to T Y + (1 - T) Y = Y$
72	71	fveq2d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to F (T Y + (1 - T) Y) = F (Y)$
73	64	oveq1d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to (T + 1 - T) F (Y) = 1 F (Y)$
74	2	adantr	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to F : D ⟶ ℝ$
75	74 9	ffvelrnd	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to F (Y) \in ℝ$
76	75	recnd	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to F (Y) \in ℂ$
77	61 67 76	adddird	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to (T + 1 - T) F (Y) = T F (Y) + (1 - T) F (Y)$
78	76	mulid2d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to 1 F (Y) = F (Y)$
79	73 77 78	3eqtr3d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to T F (Y) + (1 - T) F (Y) = F (Y)$
80	72 79	eqtr4d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to F (T Y + (1 - T) Y) = T F (Y) + (1 - T) F (Y)$
81	80	adantr	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land T \in (0, 1)) \to F (T Y + (1 - T) Y) = T F (Y) + (1 - T) F (Y)$
82		oveq2	$⊢ X = Y \to T X = T Y$
83	82	fvoveq1d	$⊢ X = Y \to F (T X + (1 - T) Y) = F (T Y + (1 - T) Y)$
84		fveq2	$⊢ X = Y \to F (X) = F (Y)$
85	84	oveq2d	$⊢ X = Y \to T F (X) = T F (Y)$
86	85	oveq1d	$⊢ X = Y \to T F (X) + (1 - T) F (Y) = T F (Y) + (1 - T) F (Y)$
87	83 86	eqeq12d	$⊢ X = Y \to (F (T X + (1 - T) Y) = T F (X) + (1 - T) F (Y) \leftrightarrow F (T Y + (1 - T) Y) = T F (Y) + (1 - T) F (Y))$
88	81 87	syl5ibrcom	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land T \in (0, 1)) \to (X = Y \to F (T X + (1 - T) Y) = T F (X) + (1 - T) F (Y))$
89		olc	$⊢ F (T X + (1 - T) Y) = T F (X) + (1 - T) F (Y) \to (F (T X + (1 - T) Y) < T F (X) + (1 - T) F (Y) \lor F (T X + (1 - T) Y) = T F (X) + (1 - T) F (Y))$
90	88 89	syl6	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land T \in (0, 1)) \to (X = Y \to (F (T X + (1 - T) Y) < T F (X) + (1 - T) F (Y) \lor F (T X + (1 - T) Y) = T F (X) + (1 - T) F (Y)))$
91		oveq1	$⊢ t = 1 - T \to t Y = (1 - T) Y$
92		oveq2	$⊢ t = 1 - T \to 1 - t = 1 - (1 - T)$
93	92	oveq1d	$⊢ t = 1 - T \to (1 - t) X = (1 - (1 - T)) X$
94	91 93	oveq12d	$⊢ t = 1 - T \to t Y + (1 - t) X = (1 - T) Y + (1 - (1 - T)) X$
95	94	fveq2d	$⊢ t = 1 - T \to F (t Y + (1 - t) X) = F ((1 - T) Y + (1 - (1 - T)) X)$
96		oveq1	$⊢ t = 1 - T \to t F (Y) = (1 - T) F (Y)$
97	92	oveq1d	$⊢ t = 1 - T \to (1 - t) F (X) = (1 - (1 - T)) F (X)$
98	96 97	oveq12d	$⊢ t = 1 - T \to t F (Y) + (1 - t) F (X) = (1 - T) F (Y) + (1 - (1 - T)) F (X)$
99	95 98	breq12d	$⊢ t = 1 - T \to (F (t Y + (1 - t) X) < t F (Y) + (1 - t) F (X) \leftrightarrow F ((1 - T) Y + (1 - (1 - T)) X) < (1 - T) F (Y) + (1 - (1 - T)) F (X))$
100	9	adantr	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land (T \in (0, 1) \land Y < X)) \to Y \in D$
101	6	adantr	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land (T \in (0, 1) \land Y < X)) \to X \in D$
102	100 101	jca	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land (T \in (0, 1) \land Y < X)) \to (Y \in D \land X \in D)$
103		simprr	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land (T \in (0, 1) \land Y < X)) \to Y < X$
104		simpll	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land (T \in (0, 1) \land Y < X)) \to φ$
105		breq1	$⊢ x = Y \to (x < y \leftrightarrow Y < y)$
106		oveq2	$⊢ x = Y \to t x = t Y$
107	106	fvoveq1d	$⊢ x = Y \to F (t x + (1 - t) y) = F (t Y + (1 - t) y)$
108		fveq2	$⊢ x = Y \to F (x) = F (Y)$
109	108	oveq2d	$⊢ x = Y \to t F (x) = t F (Y)$
110	109	oveq1d	$⊢ x = Y \to t F (x) + (1 - t) F (y) = t F (Y) + (1 - t) F (y)$
111	107 110	breq12d	$⊢ x = Y \to (F (t x + (1 - t) y) < t F (x) + (1 - t) F (y) \leftrightarrow F (t Y + (1 - t) y) < t F (Y) + (1 - t) F (y))$
112	111	ralbidv	$⊢ x = Y \to (\forall t \in (0, 1) F (t x + (1 - t) y) < t F (x) + (1 - t) F (y) \leftrightarrow \forall t \in (0, 1) F (t Y + (1 - t) y) < t F (Y) + (1 - t) F (y))$
113	112	imbi2d	$⊢ x = Y \to ((φ \to \forall t \in (0, 1) F (t x + (1 - t) y) < t F (x) + (1 - t) F (y)) \leftrightarrow (φ \to \forall t \in (0, 1) F (t Y + (1 - t) y) < t F (Y) + (1 - t) F (y)))$
114	105 113	imbi12d	$⊢ x = Y \to ((x < y \to (φ \to \forall t \in (0, 1) F (t x + (1 - t) y) < t F (x) + (1 - t) F (y))) \leftrightarrow (Y < y \to (φ \to \forall t \in (0, 1) F (t Y + (1 - t) y) < t F (Y) + (1 - t) F (y))))$
115		breq2	$⊢ y = X \to (Y < y \leftrightarrow Y < X)$
116		oveq2	$⊢ y = X \to (1 - t) y = (1 - t) X$
117	116	oveq2d	$⊢ y = X \to t Y + (1 - t) y = t Y + (1 - t) X$
118	117	fveq2d	$⊢ y = X \to F (t Y + (1 - t) y) = F (t Y + (1 - t) X)$
119		fveq2	$⊢ y = X \to F (y) = F (X)$
120	119	oveq2d	$⊢ y = X \to (1 - t) F (y) = (1 - t) F (X)$
121	120	oveq2d	$⊢ y = X \to t F (Y) + (1 - t) F (y) = t F (Y) + (1 - t) F (X)$
122	118 121	breq12d	$⊢ y = X \to (F (t Y + (1 - t) y) < t F (Y) + (1 - t) F (y) \leftrightarrow F (t Y + (1 - t) X) < t F (Y) + (1 - t) F (X))$
123	122	ralbidv	$⊢ y = X \to (\forall t \in (0, 1) F (t Y + (1 - t) y) < t F (Y) + (1 - t) F (y) \leftrightarrow \forall t \in (0, 1) F (t Y + (1 - t) X) < t F (Y) + (1 - t) F (X))$
124	123	imbi2d	$⊢ y = X \to ((φ \to \forall t \in (0, 1) F (t Y + (1 - t) y) < t F (Y) + (1 - t) F (y)) \leftrightarrow (φ \to \forall t \in (0, 1) F (t Y + (1 - t) X) < t F (Y) + (1 - t) F (X)))$
125	115 124	imbi12d	$⊢ y = X \to ((Y < y \to (φ \to \forall t \in (0, 1) F (t Y + (1 - t) y) < t F (Y) + (1 - t) F (y))) \leftrightarrow (Y < X \to (φ \to \forall t \in (0, 1) F (t Y + (1 - t) X) < t F (Y) + (1 - t) F (X))))$
126	114 125 51	vtocl2ga	$⊢ (Y \in D \land X \in D) \to (Y < X \to (φ \to \forall t \in (0, 1) F (t Y + (1 - t) X) < t F (Y) + (1 - t) F (X)))$
127	102 103 104 126	syl3c	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land (T \in (0, 1) \land Y < X)) \to \forall t \in (0, 1) F (t Y + (1 - t) X) < t F (Y) + (1 - t) F (X)$
128		1re	$⊢ 1 \in ℝ$
129		elioore	$⊢ T \in (0, 1) \to T \in ℝ$
130		resubcl	$⊢ (1 \in ℝ \land T \in ℝ) \to 1 - T \in ℝ$
131	128 129 130	sylancr	$⊢ T \in (0, 1) \to 1 - T \in ℝ$
132		eliooord	$⊢ T \in (0, 1) \to (0 < T \land T < 1)$
133	132	simprd	$⊢ T \in (0, 1) \to T < 1$
134		posdif	$⊢ (T \in ℝ \land 1 \in ℝ) \to (T < 1 \leftrightarrow 0 < 1 - T)$
135	129 128 134	sylancl	$⊢ T \in (0, 1) \to (T < 1 \leftrightarrow 0 < 1 - T)$
136	133 135	mpbid	$⊢ T \in (0, 1) \to 0 < 1 - T$
137	132	simpld	$⊢ T \in (0, 1) \to 0 < T$
138		ltsubpos	$⊢ (T \in ℝ \land 1 \in ℝ) \to (0 < T \leftrightarrow 1 - T < 1)$
139	129 128 138	sylancl	$⊢ T \in (0, 1) \to (0 < T \leftrightarrow 1 - T < 1)$
140	137 139	mpbid	$⊢ T \in (0, 1) \to 1 - T < 1$
141		0xr	$⊢ 0 \in ℝ^{*}$
142		1xr	$⊢ 1 \in ℝ^{*}$
143		elioo2	$⊢ (0 \in ℝ^{} \land 1 \in ℝ^{}) \to (1 - T \in (0, 1) \leftrightarrow (1 - T \in ℝ \land 0 < 1 - T \land 1 - T < 1))$
144	141 142 143	mp2an	$⊢ 1 - T \in (0, 1) \leftrightarrow (1 - T \in ℝ \land 0 < 1 - T \land 1 - T < 1)$
145	131 136 140 144	syl3anbrc	$⊢ T \in (0, 1) \to 1 - T \in (0, 1)$
146	145	ad2antrl	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land (T \in (0, 1) \land Y < X)) \to 1 - T \in (0, 1)$
147	99 127 146	rspcdva	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land (T \in (0, 1) \land Y < X)) \to F ((1 - T) Y + (1 - (1 - T)) X) < (1 - T) F (Y) + (1 - (1 - T)) F (X)$
148	128 60 130	sylancr	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to 1 - T \in ℝ$
149	148 10	remulcld	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to (1 - T) Y \in ℝ$
150	149	recnd	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to (1 - T) Y \in ℂ$
151	60 7	remulcld	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to T X \in ℝ$
152	151	recnd	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to T X \in ℂ$
153		nncan	$⊢ (1 \in ℂ \land T \in ℂ) \to 1 - (1 - T) = T$
154	62 61 153	sylancr	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to 1 - (1 - T) = T$
155	154	oveq1d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to (1 - (1 - T)) X = T X$
156	155	oveq2d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to (1 - T) Y + (1 - (1 - T)) X = (1 - T) Y + T X$
157	150 152 156	comraddd	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to (1 - T) Y + (1 - (1 - T)) X = T X + (1 - T) Y$
158	157	adantr	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land (T \in (0, 1) \land Y < X)) \to (1 - T) Y + (1 - (1 - T)) X = T X + (1 - T) Y$
159	158	fveq2d	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land (T \in (0, 1) \land Y < X)) \to F ((1 - T) Y + (1 - (1 - T)) X) = F (T X + (1 - T) Y)$
160	148 75	remulcld	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to (1 - T) F (Y) \in ℝ$
161	160	recnd	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to (1 - T) F (Y) \in ℂ$
162	74 6	ffvelrnd	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to F (X) \in ℝ$
163	60 162	remulcld	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to T F (X) \in ℝ$
164	163	recnd	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to T F (X) \in ℂ$
165	154	oveq1d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to (1 - (1 - T)) F (X) = T F (X)$
166	165	oveq2d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to (1 - T) F (Y) + (1 - (1 - T)) F (X) = (1 - T) F (Y) + T F (X)$
167	161 164 166	comraddd	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to (1 - T) F (Y) + (1 - (1 - T)) F (X) = T F (X) + (1 - T) F (Y)$
168	167	adantr	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land (T \in (0, 1) \land Y < X)) \to (1 - T) F (Y) + (1 - (1 - T)) F (X) = T F (X) + (1 - T) F (Y)$
169	147 159 168	3brtr3d	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land (T \in (0, 1) \land Y < X)) \to F (T X + (1 - T) Y) < T F (X) + (1 - T) F (Y)$
170	169	orcd	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land (T \in (0, 1) \land Y < X)) \to (F (T X + (1 - T) Y) < T F (X) + (1 - T) F (Y) \lor F (T X + (1 - T) Y) = T F (X) + (1 - T) F (Y))$
171	170	expr	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land T \in (0, 1)) \to (Y < X \to (F (T X + (1 - T) Y) < T F (X) + (1 - T) F (Y) \lor F (T X + (1 - T) Y) = T F (X) + (1 - T) F (Y)))$
172	57 90 171	3jaod	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land T \in (0, 1)) \to ((X < Y \lor X = Y \lor Y < X) \to (F (T X + (1 - T) Y) < T F (X) + (1 - T) F (Y) \lor F (T X + (1 - T) Y) = T F (X) + (1 - T) F (Y)))$
173	12 172	mpd	$⊢ ((φ \land (X \in D \land Y \in D \land T \in [0, 1])) \land T \in (0, 1)) \to (F (T X + (1 - T) Y) < T F (X) + (1 - T) F (Y) \lor F (T X + (1 - T) Y) = T F (X) + (1 - T) F (Y))$
174	173	ex	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to (T \in (0, 1) \to (F (T X + (1 - T) Y) < T F (X) + (1 - T) F (Y) \lor F (T X + (1 - T) Y) = T F (X) + (1 - T) F (Y)))$
175		elpri	$⊢ T \in \{0, 1\} \to (T = 0 \lor T = 1)$
176	76	addid2d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to 0 + F (Y) = F (Y)$
177	162	recnd	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to F (X) \in ℂ$
178	177	mul02d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to 0 \cdot F (X) = 0$
179	178 78	oveq12d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to 0 \cdot F (X) + 1 F (Y) = 0 + F (Y)$
180	7	recnd	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to X \in ℂ$
181	180	mul02d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to 0 \cdot X = 0$
182	181 70	oveq12d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to 0 \cdot X + 1 Y = 0 + Y$
183	68	addid2d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to 0 + Y = Y$
184	182 183	eqtrd	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to 0 \cdot X + 1 Y = Y$
185	184	fveq2d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to F (0 \cdot X + 1 Y) = F (Y)$
186	176 179 185	3eqtr4rd	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to F (0 \cdot X + 1 Y) = 0 \cdot F (X) + 1 F (Y)$
187		oveq1	$⊢ T = 0 \to T X = 0 \cdot X$
188		oveq2	$⊢ T = 0 \to 1 - T = 1 - 0$
189		1m0e1	$⊢ 1 - 0 = 1$
190	188 189	eqtrdi	$⊢ T = 0 \to 1 - T = 1$
191	190	oveq1d	$⊢ T = 0 \to (1 - T) Y = 1 Y$
192	187 191	oveq12d	$⊢ T = 0 \to T X + (1 - T) Y = 0 \cdot X + 1 Y$
193	192	fveq2d	$⊢ T = 0 \to F (T X + (1 - T) Y) = F (0 \cdot X + 1 Y)$
194		oveq1	$⊢ T = 0 \to T F (X) = 0 \cdot F (X)$
195	190	oveq1d	$⊢ T = 0 \to (1 - T) F (Y) = 1 F (Y)$
196	194 195	oveq12d	$⊢ T = 0 \to T F (X) + (1 - T) F (Y) = 0 \cdot F (X) + 1 F (Y)$
197	193 196	eqeq12d	$⊢ T = 0 \to (F (T X + (1 - T) Y) = T F (X) + (1 - T) F (Y) \leftrightarrow F (0 \cdot X + 1 Y) = 0 \cdot F (X) + 1 F (Y))$
198	186 197	syl5ibrcom	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to (T = 0 \to F (T X + (1 - T) Y) = T F (X) + (1 - T) F (Y))$
199	177	addid1d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to F (X) + 0 = F (X)$
200	177	mulid2d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to 1 F (X) = F (X)$
201	76	mul02d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to 0 \cdot F (Y) = 0$
202	200 201	oveq12d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to 1 F (X) + 0 \cdot F (Y) = F (X) + 0$
203	180	mulid2d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to 1 X = X$
204	68	mul02d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to 0 \cdot Y = 0$
205	203 204	oveq12d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to 1 X + 0 \cdot Y = X + 0$
206	180	addid1d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to X + 0 = X$
207	205 206	eqtrd	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to 1 X + 0 \cdot Y = X$
208	207	fveq2d	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to F (1 X + 0 \cdot Y) = F (X)$
209	199 202 208	3eqtr4rd	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to F (1 X + 0 \cdot Y) = 1 F (X) + 0 \cdot F (Y)$
210		oveq1	$⊢ T = 1 \to T X = 1 X$
211		oveq2	$⊢ T = 1 \to 1 - T = 1 - 1$
212		1m1e0	$⊢ 1 - 1 = 0$
213	211 212	eqtrdi	$⊢ T = 1 \to 1 - T = 0$
214	213	oveq1d	$⊢ T = 1 \to (1 - T) Y = 0 \cdot Y$
215	210 214	oveq12d	$⊢ T = 1 \to T X + (1 - T) Y = 1 X + 0 \cdot Y$
216	215	fveq2d	$⊢ T = 1 \to F (T X + (1 - T) Y) = F (1 X + 0 \cdot Y)$
217		oveq1	$⊢ T = 1 \to T F (X) = 1 F (X)$
218	213	oveq1d	$⊢ T = 1 \to (1 - T) F (Y) = 0 \cdot F (Y)$
219	217 218	oveq12d	$⊢ T = 1 \to T F (X) + (1 - T) F (Y) = 1 F (X) + 0 \cdot F (Y)$
220	216 219	eqeq12d	$⊢ T = 1 \to (F (T X + (1 - T) Y) = T F (X) + (1 - T) F (Y) \leftrightarrow F (1 X + 0 \cdot Y) = 1 F (X) + 0 \cdot F (Y))$
221	209 220	syl5ibrcom	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to (T = 1 \to F (T X + (1 - T) Y) = T F (X) + (1 - T) F (Y))$
222	198 221	jaod	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to ((T = 0 \lor T = 1) \to F (T X + (1 - T) Y) = T F (X) + (1 - T) F (Y))$
223	175 222 89	syl56	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to (T \in \{0, 1\} \to (F (T X + (1 - T) Y) < T F (X) + (1 - T) F (Y) \lor F (T X + (1 - T) Y) = T F (X) + (1 - T) F (Y)))$
224		0le1	$⊢ 0 \leq 1$
225		prunioo	$⊢ (0 \in ℝ^{} \land 1 \in ℝ^{} \land 0 \leq 1) \to (0, 1) \cup \{0, 1\} = [0, 1]$
226	141 142 224 225	mp3an	$⊢ (0, 1) \cup \{0, 1\} = [0, 1]$
227	59 226	eleqtrrdi	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to T \in ((0, 1) \cup \{0, 1\})$
228		elun	$⊢ T \in ((0, 1) \cup \{0, 1\}) \leftrightarrow (T \in (0, 1) \lor T \in \{0, 1\})$
229	227 228	sylib	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to (T \in (0, 1) \lor T \in \{0, 1\})$
230	174 223 229	mpjaod	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to (F (T X + (1 - T) Y) < T F (X) + (1 - T) F (Y) \lor F (T X + (1 - T) Y) = T F (X) + (1 - T) F (Y))$
231	1 3	cvxcl	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to T X + (1 - T) Y \in D$
232	74 231	ffvelrnd	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to F (T X + (1 - T) Y) \in ℝ$
233	163 160	readdcld	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to T F (X) + (1 - T) F (Y) \in ℝ$
234	232 233	leloed	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to (F (T X + (1 - T) Y) \leq T F (X) + (1 - T) F (Y) \leftrightarrow (F (T X + (1 - T) Y) < T F (X) + (1 - T) F (Y) \lor F (T X + (1 - T) Y) = T F (X) + (1 - T) F (Y)))$
235	230 234	mpbird	$⊢ (φ \land (X \in D \land Y \in D \land T \in [0, 1])) \to F (T X + (1 - T) Y) \leq T F (X) + (1 - T) F (Y)$

Metamath Proof Explorer

Theorem scvxcvx

Proof