isosctrlem2 - Metamath Proof Explorer

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

Theorem isosctrlem2 23018

Description: Lemma for isosctr 23020. 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 9610	. . . . . . 7 $/\$ $/\$ $/\$
2		simpl1 998	. . . . . . 7 $/\$ $/\$ $/\$
3	1, 2	negsubd 9937	. . . . . 6 $/\$ $/\$ $/\$
4		1rp 11228	. . . . . . . 8
5	4	a1i 11	. . . . . . 7 $/\$ $/\$ $/\$
6		simpl3 1000	. . . . . . . . 9 $/\$ $/\$ $/\$
7		simpl2 999	. . . . . . . . . . 11 $/\$ $/\$ $/\$
8	1, 2, 1	sub32d 9963	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
9		1m1e0 10605	. . . . . . . . . . . . . . . . 17
10	9	oveq1i 6287	. . . . . . . . . . . . . . . 16
11		df-neg 9808	. . . . . . . . . . . . . . . 16
12	10, 11	eqtr4i 2473	. . . . . . . . . . . . . . 15
13	8, 12	syl6eq 2498	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
14		1cnd 9610	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
15		simp1 995	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
16	14, 15	subcld 9931	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
17	16	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
18		ax-1cn 9548	. . . . . . . . . . . . . . . . . . . . . . 23
19		subeq0 9845	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
20	18, 19	mpan 670	. . . . . . . . . . . . . . . . . . . . . 22
21	20	biimpd 207	. . . . . . . . . . . . . . . . . . . . 21
22	21	con3dimp 441	. . . . . . . . . . . . . . . . . . . 20 $/\$
23	22	neqned 2644	. . . . . . . . . . . . . . . . . . 19 $/\$
24	23	3adant2 1014	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
25	24	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
26	17, 25	recrecd 10318	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
27	14, 16, 24	div2negd 10336	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
28	27	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
29	15	negcld 9918	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
30	29, 16, 24	cjdivd 13030	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
31	15	cjnegd 13018	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
32		fveq2 5852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
33		abs0 13092	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
34	32, 33	syl6eq 2498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
35		eqtr2 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
36	34, 35	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
37		ax-1ne0 9559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
38		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
39	38	neneqd 2643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
40	37, 39	mp1i 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
41	36, 40	pm2.65da 576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
42	41	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
43		df-ne 2638	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
44		oveq1 6284	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
45		sq1 12236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
46	44, 45	syl6eq 2498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
47	46	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
48		absvalsq 13087	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
49	48	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
50	47, 49	eqtr3d 2484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
51	50	3adant3 1015	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
52	51	oveq1d 6292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
53		simp1 995	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
54	53	cjcld 13003	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
55		simp3 997	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
56	54, 53, 55	divcan3d 10326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
57	52, 56	eqtrd 2482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
58	43, 57	syl3an3br 1268	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
59	42, 58	mpd3an3 1324	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
60	59	eqcomd 2449	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
61	60	3adant3 1015	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
62	61	negeqd 9814	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
63	31, 62	eqtrd 2482	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
64	63	oveq1d 6292	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
65		cjsub 12956	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
66	18, 65	mpan 670	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
67		1red 9609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
68	67	cjred 13033	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
69	68	oveq1d 6292	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
70	66, 69	eqtrd 2482	. . . . . . . . . . . . . . . . . . . . . . . . . 26
71	70	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
72	60	oveq2d 6293	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
73	71, 72	eqtrd 2482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
74	73	3adant3 1015	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
75	74	oveq2d 6293	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
76	30, 64, 75	3eqtrd 2486	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
77	41	3ad2ant2 1017	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
78	77	neqned 2644	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
79		1cnd 9610	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
80		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
81		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
82	79, 80, 81	divnegd 10334	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
83	82	oveq1d 6292	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
84	15, 78, 83	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
85	14	negcld 9918	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
86	85, 15, 78	divcld 10321	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
87	15, 78	reccld 10314	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
88	14, 87	subcld 9931	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
89	16, 24	cjne0d 13010	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
90	74, 89	eqnetrrd 2735	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
91	86, 88, 15, 90, 78	divcan5d 10347	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
92	85, 15, 78	divcan2d 10323	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
93	15, 14, 87	subdid 10013	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
94	15	mulid1d 9611	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
95	15, 78	recidd 10316	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
96	94, 95	oveq12d 6295	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
97	93, 96	eqtrd 2482	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
98	92, 97	oveq12d 6295	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
99	84, 91, 98	3eqtr2d 2488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
100		subcl 9819	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
101	100	negnegd 9922	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
102		negsubdi2 9878	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
103	102	negeqd 9814	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
104	101, 103	eqtr3d 2484	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
105	15, 14, 104	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
106	105	oveq2d 6293	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
107	76, 99, 106	3eqtrd 2486	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
108	107	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
109	29, 16, 24	divcld 10321	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
110	109	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
111		simpr 461	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
112	110, 111	reim0bd 13007	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
113	112	cjred 13033	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
114	113, 112	eqeltrd 2529	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
115	108, 114	eqeltrrd 2530	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
116	28, 115	eqeltrrd 2530	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
117	16, 24	recne0d 10315	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
118	117	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
119	116, 118	rereccld 10372	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
120	26, 119	eqeltrrd 2530	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
121		1red 9609	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
122	120, 121	resubcld 9988	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
123	13, 122	eqeltrrd 2530	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
124	2, 123	negrebd 9930	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
125	124	absord 13221	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\/$
126		eqeq1 2445	. . . . . . . . . . . . 13
127	126	biimpd 207	. . . . . . . . . . . 12
128		eqeq1 2445	. . . . . . . . . . . . 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 2530	. . . . . . 7 $/\$ $/\$ $/\$
135	5, 134	rpaddcld 11275	. . . . . 6 $/\$ $/\$ $/\$
136	3, 135	eqeltrrd 2530	. . . . 5 $/\$ $/\$ $/\$
137	136	relogcld 22873	. . . 4 $/\$ $/\$ $/\$
138	137	reim0d 13032	. . 3 $/\$ $/\$ $/\$
139	134, 136	rpdivcld 11277	. . . . 5 $/\$ $/\$ $/\$
140	139	relogcld 22873	. . . 4 $/\$ $/\$ $/\$
141	140	reim0d 13032	. . 3 $/\$ $/\$ $/\$
142	138, 141	eqtr4d 2485	. 2 $/\$ $/\$ $/\$
143	16, 24	logcld 22823	. . . . . 6 $/\$ $/\$
144	143	adantr 465	. . . . 5 $/\$ $/\$ $/\$
145	144	imcld 13002	. . . 4 $/\$ $/\$ $/\$
146	145	recnd 9620	. . 3 $/\$ $/\$ $/\$
147	109	adantr 465	. . . . . 6 $/\$ $/\$ $/\$
148	15, 78	negne0d 9929	. . . . . . . 8 $/\$ $/\$
149	29, 16, 148, 24	divne0d 10337	. . . . . . 7 $/\$ $/\$
150	149	adantr 465	. . . . . 6 $/\$ $/\$ $/\$
151	147, 150	logcld 22823	. . . . 5 $/\$ $/\$ $/\$
152	151	imcld 13002	. . . 4 $/\$ $/\$ $/\$
153	152	recnd 9620	. . 3 $/\$ $/\$ $/\$
154	107	fveq2d 5856	. . . . . . 7 $/\$ $/\$
155	154	adantr 465	. . . . . 6 $/\$ $/\$ $/\$
156		logcj 22856	. . . . . . 7 $/\$
157	109, 156	sylan 471	. . . . . 6 $/\$ $/\$ $/\$
158	16, 24	reccld 10314	. . . . . . . . . 10 $/\$ $/\$
159	158, 117	logcld 22823	. . . . . . . . 9 $/\$ $/\$
160	159	negnegd 9922	. . . . . . . 8 $/\$ $/\$
161		isosctrlem1 23017	. . . . . . . . . 10 $/\$ $/\$
162		logrec 23016	. . . . . . . . . 10 $/\$ $/\$
163	16, 24, 161, 162	syl3anc 1227	. . . . . . . . 9 $/\$ $/\$
164	163	negeqd 9814	. . . . . . . 8 $/\$ $/\$
165	27	fveq2d 5856	. . . . . . . 8 $/\$ $/\$
166	160, 164, 165	3eqtr4rd 2493	. . . . . . 7 $/\$ $/\$
167	166	adantr 465	. . . . . 6 $/\$ $/\$ $/\$
168	155, 157, 167	3eqtr3rd 2491	. . . . 5 $/\$ $/\$ $/\$
169	168	fveq2d 5856	. . . 4 $/\$ $/\$ $/\$
170	144	imnegd 13017	. . . 4 $/\$ $/\$ $/\$
171	151	imcjd 13012	. . . 4 $/\$ $/\$ $/\$
172	169, 170, 171	3eqtr3d 2490	. . 3 $/\$ $/\$ $/\$
173	146, 153, 172	neg11d 9943	. 2 $/\$ $/\$ $/\$
174	142, 173	pm2.61dane 2759	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1381

