scvxcvx - Metamath Proof Explorer

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

Theorem scvxcvx 24712

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 481	. . . . . . . 8 $/\$ $/\$ $/\$
3		simpr1 1067	. . . . . . . 8 $/\$ $/\$ $/\$
4	2, 3	sseldd 3604	. . . . . . 7 $/\$ $/\$ $/\$
5	4	adantr 481	. . . . . 6 $/\$ $/\$ $/\$ $/\$
6		simpr2 1068	. . . . . . . 8 $/\$ $/\$ $/\$
7	2, 6	sseldd 3604	. . . . . . 7 $/\$ $/\$ $/\$
8	7	adantr 481	. . . . . 6 $/\$ $/\$ $/\$ $/\$
9	5, 8	lttri4d 10178	. . . . 5 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
10		simprl 794	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
11	3	adantr 481	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
12	6	adantr 481	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
13	11, 12	jca 554	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
14		simprr 796	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
15		simpll 790	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
16		breq1 4656	. . . . . . . . . . . 12
17		oveq2 6658	. . . . . . . . . . . . . . . . 17
18	17	oveq1d 6665	. . . . . . . . . . . . . . . 16
19	18	fveq2d 6195	. . . . . . . . . . . . . . 15
20		fveq2 6191	. . . . . . . . . . . . . . . . 17
21	20	oveq2d 6666	. . . . . . . . . . . . . . . 16
22	21	oveq1d 6665	. . . . . . . . . . . . . . 15
23	19, 22	breq12d 4666	. . . . . . . . . . . . . 14
24	23	ralbidv 2986	. . . . . . . . . . . . 13
25	24	imbi2d 330	. . . . . . . . . . . 12
26	16, 25	imbi12d 334	. . . . . . . . . . 11
27		breq2 4657	. . . . . . . . . . . 12
28		oveq2 6658	. . . . . . . . . . . . . . . . 17
29	28	oveq2d 6666	. . . . . . . . . . . . . . . 16
30	29	fveq2d 6195	. . . . . . . . . . . . . . 15
31		fveq2 6191	. . . . . . . . . . . . . . . . 17
32	31	oveq2d 6666	. . . . . . . . . . . . . . . 16
33	32	oveq2d 6666	. . . . . . . . . . . . . . 15
34	30, 33	breq12d 4666	. . . . . . . . . . . . . 14
35	34	ralbidv 2986	. . . . . . . . . . . . 13
36	35	imbi2d 330	. . . . . . . . . . . 12
37	27, 36	imbi12d 334	. . . . . . . . . . 11
38		scvxcvx.4	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
39	38	3expia 1267	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
40	39	ralrimiv 2965	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
41	40	expcom 451	. . . . . . . . . . . 12 $/\$ $/\$
42	41	3expia 1267	. . . . . . . . . . 11 $/\$
43	26, 37, 42	vtocl2ga 3274	. . . . . . . . . 10 $/\$
44	13, 14, 15, 43	syl3c 66	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
45		oveq1 6657	. . . . . . . . . . . . 13
46		oveq2 6658	. . . . . . . . . . . . . 14
47	46	oveq1d 6665	. . . . . . . . . . . . 13
48	45, 47	oveq12d 6668	. . . . . . . . . . . 12
49	48	fveq2d 6195	. . . . . . . . . . 11
50		oveq1 6657	. . . . . . . . . . . 12
51	46	oveq1d 6665	. . . . . . . . . . . 12
52	50, 51	oveq12d 6668	. . . . . . . . . . 11
53	49, 52	breq12d 4666	. . . . . . . . . 10
54	53	rspcv 3305	. . . . . . . . 9
55	10, 44, 54	sylc 65	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
56	55	orcd 407	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
57	56	expr 643	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\/$
58		unitssre 12319	. . . . . . . . . . . . . . . 16
59		simpr3 1069	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
60	58, 59	sseldi 3601	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
61	60	recnd 10068	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
62		ax-1cn 9994	. . . . . . . . . . . . . 14
63		pncan3 10289	. . . . . . . . . . . . . 14 $/\$
64	61, 62, 63	sylancl 694	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
65	64	oveq1d 6665	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
66		subcl 10280	. . . . . . . . . . . . . 14 $/\$
67	62, 61, 66	sylancr 695	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
68	7	recnd 10068	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
69	61, 67, 68	adddird 10065	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
70	68	mulid2d 10058	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
71	65, 69, 70	3eqtr3d 2664	. . . . . . . . . . 11 $/\$ $/\$ $/\$
72	71	fveq2d 6195	. . . . . . . . . 10 $/\$ $/\$ $/\$
73	64	oveq1d 6665	. . . . . . . . . . 11 $/\$ $/\$ $/\$
74		scvxcvx.2	. . . . . . . . . . . . . . 15
75	74	adantr 481	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
76	75, 6	ffvelrnd 6360	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
77	76	recnd 10068	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
78	61, 67, 77	adddird 10065	. . . . . . . . . . 11 $/\$ $/\$ $/\$
79	77	mulid2d 10058	. . . . . . . . . . 11 $/\$ $/\$ $/\$
80	73, 78, 79	3eqtr3d 2664	. . . . . . . . . 10 $/\$ $/\$ $/\$
81	72, 80	eqtr4d 2659	. . . . . . . . 9 $/\$ $/\$ $/\$
82	81	adantr 481	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
83		oveq2 6658	. . . . . . . . . . 11
84	83	oveq1d 6665	. . . . . . . . . 10
85	84	fveq2d 6195	. . . . . . . . 9
86		fveq2 6191	. . . . . . . . . . 11
87	86	oveq2d 6666	. . . . . . . . . 10
88	87	oveq1d 6665	. . . . . . . . 9
89	85, 88	eqeq12d 2637	. . . . . . . 8
90	82, 89	syl5ibrcom 237	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
91		olc 399	. . . . . . 7 $\/$
92	90, 91	syl6 35	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\/$
93		1re 10039	. . . . . . . . . . . . 13
94		elioore 12205	. . . . . . . . . . . . 13
95		resubcl 10345	. . . . . . . . . . . . 13 $/\$
96	93, 94, 95	sylancr 695	. . . . . . . . . . . 12
97		eliooord 12233	. . . . . . . . . . . . . 14 $/\$
98	97	simprd 479	. . . . . . . . . . . . 13
99		posdif 10521	. . . . . . . . . . . . . 14 $/\$
100	94, 93, 99	sylancl 694	. . . . . . . . . . . . 13
101	98, 100	mpbid 222	. . . . . . . . . . . 12
102	97	simpld 475	. . . . . . . . . . . . 13
103		ltsubpos 10520	. . . . . . . . . . . . . 14 $/\$
104	94, 93, 103	sylancl 694	. . . . . . . . . . . . 13
105	102, 104	mpbid 222	. . . . . . . . . . . 12
106		0xr 10086	. . . . . . . . . . . . 13
107	93	rexri 10097	. . . . . . . . . . . . 13
108		elioo2 12216	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
109	106, 107, 108	mp2an 708	. . . . . . . . . . . 12 $/\$ $/\$
110	96, 101, 105, 109	syl3anbrc 1246	. . . . . . . . . . 11
111	110	ad2antrl 764	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
112	6	adantr 481	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
113	3	adantr 481	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
114	112, 113	jca 554	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
115		simprr 796	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
116		simpll 790	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
117		breq1 4656	. . . . . . . . . . . . 13
118		oveq2 6658	. . . . . . . . . . . . . . . . . 18
119	118	oveq1d 6665	. . . . . . . . . . . . . . . . 17
120	119	fveq2d 6195	. . . . . . . . . . . . . . . 16
121		fveq2 6191	. . . . . . . . . . . . . . . . . 18
122	121	oveq2d 6666	. . . . . . . . . . . . . . . . 17
123	122	oveq1d 6665	. . . . . . . . . . . . . . . 16
124	120, 123	breq12d 4666	. . . . . . . . . . . . . . 15
125	124	ralbidv 2986	. . . . . . . . . . . . . 14
126	125	imbi2d 330	. . . . . . . . . . . . 13
127	117, 126	imbi12d 334	. . . . . . . . . . . 12
128		breq2 4657	. . . . . . . . . . . . 13
129		oveq2 6658	. . . . . . . . . . . . . . . . . 18
130	129	oveq2d 6666	. . . . . . . . . . . . . . . . 17
131	130	fveq2d 6195	. . . . . . . . . . . . . . . 16
132		fveq2 6191	. . . . . . . . . . . . . . . . . 18
133	132	oveq2d 6666	. . . . . . . . . . . . . . . . 17
134	133	oveq2d 6666	. . . . . . . . . . . . . . . 16
135	131, 134	breq12d 4666	. . . . . . . . . . . . . . 15
136	135	ralbidv 2986	. . . . . . . . . . . . . 14
137	136	imbi2d 330	. . . . . . . . . . . . 13
138	128, 137	imbi12d 334	. . . . . . . . . . . 12
139	127, 138, 42	vtocl2ga 3274	. . . . . . . . . . 11 $/\$
140	114, 115, 116, 139	syl3c 66	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
141		oveq1 6657	. . . . . . . . . . . . . 14
142		oveq2 6658	. . . . . . . . . . . . . . 15
143	142	oveq1d 6665	. . . . . . . . . . . . . 14
144	141, 143	oveq12d 6668	. . . . . . . . . . . . 13
145	144	fveq2d 6195	. . . . . . . . . . . 12
146		oveq1 6657	. . . . . . . . . . . . 13
147	142	oveq1d 6665	. . . . . . . . . . . . 13
148	146, 147	oveq12d 6668	. . . . . . . . . . . 12
149	145, 148	breq12d 4666	. . . . . . . . . . 11
150	149	rspcv 3305	. . . . . . . . . 10
151	111, 140, 150	sylc 65	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
152		nncan 10310	. . . . . . . . . . . . . . 15 $/\$
153	62, 61, 152	sylancr 695	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
154	153	oveq1d 6665	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
155	154	oveq2d 6666	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
156	93, 60, 95	sylancr 695	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
157	156, 7	remulcld 10070	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
158	157	recnd 10068	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
159	60, 4	remulcld 10070	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
160	159	recnd 10068	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
161	158, 160	addcomd 10238	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
162	155, 161	eqtrd 2656	. . . . . . . . . . 11 $/\$ $/\$ $/\$
163	162	adantr 481	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
164	163	fveq2d 6195	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
165	153	oveq1d 6665	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
166	165	oveq2d 6666	. . . . . . . . . . 11 $/\$ $/\$ $/\$
167	156, 76	remulcld 10070	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
168	167	recnd 10068	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
169	75, 3	ffvelrnd 6360	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
170	60, 169	remulcld 10070	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
171	170	recnd 10068	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
172	168, 171	addcomd 10238	. . . . . . . . . . 11 $/\$ $/\$ $/\$
173	166, 172	eqtrd 2656	. . . . . . . . . 10 $/\$ $/\$ $/\$
174	173	adantr 481	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
175	151, 164, 174	3brtr3d 4684	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
176	175	orcd 407	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
177	176	expr 643	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\/$
178	57, 92, 177	3jaod 1392	. . . . 5 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$ $\/$
179	9, 178	mpd 15	. . . 4 $/\$ $/\$ $/\$ $/\$ $\/$
180	179	ex 450	. . 3 $/\$ $/\$ $/\$ $\/$
181		elpri 4197	. . . 4 $\/$
182	77	addid2d 10237	. . . . . . 7 $/\$ $/\$ $/\$
183	169	recnd 10068	. . . . . . . . 9 $/\$ $/\$ $/\$
184	183	mul02d 10234	. . . . . . . 8 $/\$ $/\$ $/\$
185	184, 79	oveq12d 6668	. . . . . . 7 $/\$ $/\$ $/\$
186	4	recnd 10068	. . . . . . . . . . 11 $/\$ $/\$ $/\$
187	186	mul02d 10234	. . . . . . . . . 10 $/\$ $/\$ $/\$
188	187, 70	oveq12d 6668	. . . . . . . . 9 $/\$ $/\$ $/\$
189	68	addid2d 10237	. . . . . . . . 9 $/\$ $/\$ $/\$
190	188, 189	eqtrd 2656	. . . . . . . 8 $/\$ $/\$ $/\$
191	190	fveq2d 6195	. . . . . . 7 $/\$ $/\$ $/\$
192	182, 185, 191	3eqtr4rd 2667	. . . . . 6 $/\$ $/\$ $/\$
193		oveq1 6657	. . . . . . . . 9
194		oveq2 6658	. . . . . . . . . . 11
195		1m0e1 11131	. . . . . . . . . . 11
196	194, 195	syl6eq 2672	. . . . . . . . . 10
197	196	oveq1d 6665	. . . . . . . . 9
198	193, 197	oveq12d 6668	. . . . . . . 8
199	198	fveq2d 6195	. . . . . . 7
200		oveq1 6657	. . . . . . . 8
201	196	oveq1d 6665	. . . . . . . 8
202	200, 201	oveq12d 6668	. . . . . . 7
203	199, 202	eqeq12d 2637	. . . . . 6
204	192, 203	syl5ibrcom 237	. . . . 5 $/\$ $/\$ $/\$
205	183	addid1d 10236	. . . . . . 7 $/\$ $/\$ $/\$
206	183	mulid2d 10058	. . . . . . . 8 $/\$ $/\$ $/\$
207	77	mul02d 10234	. . . . . . . 8 $/\$ $/\$ $/\$
208	206, 207	oveq12d 6668	. . . . . . 7 $/\$ $/\$ $/\$
209	186	mulid2d 10058	. . . . . . . . . 10 $/\$ $/\$ $/\$
210	68	mul02d 10234	. . . . . . . . . 10 $/\$ $/\$ $/\$
211	209, 210	oveq12d 6668	. . . . . . . . 9 $/\$ $/\$ $/\$
212	186	addid1d 10236	. . . . . . . . 9 $/\$ $/\$ $/\$
213	211, 212	eqtrd 2656	. . . . . . . 8 $/\$ $/\$ $/\$
214	213	fveq2d 6195	. . . . . . 7 $/\$ $/\$ $/\$
215	205, 208, 214	3eqtr4rd 2667	. . . . . 6 $/\$ $/\$ $/\$
216		oveq1 6657	. . . . . . . . 9
217		oveq2 6658	. . . . . . . . . . 11
218		1m1e0 11089	. . . . . . . . . . 11
219	217, 218	syl6eq 2672	. . . . . . . . . 10
220	219	oveq1d 6665	. . . . . . . . 9
221	216, 220	oveq12d 6668	. . . . . . . 8
222	221	fveq2d 6195	. . . . . . 7
223		oveq1 6657	. . . . . . . 8
224	219	oveq1d 6665	. . . . . . . 8
225	223, 224	oveq12d 6668	. . . . . . 7
226	222, 225	eqeq12d 2637	. . . . . 6
227	215, 226	syl5ibrcom 237	. . . . 5 $/\$ $/\$ $/\$
228	204, 227	jaod 395	. . . 4 $/\$ $/\$ $/\$ $\/$
229	181, 228, 91	syl56 36	. . 3 $/\$ $/\$ $/\$ $\/$
230		0le1 10551	. . . . . 6
231		prunioo 12301	. . . . . 6 $/\$ $/\$
232	106, 107, 230, 231	mp3an 1424	. . . . 5
233	59, 232	syl6eleqr 2712	. . . 4 $/\$ $/\$ $/\$
234		elun 3753	. . . 4 $\/$
235	233, 234	sylib 208	. . 3 $/\$ $/\$ $/\$ $\/$
236	180, 229, 235	mpjaod 396	. 2 $/\$ $/\$ $/\$ $\/$
237		scvxcvx.3	. . . . 5 $/\$ $/\$
238	1, 237	cvxcl 24711	. . . 4 $/\$ $/\$ $/\$
239	75, 238	ffvelrnd 6360	. . 3 $/\$ $/\$ $/\$
240	170, 167	readdcld 10069	. . 3 $/\$ $/\$ $/\$
241	239, 240	leloed 10180	. 2 $/\$ $/\$ $/\$ $\/$
242	236, 241	mpbird 247	1 $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384 $\/$ w3o 1036 $/\$ w3a 1037

wceq 1483

wcel 1990

wral 2912

cun 3572

wss 3574

cpr 4179 class class class wbr 4653

wf 5884

cfv 5888 (class class class)co 6650

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

cxr 10073

clt 10074

cle 10075

cmin 10266

cioo 12175

cicc 12178

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-sup 8348 df-inf 8349 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-n0 11293 df-z 11378 df-uz 11688 df-q 11789 df-rp 11833 df-ioo 12179 df-ico 12181 df-icc 12182

This theorem is referenced by: amgmlem 24716 amgmwlem 42548

W3C validator