isosctrlem2 - Metamath Proof Explorer

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

Theorem isosctrlem2 20616

Description: Lemma for isosctr 20618. 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		ax-1cn 9004	. . . . . . . 8
2	1	a1i 11	. . . . . . 7 $/\$ $/\$ $/\$
3		simpl1 960	. . . . . . 7 $/\$ $/\$ $/\$
4	2, 3	negsubd 9373	. . . . . 6 $/\$ $/\$ $/\$
5		1rp 10572	. . . . . . . 8
6	5	a1i 11	. . . . . . 7 $/\$ $/\$ $/\$
7		simpl3 962	. . . . . . . . 9 $/\$ $/\$ $/\$
8		simpl2 961	. . . . . . . . . . 11 $/\$ $/\$ $/\$
9	2, 3, 2	sub32d 9399	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
10		1m1e0 10024	. . . . . . . . . . . . . . . . 17
11	10	oveq1i 6050	. . . . . . . . . . . . . . . 16
12		df-neg 9250	. . . . . . . . . . . . . . . 16
13	11, 12	eqtr4i 2427	. . . . . . . . . . . . . . 15
14	9, 13	syl6eq 2452	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
15	1	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
16		simp1 957	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
17	15, 16	subcld 9367	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
18	17	adantr 452	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
19		subeq0 9283	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
20	1, 19	mpan 652	. . . . . . . . . . . . . . . . . . . . . 22
21	20	biimpd 199	. . . . . . . . . . . . . . . . . . . . 21
22	21	con3and 429	. . . . . . . . . . . . . . . . . . . 20 $/\$
23	22	neneqad 2637	. . . . . . . . . . . . . . . . . . 19 $/\$
24	23	3adant2 976	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
25	24	adantr 452	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
26	18, 25	recrecd 9743	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
27	15, 17, 24	div2negd 9761	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
28	27	adantr 452	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
29	16	negcld 9354	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
30	29, 17, 24	cjdivd 11983	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
31	16	cjnegd 11971	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
32		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
33		abs0 12045	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
34	32, 33	syl6eq 2452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
35		eqtr2 2422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
36	34, 35	sylan2 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
37		ax-1ne0 9015	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
38		id 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
39	38	neneqd 2583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
40	37, 39	mp1i 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
41	36, 40	pm2.65da 560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
42	41	adantl 453	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
43		df-ne 2569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
44		oveq1 6047	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
45		sq1 11431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
46	44, 45	syl6eq 2452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
47	46	adantl 453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
48		absvalsq 12040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
49	48	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
50	47, 49	eqtr3d 2438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
51	50	3adant3 977	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
52	51	oveq1d 6055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
53		simp1 957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
54	53	cjcld 11956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
55		simp3 959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
56	54, 53, 55	divcan3d 9751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
57	52, 56	eqtrd 2436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
58	43, 57	syl3an3br 1225	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
59	42, 58	mpd3an3 1280	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
60	59	eqcomd 2409	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
61	60	3adant3 977	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
62	61	negeqd 9256	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
63	31, 62	eqtrd 2436	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
64	63	oveq1d 6055	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
65		cjsub 11909	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
66	1, 65	mpan 652	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
67		1re 9046	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
68	67	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
69	68	cjred 11986	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
70	69	oveq1d 6055	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
71	66, 70	eqtrd 2436	. . . . . . . . . . . . . . . . . . . . . . . . . 26
72	71	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
73	60	oveq2d 6056	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
74	72, 73	eqtrd 2436	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
75	74	3adant3 977	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
76	75	oveq2d 6056	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
77	30, 64, 76	3eqtrd 2440	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
78	41	3ad2ant2 979	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
79	78	neneqad 2637	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
80	1	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
81		simpl 444	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
82		simpr 448	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
83	80, 81, 82	divnegd 9759	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
84	83	oveq1d 6055	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
85	16, 79, 84	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
86	15	negcld 9354	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
87	86, 16, 79	divcld 9746	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
88	16, 79	reccld 9739	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
89	15, 88	subcld 9367	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
90	17, 24	cjne0d 11963	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
91	75, 90	eqnetrrd 2587	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
92	87, 89, 16, 91, 79	divcan5d 9772	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
93	86, 16, 79	divcan2d 9748	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
94	16, 15, 88	subdid 9445	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
95	16	mulid1d 9061	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
96	16, 79	recidd 9741	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
97	95, 96	oveq12d 6058	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
98	94, 97	eqtrd 2436	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
99	93, 98	oveq12d 6058	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
100	85, 92, 99	3eqtr2d 2442	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
101		subcl 9261	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
102	101	negnegd 9358	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
103		negsubdi2 9316	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
104	103	negeqd 9256	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
105	102, 104	eqtr3d 2438	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
106	16, 15, 105	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
107	106	oveq2d 6056	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
108	77, 100, 107	3eqtrd 2440	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
109	108	adantr 452	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
110	29, 17, 24	divcld 9746	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
111	110	adantr 452	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
112		simpr 448	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
113	111, 112	reim0bd 11960	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
114	113	cjred 11986	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
115	114, 113	eqeltrd 2478	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
116	109, 115	eqeltrrd 2479	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
117	28, 116	eqeltrrd 2479	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
118	17, 24	recne0d 9740	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
119	118	adantr 452	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
120	117, 119	rereccld 9797	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
121	26, 120	eqeltrrd 2479	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
122	67	a1i 11	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
123	121, 122	resubcld 9421	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
124	14, 123	eqeltrrd 2479	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
125	3, 124	negrebd 9366	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
126	125	absord 12173	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\/$
127		eqeq1 2410	. . . . . . . . . . . . 13
128	127	biimpd 199	. . . . . . . . . . . 12
129		eqeq1 2410	. . . . . . . . . . . . 13
130	129	biimpd 199	. . . . . . . . . . . 12
131	128, 130	orim12d 812	. . . . . . . . . . 11 $\/$ $\/$
132	8, 126, 131	sylc 58	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\/$
133	132	ord 367	. . . . . . . . 9 $/\$ $/\$ $/\$
134	7, 133	mpd 15	. . . . . . . 8 $/\$ $/\$ $/\$
135	134, 6	eqeltrrd 2479	. . . . . . 7 $/\$ $/\$ $/\$
136	6, 135	rpaddcld 10619	. . . . . 6 $/\$ $/\$ $/\$
137	4, 136	eqeltrrd 2479	. . . . 5 $/\$ $/\$ $/\$
138	137	relogcld 20471	. . . 4 $/\$ $/\$ $/\$
139	138	reim0d 11985	. . 3 $/\$ $/\$ $/\$
140	135, 137	rpdivcld 10621	. . . . 5 $/\$ $/\$ $/\$
141	140	relogcld 20471	. . . 4 $/\$ $/\$ $/\$
142	141	reim0d 11985	. . 3 $/\$ $/\$ $/\$
143	139, 142	eqtr4d 2439	. 2 $/\$ $/\$ $/\$
144	17, 24	logcld 20421	. . . . . 6 $/\$ $/\$
145	144	adantr 452	. . . . 5 $/\$ $/\$ $/\$
146	145	imcld 11955	. . . 4 $/\$ $/\$ $/\$
147	146	recnd 9070	. . 3 $/\$ $/\$ $/\$
148	110	adantr 452	. . . . . 6 $/\$ $/\$ $/\$
149	16, 79	negne0d 9365	. . . . . . . 8 $/\$ $/\$
150	29, 17, 149, 24	divne0d 9762	. . . . . . 7 $/\$ $/\$
151	150	adantr 452	. . . . . 6 $/\$ $/\$ $/\$
152	148, 151	logcld 20421	. . . . 5 $/\$ $/\$ $/\$
153	152	imcld 11955	. . . 4 $/\$ $/\$ $/\$
154	153	recnd 9070	. . 3 $/\$ $/\$ $/\$
155	108	fveq2d 5691	. . . . . . 7 $/\$ $/\$
156	155	adantr 452	. . . . . 6 $/\$ $/\$ $/\$
157		logcj 20454	. . . . . . 7 $/\$
158	110, 157	sylan 458	. . . . . 6 $/\$ $/\$ $/\$
159	17, 24	reccld 9739	. . . . . . . . . 10 $/\$ $/\$
160	159, 118	logcld 20421	. . . . . . . . 9 $/\$ $/\$
161	160	negnegd 9358	. . . . . . . 8 $/\$ $/\$
162		isosctrlem1 20615	. . . . . . . . . 10 $/\$ $/\$
163		logrec 20614	. . . . . . . . . 10 $/\$ $/\$
164	17, 24, 162, 163	syl3anc 1184	. . . . . . . . 9 $/\$ $/\$
165	164	negeqd 9256	. . . . . . . 8 $/\$ $/\$
166	27	fveq2d 5691	. . . . . . . 8 $/\$ $/\$
167	161, 165, 166	3eqtr4rd 2447	. . . . . . 7 $/\$ $/\$
168	167	adantr 452	. . . . . 6 $/\$ $/\$ $/\$
169	156, 158, 168	3eqtr3rd 2445	. . . . 5 $/\$ $/\$ $/\$
170	169	fveq2d 5691	. . . 4 $/\$ $/\$ $/\$
171	145	imnegd 11970	. . . 4 $/\$ $/\$ $/\$
172	152	imcjd 11965	. . . 4 $/\$ $/\$ $/\$
173	170, 171, 172	3eqtr3d 2444	. . 3 $/\$ $/\$ $/\$
174	147, 154, 173	neg11d 9379	. 2 $/\$ $/\$ $/\$
175	143, 174	pm2.61dane 2645	1 $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $\/$ wo 358 $/\$ wa 359 $/\$ w3a 936