wcel 1802

wne 2636

cfv 5574 (class class class)co 6277

cc 9488

cr 9489

cc0 9490

c1 9491

caddc 9493

cmul 9495

cmin 9805

cneg 9806

cdiv 10207

c2 10586

crp 11224

cexp 12140

ccj 12903

cim 12905

cabs 13041

cpi 13675

clog 22807

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1603 ax-4 1616 ax-5 1689 ax-6 1732 ax-7 1774 ax-8 1804 ax-9 1806 ax-10 1821 ax-11 1826 ax-12 1838 ax-13 1983 ax-ext 2419 ax-rep 4544 ax-sep 4554 ax-nul 4562 ax-pow 4611 ax-pr 4672 ax-un 6573 ax-inf2 8056 ax-cnex 9546 ax-resscn 9547 ax-1cn 9548 ax-icn 9549 ax-addcl 9550 ax-addrcl 9551 ax-mulcl 9552 ax-mulrcl 9553 ax-mulcom 9554 ax-addass 9555 ax-mulass 9556 ax-distr 9557 ax-i2m1 9558 ax-1ne0 9559 ax-1rid 9560 ax-rnegex 9561 ax-rrecex 9562 ax-cnre 9563 ax-pre-lttri 9564 ax-pre-lttrn 9565 ax-pre-ltadd 9566 ax-pre-mulgt0 9567 ax-pre-sup 9568 ax-addf 9569 ax-mulf 9570

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 973 df-3an 974 df-tru 1384 df-fal 1387 df-ex 1598 df-nf 1602 df-sb 1725 df-eu 2270 df-mo 2271 df-clab 2427 df-cleq 2433 df-clel 2436 df-nfc 2591 df-ne 2638 df-nel 2639 df-ral 2796 df-rex 2797 df-reu 2798 df-rmo 2799 df-rab 2800 df-v 3095 df-sbc 3312 df-csb 3418 df-dif 3461 df-un 3463 df-in 3465 df-ss 3472 df-pss 3474 df-nul 3768 df-if 3923 df-pw 3995 df-sn 4011 df-pr 4013 df-tp 4015 df-op 4017 df-uni 4231 df-int 4268 df-iun 4313 df-iin 4314 df-br 4434 df-opab 4492 df-mpt 4493 df-tr 4527 df-eprel 4777 df-id 4781 df-po 4786 df-so 4787 df-fr 4824 df-se 4825 df-we 4826 df-ord 4867 df-on 4868 df-lim 4869 df-suc 4870 df-xp 4991 df-rel 4992 df-cnv 4993 df-co 4994 df-dm 4995 df-rn 4996 df-res 4997 df-ima 4998 df-iota 5537 df-fun 5576 df-fn 5577 df-f 5578 df-f1 5579 df-fo 5580 df-f1o 5581 df-fv 5582 df-isom 5583 df-riota 6238 df-ov 6280 df-oprab 6281 df-mpt2 6282 df-of 6521 df-om 6682 df-1st 6781 df-2nd 6782 df-supp 6900 df-recs 7040 df-rdg 7074 df-1o 7128 df-2o 7129 df-oadd 7132 df-er 7309 df-map 7420 df-pm 7421 df-ixp 7468 df-en 7515 df-dom 7516 df-sdom 7517 df-fin 7518 df-fsupp 7828 df-fi 7869 df-sup 7899 df-oi 7933 df-card 8318 df-cda 8546 df-pnf 9628 df-mnf 9629 df-xr 9630 df-ltxr 9631 df-le 9632 df-sub 9807 df-neg 9808 df-div 10208 df-nn 10538 df-2 10595 df-3 10596 df-4 10597 df-5 10598 df-6 10599 df-7 10600 df-8 10601 df-9 10602 df-10 10603 df-n0 10797 df-z 10866 df-dec 10980 df-uz 11086 df-q 11187 df-rp 11225 df-xneg 11322 df-xadd 11323 df-xmul 11324 df-ioo 11537 df-ioc 11538 df-ico 11539 df-icc 11540 df-fz 11677 df-fzo 11799 df-fl 11903 df-mod 11971 df-seq 12082 df-exp 12141 df-fac 12328 df-bc 12355 df-hash 12380 df-shft 12874 df-cj 12906 df-re 12907 df-im 12908 df-sqrt 13042 df-abs 13043 df-limsup 13268 df-clim 13285 df-rlim 13286 df-sum 13483 df-ef 13676 df-sin 13678 df-cos 13679 df-pi 13681 df-struct 14506 df-ndx 14507 df-slot 14508 df-base 14509 df-sets 14510 df-ress 14511 df-plusg 14582 df-mulr 14583 df-starv 14584 df-sca 14585 df-vsca 14586 df-ip 14587 df-tset 14588 df-ple 14589 df-ds 14591 df-unif 14592 df-hom 14593 df-cco 14594 df-rest 14692 df-topn 14693 df-0g 14711 df-gsum 14712 df-topgen 14713 df-pt 14714 df-prds 14717 df-xrs 14771 df-qtop 14776 df-imas 14777 df-xps 14779 df-mre 14855 df-mrc 14856 df-acs 14858 df-mgm 15741 df-sgrp 15780 df-mnd 15790 df-submnd 15836 df-mulg 15929 df-cntz 16224 df-cmn 16669 df-psmet 18279 df-xmet 18280 df-met 18281 df-bl 18282 df-mopn 18283 df-fbas 18284 df-fg 18285 df-cnfld 18289 df-top 19266 df-bases 19268 df-topon 19269 df-topsp 19270 df-cld 19386 df-ntr 19387 df-cls 19388 df-nei 19465 df-lp 19503 df-perf 19504 df-cn 19594 df-cnp 19595 df-haus 19682 df-tx 19929 df-hmeo 20122 df-fil 20213 df-fm 20305 df-flim 20306 df-flf 20307 df-xms 20689 df-ms 20690 df-tms 20691 df-cncf 21248 df-limc 22136 df-dv 22137 df-log 22809

This theorem is referenced by: isosctrlem3 23019

W3C validator