isosctrlem2 - Metamath Proof Explorer

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

Theorem isosctrlem2 23748

Description: Lemma for isosctr 23750. 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 9659	. . . . . . 7 $/\$ $/\$ $/\$
2		simpl1 1011	. . . . . . 7 $/\$ $/\$ $/\$
3	1, 2	negsubd 9992	. . . . . 6 $/\$ $/\$ $/\$
4		1rp 11306	. . . . . . . 8
5	4	a1i 11	. . . . . . 7 $/\$ $/\$ $/\$
6		simpl3 1013	. . . . . . . . 9 $/\$ $/\$ $/\$
7		simpl2 1012	. . . . . . . . . . 11 $/\$ $/\$ $/\$
8	1, 2, 1	sub32d 10018	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
9		1m1e0 10678	. . . . . . . . . . . . . . . . 17
10	9	oveq1i 6300	. . . . . . . . . . . . . . . 16
11		df-neg 9863	. . . . . . . . . . . . . . . 16
12	10, 11	eqtr4i 2476	. . . . . . . . . . . . . . 15
13	8, 12	syl6eq 2501	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
14		1cnd 9659	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
15		simp1 1008	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
16	14, 15	subcld 9986	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
17	16	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
18		ax-1cn 9597	. . . . . . . . . . . . . . . . . . . . . . 23
19		subeq0 9900	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
20	18, 19	mpan 676	. . . . . . . . . . . . . . . . . . . . . 22
21	20	biimpd 211	. . . . . . . . . . . . . . . . . . . . 21
22	21	con3dimp 443	. . . . . . . . . . . . . . . . . . . 20 $/\$
23	22	neqned 2631	. . . . . . . . . . . . . . . . . . 19 $/\$
24	23	3adant2 1027	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
25	24	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
26	17, 25	recrecd 10380	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
27	14, 16, 24	div2negd 10398	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
28	27	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
29	15	negcld 9973	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
30	29, 16, 24	cjdivd 13286	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
31	15	cjnegd 13274	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
32		fveq2 5865	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
33		abs0 13348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
34	32, 33	syl6eq 2501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
35		eqtr2 2471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
36	34, 35	sylan2 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
37		ax-1ne0 9608	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
38		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
39	38	neneqd 2629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
40	37, 39	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
41	36, 40	pm2.65da 580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
42	41	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
43		df-ne 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
44		oveq1 6297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
45		sq1 12369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
46	44, 45	syl6eq 2501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
47	46	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
48		absvalsq 13343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
49	48	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
50	47, 49	eqtr3d 2487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
51	50	3adant3 1028	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
52	51	oveq1d 6305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
53		simp1 1008	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
54	53	cjcld 13259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
55		simp3 1010	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
56	54, 53, 55	divcan3d 10388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
57	52, 56	eqtrd 2485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
58	43, 57	syl3an3br 1309	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
59	42, 58	mpd3an3 1365	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
60	59	eqcomd 2457	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
61	60	3adant3 1028	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
62	61	negeqd 9869	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
63	31, 62	eqtrd 2485	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
64	63	oveq1d 6305	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
65		cjsub 13212	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
66	18, 65	mpan 676	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
67		1red 9658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
68	67	cjred 13289	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
69	68	oveq1d 6305	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
70	66, 69	eqtrd 2485	. . . . . . . . . . . . . . . . . . . . . . . . . 26
71	70	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
72	60	oveq2d 6306	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
73	71, 72	eqtrd 2485	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
74	73	3adant3 1028	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
75	74	oveq2d 6306	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
76	30, 64, 75	3eqtrd 2489	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
77	41	3ad2ant2 1030	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
78	77	neqned 2631	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
79		1cnd 9659	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
80		simpl 459	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
81		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
82	79, 80, 81	divnegd 10396	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
83	82	oveq1d 6305	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
84	15, 78, 83	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
85	14	negcld 9973	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
86	85, 15, 78	divcld 10383	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
87	15, 78	reccld 10376	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
88	14, 87	subcld 9986	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
89	16, 24	cjne0d 13266	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
90	74, 89	eqnetrrd 2692	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
91	86, 88, 15, 90, 78	divcan5d 10409	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
92	85, 15, 78	divcan2d 10385	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
93	15, 14, 87	subdid 10074	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
94	15	mulid1d 9660	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
95	15, 78	recidd 10378	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
96	94, 95	oveq12d 6308	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
97	93, 96	eqtrd 2485	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
98	92, 97	oveq12d 6308	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
99	84, 91, 98	3eqtr2d 2491	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
100		subcl 9874	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
101	100	negnegd 9977	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
102		negsubdi2 9933	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
103	102	negeqd 9869	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
104	101, 103	eqtr3d 2487	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
105	15, 14, 104	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
106	105	oveq2d 6306	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
107	76, 99, 106	3eqtrd 2489	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
108	107	adantr 467	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
109	29, 16, 24	divcld 10383	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
110	109	adantr 467	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
111		simpr 463	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
112	110, 111	reim0bd 13263	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
113	112	cjred 13289	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
114	113, 112	eqeltrd 2529	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
115	108, 114	eqeltrrd 2530	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
116	28, 115	eqeltrrd 2530	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
117	16, 24	recne0d 10377	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
118	117	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
119	116, 118	rereccld 10434	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
120	26, 119	eqeltrrd 2530	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
121		1red 9658	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
122	120, 121	resubcld 10047	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
123	13, 122	eqeltrrd 2530	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
124	2, 123	negrebd 9985	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
125	124	absord 13477	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\/$
126		eqeq1 2455	. . . . . . . . . . . . 13
127	126	biimpd 211	. . . . . . . . . . . 12
128		eqeq1 2455	. . . . . . . . . . . . 13
129	128	biimpd 211	. . . . . . . . . . . 12
130	127, 129	orim12d 849	. . . . . . . . . . 11 $\/$ $\/$
131	7, 125, 130	sylc 62	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\/$
132	131	ord 379	. . . . . . . . 9 $/\$ $/\$ $/\$
133	6, 132	mpd 15	. . . . . . . 8 $/\$ $/\$ $/\$
134	133, 5	eqeltrrd 2530	. . . . . . 7 $/\$ $/\$ $/\$
135	5, 134	rpaddcld 11356	. . . . . 6 $/\$ $/\$ $/\$
136	3, 135	eqeltrrd 2530	. . . . 5 $/\$ $/\$ $/\$
137	136	relogcld 23572	. . . 4 $/\$ $/\$ $/\$
138	137	reim0d 13288	. . 3 $/\$ $/\$ $/\$
139	134, 136	rpdivcld 11358	. . . . 5 $/\$ $/\$ $/\$
140	139	relogcld 23572	. . . 4 $/\$ $/\$ $/\$
141	140	reim0d 13288	. . 3 $/\$ $/\$ $/\$
142	138, 141	eqtr4d 2488	. 2 $/\$ $/\$ $/\$
143	16, 24	logcld 23520	. . . . . 6 $/\$ $/\$
144	143	adantr 467	. . . . 5 $/\$ $/\$ $/\$
145	144	imcld 13258	. . . 4 $/\$ $/\$ $/\$
146	145	recnd 9669	. . 3 $/\$ $/\$ $/\$
147	109	adantr 467	. . . . . 6 $/\$ $/\$ $/\$
148	15, 78	negne0d 9984	. . . . . . . 8 $/\$ $/\$
149	29, 16, 148, 24	divne0d 10399	. . . . . . 7 $/\$ $/\$
150	149	adantr 467	. . . . . 6 $/\$ $/\$ $/\$
151	147, 150	logcld 23520	. . . . 5 $/\$ $/\$ $/\$
152	151	imcld 13258	. . . 4 $/\$ $/\$ $/\$
153	152	recnd 9669	. . 3 $/\$ $/\$ $/\$
154	107	fveq2d 5869	. . . . . . 7 $/\$ $/\$
155	154	adantr 467	. . . . . 6 $/\$ $/\$ $/\$
156		logcj 23555	. . . . . . 7 $/\$
157	109, 156	sylan 474	. . . . . 6 $/\$ $/\$ $/\$
158	16, 24	reccld 10376	. . . . . . . . . 10 $/\$ $/\$
159	158, 117	logcld 23520	. . . . . . . . 9 $/\$ $/\$
160	159	negnegd 9977	. . . . . . . 8 $/\$ $/\$
161		isosctrlem1 23747	. . . . . . . . . 10 $/\$ $/\$
162		logrec 23700	. . . . . . . . . 10 $/\$ $/\$
163	16, 24, 161, 162	syl3anc 1268	. . . . . . . . 9 $/\$ $/\$
164	163	negeqd 9869	. . . . . . . 8 $/\$ $/\$
165	27	fveq2d 5869	. . . . . . . 8 $/\$ $/\$
166	160, 164, 165	3eqtr4rd 2496	. . . . . . 7 $/\$ $/\$
167	166	adantr 467	. . . . . 6 $/\$ $/\$ $/\$
168	155, 157, 167	3eqtr3rd 2494	. . . . 5 $/\$ $/\$ $/\$
169	168	fveq2d 5869	. . . 4 $/\$ $/\$ $/\$
170	144	imnegd 13273	. . . 4 $/\$ $/\$ $/\$
171	151	imcjd 13268	. . . 4 $/\$ $/\$ $/\$
172	169, 170, 171	3eqtr3d 2493	. . 3 $/\$ $/\$ $/\$
173	146, 153, 172	neg11d 9998	. 2 $/\$ $/\$ $/\$
174	142, 173	pm2.61dane 2711	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $\/$ wo 370 $/\$ wa 371 $/\$ w3a 985

