scvxcvx - Metamath Proof Explorer

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

Theorem scvxcvx 20829

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 453	. . . . . . . 8 $/\$ $/\$ $/\$
3		simpr1 964	. . . . . . . 8 $/\$ $/\$ $/\$
4	2, 3	sseldd 3351	. . . . . . 7 $/\$ $/\$ $/\$
5	4	adantr 453	. . . . . 6 $/\$ $/\$ $/\$ $/\$
6		simpr2 965	. . . . . . . 8 $/\$ $/\$ $/\$
7	2, 6	sseldd 3351	. . . . . . 7 $/\$ $/\$ $/\$
8	7	adantr 453	. . . . . 6 $/\$ $/\$ $/\$ $/\$
9	5, 8	lttri4d 9219	. . . . 5 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
10		simprl 734	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
11	3	adantr 453	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
12	6	adantr 453	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
13	11, 12	jca 520	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
14		simprr 735	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
15		simpll 732	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
16		breq1 4218	. . . . . . . . . . . 12
17		oveq2 6092	. . . . . . . . . . . . . . . . 17
18	17	oveq1d 6099	. . . . . . . . . . . . . . . 16
19	18	fveq2d 5735	. . . . . . . . . . . . . . 15
20		fveq2 5731	. . . . . . . . . . . . . . . . 17
21	20	oveq2d 6100	. . . . . . . . . . . . . . . 16
22	21	oveq1d 6099	. . . . . . . . . . . . . . 15
23	19, 22	breq12d 4228	. . . . . . . . . . . . . 14
24	23	ralbidv 2727	. . . . . . . . . . . . 13
25	24	imbi2d 309	. . . . . . . . . . . 12
26	16, 25	imbi12d 313	. . . . . . . . . . 11
27		breq2 4219	. . . . . . . . . . . 12
28		oveq2 6092	. . . . . . . . . . . . . . . . 17
29	28	oveq2d 6100	. . . . . . . . . . . . . . . 16
30	29	fveq2d 5735	. . . . . . . . . . . . . . 15
31		fveq2 5731	. . . . . . . . . . . . . . . . 17
32	31	oveq2d 6100	. . . . . . . . . . . . . . . 16
33	32	oveq2d 6100	. . . . . . . . . . . . . . 15
34	30, 33	breq12d 4228	. . . . . . . . . . . . . 14
35	34	ralbidv 2727	. . . . . . . . . . . . 13
36	35	imbi2d 309	. . . . . . . . . . . 12
37	27, 36	imbi12d 313	. . . . . . . . . . 11
38		scvxcvx.4	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
39	38	3expia 1156	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
40	39	ralrimiv 2790	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
41	40	expcom 426	. . . . . . . . . . . 12 $/\$ $/\$
42	41	3expia 1156	. . . . . . . . . . 11 $/\$
43	26, 37, 42	vtocl2ga 3021	. . . . . . . . . 10 $/\$
44	13, 14, 15, 43	syl3c 60	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
45		oveq1 6091	. . . . . . . . . . . . 13
46		oveq2 6092	. . . . . . . . . . . . . 14
47	46	oveq1d 6099	. . . . . . . . . . . . 13
48	45, 47	oveq12d 6102	. . . . . . . . . . . 12
49	48	fveq2d 5735	. . . . . . . . . . 11
50		oveq1 6091	. . . . . . . . . . . 12
51	46	oveq1d 6099	. . . . . . . . . . . 12
52	50, 51	oveq12d 6102	. . . . . . . . . . 11
53	49, 52	breq12d 4228	. . . . . . . . . 10
54	53	rspcv 3050	. . . . . . . . 9
55	10, 44, 54	sylc 59	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
56	55	orcd 383	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
57	56	expr 600	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\/$
58		unitssre 11047	. . . . . . . . . . . . . . . 16
59		simpr3 966	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
60	58, 59	sseldi 3348	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
61	60	recnd 9119	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
62		ax-1cn 9053	. . . . . . . . . . . . . 14
63		pncan3 9318	. . . . . . . . . . . . . 14 $/\$
64	61, 62, 63	sylancl 645	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
65	64	oveq1d 6099	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
66		subcl 9310	. . . . . . . . . . . . . 14 $/\$
67	62, 61, 66	sylancr 646	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
68	7	recnd 9119	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
69	61, 67, 68	adddird 9118	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
70	68	mulid2d 9111	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
71	65, 69, 70	3eqtr3d 2478	. . . . . . . . . . 11 $/\$ $/\$ $/\$
72	71	fveq2d 5735	. . . . . . . . . 10 $/\$ $/\$ $/\$
73	64	oveq1d 6099	. . . . . . . . . . 11 $/\$ $/\$ $/\$
74		scvxcvx.2	. . . . . . . . . . . . . . 15
75	74	adantr 453	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
76	75, 6	ffvelrnd 5874	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
77	76	recnd 9119	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
78	61, 67, 77	adddird 9118	. . . . . . . . . . 11 $/\$ $/\$ $/\$
79	77	mulid2d 9111	. . . . . . . . . . 11 $/\$ $/\$ $/\$
80	73, 78, 79	3eqtr3d 2478	. . . . . . . . . 10 $/\$ $/\$ $/\$
81	72, 80	eqtr4d 2473	. . . . . . . . 9 $/\$ $/\$ $/\$
82	81	adantr 453	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
83		oveq2 6092	. . . . . . . . . . 11
84	83	oveq1d 6099	. . . . . . . . . 10
85	84	fveq2d 5735	. . . . . . . . 9
86		fveq2 5731	. . . . . . . . . . 11
87	86	oveq2d 6100	. . . . . . . . . 10
88	87	oveq1d 6099	. . . . . . . . 9
89	85, 88	eqeq12d 2452	. . . . . . . 8
90	82, 89	syl5ibrcom 215	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
91		olc 375	. . . . . . 7 $\/$
92	90, 91	syl6 32	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\/$
93		1re 9095	. . . . . . . . . . . . 13
94		elioore 10951	. . . . . . . . . . . . 13
95		resubcl 9370	. . . . . . . . . . . . 13 $/\$
96	93, 94, 95	sylancr 646	. . . . . . . . . . . 12
97		eliooord 10975	. . . . . . . . . . . . . 14 $/\$
98	97	simprd 451	. . . . . . . . . . . . 13
99		posdif 9526	. . . . . . . . . . . . . 14 $/\$
100	94, 93, 99	sylancl 645	. . . . . . . . . . . . 13
101	98, 100	mpbid 203	. . . . . . . . . . . 12
102	97	simpld 447	. . . . . . . . . . . . 13
103		ltsubpos 9525	. . . . . . . . . . . . . 14 $/\$
104	94, 93, 103	sylancl 645	. . . . . . . . . . . . 13
105	102, 104	mpbid 203	. . . . . . . . . . . 12
106		0xr 9136	. . . . . . . . . . . . 13
107	93	rexri 9142	. . . . . . . . . . . . 13
108		elioo2 10962	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
109	106, 107, 108	mp2an 655	. . . . . . . . . . . 12 $/\$ $/\$
110	96, 101, 105, 109	syl3anbrc 1139	. . . . . . . . . . 11
111	110	ad2antrl 710	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
112	6	adantr 453	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
113	3	adantr 453	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
114	112, 113	jca 520	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
115		simprr 735	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
116		simpll 732	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
117		breq1 4218	. . . . . . . . . . . . 13
118		oveq2 6092	. . . . . . . . . . . . . . . . . 18
119	118	oveq1d 6099	. . . . . . . . . . . . . . . . 17
120	119	fveq2d 5735	. . . . . . . . . . . . . . . 16
121		fveq2 5731	. . . . . . . . . . . . . . . . . 18
122	121	oveq2d 6100	. . . . . . . . . . . . . . . . 17
123	122	oveq1d 6099	. . . . . . . . . . . . . . . 16
124	120, 123	breq12d 4228	. . . . . . . . . . . . . . 15
125	124	ralbidv 2727	. . . . . . . . . . . . . 14
126	125	imbi2d 309	. . . . . . . . . . . . 13
127	117, 126	imbi12d 313	. . . . . . . . . . . 12
128		breq2 4219	. . . . . . . . . . . . 13
129		oveq2 6092	. . . . . . . . . . . . . . . . . 18
130	129	oveq2d 6100	. . . . . . . . . . . . . . . . 17
131	130	fveq2d 5735	. . . . . . . . . . . . . . . 16
132		fveq2 5731	. . . . . . . . . . . . . . . . . 18
133	132	oveq2d 6100	. . . . . . . . . . . . . . . . 17
134	133	oveq2d 6100	. . . . . . . . . . . . . . . 16
135	131, 134	breq12d 4228	. . . . . . . . . . . . . . 15
136	135	ralbidv 2727	. . . . . . . . . . . . . 14
137	136	imbi2d 309	. . . . . . . . . . . . 13
138	128, 137	imbi12d 313	. . . . . . . . . . . 12
139	127, 138, 42	vtocl2ga 3021	. . . . . . . . . . 11 $/\$
140	114, 115, 116, 139	syl3c 60	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
141		oveq1 6091	. . . . . . . . . . . . . 14
142		oveq2 6092	. . . . . . . . . . . . . . 15
143	142	oveq1d 6099	. . . . . . . . . . . . . 14
144	141, 143	oveq12d 6102	. . . . . . . . . . . . 13
145	144	fveq2d 5735	. . . . . . . . . . . 12
146		oveq1 6091	. . . . . . . . . . . . 13
147	142	oveq1d 6099	. . . . . . . . . . . . 13
148	146, 147	oveq12d 6102	. . . . . . . . . . . 12
149	145, 148	breq12d 4228	. . . . . . . . . . 11
150	149	rspcv 3050	. . . . . . . . . 10
151	111, 140, 150	sylc 59	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
152		nncan 9335	. . . . . . . . . . . . . . 15 $/\$
153	62, 61, 152	sylancr 646	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
154	153	oveq1d 6099	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
155	154	oveq2d 6100	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
156	93, 60, 95	sylancr 646	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
157	156, 7	remulcld 9121	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
158	157	recnd 9119	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
159	60, 4	remulcld 9121	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
160	159	recnd 9119	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
161	158, 160	addcomd 9273	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
162	155, 161	eqtrd 2470	. . . . . . . . . . 11 $/\$ $/\$ $/\$
163	162	adantr 453	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
164	163	fveq2d 5735	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
165	153	oveq1d 6099	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
166	165	oveq2d 6100	. . . . . . . . . . 11 $/\$ $/\$ $/\$
167	156, 76	remulcld 9121	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
168	167	recnd 9119	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
169	75, 3	ffvelrnd 5874	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
170	60, 169	remulcld 9121	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
171	170	recnd 9119	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
172	168, 171	addcomd 9273	. . . . . . . . . . 11 $/\$ $/\$ $/\$
173	166, 172	eqtrd 2470	. . . . . . . . . 10 $/\$ $/\$ $/\$
174	173	adantr 453	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
175	151, 164, 174	3brtr3d 4244	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
176	175	orcd 383	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
177	176	expr 600	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\/$
178	57, 92, 177	3jaod 1249	. . . . 5 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$ $\/$
179	9, 178	mpd 15	. . . 4 $/\$ $/\$ $/\$ $/\$ $\/$
180	179	ex 425	. . 3 $/\$ $/\$ $/\$ $\/$
181		elpri 3836	. . . 4 $\/$
182	77	addid2d 9272	. . . . . . 7 $/\$ $/\$ $/\$
183	169	recnd 9119	. . . . . . . . 9 $/\$ $/\$ $/\$
184	183	mul02d 9269	. . . . . . . 8 $/\$ $/\$ $/\$
185	184, 79	oveq12d 6102	. . . . . . 7 $/\$ $/\$ $/\$
186	4	recnd 9119	. . . . . . . . . . 11 $/\$ $/\$ $/\$
187	186	mul02d 9269	. . . . . . . . . 10 $/\$ $/\$ $/\$
188	187, 70	oveq12d 6102	. . . . . . . . 9 $/\$ $/\$ $/\$
189	68	addid2d 9272	. . . . . . . . 9 $/\$ $/\$ $/\$
190	188, 189	eqtrd 2470	. . . . . . . 8 $/\$ $/\$ $/\$
191	190	fveq2d 5735	. . . . . . 7 $/\$ $/\$ $/\$
192	182, 185, 191	3eqtr4rd 2481	. . . . . 6 $/\$ $/\$ $/\$
193		oveq1 6091	. . . . . . . . 9
194		oveq2 6092	. . . . . . . . . . 11
195	62	subid1i 9377	. . . . . . . . . . 11
196	194, 195	syl6eq 2486	. . . . . . . . . 10
197	196	oveq1d 6099	. . . . . . . . 9
198	193, 197	oveq12d 6102	. . . . . . . 8
199	198	fveq2d 5735	. . . . . . 7
200		oveq1 6091	. . . . . . . 8
201	196	oveq1d 6099	. . . . . . . 8
202	200, 201	oveq12d 6102	. . . . . . 7
203	199, 202	eqeq12d 2452	. . . . . 6
204	192, 203	syl5ibrcom 215	. . . . 5 $/\$ $/\$ $/\$
205	183	addid1d 9271	. . . . . . 7 $/\$ $/\$ $/\$
206	183	mulid2d 9111	. . . . . . . 8 $/\$ $/\$ $/\$
207	77	mul02d 9269	. . . . . . . 8 $/\$ $/\$ $/\$
208	206, 207	oveq12d 6102	. . . . . . 7 $/\$ $/\$ $/\$
209	186	mulid2d 9111	. . . . . . . . . 10 $/\$ $/\$ $/\$
210	68	mul02d 9269	. . . . . . . . . 10 $/\$ $/\$ $/\$
211	209, 210	oveq12d 6102	. . . . . . . . 9 $/\$ $/\$ $/\$
212	186	addid1d 9271	. . . . . . . . 9 $/\$ $/\$ $/\$
213	211, 212	eqtrd 2470	. . . . . . . 8 $/\$ $/\$ $/\$
214	213	fveq2d 5735	. . . . . . 7 $/\$ $/\$ $/\$
215	205, 208, 214	3eqtr4rd 2481	. . . . . 6 $/\$ $/\$ $/\$
216		oveq1 6091	. . . . . . . . 9
217		oveq2 6092	. . . . . . . . . . 11
218		1m1e0 10073	. . . . . . . . . . 11
219	217, 218	syl6eq 2486	. . . . . . . . . 10
220	219	oveq1d 6099	. . . . . . . . 9
221	216, 220	oveq12d 6102	. . . . . . . 8
222	221	fveq2d 5735	. . . . . . 7
223		oveq1 6091	. . . . . . . 8
224	219	oveq1d 6099	. . . . . . . 8
225	223, 224	oveq12d 6102	. . . . . . 7
226	222, 225	eqeq12d 2452	. . . . . 6
227	215, 226	syl5ibrcom 215	. . . . 5 $/\$ $/\$ $/\$
228	204, 227	jaod 371	. . . 4 $/\$ $/\$ $/\$ $\/$
229	181, 228, 91	syl56 33	. . 3 $/\$ $/\$ $/\$ $\/$
230		0le1 9556	. . . . . 6
231		prunioo 11030	. . . . . 6 $/\$ $/\$
232	106, 107, 230, 231	mp3an 1280	. . . . 5
233	59, 232	syl6eleqr 2529	. . . 4 $/\$ $/\$ $/\$
234		elun 3490	. . . 4 $\/$
235	233, 234	sylib 190	. . 3 $/\$ $/\$ $/\$ $\/$
236	180, 229, 235	mpjaod 372	. 2 $/\$ $/\$ $/\$ $\/$
237		scvxcvx.3	. . . . 5 $/\$ $/\$
238	1, 237	cvxcl 20828	. . . 4 $/\$ $/\$ $/\$
239	75, 238	ffvelrnd 5874	. . 3 $/\$ $/\$ $/\$
240	170, 167	readdcld 9120	. . 3 $/\$ $/\$ $/\$
241	239, 240	leloed 9221	. 2 $/\$ $/\$ $/\$ $\/$
242	236, 241	mpbird 225	1 $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4

