isosctrlem2 - Metamath Proof Explorer

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

Theorem isosctrlem2 22229

Description: Lemma for isosctr 22231. 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 9414	. . . . . . 7 $/\$ $/\$ $/\$
2		simpl1 991	. . . . . . 7 $/\$ $/\$ $/\$
3	1, 2	negsubd 9737	. . . . . 6 $/\$ $/\$ $/\$
4		1rp 11007	. . . . . . . 8
5	4	a1i 11	. . . . . . 7 $/\$ $/\$ $/\$
6		simpl3 993	. . . . . . . . 9 $/\$ $/\$ $/\$
7		simpl2 992	. . . . . . . . . . 11 $/\$ $/\$ $/\$
8	1, 2, 1	sub32d 9763	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
9		1m1e0 10402	. . . . . . . . . . . . . . . . 17
10	9	oveq1i 6113	. . . . . . . . . . . . . . . 16
11		df-neg 9610	. . . . . . . . . . . . . . . 16
12	10, 11	eqtr4i 2466	. . . . . . . . . . . . . . 15
13	8, 12	syl6eq 2491	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
14		1cnd 9414	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
15		simp1 988	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
16	14, 15	subcld 9731	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
17	16	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
18		ax-1cn 9352	. . . . . . . . . . . . . . . . . . . . . . 23
19		subeq0 9647	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
20	18, 19	mpan 670	. . . . . . . . . . . . . . . . . . . . . 22
21	20	biimpd 207	. . . . . . . . . . . . . . . . . . . . 21
22	21	con3dimp 441	. . . . . . . . . . . . . . . . . . . 20 $/\$
23	22	neneqad 2693	. . . . . . . . . . . . . . . . . . 19 $/\$
24	23	3adant2 1007	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
25	24	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
26	17, 25	recrecd 10116	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
27	14, 16, 24	div2negd 10134	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
28	27	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
29	15	negcld 9718	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
30	29, 16, 24	cjdivd 12724	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
31	15	cjnegd 12712	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
32		fveq2 5703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
33		abs0 12786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
34	32, 33	syl6eq 2491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
35		eqtr2 2461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
36	34, 35	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
37		ax-1ne0 9363	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
38		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
39	38	neneqd 2636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
40	37, 39	mp1i 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
41	36, 40	pm2.65da 576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
42	41	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
43		df-ne 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
44		oveq1 6110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
45		sq1 11972	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
46	44, 45	syl6eq 2491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
47	46	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
48		absvalsq 12781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
49	48	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
50	47, 49	eqtr3d 2477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
51	50	3adant3 1008	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
52	51	oveq1d 6118	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
53		simp1 988	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
54	53	cjcld 12697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
55		simp3 990	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
56	54, 53, 55	divcan3d 10124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
57	52, 56	eqtrd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
58	43, 57	syl3an3br 1259	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
59	42, 58	mpd3an3 1315	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
60	59	eqcomd 2448	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
61	60	3adant3 1008	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
62	61	negeqd 9616	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
63	31, 62	eqtrd 2475	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
64	63	oveq1d 6118	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
65		cjsub 12650	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
66	18, 65	mpan 670	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
67		1red 9413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
68	67	cjred 12727	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
69	68	oveq1d 6118	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
70	66, 69	eqtrd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . 26
71	70	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
72	60	oveq2d 6119	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
73	71, 72	eqtrd 2475	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
74	73	3adant3 1008	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
75	74	oveq2d 6119	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
76	30, 64, 75	3eqtrd 2479	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
77	41	3ad2ant2 1010	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
78	77	neneqad 2693	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
79		1cnd 9414	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
80		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
81		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
82	79, 80, 81	divnegd 10132	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
83	82	oveq1d 6118	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
84	15, 78, 83	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
85	14	negcld 9718	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
86	85, 15, 78	divcld 10119	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
87	15, 78	reccld 10112	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
88	14, 87	subcld 9731	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
89	16, 24	cjne0d 12704	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
90	74, 89	eqnetrrd 2640	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
91	86, 88, 15, 90, 78	divcan5d 10145	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
92	85, 15, 78	divcan2d 10121	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
93	15, 14, 87	subdid 9812	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
94	15	mulid1d 9415	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
95	15, 78	recidd 10114	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
96	94, 95	oveq12d 6121	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
97	93, 96	eqtrd 2475	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
98	92, 97	oveq12d 6121	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
99	84, 91, 98	3eqtr2d 2481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
100		subcl 9621	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
101	100	negnegd 9722	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
102		negsubdi2 9680	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
103	102	negeqd 9616	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
104	101, 103	eqtr3d 2477	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
105	15, 14, 104	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
106	105	oveq2d 6119	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
107	76, 99, 106	3eqtrd 2479	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
108	107	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
109	29, 16, 24	divcld 10119	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
110	109	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
111		simpr 461	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
112	110, 111	reim0bd 12701	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
113	112	cjred 12727	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
114	113, 112	eqeltrd 2517	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
115	108, 114	eqeltrrd 2518	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
116	28, 115	eqeltrrd 2518	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
117	16, 24	recne0d 10113	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
118	117	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
119	116, 118	rereccld 10170	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
120	26, 119	eqeltrrd 2518	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
121		1red 9413	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
122	120, 121	resubcld 9788	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
123	13, 122	eqeltrrd 2518	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
124	2, 123	negrebd 9730	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
125	124	absord 12914	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\/$
126		eqeq1 2449	. . . . . . . . . . . . 13
127	126	biimpd 207	. . . . . . . . . . . 12
128		eqeq1 2449	. . . . . . . . . . . . 13
129	128	biimpd 207	. . . . . . . . . . . 12
130	127, 129	orim12d 834	. . . . . . . . . . 11 $\/$ $\/$
131	7, 125, 130	sylc 60	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\/$
132	131	ord 377	. . . . . . . . 9 $/\$ $/\$ $/\$
133	6, 132	mpd 15	. . . . . . . 8 $/\$ $/\$ $/\$
134	133, 5	eqeltrrd 2518	. . . . . . 7 $/\$ $/\$ $/\$
135	5, 134	rpaddcld 11054	. . . . . 6 $/\$ $/\$ $/\$
136	3, 135	eqeltrrd 2518	. . . . 5 $/\$ $/\$ $/\$
137	136	relogcld 22084	. . . 4 $/\$ $/\$ $/\$
138	137	reim0d 12726	. . 3 $/\$ $/\$ $/\$
139	134, 136	rpdivcld 11056	. . . . 5 $/\$ $/\$ $/\$
140	139	relogcld 22084	. . . 4 $/\$ $/\$ $/\$
141	140	reim0d 12726	. . 3 $/\$ $/\$ $/\$
142	138, 141	eqtr4d 2478	. 2 $/\$ $/\$ $/\$
143	16, 24	logcld 22034	. . . . . 6 $/\$ $/\$
144	143	adantr 465	. . . . 5 $/\$ $/\$ $/\$
145	144	imcld 12696	. . . 4 $/\$ $/\$ $/\$
146	145	recnd 9424	. . 3 $/\$ $/\$ $/\$
147	109	adantr 465	. . . . . 6 $/\$ $/\$ $/\$
148	15, 78	negne0d 9729	. . . . . . . 8 $/\$ $/\$
149	29, 16, 148, 24	divne0d 10135	. . . . . . 7 $/\$ $/\$
150	149	adantr 465	. . . . . 6 $/\$ $/\$ $/\$
151	147, 150	logcld 22034	. . . . 5 $/\$ $/\$ $/\$
152	151	imcld 12696	. . . 4 $/\$ $/\$ $/\$
153	152	recnd 9424	. . 3 $/\$ $/\$ $/\$
154	107	fveq2d 5707	. . . . . . 7 $/\$ $/\$
155	154	adantr 465	. . . . . 6 $/\$ $/\$ $/\$
156		logcj 22067	. . . . . . 7 $/\$
157	109, 156	sylan 471	. . . . . 6 $/\$ $/\$ $/\$
158	16, 24	reccld 10112	. . . . . . . . . 10 $/\$ $/\$
159	158, 117	logcld 22034	. . . . . . . . 9 $/\$ $/\$
160	159	negnegd 9722	. . . . . . . 8 $/\$ $/\$
161		isosctrlem1 22228	. . . . . . . . . 10 $/\$ $/\$
162		logrec 22227	. . . . . . . . . 10 $/\$ $/\$
163	16, 24, 161, 162	syl3anc 1218	. . . . . . . . 9 $/\$ $/\$
164	163	negeqd 9616	. . . . . . . 8 $/\$ $/\$
165	27	fveq2d 5707	. . . . . . . 8 $/\$ $/\$
166	160, 164, 165	3eqtr4rd 2486	. . . . . . 7 $/\$ $/\$
167	166	adantr 465	. . . . . 6 $/\$ $/\$ $/\$
168	155, 157, 167	3eqtr3rd 2484	. . . . 5 $/\$ $/\$ $/\$
169	168	fveq2d 5707	. . . 4 $/\$ $/\$ $/\$
170	144	imnegd 12711	. . . 4 $/\$ $/\$ $/\$
171	151	imcjd 12706	. . . 4 $/\$ $/\$ $/\$
172	169, 170, 171	3eqtr3d 2483	. . 3 $/\$ $/\$ $/\$
173	146, 153, 172	neg11d 9743	. 2 $/\$ $/\$ $/\$
174	142, 173	pm2.61dane 2701	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1369