wceq 1444

wcel 1887

wne 2622

cfv 5582 (class class class)co 6290

cc 9537

cr 9538

cc0 9539

c1 9540

caddc 9542

cmul 9544

cmin 9860

cneg 9861

cdiv 10269

c2 10659

crp 11302

cexp 12272

ccj 13159

cim 13161

cabs 13297

cpi 14119

clog 23504

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-inf2 8146 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 ax-pre-sup 9617 ax-addf 9618 ax-mulf 9619

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-fal 1450 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-iin 4281 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-se 4794 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-isom 5591 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-of 6531 df-om 6693 df-1st 6793 df-2nd 6794 df-supp 6915 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-2o 7183 df-oadd 7186 df-er 7363 df-map 7474 df-pm 7475 df-ixp 7523 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-fsupp 7884 df-fi 7925 df-sup 7956 df-inf 7957 df-oi 8025 df-card 8373 df-cda 8598 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-div 10270 df-nn 10610 df-2 10668 df-3 10669 df-4 10670 df-5 10671 df-6 10672 df-7 10673 df-8 10674 df-9 10675 df-10 10676 df-n0 10870 df-z 10938 df-dec 11052 df-uz 11160 df-q 11265 df-rp 11303 df-xneg 11409 df-xadd 11410 df-xmul 11411 df-ioo 11639 df-ioc 11640 df-ico 11641 df-icc 11642 df-fz 11785 df-fzo 11916 df-fl 12028 df-mod 12097 df-seq 12214 df-exp 12273 df-fac 12460 df-bc 12488 df-hash 12516 df-shft 13130 df-cj 13162 df-re 13163 df-im 13164 df-sqrt 13298 df-abs 13299 df-limsup 13526 df-clim 13552 df-rlim 13553 df-sum 13753 df-ef 14121 df-sin 14123 df-cos 14124 df-pi 14126 df-struct 15123 df-ndx 15124 df-slot 15125 df-base 15126 df-sets 15127 df-ress 15128 df-plusg 15203 df-mulr 15204 df-starv 15205 df-sca 15206 df-vsca 15207 df-ip 15208 df-tset 15209 df-ple 15210 df-ds 15212 df-unif 15213 df-hom 15214 df-cco 15215 df-rest 15321 df-topn 15322 df-0g 15340 df-gsum 15341 df-topgen 15342 df-pt 15343 df-prds 15346 df-xrs 15400 df-qtop 15406 df-imas 15407 df-xps 15410 df-mre 15492 df-mrc 15493 df-acs 15495 df-mgm 16488 df-sgrp 16527 df-mnd 16537 df-submnd 16583 df-mulg 16676 df-cntz 16971 df-cmn 17432 df-psmet 18962 df-xmet 18963 df-met 18964 df-bl 18965 df-mopn 18966 df-fbas 18967 df-fg 18968 df-cnfld 18971 df-top 19921 df-bases 19922 df-topon 19923 df-topsp 19924 df-cld 20034 df-ntr 20035 df-cls 20036 df-nei 20114 df-lp 20152 df-perf 20153 df-cn 20243 df-cnp 20244 df-haus 20331 df-tx 20577 df-hmeo 20770 df-fil 20861 df-fm 20953 df-flim 20954 df-flf 20955 df-xms 21335 df-ms 21336 df-tms 21337 df-cncf 21910 df-limc 22821 df-dv 22822 df-log 23506

This theorem is referenced by: isosctrlem3 23749

W3C validator