scvxcvx - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > scvxcvx		Unicode version

Theorem scvxcvx 20781

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

**Hypotheses**
Ref	Expression
scvxcvx.1
scvxcvx.2
scvxcvx.3	$/\$ $/\$
scvxcvx.4	$/\$ $/\$ $/\$ $/\$

**Assertion**
Ref	Expression
scvxcvx	$/\$ $/\$ $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

**Proof of Theorem scvxcvx**
Step	Hyp	Ref	Expression
1		scvxcvx.1	. . . . . . . . 9
2	1	adantr 452	. . . . . . . 8 $/\$ $/\$ $/\$
3		simpr1 963	. . . . . . . 8 $/\$ $/\$ $/\$
4	2, 3	sseldd 3313	. . . . . . 7 $/\$ $/\$ $/\$
5	4	adantr 452	. . . . . 6 $/\$ $/\$ $/\$ $/\$
6		simpr2 964	. . . . . . . 8 $/\$ $/\$ $/\$
7	2, 6	sseldd 3313	. . . . . . 7 $/\$ $/\$ $/\$
8	7	adantr 452	. . . . . 6 $/\$ $/\$ $/\$ $/\$
9	5, 8	lttri4d 9174	. . . . 5 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
10		simprl 733	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
11	3	adantr 452	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
12	6	adantr 452	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
13	11, 12	jca 519	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
14		simprr 734	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
15		simpll 731	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
16		breq1 4179	. . . . . . . . . . . 12
17		oveq2 6052	. . . . . . . . . . . . . . . . 17
18	17	oveq1d 6059	. . . . . . . . . . . . . . . 16
19	18	fveq2d 5695	. . . . . . . . . . . . . . 15
20		fveq2 5691	. . . . . . . . . . . . . . . . 17
21	20	oveq2d 6060	. . . . . . . . . . . . . . . 16
22	21	oveq1d 6059	. . . . . . . . . . . . . . 15
23	19, 22	breq12d 4189	. . . . . . . . . . . . . 14
24	23	ralbidv 2690	. . . . . . . . . . . . 13
25	24	imbi2d 308	. . . . . . . . . . . 12
26	16, 25	imbi12d 312	. . . . . . . . . . 11
27		breq2 4180	. . . . . . . . . . . 12
28		oveq2 6052	. . . . . . . . . . . . . . . . 17
29	28	oveq2d 6060	. . . . . . . . . . . . . . . 16
30	29	fveq2d 5695	. . . . . . . . . . . . . . 15
31		fveq2 5691	. . . . . . . . . . . . . . . . 17
32	31	oveq2d 6060	. . . . . . . . . . . . . . . 16
33	32	oveq2d 6060	. . . . . . . . . . . . . . 15
34	30, 33	breq12d 4189	. . . . . . . . . . . . . 14
35	34	ralbidv 2690	. . . . . . . . . . . . 13
36	35	imbi2d 308	. . . . . . . . . . . 12
37	27, 36	imbi12d 312	. . . . . . . . . . 11
38		scvxcvx.4	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
39	38	3expia 1155	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
40	39	ralrimiv 2752	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
41	40	expcom 425	. . . . . . . . . . . 12 $/\$ $/\$
42	41	3expia 1155	. . . . . . . . . . 11 $/\$
43	26, 37, 42	vtocl2ga 2983	. . . . . . . . . 10 $/\$
44	13, 14, 15, 43	syl3c 59	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
45		oveq1 6051	. . . . . . . . . . . . 13
46		oveq2 6052	. . . . . . . . . . . . . 14
47	46	oveq1d 6059	. . . . . . . . . . . . 13
48	45, 47	oveq12d 6062	. . . . . . . . . . . 12
49	48	fveq2d 5695	. . . . . . . . . . 11
50		oveq1 6051	. . . . . . . . . . . 12
51	46	oveq1d 6059	. . . . . . . . . . . 12
52	50, 51	oveq12d 6062	. . . . . . . . . . 11
53	49, 52	breq12d 4189	. . . . . . . . . 10
54	53	rspcv 3012	. . . . . . . . 9
55	10, 44, 54	sylc 58	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
56	55	orcd 382	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
57	56	expr 599	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\/$
58		unitssre 11002	. . . . . . . . . . . . . . . 16
59		simpr3 965	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
60	58, 59	sseldi 3310	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
61	60	recnd 9074	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
62		ax-1cn 9008	. . . . . . . . . . . . . 14
63		pncan3 9273	. . . . . . . . . . . . . 14 $/\$
64	61, 62, 63	sylancl 644	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
65	64	oveq1d 6059	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
66		subcl 9265	. . . . . . . . . . . . . 14 $/\$
67	62, 61, 66	sylancr 645	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
68	7	recnd 9074	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
69	61, 67, 68	adddird 9073	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
70	68	mulid2d 9066	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
71	65, 69, 70	3eqtr3d 2448	. . . . . . . . . . 11 $/\$ $/\$ $/\$
72	71	fveq2d 5695	. . . . . . . . . 10 $/\$ $/\$ $/\$
73	64	oveq1d 6059	. . . . . . . . . . 11 $/\$ $/\$ $/\$
74		scvxcvx.2	. . . . . . . . . . . . . . 15
75	74	adantr 452	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
76	75, 6	ffvelrnd 5834	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
77	76	recnd 9074	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
78	61, 67, 77	adddird 9073	. . . . . . . . . . 11 $/\$ $/\$ $/\$
79	77	mulid2d 9066	. . . . . . . . . . 11 $/\$ $/\$ $/\$
80	73, 78, 79	3eqtr3d 2448	. . . . . . . . . 10 $/\$ $/\$ $/\$
81	72, 80	eqtr4d 2443	. . . . . . . . 9 $/\$ $/\$ $/\$
82	81	adantr 452	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
83		oveq2 6052	. . . . . . . . . . 11
84	83	oveq1d 6059	. . . . . . . . . 10
85	84	fveq2d 5695	. . . . . . . . 9
86		fveq2 5691	. . . . . . . . . . 11
87	86	oveq2d 6060	. . . . . . . . . 10
88	87	oveq1d 6059	. . . . . . . . 9
89	85, 88	eqeq12d 2422	. . . . . . . 8
90	82, 89	syl5ibrcom 214	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
91		olc 374	. . . . . . 7 $\/$
92	90, 91	syl6 31	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\/$
93		1re 9050	. . . . . . . . . . . . 13
94		elioore 10906	. . . . . . . . . . . . 13
95		resubcl 9325	. . . . . . . . . . . . 13 $/\$
96	93, 94, 95	sylancr 645	. . . . . . . . . . . 12
97		eliooord 10930	. . . . . . . . . . . . . 14 $/\$
98	97	simprd 450	. . . . . . . . . . . . 13
99		posdif 9481	. . . . . . . . . . . . . 14 $/\$
100	94, 93, 99	sylancl 644	. . . . . . . . . . . . 13
101	98, 100	mpbid 202	. . . . . . . . . . . 12
102	97	simpld 446	. . . . . . . . . . . . 13
103		ltsubpos 9480	. . . . . . . . . . . . . 14 $/\$
104	94, 93, 103	sylancl 644	. . . . . . . . . . . . 13
105	102, 104	mpbid 202	. . . . . . . . . . . 12
106		0xr 9091	. . . . . . . . . . . . 13
107	93	rexri 9097	. . . . . . . . . . . . 13
108		elioo2 10917	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
109	106, 107, 108	mp2an 654	. . . . . . . . . . . 12 $/\$ $/\$
110	96, 101, 105, 109	syl3anbrc 1138	. . . . . . . . . . 11
111	110	ad2antrl 709	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
112	6	adantr 452	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
113	3	adantr 452	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
114	112, 113	jca 519	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
115		simprr 734	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
116		simpll 731	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
117		breq1 4179	. . . . . . . . . . . . 13
118		oveq2 6052	. . . . . . . . . . . . . . . . . 18
119	118	oveq1d 6059	. . . . . . . . . . . . . . . . 17
120	119	fveq2d 5695	. . . . . . . . . . . . . . . 16
121		fveq2 5691	. . . . . . . . . . . . . . . . . 18
122	121	oveq2d 6060	. . . . . . . . . . . . . . . . 17
123	122	oveq1d 6059	. . . . . . . . . . . . . . . 16
124	120, 123	breq12d 4189	. . . . . . . . . . . . . . 15
125	124	ralbidv 2690	. . . . . . . . . . . . . 14
126	125	imbi2d 308	. . . . . . . . . . . . 13
127	117, 126	imbi12d 312	. . . . . . . . . . . 12
128		breq2 4180	. . . . . . . . . . . . 13
129		oveq2 6052	. . . . . . . . . . . . . . . . . 18
130	129	oveq2d 6060	. . . . . . . . . . . . . . . . 17
131	130	fveq2d 5695	. . . . . . . . . . . . . . . 16
132		fveq2 5691	. . . . . . . . . . . . . . . . . 18
133	132	oveq2d 6060	. . . . . . . . . . . . . . . . 17
134	133	oveq2d 6060	. . . . . . . . . . . . . . . 16
135	131, 134	breq12d 4189	. . . . . . . . . . . . . . 15
136	135	ralbidv 2690	. . . . . . . . . . . . . 14
137	136	imbi2d 308	. . . . . . . . . . . . 13
138	128, 137	imbi12d 312	. . . . . . . . . . . 12
139	127, 138, 42	vtocl2ga 2983	. . . . . . . . . . 11 $/\$
140	114, 115, 116, 139	syl3c 59	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
141		oveq1 6051	. . . . . . . . . . . . . 14
142		oveq2 6052	. . . . . . . . . . . . . . 15
143	142	oveq1d 6059	. . . . . . . . . . . . . 14
144	141, 143	oveq12d 6062	. . . . . . . . . . . . 13
145	144	fveq2d 5695	. . . . . . . . . . . 12
146		oveq1 6051	. . . . . . . . . . . . 13
147	142	oveq1d 6059	. . . . . . . . . . . . 13
148	146, 147	oveq12d 6062	. . . . . . . . . . . 12
149	145, 148	breq12d 4189	. . . . . . . . . . 11
150	149	rspcv 3012	. . . . . . . . . 10
151	111, 140, 150	sylc 58	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
152		nncan 9290	. . . . . . . . . . . . . . 15 $/\$
153	62, 61, 152	sylancr 645	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
154	153	oveq1d 6059	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
155	154	oveq2d 6060	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
156	93, 60, 95	sylancr 645	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
157	156, 7	remulcld 9076	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
158	157	recnd 9074	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
159	60, 4	remulcld 9076	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
160	159	recnd 9074	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
161	158, 160	addcomd 9228	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
162	155, 161	eqtrd 2440	. . . . . . . . . . 11 $/\$ $/\$ $/\$
163	162	adantr 452	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
164	163	fveq2d 5695	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
165	153	oveq1d 6059	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
166	165	oveq2d 6060	. . . . . . . . . . 11 $/\$ $/\$ $/\$
167	156, 76	remulcld 9076	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
168	167	recnd 9074	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
169	75, 3	ffvelrnd 5834	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
170	60, 169	remulcld 9076	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
171	170	recnd 9074	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
172	168, 171	addcomd 9228	. . . . . . . . . . 11 $/\$ $/\$ $/\$
173	166, 172	eqtrd 2440	. . . . . . . . . 10 $/\$ $/\$ $/\$
174	173	adantr 452	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
175	151, 164, 174	3brtr3d 4205	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
176	175	orcd 382	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
177	176	expr 599	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\/$
178	57, 92, 177	3jaod 1248	. . . . 5 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$ $\/$
179	9, 178	mpd 15	. . . 4 $/\$ $/\$ $/\$ $/\$ $\/$
180	179	ex 424	. . 3 $/\$ $/\$ $/\$ $\/$
181		elpri 3798	. . . 4 $\/$
182	77	addid2d 9227	. . . . . . 7 $/\$ $/\$ $/\$
183	169	recnd 9074	. . . . . . . . 9 $/\$ $/\$ $/\$
184	183	mul02d 9224	. . . . . . . 8 $/\$ $/\$ $/\$
185	184, 79	oveq12d 6062	. . . . . . 7 $/\$ $/\$ $/\$
186	4	recnd 9074	. . . . . . . . . . 11 $/\$ $/\$ $/\$
187	186	mul02d 9224	. . . . . . . . . 10 $/\$ $/\$ $/\$
188	187, 70	oveq12d 6062	. . . . . . . . 9 $/\$ $/\$ $/\$
189	68	addid2d 9227	. . . . . . . . 9 $/\$ $/\$ $/\$
190	188, 189	eqtrd 2440	. . . . . . . 8 $/\$ $/\$ $/\$
191	190	fveq2d 5695	. . . . . . 7 $/\$ $/\$ $/\$
192	182, 185, 191	3eqtr4rd 2451	. . . . . 6 $/\$ $/\$ $/\$
193		oveq1 6051	. . . . . . . . 9
194		oveq2 6052	. . . . . . . . . . 11
195	62	subid1i 9332	. . . . . . . . . . 11
196	194, 195	syl6eq 2456	. . . . . . . . . 10
197	196	oveq1d 6059	. . . . . . . . 9
198	193, 197	oveq12d 6062	. . . . . . . 8
199	198	fveq2d 5695	. . . . . . 7
200		oveq1 6051	. . . . . . . 8
201	196	oveq1d 6059	. . . . . . . 8
202	200, 201	oveq12d 6062	. . . . . . 7
203	199, 202	eqeq12d 2422	. . . . . 6
204	192, 203	syl5ibrcom 214	. . . . 5 $/\$ $/\$ $/\$
205	183	addid1d 9226	. . . . . . 7 $/\$ $/\$ $/\$
206	183	mulid2d 9066	. . . . . . . 8 $/\$ $/\$ $/\$
207	77	mul02d 9224	. . . . . . . 8 $/\$ $/\$ $/\$
208	206, 207	oveq12d 6062	. . . . . . 7 $/\$ $/\$ $/\$
209	186	mulid2d 9066	. . . . . . . . . 10 $/\$ $/\$ $/\$
210	68	mul02d 9224	. . . . . . . . . 10 $/\$ $/\$ $/\$
211	209, 210	oveq12d 6062	. . . . . . . . 9 $/\$ $/\$ $/\$
212	186	addid1d 9226	. . . . . . . . 9 $/\$ $/\$ $/\$
213	211, 212	eqtrd 2440	. . . . . . . 8 $/\$ $/\$ $/\$
214	213	fveq2d 5695	. . . . . . 7 $/\$ $/\$ $/\$
215	205, 208, 214	3eqtr4rd 2451	. . . . . 6 $/\$ $/\$ $/\$
216		oveq1 6051	. . . . . . . . 9
217		oveq2 6052	. . . . . . . . . . 11
218		1m1e0 10028	. . . . . . . . . . 11
219	217, 218	syl6eq 2456	. . . . . . . . . 10
220	219	oveq1d 6059	. . . . . . . . 9
221	216, 220	oveq12d 6062	. . . . . . . 8
222	221	fveq2d 5695	. . . . . . 7
223		oveq1 6051	. . . . . . . 8
224	219	oveq1d 6059	. . . . . . . 8
225	223, 224	oveq12d 6062	. . . . . . 7
226	222, 225	eqeq12d 2422	. . . . . 6
227	215, 226	syl5ibrcom 214	. . . . 5 $/\$ $/\$ $/\$
228	204, 227	jaod 370	. . . 4 $/\$ $/\$ $/\$ $\/$
229	181, 228, 91	syl56 32	. . 3 $/\$ $/\$ $/\$ $\/$
230		0le1 9511	. . . . . 6
231		prunioo 10985	. . . . . 6 $/\$ $/\$
232	106, 107, 230, 231	mp3an 1279	. . . . 5
233	59, 232	syl6eleqr 2499	. . . 4 $/\$ $/\$ $/\$
234		elun 3452	. . . 4 $\/$
235	233, 234	sylib 189	. . 3 $/\$ $/\$ $/\$ $\/$
236	180, 229, 235	mpjaod 371	. 2 $/\$ $/\$ $/\$ $\/$
237		scvxcvx.3	. . . . 5 $/\$ $/\$
238	1, 237	cvxcl 20780	. . . 4 $/\$ $/\$ $/\$
239	75, 238	ffvelrnd 5834	. . 3 $/\$ $/\$ $/\$
240	170, 167	readdcld 9075	. . 3 $/\$ $/\$ $/\$
241	239, 240	leloed 9176	. 2 $/\$ $/\$ $/\$ $\/$
242	236, 241	mpbird 224	1 $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4