wb 178 $\/$ wo 359 $/\$ wa 360 $\/$ w3o 936 $/\$ w3a 937

wceq 1653

wcel 1726

wral 2707

cun 3320

wss 3322

cpr 3817 class class class wbr 4215

wf 5453

cfv 5457 (class class class)co 6084

cc 8993

cr 8994

cc0 8995

c1 8996

caddc 8998

cmul 9000

cxr 9124

clt 9125

cle 9126

cmin 9296

cioo 10921

cicc 10924

This theorem is referenced by: amgmlem 20833

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1556 ax-5 1567 ax-17 1627 ax-9 1667 ax-8 1688 ax-13 1728 ax-14 1730 ax-6 1745 ax-7 1750 ax-11 1762 ax-12 1951 ax-ext 2419 ax-sep 4333 ax-nul 4341 ax-pow 4380 ax-pr 4406 ax-un 4704 ax-cnex 9051 ax-resscn 9052 ax-1cn 9053 ax-icn 9054 ax-addcl 9055 ax-addrcl 9056 ax-mulcl 9057 ax-mulrcl 9058 ax-mulcom 9059 ax-addass 9060 ax-mulass 9061 ax-distr 9062 ax-i2m1 9063 ax-1ne0 9064 ax-1rid 9065 ax-rnegex 9066 ax-rrecex 9067 ax-cnre 9068 ax-pre-lttri 9069 ax-pre-lttrn 9070 ax-pre-ltadd 9071 ax-pre-mulgt0 9072 ax-pre-sup 9073

