isosctrlem2 - Metamath Proof Explorer

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

Theorem isosctrlem2 22897

Description: Lemma for isosctr 22899. 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 9611	. . . . . . 7 $/\$ $/\$ $/\$
2		simpl1 999	. . . . . . 7 $/\$ $/\$ $/\$
3	1, 2	negsubd 9935	. . . . . 6 $/\$ $/\$ $/\$
4		1rp 11223	. . . . . . . 8
5	4	a1i 11	. . . . . . 7 $/\$ $/\$ $/\$
6		simpl3 1001	. . . . . . . . 9 $/\$ $/\$ $/\$
7		simpl2 1000	. . . . . . . . . . 11 $/\$ $/\$ $/\$
8	1, 2, 1	sub32d 9961	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
9		1m1e0 10603	. . . . . . . . . . . . . . . . 17
10	9	oveq1i 6293	. . . . . . . . . . . . . . . 16
11		df-neg 9807	. . . . . . . . . . . . . . . 16
12	10, 11	eqtr4i 2499	. . . . . . . . . . . . . . 15
13	8, 12	syl6eq 2524	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
14		1cnd 9611	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
15		simp1 996	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
16	14, 15	subcld 9929	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
17	16	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
18		ax-1cn 9549	. . . . . . . . . . . . . . . . . . . . . . 23
19		subeq0 9844	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
20	18, 19	mpan 670	. . . . . . . . . . . . . . . . . . . . . 22
21	20	biimpd 207	. . . . . . . . . . . . . . . . . . . . 21
22	21	con3dimp 441	. . . . . . . . . . . . . . . . . . . 20 $/\$
23	22	neqned 2670	. . . . . . . . . . . . . . . . . . 19 $/\$
24	23	3adant2 1015	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
25	24	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
26	17, 25	recrecd 10316	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
27	14, 16, 24	div2negd 10334	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
28	27	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
29	15	negcld 9916	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
30	29, 16, 24	cjdivd 13018	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
31	15	cjnegd 13006	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
32		fveq2 5865	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
33		abs0 13080	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
34	32, 33	syl6eq 2524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
35		eqtr2 2494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
36	34, 35	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
37		ax-1ne0 9560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
38		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
39	38	neneqd 2669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
40	37, 39	mp1i 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
41	36, 40	pm2.65da 576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
42	41	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
43		df-ne 2664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
44		oveq1 6290	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
45		sq1 12229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
46	44, 45	syl6eq 2524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
47	46	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
48		absvalsq 13075	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
49	48	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
50	47, 49	eqtr3d 2510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
51	50	3adant3 1016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
52	51	oveq1d 6298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
53		simp1 996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
54	53	cjcld 12991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
55		simp3 998	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
56	54, 53, 55	divcan3d 10324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
57	52, 56	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
58	43, 57	syl3an3br 1269	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
59	42, 58	mpd3an3 1325	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
60	59	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
61	60	3adant3 1016	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
62	61	negeqd 9813	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
63	31, 62	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
64	63	oveq1d 6298	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
65		cjsub 12944	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
66	18, 65	mpan 670	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
67		1red 9610	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
68	67	cjred 13021	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
69	68	oveq1d 6298	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
70	66, 69	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . . . 26
71	70	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
72	60	oveq2d 6299	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
73	71, 72	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
74	73	3adant3 1016	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
75	74	oveq2d 6299	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
76	30, 64, 75	3eqtrd 2512	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
77	41	3ad2ant2 1018	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
78	77	neqned 2670	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
79		1cnd 9611	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
80		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
81		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
82	79, 80, 81	divnegd 10332	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
83	82	oveq1d 6298	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
84	15, 78, 83	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
85	14	negcld 9916	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
86	85, 15, 78	divcld 10319	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
87	15, 78	reccld 10312	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
88	14, 87	subcld 9929	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
89	16, 24	cjne0d 12998	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
90	74, 89	eqnetrrd 2761	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
91	86, 88, 15, 90, 78	divcan5d 10345	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
92	85, 15, 78	divcan2d 10321	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
93	15, 14, 87	subdid 10011	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
94	15	mulid1d 9612	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
95	15, 78	recidd 10314	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
96	94, 95	oveq12d 6301	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
97	93, 96	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
98	92, 97	oveq12d 6301	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
99	84, 91, 98	3eqtr2d 2514	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
100		subcl 9818	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
101	100	negnegd 9920	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
102		negsubdi2 9877	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
103	102	negeqd 9813	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
104	101, 103	eqtr3d 2510	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
105	15, 14, 104	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
106	105	oveq2d 6299	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
107	76, 99, 106	3eqtrd 2512	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
108	107	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
109	29, 16, 24	divcld 10319	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
110	109	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
111		simpr 461	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
112	110, 111	reim0bd 12995	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
113	112	cjred 13021	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
114	113, 112	eqeltrd 2555	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
115	108, 114	eqeltrrd 2556	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
116	28, 115	eqeltrrd 2556	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
117	16, 24	recne0d 10313	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
118	117	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
119	116, 118	rereccld 10370	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
120	26, 119	eqeltrrd 2556	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
121		1red 9610	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
122	120, 121	resubcld 9986	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
123	13, 122	eqeltrrd 2556	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
124	2, 123	negrebd 9928	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
125	124	absord 13209	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\/$
126		eqeq1 2471	. . . . . . . . . . . . 13
127	126	biimpd 207	. . . . . . . . . . . 12
128		eqeq1 2471	. . . . . . . . . . . . 13
129	128	biimpd 207	. . . . . . . . . . . 12
130	127, 129	orim12d 836	. . . . . . . . . . 11 $\/$ $\/$
131	7, 125, 130	sylc 60	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\/$
132	131	ord 377	. . . . . . . . 9 $/\$ $/\$ $/\$
133	6, 132	mpd 15	. . . . . . . 8 $/\$ $/\$ $/\$
134	133, 5	eqeltrrd 2556	. . . . . . 7 $/\$ $/\$ $/\$
135	5, 134	rpaddcld 11270	. . . . . 6 $/\$ $/\$ $/\$
136	3, 135	eqeltrrd 2556	. . . . 5 $/\$ $/\$ $/\$
137	136	relogcld 22752	. . . 4 $/\$ $/\$ $/\$
138	137	reim0d 13020	. . 3 $/\$ $/\$ $/\$
139	134, 136	rpdivcld 11272	. . . . 5 $/\$ $/\$ $/\$
140	139	relogcld 22752	. . . 4 $/\$ $/\$ $/\$
141	140	reim0d 13020	. . 3 $/\$ $/\$ $/\$
142	138, 141	eqtr4d 2511	. 2 $/\$ $/\$ $/\$
143	16, 24	logcld 22702	. . . . . 6 $/\$ $/\$
144	143	adantr 465	. . . . 5 $/\$ $/\$ $/\$
145	144	imcld 12990	. . . 4 $/\$ $/\$ $/\$
146	145	recnd 9621	. . 3 $/\$ $/\$ $/\$
147	109	adantr 465	. . . . . 6 $/\$ $/\$ $/\$
148	15, 78	negne0d 9927	. . . . . . . 8 $/\$ $/\$
149	29, 16, 148, 24	divne0d 10335	. . . . . . 7 $/\$ $/\$
150	149	adantr 465	. . . . . 6 $/\$ $/\$ $/\$
151	147, 150	logcld 22702	. . . . 5 $/\$ $/\$ $/\$
152	151	imcld 12990	. . . 4 $/\$ $/\$ $/\$
153	152	recnd 9621	. . 3 $/\$ $/\$ $/\$
154	107	fveq2d 5869	. . . . . . 7 $/\$ $/\$
155	154	adantr 465	. . . . . 6 $/\$ $/\$ $/\$
156		logcj 22735	. . . . . . 7 $/\$
157	109, 156	sylan 471	. . . . . 6 $/\$ $/\$ $/\$
158	16, 24	reccld 10312	. . . . . . . . . 10 $/\$ $/\$
159	158, 117	logcld 22702	. . . . . . . . 9 $/\$ $/\$
160	159	negnegd 9920	. . . . . . . 8 $/\$ $/\$
161		isosctrlem1 22896	. . . . . . . . . 10 $/\$ $/\$
162		logrec 22895	. . . . . . . . . 10 $/\$ $/\$
163	16, 24, 161, 162	syl3anc 1228	. . . . . . . . 9 $/\$ $/\$
164	163	negeqd 9813	. . . . . . . 8 $/\$ $/\$
165	27	fveq2d 5869	. . . . . . . 8 $/\$ $/\$
166	160, 164, 165	3eqtr4rd 2519	. . . . . . 7 $/\$ $/\$
167	166	adantr 465	. . . . . 6 $/\$ $/\$ $/\$
168	155, 157, 167	3eqtr3rd 2517	. . . . 5 $/\$ $/\$ $/\$
169	168	fveq2d 5869	. . . 4 $/\$ $/\$ $/\$
170	144	imnegd 13005	. . . 4 $/\$ $/\$ $/\$
171	151	imcjd 13000	. . . 4 $/\$ $/\$ $/\$
172	169, 170, 171	3eqtr3d 2516	. . 3 $/\$ $/\$ $/\$
173	146, 153, 172	neg11d 9941	. 2 $/\$ $/\$ $/\$
174	142, 173	pm2.61dane 2785	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1379