wceq 1649

wcel 1721

wne 2567

cfv 5413 (class class class)co 6040

cc 8944

cr 8945

cc0 8946

c1 8947

caddc 8949

cmul 8951

cmin 9247

cneg 9248

cdiv 9633

c2 10005

crp 10568

cexp 11337

ccj 11856

cim 11858

cabs 11994

cpi 12624

clog 20405

This theorem is referenced by: isosctrlem3 20617

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-inf2 7552 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024 ax-addf 9025 ax-mulf 9026

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-iin 4056 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-se 4502 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-of 6264 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-2o 6684 df-oadd 6687 df-er 6864 df-map 6979 df-pm 6980 df-ixp 7023 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-fi 7374 df-sup 7404 df-oi 7435 df-card 7782 df-cda 8004 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-4 10016 df-5 10017 df-6 10018 df-7 10019 df-8 10020 df-9 10021 df-10 10022 df-n0 10178 df-z 10239 df-dec 10339 df-uz 10445 df-q 10531 df-rp 10569 df-xneg 10666 df-xadd 10667 df-xmul 10668 df-ioo 10876 df-ioc 10877 df-ico 10878 df-icc 10879 df-fz 11000 df-fzo 11091 df-fl 11157 df-mod 11206 df-seq 11279 df-exp 11338 df-fac 11522 df-bc 11549 df-hash 11574 df-shft 11837 df-cj 11859 df-re 11860 df-im 11861 df-sqr 11995 df-abs 11996 df-limsup 12220 df-clim 12237 df-rlim 12238 df-sum 12435 df-ef 12625 df-sin 12627 df-cos 12628 df-pi 12630 df-struct 13426 df-ndx 13427 df-slot 13428 df-base 13429 df-sets 13430 df-ress 13431 df-plusg 13497 df-mulr 13498 df-starv 13499 df-sca 13500 df-vsca 13501 df-tset 13503 df-ple 13504 df-ds 13506 df-unif 13507 df-hom 13508 df-cco 13509 df-rest 13605 df-topn 13606 df-topgen 13622 df-pt 13623 df-prds 13626 df-xrs 13681 df-0g 13682 df-gsum 13683 df-qtop 13688 df-imas 13689 df-xps 13691 df-mre 13766 df-mrc 13767 df-acs 13769 df-mnd 14645 df-submnd 14694 df-mulg 14770 df-cntz 15071 df-cmn 15369 df-psmet 16649 df-xmet 16650 df-met 16651 df-bl 16652 df-mopn 16653 df-fbas 16654 df-fg 16655 df-cnfld 16659 df-top 16918 df-bases 16920 df-topon 16921 df-topsp 16922 df-cld 17038 df-ntr 17039 df-cls 17040 df-nei 17117 df-lp 17155 df-perf 17156 df-cn 17245 df-cnp 17246 df-haus 17333 df-tx 17547 df-hmeo 17740 df-fil 17831 df-fm 17923 df-flim 17924 df-flf 17925 df-xms 18303 df-ms 18304 df-tms 18305 df-cncf 18861 df-limc 19706 df-dv 19707 df-log 20407

W3C validator