This theorem depends on definitions: df-bi 179 df-or 361 df-an 362 df-3or 938 df-3an 939 df-tru 1329 df-ex 1552 df-nf 1555 df-sb 1660 df-eu 2287 df-mo 2288 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2712 df-rex 2713 df-reu 2714 df-rmo 2715 df-rab 2716 df-v 2960 df-sbc 3164 df-csb 3254 df-dif 3325 df-un 3327 df-in 3329 df-ss 3336 df-pss 3338 df-nul 3631 df-if 3742 df-pw 3803 df-sn 3822 df-pr 3823 df-tp 3824 df-op 3825 df-uni 4018 df-iun 4097 df-br 4216 df-opab 4270 df-mpt 4271 df-tr 4306 df-eprel 4497 df-id 4501 df-po 4506 df-so 4507 df-fr 4544 df-we 4546 df-ord 4587 df-on 4588 df-lim 4589 df-suc 4590 df-om 4849 df-xp 4887 df-rel 4888 df-cnv 4889 df-co 4890 df-dm 4891 df-rn 4892 df-res 4893 df-ima 4894 df-iota 5421 df-fun 5459 df-fn 5460 df-f 5461 df-f1 5462 df-fo 5463 df-f1o 5464 df-fv 5465 df-ov 6087 df-oprab 6088 df-mpt2 6089 df-1st 6352 df-2nd 6353 df-riota 6552 df-recs 6636 df-rdg 6671 df-er 6908 df-en 7113 df-dom 7114 df-sdom 7115 df-sup 7449 df-pnf 9127 df-mnf 9128 df-xr 9129 df-ltxr 9130 df-le 9131 df-sub 9298 df-neg 9299 df-div 9683 df-nn 10006 df-n0 10227 df-z 10288 df-uz 10494 df-q 10580 df-rp 10618 df-ioo 10925 df-ico 10927 df-icc 10928

W3C validator