wcel 1767

wne 2662

cfv 5587 (class class class)co 6283

cc 9489

cr 9490

cc0 9491

c1 9492

caddc 9494

cmul 9496

cmin 9804

cneg 9805

cdiv 10205

c2 10584

crp 11219

cexp 12133

ccj 12891

cim 12893

cabs 13029

cpi 13663

clog 22686

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6575 ax-inf2 8057 ax-cnex 9547 ax-resscn 9548 ax-1cn 9549 ax-icn 9550 ax-addcl 9551 ax-addrcl 9552 ax-mulcl 9553 ax-mulrcl 9554 ax-mulcom 9555 ax-addass 9556 ax-mulass 9557 ax-distr 9558 ax-i2m1 9559 ax-1ne0 9560 ax-1rid 9561 ax-rnegex 9562 ax-rrecex 9563 ax-cnre 9564 ax-pre-lttri 9565 ax-pre-lttrn 9566 ax-pre-ltadd 9567 ax-pre-mulgt0 9568 ax-pre-sup 9569 ax-addf 9570 ax-mulf 9571

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-iin 4328 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5550 df-fun 5589 df-fn 5590 df-f 5591 df-f1 5592 df-fo 5593 df-f1o 5594 df-fv 5595 df-isom 5596 df-riota 6244 df-ov 6286 df-oprab 6287 df-mpt2 6288 df-of 6523 df-om 6680 df-1st 6784 df-2nd 6785 df-supp 6902 df-recs 7042 df-rdg 7076 df-1o 7130 df-2o 7131 df-oadd 7134 df-er 7311 df-map 7422 df-pm 7423 df-ixp 7470 df-en 7517 df-dom 7518 df-sdom 7519 df-fin 7520 df-fsupp 7829 df-fi 7870 df-sup 7900 df-oi 7934 df-card 8319 df-cda 8547 df-pnf 9629 df-mnf 9630 df-xr 9631 df-ltxr 9632 df-le 9633 df-sub 9806 df-neg 9807 df-div 10206 df-nn 10536 df-2 10593 df-3 10594 df-4 10595 df-5 10596 df-6 10597 df-7 10598 df-8 10599 df-9 10600 df-10 10601 df-n0 10795 df-z 10864 df-dec 10976 df-uz 11082 df-q 11182 df-rp 11220 df-xneg 11317 df-xadd 11318 df-xmul 11319 df-ioo 11532 df-ioc 11533 df-ico 11534 df-icc 11535 df-fz 11672 df-fzo 11792 df-fl 11896 df-mod 11964 df-seq 12075 df-exp 12134 df-fac 12321 df-bc 12348 df-hash 12373 df-shft 12862 df-cj 12894 df-re 12895 df-im 12896 df-sqrt 13030 df-abs 13031 df-limsup 13256 df-clim 13273 df-rlim 13274 df-sum 13471 df-ef 13664 df-sin 13666 df-cos 13667 df-pi 13669 df-struct 14491 df-ndx 14492 df-slot 14493 df-base 14494 df-sets 14495 df-ress 14496 df-plusg 14567 df-mulr 14568 df-starv 14569 df-sca 14570 df-vsca 14571 df-ip 14572 df-tset 14573 df-ple 14574 df-ds 14576 df-unif 14577 df-hom 14578 df-cco 14579 df-rest 14677 df-topn 14678 df-0g 14696 df-gsum 14697 df-topgen 14698 df-pt 14699 df-prds 14702 df-xrs 14756 df-qtop 14761 df-imas 14762 df-xps 14764 df-mre 14840 df-mrc 14841 df-acs 14843 df-mnd 15731 df-submnd 15784 df-mulg 15867 df-cntz 16157 df-cmn 16603 df-psmet 18198 df-xmet 18199 df-met 18200 df-bl 18201 df-mopn 18202 df-fbas 18203 df-fg 18204 df-cnfld 18208 df-top 19182 df-bases 19184 df-topon 19185 df-topsp 19186 df-cld 19302 df-ntr 19303 df-cls 19304 df-nei 19381 df-lp 19419 df-perf 19420 df-cn 19510 df-cnp 19511 df-haus 19598 df-tx 19814 df-hmeo 20007 df-fil 20098 df-fm 20190 df-flim 20191 df-flf 20192 df-xms 20574 df-ms 20575 df-tms 20576 df-cncf 21133 df-limc 22021 df-dv 22022 df-log 22688

This theorem is referenced by: isosctrlem3 22898

W3C validator