wb 177 $\/$ wo 358 $/\$ wa 359 $\/$ w3o 935 $/\$ w3a 936

wceq 1649

wcel 1721

wral 2670

cun 3282

wss 3284

cpr 3779 class class class wbr 4176

wf 5413

cfv 5417 (class class class)co 6044

cc 8948

cr 8949

cc0 8950

c1 8951

caddc 8953

cmul 8955

cxr 9079

clt 9080

cle 9081

cmin 9251

cioo 10876

cicc 10879

This theorem is referenced by: amgmlem 20785

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2389 ax-sep 4294 ax-nul 4302 ax-pow 4341 ax-pr 4367 ax-un 4664 ax-cnex 9006 ax-resscn 9007 ax-1cn 9008 ax-icn 9009 ax-addcl 9010 ax-addrcl 9011 ax-mulcl 9012 ax-mulrcl 9013 ax-mulcom 9014 ax-addass 9015 ax-mulass 9016 ax-distr 9017 ax-i2m1 9018 ax-1ne0 9019 ax-1rid 9020 ax-rnegex 9021 ax-rrecex 9022 ax-cnre 9023 ax-pre-lttri 9024 ax-pre-lttrn 9025 ax-pre-ltadd 9026 ax-pre-mulgt0 9027 ax-pre-sup 9028

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2262 df-mo 2263 df-clab 2395 df-cleq 2401 df-clel 2404 df-nfc 2533 df-ne 2573 df-nel 2574 df-ral 2675 df-rex 2676 df-reu 2677 df-rmo 2678 df-rab 2679 df-v 2922 df-sbc 3126 df-csb 3216 df-dif 3287 df-un 3289 df-in 3291 df-ss 3298 df-pss 3300 df-nul 3593 df-if 3704 df-pw 3765 df-sn 3784 df-pr 3785 df-tp 3786 df-op 3787 df-uni 3980 df-iun 4059 df-br 4177 df-opab 4231 df-mpt 4232 df-tr 4267 df-eprel 4458 df-id 4462 df-po 4467 df-so 4468 df-fr 4505 df-we 4507 df-ord 4548 df-on 4549 df-lim 4550 df-suc 4551 df-om 4809 df-xp 4847 df-rel 4848 df-cnv 4849 df-co 4850 df-dm 4851 df-rn 4852 df-res 4853 df-ima 4854 df-iota 5381 df-fun 5419 df-fn 5420 df-f 5421 df-f1 5422 df-fo 5423 df-f1o 5424 df-fv 5425 df-ov 6047 df-oprab 6048 df-mpt2 6049 df-1st 6312 df-2nd 6313 df-riota 6512 df-recs 6596 df-rdg 6631 df-er 6868 df-en 7073 df-dom 7074 df-sdom 7075 df-sup 7408 df-pnf 9082 df-mnf 9083 df-xr 9084 df-ltxr 9085 df-le 9086 df-sub 9253 df-neg 9254 df-div 9638 df-nn 9961 df-n0 10182 df-z 10243 df-uz 10449 df-q 10535 df-rp 10573 df-ioo 10880 df-ico 10882 df-icc 10883

W3C validator