isosctrlem2 - Metamath Proof Explorer

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

Theorem isosctrlem2 22176

Description: Lemma for isosctr 22178. Corresponds to the case where one vertex is at 0, another at 1 and the third lies on the unit circle. (Contributed by Saveliy Skresanov, 31-Dec-2016.)

**Assertion**
Ref	Expression
isosctrlem2	$/\$ $/\$

**Proof of Theorem isosctrlem2**
Step	Hyp	Ref	Expression
1		1cnd 9398	. . . . . . 7 $/\$ $/\$ $/\$
2		simpl1 986	. . . . . . 7 $/\$ $/\$ $/\$
3	1, 2	negsubd 9721	. . . . . 6 $/\$ $/\$ $/\$
4		1rp 10991	. . . . . . . 8
5	4	a1i 11	. . . . . . 7 $/\$ $/\$ $/\$
6		simpl3 988	. . . . . . . . 9 $/\$ $/\$ $/\$
7		simpl2 987	. . . . . . . . . . 11 $/\$ $/\$ $/\$
8	1, 2, 1	sub32d 9747	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
9		1m1e0 10386	. . . . . . . . . . . . . . . . 17
10	9	oveq1i 6100	. . . . . . . . . . . . . . . 16
11		df-neg 9594	. . . . . . . . . . . . . . . 16
12	10, 11	eqtr4i 2464	. . . . . . . . . . . . . . 15
13	8, 12	syl6eq 2489	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
14		1cnd 9398	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
15		simp1 983	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
16	14, 15	subcld 9715	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
17	16	adantr 462	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
18		ax-1cn 9336	. . . . . . . . . . . . . . . . . . . . . . 23
19		subeq0 9631	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
20	18, 19	mpan 665	. . . . . . . . . . . . . . . . . . . . . 22
21	20	biimpd 207	. . . . . . . . . . . . . . . . . . . . 21
22	21	con3and 439	. . . . . . . . . . . . . . . . . . . 20 $/\$
23	22	neneqad 2679	. . . . . . . . . . . . . . . . . . 19 $/\$
24	23	3adant2 1002	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
25	24	adantr 462	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
26	17, 25	recrecd 10100	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
27	14, 16, 24	div2negd 10118	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
28	27	adantr 462	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
29	15	negcld 9702	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
30	29, 16, 24	cjdivd 12708	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
31	15	cjnegd 12696	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
32		fveq2 5688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
33		abs0 12770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
34	32, 33	syl6eq 2489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
35		eqtr2 2459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
36	34, 35	sylan2 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
37		ax-1ne0 9347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
38		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
39	38	neneqd 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
40	37, 39	mp1i 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
41	36, 40	pm2.65da 573	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
42	41	adantl 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
43		df-ne 2606	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
44		oveq1 6097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
45		sq1 11956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
46	44, 45	syl6eq 2489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
47	46	adantl 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
48		absvalsq 12765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
49	48	adantr 462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
50	47, 49	eqtr3d 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
51	50	3adant3 1003	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
52	51	oveq1d 6105	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
53		simp1 983	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
54	53	cjcld 12681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
55		simp3 985	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
56	54, 53, 55	divcan3d 10108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
57	52, 56	eqtrd 2473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
58	43, 57	syl3an3br 1254	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
59	42, 58	mpd3an3 1310	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
60	59	eqcomd 2446	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
61	60	3adant3 1003	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
62	61	negeqd 9600	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
63	31, 62	eqtrd 2473	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
64	63	oveq1d 6105	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
65		cjsub 12634	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
66	18, 65	mpan 665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
67		1red 9397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
68	67	cjred 12711	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
69	68	oveq1d 6105	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
70	66, 69	eqtrd 2473	. . . . . . . . . . . . . . . . . . . . . . . . . 26
71	70	adantr 462	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
72	60	oveq2d 6106	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
73	71, 72	eqtrd 2473	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
74	73	3adant3 1003	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
75	74	oveq2d 6106	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
76	30, 64, 75	3eqtrd 2477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
77	41	3ad2ant2 1005	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
78	77	neneqad 2679	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
79		1cnd 9398	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
80		simpl 454	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
81		simpr 458	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
82	79, 80, 81	divnegd 10116	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
83	82	oveq1d 6105	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
84	15, 78, 83	syl2anc 656	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
85	14	negcld 9702	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
86	85, 15, 78	divcld 10103	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
87	15, 78	reccld 10096	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
88	14, 87	subcld 9715	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
89	16, 24	cjne0d 12688	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
90	74, 89	eqnetrrd 2626	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
91	86, 88, 15, 90, 78	divcan5d 10129	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
92	85, 15, 78	divcan2d 10105	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
93	15, 14, 87	subdid 9796	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
94	15	mulid1d 9399	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
95	15, 78	recidd 10098	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
96	94, 95	oveq12d 6108	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
97	93, 96	eqtrd 2473	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
98	92, 97	oveq12d 6108	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
99	84, 91, 98	3eqtr2d 2479	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
100		subcl 9605	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
101	100	negnegd 9706	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
102		negsubdi2 9664	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
103	102	negeqd 9600	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
104	101, 103	eqtr3d 2475	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
105	15, 14, 104	syl2anc 656	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
106	105	oveq2d 6106	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
107	76, 99, 106	3eqtrd 2477	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
108	107	adantr 462	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
109	29, 16, 24	divcld 10103	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
110	109	adantr 462	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
111		simpr 458	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
112	110, 111	reim0bd 12685	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
113	112	cjred 12711	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
114	113, 112	eqeltrd 2515	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
115	108, 114	eqeltrrd 2516	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
116	28, 115	eqeltrrd 2516	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
117	16, 24	recne0d 10097	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
118	117	adantr 462	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
119	116, 118	rereccld 10154	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
120	26, 119	eqeltrrd 2516	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
121		1red 9397	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
122	120, 121	resubcld 9772	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
123	13, 122	eqeltrrd 2516	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
124	2, 123	negrebd 9714	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
125	124	absord 12898	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\/$
126		eqeq1 2447	. . . . . . . . . . . . 13
127	126	biimpd 207	. . . . . . . . . . . 12
128		eqeq1 2447	. . . . . . . . . . . . 13
129	128	biimpd 207	. . . . . . . . . . . 12
130	127, 129	orim12d 829	. . . . . . . . . . 11 $\/$ $\/$
131	7, 125, 130	sylc 60	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\/$
132	131	ord 377	. . . . . . . . 9 $/\$ $/\$ $/\$
133	6, 132	mpd 15	. . . . . . . 8 $/\$ $/\$ $/\$
134	133, 5	eqeltrrd 2516	. . . . . . 7 $/\$ $/\$ $/\$
135	5, 134	rpaddcld 11038	. . . . . 6 $/\$ $/\$ $/\$
136	3, 135	eqeltrrd 2516	. . . . 5 $/\$ $/\$ $/\$
137	136	relogcld 22031	. . . 4 $/\$ $/\$ $/\$
138	137	reim0d 12710	. . 3 $/\$ $/\$ $/\$
139	134, 136	rpdivcld 11040	. . . . 5 $/\$ $/\$ $/\$
140	139	relogcld 22031	. . . 4 $/\$ $/\$ $/\$
141	140	reim0d 12710	. . 3 $/\$ $/\$ $/\$
142	138, 141	eqtr4d 2476	. 2 $/\$ $/\$ $/\$
143	16, 24	logcld 21981	. . . . . 6 $/\$ $/\$
144	143	adantr 462	. . . . 5 $/\$ $/\$ $/\$
145	144	imcld 12680	. . . 4 $/\$ $/\$ $/\$
146	145	recnd 9408	. . 3 $/\$ $/\$ $/\$
147	109	adantr 462	. . . . . 6 $/\$ $/\$ $/\$
148	15, 78	negne0d 9713	. . . . . . . 8 $/\$ $/\$
149	29, 16, 148, 24	divne0d 10119	. . . . . . 7 $/\$ $/\$
150	149	adantr 462	. . . . . 6 $/\$ $/\$ $/\$
151	147, 150	logcld 21981	. . . . 5 $/\$ $/\$ $/\$
152	151	imcld 12680	. . . 4 $/\$ $/\$ $/\$
153	152	recnd 9408	. . 3 $/\$ $/\$ $/\$
154	107	fveq2d 5692	. . . . . . 7 $/\$ $/\$
155	154	adantr 462	. . . . . 6 $/\$ $/\$ $/\$
156		logcj 22014	. . . . . . 7 $/\$
157	109, 156	sylan 468	. . . . . 6 $/\$ $/\$ $/\$
158	16, 24	reccld 10096	. . . . . . . . . 10 $/\$ $/\$
159	158, 117	logcld 21981	. . . . . . . . 9 $/\$ $/\$
160	159	negnegd 9706	. . . . . . . 8 $/\$ $/\$
161		isosctrlem1 22175	. . . . . . . . . 10 $/\$ $/\$
162		logrec 22174	. . . . . . . . . 10 $/\$ $/\$
163	16, 24, 161, 162	syl3anc 1213	. . . . . . . . 9 $/\$ $/\$
164	163	negeqd 9600	. . . . . . . 8 $/\$ $/\$
165	27	fveq2d 5692	. . . . . . . 8 $/\$ $/\$
166	160, 164, 165	3eqtr4rd 2484	. . . . . . 7 $/\$ $/\$
167	166	adantr 462	. . . . . 6 $/\$ $/\$ $/\$
168	155, 157, 167	3eqtr3rd 2482	. . . . 5 $/\$ $/\$ $/\$
169	168	fveq2d 5692	. . . 4 $/\$ $/\$ $/\$
170	144	imnegd 12695	. . . 4 $/\$ $/\$ $/\$
171	151	imcjd 12690	. . . 4 $/\$ $/\$ $/\$
172	169, 170, 171	3eqtr3d 2481	. . 3 $/\$ $/\$ $/\$
173	146, 153, 172	neg11d 9727	. 2 $/\$ $/\$ $/\$
174	142, 173	pm2.61dane 2687	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369 $/\$ w3a 960

