dvasin - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dvasin		Structured version Unicode version

Theorem dvasin 29667

Description: Derivative of arcsine. (Contributed by Brendan Leahy, 18-Dec-2018.)

**Hypothesis**
Ref	Expression
dvasin.d	$\$

**Assertion**
Ref	Expression
dvasin	arcsin

Distinct variable group:

Proof of Theorem dvasin Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-asin 22917	. . . . 5 arcsin
2	1	reseq1i 5260	. . . 4 arcsin
3		dvasin.d	. . . . . 6 $\$
4		difss 3624	. . . . . 6 $\$
5	3, 4	eqsstri 3527	. . . . 5
6		resmpt 5314	. . . . 5
7	5, 6	ax-mp 5	. . . 4
8	2, 7	eqtri 2489	. . 3 arcsin
9	8	oveq2i 6286	. 2 arcsin
10		cnelprrecn 9574	. . . . 5
11	10	a1i 11	. . . 4
12	5	sseli 3493	. . . . . . 7
13		ax-icn 9540	. . . . . . . . 9
14		mulcl 9565	. . . . . . . . 9 $/\$
15	13, 14	mpan 670	. . . . . . . 8
16		ax-1cn 9539	. . . . . . . . . 10
17		sqcl 12185	. . . . . . . . . 10
18		subcl 9808	. . . . . . . . . 10 $/\$
19	16, 17, 18	sylancr 663	. . . . . . . . 9
20	19	sqrcld 13217	. . . . . . . 8
21	15, 20	addcld 9604	. . . . . . 7
22	12, 21	syl 16	. . . . . 6
23		asinlem 22920	. . . . . . 7
24	12, 23	syl 16	. . . . . 6
25	22, 24	logcld 22679	. . . . 5
26	25	adantl 466	. . . 4 $/\$
27		ovex 6300	. . . . 5
28	27	a1i 11	. . . 4 $/\$
29		simpr 461	. . . . . . . . . . . . . . . 16 $/\$
30		asinlem3 22923	. . . . . . . . . . . . . . . . 17
31		rere 12905	. . . . . . . . . . . . . . . . . . 19
32	31	breq2d 4452	. . . . . . . . . . . . . . . . . 18
33	32	biimpac 486	. . . . . . . . . . . . . . . . 17 $/\$
34	30, 33	sylan 471	. . . . . . . . . . . . . . . 16 $/\$
35	23	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
36	29, 34, 35	ne0gt0d 9710	. . . . . . . . . . . . . . 15 $/\$
37		0re 9585	. . . . . . . . . . . . . . . . 17
38		ltnle 9653	. . . . . . . . . . . . . . . . 17 $/\$
39	37, 38	mpan 670	. . . . . . . . . . . . . . . 16
40	39	adantl 466	. . . . . . . . . . . . . . 15 $/\$
41	36, 40	mpbid 210	. . . . . . . . . . . . . 14 $/\$
42	41	ex 434	. . . . . . . . . . . . 13
43	12, 42	syl 16	. . . . . . . . . . . 12
44		imor 412	. . . . . . . . . . . 12 $\/$
45	43, 44	sylib 196	. . . . . . . . . . 11 $\/$
46	45	orcomd 388	. . . . . . . . . 10 $\/$
47	46	olcd 393	. . . . . . . . 9 $\/$ $\/$
48		3ianor 985	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $\/$
49		3orrot 974	. . . . . . . . . . 11 $\/$ $\/$ $\/$ $\/$
50		3orass 971	. . . . . . . . . . 11 $\/$ $\/$ $\/$ $\/$
51	48, 49, 50	3bitrri 272	. . . . . . . . . 10 $\/$ $\/$ $/\$ $/\$
52		mnfxr 11312	. . . . . . . . . . 11
53		elioc2 11576	. . . . . . . . . . 11 $/\$ $/\$ $/\$
54	52, 37, 53	mp2an 672	. . . . . . . . . 10 $/\$ $/\$
55	51, 54	xchbinxr 311	. . . . . . . . 9 $\/$ $\/$
56	47, 55	sylib 196	. . . . . . . 8
57	22, 56	eldifd 3480	. . . . . . 7 $\$
58	57	adantl 466	. . . . . 6 $/\$ $\$
59		ovex 6300	. . . . . . 7
60	59	a1i 11	. . . . . 6 $/\$
61		eldifi 3619	. . . . . . . 8 $\$
62		eldifn 3620	. . . . . . . . 9 $\$
63		0xr 9629	. . . . . . . . . . . 12
64		mnflt0 11323	. . . . . . . . . . . 12
65		ubioc1 11567	. . . . . . . . . . . 12 $/\$ $/\$
66	52, 63, 64, 65	mp3an 1319	. . . . . . . . . . 11
67		eleq1 2532	. . . . . . . . . . 11
68	66, 67	mpbiri 233	. . . . . . . . . 10
69	68	necon3bi 2689	. . . . . . . . 9
70	62, 69	syl 16	. . . . . . . 8 $\$
71	61, 70	logcld 22679	. . . . . . 7 $\$
72	71	adantl 466	. . . . . 6 $/\$ $\$
73		ovex 6300	. . . . . . 7
74	73	a1i 11	. . . . . 6 $/\$ $\$
75	13	a1i 11	. . . . . . . . . 10
76	75, 12	mulcld 9605	. . . . . . . . 9
77	76	adantl 466	. . . . . . . 8 $/\$
78	13	a1i 11	. . . . . . . 8 $/\$
79	12	adantl 466	. . . . . . . . . 10 $/\$
80		1cnd 9601	. . . . . . . . . 10 $/\$
81		simpr 461	. . . . . . . . . . 11 $/\$
82		1cnd 9601	. . . . . . . . . . 11 $/\$
83	11	dvmptid 22088	. . . . . . . . . . 11
84	5	a1i 11	. . . . . . . . . . 11
85		eqid 2460	. . . . . . . . . . . . . 14 ℂ_fld ℂ_fld
86	85	cnfldtopon 21018	. . . . . . . . . . . . 13 ℂ_fld TopOn
87	86	toponunii 19193	. . . . . . . . . . . . . 14 ℂ_fld
88	87	restid 14678	. . . . . . . . . . . . 13 ℂ_fld TopOn ℂ_fld ↾_t ℂ_fld
89	86, 88	ax-mp 5	. . . . . . . . . . . 12 ℂ_fld ↾_t ℂ_fld
90	89	eqcomi 2473	. . . . . . . . . . 11 ℂ_fld ℂ_fld ↾_t
91	85	recld2 21047	. . . . . . . . . . . . . . 15 ℂ_fld
92		neg1rr 10629	. . . . . . . . . . . . . . . . . 18
93		iocmnfcld 21004	. . . . . . . . . . . . . . . . . 18
94	92, 93	ax-mp 5	. . . . . . . . . . . . . . . . 17
95		1re 9584	. . . . . . . . . . . . . . . . . 18
96		icopnfcld 21003	. . . . . . . . . . . . . . . . . 18
97	95, 96	ax-mp 5	. . . . . . . . . . . . . . . . 17
98		uncld 19301	. . . . . . . . . . . . . . . . 17 $/\$
99	94, 97, 98	mp2an 672	. . . . . . . . . . . . . . . 16
100	85	tgioo2 21036	. . . . . . . . . . . . . . . . 17 ℂ_fld ↾_t
101	100	fveq2i 5860	. . . . . . . . . . . . . . . 16 ℂ_fld ↾_t
102	99, 101	eleqtri 2546	. . . . . . . . . . . . . . 15 ℂ_fld ↾_t
103		restcldr 19434	. . . . . . . . . . . . . . 15 ℂ_fld $/\$ ℂ_fld ↾_t ℂ_fld
104	91, 102, 103	mp2an 672	. . . . . . . . . . . . . 14 ℂ_fld
105	87	cldopn 19291	. . . . . . . . . . . . . 14 ℂ_fld $\$ ℂ_fld
106	104, 105	ax-mp 5	. . . . . . . . . . . . 13 $\$ ℂ_fld
107	3, 106	eqeltri 2544	. . . . . . . . . . . 12 ℂ_fld
108	107	a1i 11	. . . . . . . . . . 11 ℂ_fld
109	11, 81, 82, 83, 84, 90, 85, 108	dvmptres 22094	. . . . . . . . . 10
110	13	a1i 11	. . . . . . . . . 10
111	11, 79, 80, 109, 110	dvmptcmul 22095	. . . . . . . . 9
112	13	mulid1i 9587	. . . . . . . . . 10
113	112	mpteq2i 4523	. . . . . . . . 9
114	111, 113	syl6eq 2517	. . . . . . . 8
115	12	sqcld 12263	. . . . . . . . . . 11
116	16, 115, 18	sylancr 663	. . . . . . . . . 10
117	116	sqrcld 13217	. . . . . . . . 9
118	117	adantl 466	. . . . . . . 8 $/\$
119		ovex 6300	. . . . . . . . 9
120	119	a1i 11	. . . . . . . 8 $/\$
121		elin 3680	. . . . . . . . . . . . . . 15 $/\$
122	3	asindmre 29666	. . . . . . . . . . . . . . . . 17
123	122	eqimssi 3551	. . . . . . . . . . . . . . . 16
124	123	sseli 3493	. . . . . . . . . . . . . . 15
125	121, 124	sylbir 213	. . . . . . . . . . . . . 14 $/\$
126		incom 3684	. . . . . . . . . . . . . . . 16
127		pnfxr 11310	. . . . . . . . . . . . . . . . 17
128		df-ioc 11523	. . . . . . . . . . . . . . . . . 18 $/\$
129		df-ioo 11522	. . . . . . . . . . . . . . . . . 18 $/\$
130		xrltnle 9642	. . . . . . . . . . . . . . . . . 18 $/\$
131	128, 129, 130	ixxdisj 11533	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
132	52, 63, 127, 131	mp3an 1319	. . . . . . . . . . . . . . . 16
133	126, 132	eqtri 2489	. . . . . . . . . . . . . . 15
134		elioore 11548	. . . . . . . . . . . . . . . . . . 19
135	134	resqcld 12291	. . . . . . . . . . . . . . . . . 18
136		resubcl 9872	. . . . . . . . . . . . . . . . . 18 $/\$
137	95, 135, 136	sylancr 663	. . . . . . . . . . . . . . . . 17
138	92	rexri 9635	. . . . . . . . . . . . . . . . . . 19
139	95	rexri 9635	. . . . . . . . . . . . . . . . . . 19
140		elioo2 11559	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
141	138, 139, 140	mp2an 672	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
142		recn 9571	. . . . . . . . . . . . . . . . . . . . . . 23
143	142	abscld 13216	. . . . . . . . . . . . . . . . . . . . . 22
144	142	absge0d 13224	. . . . . . . . . . . . . . . . . . . . . 22
145		0le1 10065	. . . . . . . . . . . . . . . . . . . . . . 23
146		lt2sq 12196	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
147	95, 145, 146	mpanr12 685	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
148	143, 144, 147	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21
149		abslt 13096	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
150	95, 149	mpan2 671	. . . . . . . . . . . . . . . . . . . . 21 $/\$
151		absresq 13085	. . . . . . . . . . . . . . . . . . . . . . 23
152		sq1 12217	. . . . . . . . . . . . . . . . . . . . . . . 24
153	152	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
154	151, 153	breq12d 4453	. . . . . . . . . . . . . . . . . . . . . 22
155		resqcl 12190	. . . . . . . . . . . . . . . . . . . . . . 23
156		posdif 10034	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
157	155, 95, 156	sylancl 662	. . . . . . . . . . . . . . . . . . . . . 22
158	154, 157	bitrd 253	. . . . . . . . . . . . . . . . . . . . 21
159	148, 150, 158	3bitr3d 283	. . . . . . . . . . . . . . . . . . . 20 $/\$
160	159	biimpd 207	. . . . . . . . . . . . . . . . . . 19 $/\$
161	160	3impib 1189	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
162	141, 161	sylbi 195	. . . . . . . . . . . . . . . . 17
163	137, 162	elrpd 11243	. . . . . . . . . . . . . . . 16
164		ioorp 11591	. . . . . . . . . . . . . . . 16
165	163, 164	syl6eleqr 2559	. . . . . . . . . . . . . . 15
166		disjel 3866	. . . . . . . . . . . . . . 15 $/\$
167	133, 165, 166	sylancr 663	. . . . . . . . . . . . . 14
168	125, 167	syl 16	. . . . . . . . . . . . 13 $/\$
169		elioc2 11576	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
170	52, 37, 169	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
171	170	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
172	171	simp1d 1003	. . . . . . . . . . . . . . . . . . . . . 22
173		resubcl 9872	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
174	95, 172, 173	sylancr 663	. . . . . . . . . . . . . . . . . . . . 21
175		nncan 9837	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
176	16, 175	mpan 670	. . . . . . . . . . . . . . . . . . . . . . 23
177	176	eleq1d 2529	. . . . . . . . . . . . . . . . . . . . . 22
178	177	biimpa 484	. . . . . . . . . . . . . . . . . . . . 21 $/\$
179	174, 178	sylan2 474	. . . . . . . . . . . . . . . . . . . 20 $/\$
180	172	adantl 466	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
181	171	simp3d 1005	. . . . . . . . . . . . . . . . . . . . . . . 24
182	181	adantl 466	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
183		letr 9667	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
184	37, 95, 183	mp3an23 1311	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
185	145, 184	mpan2i 677	. . . . . . . . . . . . . . . . . . . . . . 23
186	180, 182, 185	sylc 60	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
187		subge0 10054	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
188	95, 180, 187	sylancr 663	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
189	186, 188	mpbird 232	. . . . . . . . . . . . . . . . . . . . 21 $/\$
190	176	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 $/\$
191	189, 190	breqtrd 4464	. . . . . . . . . . . . . . . . . . . 20 $/\$
192	179, 191	resqrcld 13198	. . . . . . . . . . . . . . . . . . 19 $/\$
193	17, 192	sylan 471	. . . . . . . . . . . . . . . . . 18 $/\$
194		eleq1 2532	. . . . . . . . . . . . . . . . . 18
195	193, 194	syl5ibrcom 222	. . . . . . . . . . . . . . . . 17 $/\$
196	193	renegcld 9975	. . . . . . . . . . . . . . . . . 18 $/\$
197		eleq1 2532	. . . . . . . . . . . . . . . . . 18
198	196, 197	syl5ibrcom 222	. . . . . . . . . . . . . . . . 17 $/\$
199		eqid 2460	. . . . . . . . . . . . . . . . . . 19
200		eqsqror 13148	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\/$
201	17, 200	mpdan 668	. . . . . . . . . . . . . . . . . . 19 $\/$
202	199, 201	mpbii 211	. . . . . . . . . . . . . . . . . 18 $\/$
203	202	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $\/$
204	195, 198, 203	mpjaod 381	. . . . . . . . . . . . . . . 16 $/\$
205	204	ex 434	. . . . . . . . . . . . . . 15
206	205	con3dimp 441	. . . . . . . . . . . . . 14 $/\$
207	12, 206	sylan 471	. . . . . . . . . . . . 13 $/\$
208	168, 207	pm2.61dan 789	. . . . . . . . . . . 12
209	116, 208	eldifd 3480	. . . . . . . . . . 11 $\$
210	209	adantl 466	. . . . . . . . . 10 $/\$ $\$
211		2cnd 10597	. . . . . . . . . . . . . 14
212		id 22	. . . . . . . . . . . . . 14
213	211, 212	mulcld 9605	. . . . . . . . . . . . 13
214	213	negcld 9906	. . . . . . . . . . . 12
215	214	adantl 466	. . . . . . . . . . 11 $/\$
216	12, 215	sylan2 474	. . . . . . . . . 10 $/\$
217	61	sqrcld 13217	. . . . . . . . . . 11 $\$
218	217	adantl 466	. . . . . . . . . 10 $/\$ $\$
219		ovex 6300	. . . . . . . . . . 11
220	219	a1i 11	. . . . . . . . . 10 $/\$ $\$
221	19	adantl 466	. . . . . . . . . . 11 $/\$
222	37	a1i 11	. . . . . . . . . . . . 13 $/\$
223		1cnd 9601	. . . . . . . . . . . . . 14
224	11, 223	dvmptc 22089	. . . . . . . . . . . . 13
225	17	adantl 466	. . . . . . . . . . . . 13 $/\$
226		2cn 10595	. . . . . . . . . . . . . . 15
227		mulcl 9565	. . . . . . . . . . . . . . 15 $/\$
228	226, 227	mpan 670	. . . . . . . . . . . . . 14
229	228	adantl 466	. . . . . . . . . . . . 13 $/\$
230		2nn 10682	. . . . . . . . . . . . . . . 16
231		dvexp 22084	. . . . . . . . . . . . . . . 16
232	230, 231	ax-mp 5	. . . . . . . . . . . . . . 15
233		2m1e1 10639	. . . . . . . . . . . . . . . . . . 19
234	233	oveq2i 6286	. . . . . . . . . . . . . . . . . 18
235		exp1 12128	. . . . . . . . . . . . . . . . . 18
236	234, 235	syl5eq 2513	. . . . . . . . . . . . . . . . 17
237	236	oveq2d 6291	. . . . . . . . . . . . . . . 16
238	237	mpteq2ia 4522	. . . . . . . . . . . . . . 15
239	232, 238	eqtri 2489	. . . . . . . . . . . . . 14
240	239	a1i 11	. . . . . . . . . . . . 13
241	11, 82, 222, 224, 225, 229, 240	dvmptsub 22098	. . . . . . . . . . . 12
242		df-neg 9797	. . . . . . . . . . . . 13
243	242	mpteq2i 4523	. . . . . . . . . . . 12
244	241, 243	syl6eqr 2519	. . . . . . . . . . 11
245	11, 221, 215, 244, 84, 90, 85, 108	dvmptres 22094	. . . . . . . . . 10
246		eqid 2460	. . . . . . . . . . . 12 $\$ $\$
247	246	dvcnsqr 29665	. . . . . . . . . . 11 $\$ $\$
248	247	a1i 11	. . . . . . . . . 10 $\$ $\$
249		fveq2 5857	. . . . . . . . . 10
250	249	oveq2d 6291	. . . . . . . . . . 11
251	250	oveq2d 6291	. . . . . . . . . 10
252	11, 11, 210, 216, 218, 220, 245, 248, 249, 251	dvmptco 22103	. . . . . . . . 9
253		mulneg2 9983	. . . . . . . . . . . . 13 $/\$
254	226, 12, 253	sylancr 663	. . . . . . . . . . . 12
255	254	oveq1d 6290	. . . . . . . . . . 11
256	12	negcld 9906	. . . . . . . . . . . 12
257		eldifn 3620	. . . . . . . . . . . . . . 15 $\$
258	257, 3	eleq2s 2568	. . . . . . . . . . . . . 14
259		id 22	. . . . . . . . . . . . . . . . . 18
260		mnflt 11322	. . . . . . . . . . . . . . . . . . . 20
261	92, 260	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
262		ubioc1 11567	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
263	52, 138, 261, 262	mp3an 1319	. . . . . . . . . . . . . . . . . 18
264	259, 263	syl6eqel 2556	. . . . . . . . . . . . . . . . 17
265		id 22	. . . . . . . . . . . . . . . . . 18
266		ltpnf 11320	. . . . . . . . . . . . . . . . . . . 20
267	95, 266	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
268		lbico1 11568	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
269	139, 127, 267, 268	mp3an 1319	. . . . . . . . . . . . . . . . . 18
270	265, 269	syl6eqel 2556	. . . . . . . . . . . . . . . . 17
271	264, 270	orim12i 516	. . . . . . . . . . . . . . . 16 $\/$ $\/$
272	271	orcoms 389	. . . . . . . . . . . . . . 15 $\/$ $\/$
273		elun 3638	. . . . . . . . . . . . . . 15 $\/$
274	272, 273	sylibr 212	. . . . . . . . . . . . . 14 $\/$
275	258, 274	nsyl 121	. . . . . . . . . . . . 13 $\/$
276		1cnd 9601	. . . . . . . . . . . . . . . . . 18 $/\$
277	17	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
278	19	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
279		simpr 461	. . . . . . . . . . . . . . . . . . 19 $/\$
280	278, 279	sqr00d 13221	. . . . . . . . . . . . . . . . . 18 $/\$
281	276, 277, 280	subeq0d 9927	. . . . . . . . . . . . . . . . 17 $/\$
282	152, 281	syl5req 2514	. . . . . . . . . . . . . . . 16 $/\$
283	282	ex 434	. . . . . . . . . . . . . . 15
284		sqeqor 12237	. . . . . . . . . . . . . . . 16 $/\$ $\/$
285	16, 284	mpan2 671	. . . . . . . . . . . . . . 15 $\/$
286	283, 285	sylibd 214	. . . . . . . . . . . . . 14 $\/$
287	286	necon3bd 2672	. . . . . . . . . . . . 13 $\/$
288	12, 275, 287	sylc 60	. . . . . . . . . . . 12
289		2cnne0 10739	. . . . . . . . . . . . 13 $/\$
290		divcan5 10235	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
291	289, 290	mp3an3 1308	. . . . . . . . . . . 12 $/\$ $/\$
292	256, 117, 288, 291	syl12anc 1221	. . . . . . . . . . 11
293	226, 12, 227	sylancr 663	. . . . . . . . . . . . 13
294	293	negcld 9906	. . . . . . . . . . . 12
295		mulcl 9565	. . . . . . . . . . . . 13 $/\$
296	226, 117, 295	sylancr 663	. . . . . . . . . . . 12
297		mulne0 10180	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
298	289, 297	mpan 670	. . . . . . . . . . . . 13 $/\$
299	117, 288, 298	syl2anc 661	. . . . . . . . . . . 12
300	294, 296, 299	divrec2d 10313	. . . . . . . . . . 11
301	255, 292, 300	3eqtr3rd 2510	. . . . . . . . . 10
302	301	mpteq2ia 4522	. . . . . . . . 9
303	252, 302	syl6eq 2517	. . . . . . . 8
304	11, 77, 78, 114, 118, 120, 303	dvmptadd 22091	. . . . . . 7
305		mulcl 9565	. . . . . . . . . . . 12 $/\$
306	13, 20, 305	sylancr 663	. . . . . . . . . . 11
307	12, 306	syl 16	. . . . . . . . . 10
308	307, 256, 117, 288	divdird 10347	. . . . . . . . 9
309		ixi 10167	. . . . . . . . . . . . . . . 16
310	309	eqcomi 2473	. . . . . . . . . . . . . . 15
311	310	oveq1i 6285	. . . . . . . . . . . . . 14
312		mulm1 9987	. . . . . . . . . . . . . 14
313		mulass 9569	. . . . . . . . . . . . . . 15 $/\$ $/\$
314	13, 13, 313	mp3an12 1309	. . . . . . . . . . . . . 14
315	311, 312, 314	3eqtr3a 2525	. . . . . . . . . . . . 13
316	315	oveq1d 6290	. . . . . . . . . . . 12
317		negcl 9809	. . . . . . . . . . . . 13
318	306, 317	addcomd 9770	. . . . . . . . . . . 12
319	13	a1i 11	. . . . . . . . . . . . 13
320	319, 15, 20	adddid 9609	. . . . . . . . . . . 12
321	316, 318, 320	3eqtr4d 2511	. . . . . . . . . . 11
322	12, 321	syl 16	. . . . . . . . . 10
323	322	oveq1d 6290	. . . . . . . . 9
324	75, 117, 288	divcan4d 10315	. . . . . . . . . 10
325	324	oveq1d 6290	. . . . . . . . 9
326	308, 323, 325	3eqtr3rd 2510	. . . . . . . 8
327	326	mpteq2ia 4522	. . . . . . 7
328	304, 327	syl6eq 2517	. . . . . 6
329	246	dvlog 22753	. . . . . . 7 $\$ $\$
330		logf1o 22673	. . . . . . . . . 10 $\$
331		f1of 5807	. . . . . . . . . 10 $\$ $\$
332	330, 331	mp1i 12	. . . . . . . . 9 $\$
333		snssi 4164	. . . . . . . . . . 11
334	66, 333	ax-mp 5	. . . . . . . . . 10
335		sscon 3631	. . . . . . . . . 10 $\$ $\$
336	334, 335	mp1i 12	. . . . . . . . 9 $\$ $\$
337	332, 336	feqresmpt 5912	. . . . . . . 8 $\$ $\$
338	337	oveq2d 6291	. . . . . . 7 $\$ $\$
339	329, 338	syl5reqr 2516	. . . . . 6 $\$ $\$
340		fveq2 5857	. . . . . 6
341		oveq2 6283	. . . . . 6
342	11, 11, 58, 60, 72, 74, 328, 339, 340, 341	dvmptco 22103	. . . . 5
343	22, 24	reccld 10302	. . . . . . . 8
344		mulcl 9565	. . . . . . . . . 10 $/\$
345	13, 21, 344	sylancr 663	. . . . . . . . 9
346	12, 345	syl 16	. . . . . . . 8
347	343, 346, 117, 288	divassd 10344	. . . . . . 7
348	346, 22, 24	divrec2d 10313	. . . . . . . . 9
349	75, 22, 24	divcan4d 10315	. . . . . . . . 9
350	348, 349	eqtr3d 2503	. . . . . . . 8
351	350	oveq1d 6290	. . . . . . 7
352	347, 351	eqtr3d 2503	. . . . . 6
353	352	mpteq2ia 4522	. . . . 5
354	342, 353	syl6eq 2517	. . . 4
355		negicn 9810	. . . . 5
356	355	a1i 11	. . . 4
357	11, 26, 28, 354, 356	dvmptcmul 22095	. . 3
358	357	trud 1383	. 2
359	13, 13	mulneg1i 9991	. . . . . 6
360	309	negeqi 9802	. . . . . 6
361		negneg1e1 10632	. . . . . 6
362	359, 360, 361	3eqtri 2493	. . . . 5
363	362	oveq1i 6285	. . . 4
364		divass 10214	. . . . . 6 $/\$ $/\$ $/\$
365	355, 13, 364	mp3an12 1309	. . . . 5 $/\$
366	117, 288, 365	syl2anc 661	. . . 4
367	363, 366	syl5reqr 2516	. . 3
368	367	mpteq2ia 4522	. 2
369	9, 358, 368	3eqtri 2493	1 arcsin

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369 $\/$ w3o 967 $/\$ w3a 968