wcel 1756

wne 2618

cfv 5430 (class class class)co 6103

cc 9292

cr 9293

cc0 9294

c1 9295

caddc 9297

cmul 9299

cmin 9607

cneg 9608

cdiv 10005

c2 10383

crp 11003

cexp 11877

ccj 12597

cim 12599

cabs 12735

cpi 13364

clog 22018

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4415 ax-sep 4425 ax-nul 4433 ax-pow 4482 ax-pr 4543 ax-un 6384 ax-inf2 7859 ax-cnex 9350 ax-resscn 9351 ax-1cn 9352 ax-icn 9353 ax-addcl 9354 ax-addrcl 9355 ax-mulcl 9356 ax-mulrcl 9357 ax-mulcom 9358 ax-addass 9359 ax-mulass 9360 ax-distr 9361 ax-i2m1 9362 ax-1ne0 9363 ax-1rid 9364 ax-rnegex 9365 ax-rrecex 9366 ax-cnre 9367 ax-pre-lttri 9368 ax-pre-lttrn 9369 ax-pre-ltadd 9370 ax-pre-mulgt0 9371 ax-pre-sup 9372 ax-addf 9373 ax-mulf 9374

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-fal 1375 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2577 df-ne 2620 df-nel 2621 df-ral 2732 df-rex 2733 df-reu 2734 df-rmo 2735 df-rab 2736 df-v 2986 df-sbc 3199 df-csb 3301 df-dif 3343 df-un 3345 df-in 3347 df-ss 3354 df-pss 3356 df-nul 3650 df-if 3804 df-pw 3874 df-sn 3890 df-pr 3892 df-tp 3894 df-op 3896 df-uni 4104 df-int 4141 df-iun 4185 df-iin 4186 df-br 4305 df-opab 4363 df-mpt 4364 df-tr 4398 df-eprel 4644 df-id 4648 df-po 4653 df-so 4654 df-fr 4691 df-se 4692 df-we 4693 df-ord 4734 df-on 4735 df-lim 4736 df-suc 4737 df-xp 4858 df-rel 4859 df-cnv 4860 df-co 4861 df-dm 4862 df-rn 4863 df-res 4864 df-ima 4865 df-iota 5393 df-fun 5432 df-fn 5433 df-f 5434 df-f1 5435 df-fo 5436 df-f1o 5437 df-fv 5438 df-isom 5439 df-riota 6064 df-ov 6106 df-oprab 6107 df-mpt2 6108 df-of 6332 df-om 6489 df-1st 6589 df-2nd 6590 df-supp 6703 df-recs 6844 df-rdg 6878 df-1o 6932 df-2o 6933 df-oadd 6936 df-er 7113 df-map 7228 df-pm 7229 df-ixp 7276 df-en 7323 df-dom 7324 df-sdom 7325 df-fin 7326 df-fsupp 7633 df-fi 7673 df-sup 7703 df-oi 7736 df-card 8121 df-cda 8349 df-pnf 9432 df-mnf 9433 df-xr 9434 df-ltxr 9435 df-le 9436 df-sub 9609 df-neg 9610 df-div 10006 df-nn 10335 df-2 10392 df-3 10393 df-4 10394 df-5 10395 df-6 10396 df-7 10397 df-8 10398 df-9 10399 df-10 10400 df-n0 10592 df-z 10659 df-dec 10768 df-uz 10874 df-q 10966 df-rp 11004 df-xneg 11101 df-xadd 11102 df-xmul 11103 df-ioo 11316 df-ioc 11317 df-ico 11318 df-icc 11319 df-fz 11450 df-fzo 11561 df-fl 11654 df-mod 11721 df-seq 11819 df-exp 11878 df-fac 12064 df-bc 12091 df-hash 12116 df-shft 12568 df-cj 12600 df-re 12601 df-im 12602 df-sqr 12736 df-abs 12737 df-limsup 12961 df-clim 12978 df-rlim 12979 df-sum 13176 df-ef 13365 df-sin 13367 df-cos 13368 df-pi 13370 df-struct 14188 df-ndx 14189 df-slot 14190 df-base 14191 df-sets 14192 df-ress 14193 df-plusg 14263 df-mulr 14264 df-starv 14265 df-sca 14266 df-vsca 14267 df-ip 14268 df-tset 14269 df-ple 14270 df-ds 14272 df-unif 14273 df-hom 14274 df-cco 14275 df-rest 14373 df-topn 14374 df-0g 14392 df-gsum 14393 df-topgen 14394 df-pt 14395 df-prds 14398 df-xrs 14452 df-qtop 14457 df-imas 14458 df-xps 14460 df-mre 14536 df-mrc 14537 df-acs 14539 df-mnd 15427 df-submnd 15477 df-mulg 15560 df-cntz 15847 df-cmn 16291 df-psmet 17821 df-xmet 17822 df-met 17823 df-bl 17824 df-mopn 17825 df-fbas 17826 df-fg 17827 df-cnfld 17831 df-top 18515 df-bases 18517 df-topon 18518 df-topsp 18519 df-cld 18635 df-ntr 18636 df-cls 18637 df-nei 18714 df-lp 18752 df-perf 18753 df-cn 18843 df-cnp 18844 df-haus 18931 df-tx 19147 df-hmeo 19340 df-fil 19431 df-fm 19523 df-flim 19524 df-flf 19525 df-xms 19907 df-ms 19908 df-tms 19909 df-cncf 20466 df-limc 21353 df-dv 21354 df-log 22020

This theorem is referenced by: isosctrlem3 22230

W3C validator