wceq 1364

wcel 1761

wne 2604

cfv 5415 (class class class)co 6090

cc 9276

cr 9277

cc0 9278

c1 9279

caddc 9281

cmul 9283

cmin 9591

cneg 9592

cdiv 9989

c2 10367

crp 10987

cexp 11861

ccj 12581

cim 12583

cabs 12719

cpi 13348

clog 21965

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-rep 4400 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371 ax-inf2 7843 ax-cnex 9334 ax-resscn 9335 ax-1cn 9336 ax-icn 9337 ax-addcl 9338 ax-addrcl 9339 ax-mulcl 9340 ax-mulrcl 9341 ax-mulcom 9342 ax-addass 9343 ax-mulass 9344 ax-distr 9345 ax-i2m1 9346 ax-1ne0 9347 ax-1rid 9348 ax-rnegex 9349 ax-rrecex 9350 ax-cnre 9351 ax-pre-lttri 9352 ax-pre-lttrn 9353 ax-pre-ltadd 9354 ax-pre-mulgt0 9355 ax-pre-sup 9356 ax-addf 9357 ax-mulf 9358

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 961 df-3an 962 df-tru 1367 df-fal 1370 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2261 df-mo 2262 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-nel 2607 df-ral 2718 df-rex 2719 df-reu 2720 df-rmo 2721 df-rab 2722 df-v 2972 df-sbc 3184 df-csb 3286 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-pss 3341 df-nul 3635 df-if 3789 df-pw 3859 df-sn 3875 df-pr 3877 df-tp 3879 df-op 3881 df-uni 4089 df-int 4126 df-iun 4170 df-iin 4171 df-br 4290 df-opab 4348 df-mpt 4349 df-tr 4383 df-eprel 4628 df-id 4632 df-po 4637 df-so 4638 df-fr 4675 df-se 4676 df-we 4677 df-ord 4718 df-on 4719 df-lim 4720 df-suc 4721 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-res 4848 df-ima 4849 df-iota 5378 df-fun 5417 df-fn 5418 df-f 5419 df-f1 5420 df-fo 5421 df-f1o 5422 df-fv 5423 df-isom 5424 df-riota 6049 df-ov 6093 df-oprab 6094 df-mpt2 6095 df-of 6319 df-om 6476 df-1st 6576 df-2nd 6577 df-supp 6690 df-recs 6828 df-rdg 6862 df-1o 6916 df-2o 6917 df-oadd 6920 df-er 7097 df-map 7212 df-pm 7213 df-ixp 7260 df-en 7307 df-dom 7308 df-sdom 7309 df-fin 7310 df-fsupp 7617 df-fi 7657 df-sup 7687 df-oi 7720 df-card 8105 df-cda 8333 df-pnf 9416 df-mnf 9417 df-xr 9418 df-ltxr 9419 df-le 9420 df-sub 9593 df-neg 9594 df-div 9990 df-nn 10319 df-2 10376 df-3 10377 df-4 10378 df-5 10379 df-6 10380 df-7 10381 df-8 10382 df-9 10383 df-10 10384 df-n0 10576 df-z 10643 df-dec 10752 df-uz 10858 df-q 10950 df-rp 10988 df-xneg 11085 df-xadd 11086 df-xmul 11087 df-ioo 11300 df-ioc 11301 df-ico 11302 df-icc 11303 df-fz 11434 df-fzo 11545 df-fl 11638 df-mod 11705 df-seq 11803 df-exp 11862 df-fac 12048 df-bc 12075 df-hash 12100 df-shft 12552 df-cj 12584 df-re 12585 df-im 12586 df-sqr 12720 df-abs 12721 df-limsup 12945 df-clim 12962 df-rlim 12963 df-sum 13160 df-ef 13349 df-sin 13351 df-cos 13352 df-pi 13354 df-struct 14172 df-ndx 14173 df-slot 14174 df-base 14175 df-sets 14176 df-ress 14177 df-plusg 14247 df-mulr 14248 df-starv 14249 df-sca 14250 df-vsca 14251 df-ip 14252 df-tset 14253 df-ple 14254 df-ds 14256 df-unif 14257 df-hom 14258 df-cco 14259 df-rest 14357 df-topn 14358 df-0g 14376 df-gsum 14377 df-topgen 14378 df-pt 14379 df-prds 14382 df-xrs 14436 df-qtop 14441 df-imas 14442 df-xps 14444 df-mre 14520 df-mrc 14521 df-acs 14523 df-mnd 15411 df-submnd 15461 df-mulg 15541 df-cntz 15828 df-cmn 16272 df-psmet 17768 df-xmet 17769 df-met 17770 df-bl 17771 df-mopn 17772 df-fbas 17773 df-fg 17774 df-cnfld 17778 df-top 18462 df-bases 18464 df-topon 18465 df-topsp 18466 df-cld 18582 df-ntr 18583 df-cls 18584 df-nei 18661 df-lp 18699 df-perf 18700 df-cn 18790 df-cnp 18791 df-haus 18878 df-tx 19094 df-hmeo 19287 df-fil 19378 df-fm 19470 df-flim 19471 df-flf 19472 df-xms 19854 df-ms 19855 df-tms 19856 df-cncf 20413 df-limc 21300 df-dv 21301 df-log 21967

This theorem is referenced by: isosctrlem3 22177

W3C validator