wceq 1374

wtru 1375

wcel 1762

wne 2655

cvv 3106 $\$ cdif 3466

cun 3467

cin 3468

wss 3469

c0 3778

csn 4020

cpr 4022 class class class wbr 4440

cmpt 4498

crn 4993

cres 4994

wf 5575

wf1o 5578

cfv 5579 (class class class)co 6275

cc 9479

cr 9480

cc0 9481

c1 9482

ci 9483

caddc 9484

cmul 9486

cpnf 9614

cmnf 9615

cxr 9616

clt 9617

cle 9618

cmin 9794

cneg 9795

cdiv 10195

cn 10525

c2 10574

crp 11209

cioo 11518

cioc 11519

cico 11520

cexp 12122

cre 12880

csqr 13016

cabs 13017 ↾_t crest 14665

ctopn 14666

ctg 14682 ℂ_fldccnfld 18184 TopOnctopon 19155

ccld 19276

cdv 21995

clog 22663 arcsincasin 22914

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-8 1764 ax-9 1766 ax-10 1781 ax-11 1786 ax-12 1798 ax-13 1961 ax-ext 2438 ax-rep 4551 ax-sep 4561 ax-nul 4569 ax-pow 4618 ax-pr 4679 ax-un 6567 ax-inf2 8047 ax-cnex 9537 ax-resscn 9538 ax-1cn 9539 ax-icn 9540 ax-addcl 9541 ax-addrcl 9542 ax-mulcl 9543 ax-mulrcl 9544 ax-mulcom 9545 ax-addass 9546 ax-mulass 9547 ax-distr 9548 ax-i2m1 9549 ax-1ne0 9550 ax-1rid 9551 ax-rnegex 9552 ax-rrecex 9553 ax-cnre 9554 ax-pre-lttri 9555 ax-pre-lttrn 9556 ax-pre-ltadd 9557 ax-pre-mulgt0 9558 ax-pre-sup 9559 ax-addf 9560 ax-mulf 9561

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 969 df-3an 970 df-tru 1377 df-fal 1380 df-ex 1592 df-nf 1595 df-sb 1707 df-eu 2272 df-mo 2273 df-clab 2446 df-cleq 2452 df-clel 2455 df-nfc 2610 df-ne 2657 df-nel 2658 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3108 df-sbc 3325 df-csb 3429 df-dif 3472 df-un 3474 df-in 3476 df-ss 3483 df-pss 3485 df-nul 3779 df-if 3933 df-pw 4005 df-sn 4021 df-pr 4023 df-tp 4025 df-op 4027 df-uni 4239 df-int 4276 df-iun 4320 df-iin 4321 df-br 4441 df-opab 4499 df-mpt 4500 df-tr 4534 df-eprel 4784 df-id 4788 df-po 4793 df-so 4794 df-fr 4831 df-se 4832 df-we 4833 df-ord 4874 df-on 4875 df-lim 4876 df-suc 4877 df-xp 4998 df-rel 4999 df-cnv 5000 df-co 5001 df-dm 5002 df-rn 5003 df-res 5004 df-ima 5005 df-iota 5542 df-fun 5581 df-fn 5582 df-f 5583 df-f1 5584 df-fo 5585 df-f1o 5586 df-fv 5587 df-isom 5588 df-riota 6236 df-ov 6278 df-oprab 6279 df-mpt2 6280 df-of 6515 df-om 6672 df-1st 6774 df-2nd 6775 df-supp 6892 df-recs 7032 df-rdg 7066 df-1o 7120 df-2o 7121 df-oadd 7124 df-er 7301 df-map 7412 df-pm 7413 df-ixp 7460 df-en 7507 df-dom 7508 df-sdom 7509 df-fin 7510 df-fsupp 7819 df-fi 7860 df-sup 7890 df-oi 7924 df-card 8309 df-cda 8537 df-pnf 9619 df-mnf 9620 df-xr 9621 df-ltxr 9622 df-le 9623 df-sub 9796 df-neg 9797 df-div 10196 df-nn 10526 df-2 10583 df-3 10584 df-4 10585 df-5 10586 df-6 10587 df-7 10588 df-8 10589 df-9 10590 df-10 10591 df-n0 10785 df-z 10854 df-dec 10966 df-uz 11072 df-q 11172 df-rp 11210 df-xneg 11307 df-xadd 11308 df-xmul 11309 df-ioo 11522 df-ioc 11523 df-ico 11524 df-icc 11525 df-fz 11662 df-fzo 11782 df-fl 11886 df-mod 11953 df-seq 12064 df-exp 12123 df-fac 12309 df-bc 12336 df-hash 12361 df-shft 12850 df-cj 12882 df-re 12883 df-im 12884 df-sqr 13018 df-abs 13019 df-limsup 13243 df-clim 13260 df-rlim 13261 df-sum 13458 df-ef 13654 df-sin 13656 df-cos 13657 df-tan 13658 df-pi 13659 df-struct 14481 df-ndx 14482 df-slot 14483 df-base 14484 df-sets 14485 df-ress 14486 df-plusg 14557 df-mulr 14558 df-starv 14559 df-sca 14560 df-vsca 14561 df-ip 14562 df-tset 14563 df-ple 14564 df-ds 14566 df-unif 14567 df-hom 14568 df-cco 14569 df-rest 14667 df-topn 14668 df-0g 14686 df-gsum 14687 df-topgen 14688 df-pt 14689 df-prds 14692 df-xrs 14746 df-qtop 14751 df-imas 14752 df-xps 14754 df-mre 14830 df-mrc 14831 df-acs 14833 df-mnd 15721 df-submnd 15771 df-mulg 15854 df-cntz 16143 df-cmn 16589 df-psmet 18175 df-xmet 18176 df-met 18177 df-bl 18178 df-mopn 18179 df-fbas 18180 df-fg 18181 df-cnfld 18185 df-top 19159 df-bases 19161 df-topon 19162 df-topsp 19163 df-cld 19279 df-ntr 19280 df-cls 19281 df-nei 19358 df-lp 19396 df-perf 19397 df-cn 19487 df-cnp 19488 df-haus 19575 df-cmp 19646 df-tx 19791 df-hmeo 19984 df-fil 20075 df-fm 20167 df-flim 20168 df-flf 20169 df-xms 20551 df-ms 20552 df-tms 20553 df-cncf 21110 df-limc 21998 df-dv 21999 df-log 22665 df-cxp 22666 df-asin 22917

This theorem is referenced by: dvacos 29668 dvreasin 29669

W3C validator