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 28483

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 22263	. . . . 5 arcsin
2	1	reseq1i 5109	. . . 4 arcsin
3		dvasin.d	. . . . . 6 $\$
4		difss 3486	. . . . . 6 $\$
5	3, 4	eqsstri 3389	. . . . 5
6		resmpt 5159	. . . . 5
7	5, 6	ax-mp 5	. . . 4
8	2, 7	eqtri 2463	. . 3 arcsin
9	8	oveq2i 6105	. 2 arcsin
10		cnelprrecn 9378	. . . . 5
11	10	a1i 11	. . . 4
12	5	sseli 3355	. . . . . . 7
13		ax-icn 9344	. . . . . . . . 9
14		mulcl 9369	. . . . . . . . 9 $/\$
15	13, 14	mpan 670	. . . . . . . 8
16		ax-1cn 9343	. . . . . . . . . 10
17		sqcl 11931	. . . . . . . . . 10
18		subcl 9612	. . . . . . . . . 10 $/\$
19	16, 17, 18	sylancr 663	. . . . . . . . 9
20	19	sqrcld 12926	. . . . . . . 8
21	15, 20	addcld 9408	. . . . . . 7
22	12, 21	syl 16	. . . . . 6
23		asinlem 22266	. . . . . . 7
24	12, 23	syl 16	. . . . . 6
25	22, 24	logcld 22025	. . . . 5
26	25	adantl 466	. . . 4 $/\$
27		ovex 6119	. . . . 5
28	27	a1i 11	. . . 4 $/\$
29		simpr 461	. . . . . . . . . . . . . . . 16 $/\$
30		asinlem3 22269	. . . . . . . . . . . . . . . . 17
31		rere 12614	. . . . . . . . . . . . . . . . . . 19
32	31	breq2d 4307	. . . . . . . . . . . . . . . . . 18
33	32	biimpac 486	. . . . . . . . . . . . . . . . 17 $/\$
34	30, 33	sylan 471	. . . . . . . . . . . . . . . 16 $/\$
35	23	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
36	29, 34, 35	ne0gt0d 9514	. . . . . . . . . . . . . . 15 $/\$
37		0re 9389	. . . . . . . . . . . . . . . . 17
38		ltnle 9457	. . . . . . . . . . . . . . . . 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 982	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $\/$
49		3orrot 971	. . . . . . . . . . 11 $\/$ $\/$ $\/$ $\/$
50		3orass 968	. . . . . . . . . . 11 $\/$ $\/$ $\/$ $\/$
51	48, 49, 50	3bitrri 272	. . . . . . . . . 10 $\/$ $\/$ $/\$ $/\$
52		mnfxr 11097	. . . . . . . . . . 11
53		elioc2 11361	. . . . . . . . . . 11 $/\$ $/\$ $/\$
54	52, 37, 53	mp2an 672	. . . . . . . . . 10 $/\$ $/\$
55	51, 54	xchbinxr 311	. . . . . . . . 9 $\/$ $\/$
56	47, 55	sylib 196	. . . . . . . 8
57	22, 56	eldifd 3342	. . . . . . 7 $\$
58	57	adantl 466	. . . . . 6 $/\$ $\$
59		ovex 6119	. . . . . . 7
60	59	a1i 11	. . . . . 6 $/\$
61		eldifi 3481	. . . . . . . 8 $\$
62		eldifn 3482	. . . . . . . . 9 $\$
63		0xr 9433	. . . . . . . . . . . 12
64		mnflt0 11108	. . . . . . . . . . . 12
65		ubioc1 11352	. . . . . . . . . . . 12 $/\$ $/\$
66	52, 63, 64, 65	mp3an 1314	. . . . . . . . . . 11
67		eleq1 2503	. . . . . . . . . . 11
68	66, 67	mpbiri 233	. . . . . . . . . 10
69	68	necon3bi 2655	. . . . . . . . 9
70	62, 69	syl 16	. . . . . . . 8 $\$
71	61, 70	logcld 22025	. . . . . . 7 $\$
72	71	adantl 466	. . . . . 6 $/\$ $\$
73		ovex 6119	. . . . . . 7
74	73	a1i 11	. . . . . 6 $/\$ $\$
75	13	a1i 11	. . . . . . . . . 10
76	75, 12	mulcld 9409	. . . . . . . . 9
77	76	adantl 466	. . . . . . . 8 $/\$
78	13	a1i 11	. . . . . . . 8 $/\$
79	12	adantl 466	. . . . . . . . . 10 $/\$
80		1cnd 9405	. . . . . . . . . 10 $/\$
81		simpr 461	. . . . . . . . . . 11 $/\$
82		1cnd 9405	. . . . . . . . . . 11 $/\$
83	11	dvmptid 21434	. . . . . . . . . . 11
84	5	a1i 11	. . . . . . . . . . 11
85		eqid 2443	. . . . . . . . . . . . . 14 ℂ_fld ℂ_fld
86	85	cnfldtopon 20365	. . . . . . . . . . . . 13 ℂ_fld TopOn
87	86	toponunii 18540	. . . . . . . . . . . . . 14 ℂ_fld
88	87	restid 14375	. . . . . . . . . . . . 13 ℂ_fld TopOn ℂ_fld ↾_t ℂ_fld
89	86, 88	ax-mp 5	. . . . . . . . . . . 12 ℂ_fld ↾_t ℂ_fld
90	89	eqcomi 2447	. . . . . . . . . . 11 ℂ_fld ℂ_fld ↾_t
91	85	recld2 20394	. . . . . . . . . . . . . . 15 ℂ_fld
92		neg1rr 10429	. . . . . . . . . . . . . . . . . 18
93		iocmnfcld 20351	. . . . . . . . . . . . . . . . . 18
94	92, 93	ax-mp 5	. . . . . . . . . . . . . . . . 17
95		1re 9388	. . . . . . . . . . . . . . . . . 18
96		icopnfcld 20350	. . . . . . . . . . . . . . . . . 18
97	95, 96	ax-mp 5	. . . . . . . . . . . . . . . . 17
98		uncld 18648	. . . . . . . . . . . . . . . . 17 $/\$
99	94, 97, 98	mp2an 672	. . . . . . . . . . . . . . . 16
100	85	tgioo2 20383	. . . . . . . . . . . . . . . . 17 ℂ_fld ↾_t
101	100	fveq2i 5697	. . . . . . . . . . . . . . . 16 ℂ_fld ↾_t
102	99, 101	eleqtri 2515	. . . . . . . . . . . . . . 15 ℂ_fld ↾_t
103		restcldr 18781	. . . . . . . . . . . . . . 15 ℂ_fld $/\$ ℂ_fld ↾_t ℂ_fld
104	91, 102, 103	mp2an 672	. . . . . . . . . . . . . 14 ℂ_fld
105	87	cldopn 18638	. . . . . . . . . . . . . 14 ℂ_fld $\$ ℂ_fld
106	104, 105	ax-mp 5	. . . . . . . . . . . . 13 $\$ ℂ_fld
107	3, 106	eqeltri 2513	. . . . . . . . . . . 12 ℂ_fld
108	107	a1i 11	. . . . . . . . . . 11 ℂ_fld
109	11, 81, 82, 83, 84, 90, 85, 108	dvmptres 21440	. . . . . . . . . 10
110	13	a1i 11	. . . . . . . . . 10
111	11, 79, 80, 109, 110	dvmptcmul 21441	. . . . . . . . 9
112	13	mulid1i 9391	. . . . . . . . . 10
113	112	mpteq2i 4378	. . . . . . . . 9
114	111, 113	syl6eq 2491	. . . . . . . 8
115	12	sqcld 12009	. . . . . . . . . . 11
116	16, 115, 18	sylancr 663	. . . . . . . . . 10
117	116	sqrcld 12926	. . . . . . . . 9
118	117	adantl 466	. . . . . . . 8 $/\$
119		ovex 6119	. . . . . . . . 9
120	119	a1i 11	. . . . . . . 8 $/\$
121		elin 3542	. . . . . . . . . . . . . . 15 $/\$
122	3	asindmre 28482	. . . . . . . . . . . . . . . . 17
123	122	eqimssi 3413	. . . . . . . . . . . . . . . 16
124	123	sseli 3355	. . . . . . . . . . . . . . 15
125	121, 124	sylbir 213	. . . . . . . . . . . . . 14 $/\$
126		incom 3546	. . . . . . . . . . . . . . . 16
127		pnfxr 11095	. . . . . . . . . . . . . . . . 17
128		df-ioc 11308	. . . . . . . . . . . . . . . . . 18 $/\$
129		df-ioo 11307	. . . . . . . . . . . . . . . . . 18 $/\$
130		xrltnle 9446	. . . . . . . . . . . . . . . . . 18 $/\$
131	128, 129, 130	ixxdisj 11318	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
132	52, 63, 127, 131	mp3an 1314	. . . . . . . . . . . . . . . 16
133	126, 132	eqtri 2463	. . . . . . . . . . . . . . 15
134		elioore 11333	. . . . . . . . . . . . . . . . . . 19
135	134	resqcld 12037	. . . . . . . . . . . . . . . . . 18
136		resubcl 9676	. . . . . . . . . . . . . . . . . 18 $/\$
137	95, 135, 136	sylancr 663	. . . . . . . . . . . . . . . . 17
138	92	rexri 9439	. . . . . . . . . . . . . . . . . . 19
139	95	rexri 9439	. . . . . . . . . . . . . . . . . . 19
140		elioo2 11344	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
141	138, 139, 140	mp2an 672	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
142		recn 9375	. . . . . . . . . . . . . . . . . . . . . . 23
143	142	abscld 12925	. . . . . . . . . . . . . . . . . . . . . 22
144	142	absge0d 12933	. . . . . . . . . . . . . . . . . . . . . 22
145		0le1 9866	. . . . . . . . . . . . . . . . . . . . . . 23
146		lt2sq 11942	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
147	95, 145, 146	mpanr12 685	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
148	143, 144, 147	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21
149		abslt 12805	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
150	95, 149	mpan2 671	. . . . . . . . . . . . . . . . . . . . 21 $/\$
151		absresq 12794	. . . . . . . . . . . . . . . . . . . . . . 23
152		sq1 11963	. . . . . . . . . . . . . . . . . . . . . . . 24
153	152	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
154	151, 153	breq12d 4308	. . . . . . . . . . . . . . . . . . . . . 22
155		resqcl 11936	. . . . . . . . . . . . . . . . . . . . . . 23
156		posdif 9835	. . . . . . . . . . . . . . . . . . . . . . 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 1185	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
162	141, 161	sylbi 195	. . . . . . . . . . . . . . . . 17
163	137, 162	elrpd 11028	. . . . . . . . . . . . . . . 16
164		ioorp 11376	. . . . . . . . . . . . . . . 16
165	163, 164	syl6eleqr 2534	. . . . . . . . . . . . . . 15
166		disjel 3728	. . . . . . . . . . . . . . 15 $/\$
167	133, 165, 166	sylancr 663	. . . . . . . . . . . . . 14
168	125, 167	syl 16	. . . . . . . . . . . . 13 $/\$
169		elioc2 11361	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
170	52, 37, 169	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
171	170	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
172	171	simp1d 1000	. . . . . . . . . . . . . . . . . . . . . 22
173		resubcl 9676	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
174	95, 172, 173	sylancr 663	. . . . . . . . . . . . . . . . . . . . 21
175		nncan 9641	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
176	16, 175	mpan 670	. . . . . . . . . . . . . . . . . . . . . . 23
177	176	eleq1d 2509	. . . . . . . . . . . . . . . . . . . . . 22
178	177	biimpa 484	. . . . . . . . . . . . . . . . . . . . 21 $/\$
179	174, 178	sylan2 474	. . . . . . . . . . . . . . . . . . . 20 $/\$
180	172	adantl 466	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
181	171	simp3d 1002	. . . . . . . . . . . . . . . . . . . . . . . 24
182	181	adantl 466	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
183		letr 9471	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
184	37, 95, 183	mp3an23 1306	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
185	145, 184	mpan2i 677	. . . . . . . . . . . . . . . . . . . . . . 23
186	180, 182, 185	sylc 60	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
187		subge0 9855	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
188	95, 180, 187	sylancr 663	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
189	186, 188	mpbird 232	. . . . . . . . . . . . . . . . . . . . 21 $/\$
190	176	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 $/\$
191	189, 190	breqtrd 4319	. . . . . . . . . . . . . . . . . . . 20 $/\$
192	179, 191	resqrcld 12907	. . . . . . . . . . . . . . . . . . 19 $/\$
193	17, 192	sylan 471	. . . . . . . . . . . . . . . . . 18 $/\$
194		eleq1 2503	. . . . . . . . . . . . . . . . . 18
195	193, 194	syl5ibrcom 222	. . . . . . . . . . . . . . . . 17 $/\$
196	193	renegcld 9778	. . . . . . . . . . . . . . . . . 18 $/\$
197		eleq1 2503	. . . . . . . . . . . . . . . . . 18
198	196, 197	syl5ibrcom 222	. . . . . . . . . . . . . . . . 17 $/\$
199		eqid 2443	. . . . . . . . . . . . . . . . . . 19
200		eqsqror 12857	. . . . . . . . . . . . . . . . . . . 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 3342	. . . . . . . . . . 11 $\$
210	209	adantl 466	. . . . . . . . . 10 $/\$ $\$
211		2cnd 10397	. . . . . . . . . . . . . 14
212		id 22	. . . . . . . . . . . . . 14
213	211, 212	mulcld 9409	. . . . . . . . . . . . 13
214	213	negcld 9709	. . . . . . . . . . . 12
215	214	adantl 466	. . . . . . . . . . 11 $/\$
216	12, 215	sylan2 474	. . . . . . . . . 10 $/\$
217	61	sqrcld 12926	. . . . . . . . . . 11 $\$
218	217	adantl 466	. . . . . . . . . 10 $/\$ $\$
219		ovex 6119	. . . . . . . . . . 11
220	219	a1i 11	. . . . . . . . . 10 $/\$ $\$
221	19	adantl 466	. . . . . . . . . . 11 $/\$
222	37	a1i 11	. . . . . . . . . . . . 13 $/\$
223		1cnd 9405	. . . . . . . . . . . . . 14
224	11, 223	dvmptc 21435	. . . . . . . . . . . . 13
225	17	adantl 466	. . . . . . . . . . . . 13 $/\$
226		2cn 10395	. . . . . . . . . . . . . . 15
227		mulcl 9369	. . . . . . . . . . . . . . 15 $/\$
228	226, 227	mpan 670	. . . . . . . . . . . . . 14
229	228	adantl 466	. . . . . . . . . . . . 13 $/\$
230		2nn 10482	. . . . . . . . . . . . . . . 16
231		dvexp 21430	. . . . . . . . . . . . . . . 16
232	230, 231	ax-mp 5	. . . . . . . . . . . . . . 15
233		2m1e1 10439	. . . . . . . . . . . . . . . . . . 19
234	233	oveq2i 6105	. . . . . . . . . . . . . . . . . 18
235		exp1 11874	. . . . . . . . . . . . . . . . . 18
236	234, 235	syl5eq 2487	. . . . . . . . . . . . . . . . 17
237	236	oveq2d 6110	. . . . . . . . . . . . . . . 16
238	237	mpteq2ia 4377	. . . . . . . . . . . . . . 15
239	232, 238	eqtri 2463	. . . . . . . . . . . . . 14
240	239	a1i 11	. . . . . . . . . . . . 13
241	11, 82, 222, 224, 225, 229, 240	dvmptsub 21444	. . . . . . . . . . . 12
242		df-neg 9601	. . . . . . . . . . . . 13
243	242	mpteq2i 4378	. . . . . . . . . . . 12
244	241, 243	syl6eqr 2493	. . . . . . . . . . 11
245	11, 221, 215, 244, 84, 90, 85, 108	dvmptres 21440	. . . . . . . . . 10
246		eqid 2443	. . . . . . . . . . . 12 $\$ $\$
247	246	dvcnsqr 28481	. . . . . . . . . . 11 $\$ $\$
248	247	a1i 11	. . . . . . . . . 10 $\$ $\$
249		fveq2 5694	. . . . . . . . . 10
250	249	oveq2d 6110	. . . . . . . . . . 11
251	250	oveq2d 6110	. . . . . . . . . 10
252	11, 11, 210, 216, 218, 220, 245, 248, 249, 251	dvmptco 21449	. . . . . . . . 9
253		mulneg2 9785	. . . . . . . . . . . . 13 $/\$
254	226, 12, 253	sylancr 663	. . . . . . . . . . . 12
255	254	oveq1d 6109	. . . . . . . . . . 11
256	12	negcld 9709	. . . . . . . . . . . 12
257		eldifn 3482	. . . . . . . . . . . . . . 15 $\$
258	257, 3	eleq2s 2535	. . . . . . . . . . . . . 14
259		id 22	. . . . . . . . . . . . . . . . . 18
260		mnflt 11107	. . . . . . . . . . . . . . . . . . . 20
261	92, 260	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
262		ubioc1 11352	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
263	52, 138, 261, 262	mp3an 1314	. . . . . . . . . . . . . . . . . 18
264	259, 263	syl6eqel 2531	. . . . . . . . . . . . . . . . 17
265		id 22	. . . . . . . . . . . . . . . . . 18
266		ltpnf 11105	. . . . . . . . . . . . . . . . . . . 20
267	95, 266	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
268		lbico1 11353	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
269	139, 127, 267, 268	mp3an 1314	. . . . . . . . . . . . . . . . . 18
270	265, 269	syl6eqel 2531	. . . . . . . . . . . . . . . . 17
271	264, 270	orim12i 516	. . . . . . . . . . . . . . . 16 $\/$ $\/$
272	271	orcoms 389	. . . . . . . . . . . . . . 15 $\/$ $\/$
273		elun 3500	. . . . . . . . . . . . . . 15 $\/$
274	272, 273	sylibr 212	. . . . . . . . . . . . . 14 $\/$
275	258, 274	nsyl 121	. . . . . . . . . . . . 13 $\/$
276		1cnd 9405	. . . . . . . . . . . . . . . . . 18 $/\$
277	17	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
278	19	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
279		simpr 461	. . . . . . . . . . . . . . . . . . 19 $/\$
280	278, 279	sqr00d 12930	. . . . . . . . . . . . . . . . . 18 $/\$
281	276, 277, 280	subeq0d 9730	. . . . . . . . . . . . . . . . 17 $/\$
282	152, 281	syl5req 2488	. . . . . . . . . . . . . . . 16 $/\$
283	282	ex 434	. . . . . . . . . . . . . . 15
284		sqeqor 11983	. . . . . . . . . . . . . . . 16 $/\$ $\/$
285	16, 284	mpan2 671	. . . . . . . . . . . . . . 15 $\/$
286	283, 285	sylibd 214	. . . . . . . . . . . . . 14 $\/$
287	286	necon3bd 2648	. . . . . . . . . . . . 13 $\/$
288	12, 275, 287	sylc 60	. . . . . . . . . . . 12
289		2cnne0 10539	. . . . . . . . . . . . 13 $/\$
290		divcan5 10036	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
291	289, 290	mp3an3 1303	. . . . . . . . . . . 12 $/\$ $/\$
292	256, 117, 288, 291	syl12anc 1216	. . . . . . . . . . 11
293	226, 12, 227	sylancr 663	. . . . . . . . . . . . 13
294	293	negcld 9709	. . . . . . . . . . . 12
295		mulcl 9369	. . . . . . . . . . . . 13 $/\$
296	226, 117, 295	sylancr 663	. . . . . . . . . . . 12
297		mulne0 9981	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
298	289, 297	mpan 670	. . . . . . . . . . . . 13 $/\$
299	117, 288, 298	syl2anc 661	. . . . . . . . . . . 12
300	294, 296, 299	divrec2d 10114	. . . . . . . . . . 11
301	255, 292, 300	3eqtr3rd 2484	. . . . . . . . . 10
302	301	mpteq2ia 4377	. . . . . . . . 9
303	252, 302	syl6eq 2491	. . . . . . . 8
304	11, 77, 78, 114, 118, 120, 303	dvmptadd 21437	. . . . . . 7
305		mulcl 9369	. . . . . . . . . . . 12 $/\$
306	13, 20, 305	sylancr 663	. . . . . . . . . . 11
307	12, 306	syl 16	. . . . . . . . . 10
308	307, 256, 117, 288	divdird 10148	. . . . . . . . 9
309		ixi 9968	. . . . . . . . . . . . . . . 16
310	309	eqcomi 2447	. . . . . . . . . . . . . . 15
311	310	oveq1i 6104	. . . . . . . . . . . . . 14
312		mulm1 9789	. . . . . . . . . . . . . 14
313		mulass 9373	. . . . . . . . . . . . . . 15 $/\$ $/\$
314	13, 13, 313	mp3an12 1304	. . . . . . . . . . . . . 14
315	311, 312, 314	3eqtr3a 2499	. . . . . . . . . . . . 13
316	315	oveq1d 6109	. . . . . . . . . . . 12
317		negcl 9613	. . . . . . . . . . . . 13
318	306, 317	addcomd 9574	. . . . . . . . . . . 12
319	13	a1i 11	. . . . . . . . . . . . 13
320	319, 15, 20	adddid 9413	. . . . . . . . . . . 12
321	316, 318, 320	3eqtr4d 2485	. . . . . . . . . . 11
322	12, 321	syl 16	. . . . . . . . . 10
323	322	oveq1d 6109	. . . . . . . . 9
324	75, 117, 288	divcan4d 10116	. . . . . . . . . 10
325	324	oveq1d 6109	. . . . . . . . 9
326	308, 323, 325	3eqtr3rd 2484	. . . . . . . 8
327	326	mpteq2ia 4377	. . . . . . 7
328	304, 327	syl6eq 2491	. . . . . 6
329	246	dvlog 22099	. . . . . . 7 $\$ $\$
330		logf1o 22019	. . . . . . . . . 10 $\$
331		f1of 5644	. . . . . . . . . 10 $\$ $\$
332	330, 331	mp1i 12	. . . . . . . . 9 $\$
333		snssi 4020	. . . . . . . . . . 11
334	66, 333	ax-mp 5	. . . . . . . . . 10
335		sscon 3493	. . . . . . . . . 10 $\$ $\$
336	334, 335	mp1i 12	. . . . . . . . 9 $\$ $\$
337	332, 336	feqresmpt 5748	. . . . . . . 8 $\$ $\$
338	337	oveq2d 6110	. . . . . . 7 $\$ $\$
339	329, 338	syl5reqr 2490	. . . . . 6 $\$ $\$
340		fveq2 5694	. . . . . 6
341		oveq2 6102	. . . . . 6
342	11, 11, 58, 60, 72, 74, 328, 339, 340, 341	dvmptco 21449	. . . . 5
343	22, 24	reccld 10103	. . . . . . . 8
344		mulcl 9369	. . . . . . . . . 10 $/\$
345	13, 21, 344	sylancr 663	. . . . . . . . 9
346	12, 345	syl 16	. . . . . . . 8
347	343, 346, 117, 288	divassd 10145	. . . . . . 7
348	346, 22, 24	divrec2d 10114	. . . . . . . . 9
349	75, 22, 24	divcan4d 10116	. . . . . . . . 9
350	348, 349	eqtr3d 2477	. . . . . . . 8
351	350	oveq1d 6109	. . . . . . 7
352	347, 351	eqtr3d 2477	. . . . . 6
353	352	mpteq2ia 4377	. . . . 5
354	342, 353	syl6eq 2491	. . . 4
355		negicn 9614	. . . . 5
356	355	a1i 11	. . . 4
357	11, 26, 28, 354, 356	dvmptcmul 21441	. . 3
358	357	trud 1378	. 2
359	13, 13	mulneg1i 9793	. . . . . 6
360	309	negeqi 9606	. . . . . 6
361		negneg1e1 10432	. . . . . 6
362	359, 360, 361	3eqtri 2467	. . . . 5
363	362	oveq1i 6104	. . . 4
364		divass 10015	. . . . . 6 $/\$ $/\$ $/\$
365	355, 13, 364	mp3an12 1304	. . . . 5 $/\$
366	117, 288, 365	syl2anc 661	. . . 4
367	363, 366	syl5reqr 2490	. . 3
368	367	mpteq2ia 4377	. 2
369	9, 358, 368	3eqtri 2467	1 arcsin

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1369

wtru 1370

wcel 1756

wne 2609

cvv 2975 $\$ cdif 3328

cun 3329

cin 3330

wss 3331

c0 3640

csn 3880

cpr 3882 class class class wbr 4295

cmpt 4353

crn 4844

cres 4845

wf 5417

wf1o 5420

cfv 5421 (class class class)co 6094

cc 9283

cr 9284

cc0 9285

c1 9286

ci 9287

caddc 9288

cmul 9290

cpnf 9418

cmnf 9419

cxr 9420

clt 9421

cle 9422

cmin 9598

cneg 9599

cdiv 9996

cn 10325

c2 10374

crp 10994

cioo 11303

cioc 11304

cico 11305

cexp 11868

cre 12589

csqr 12725

cabs 12726 ↾_t crest 14362

ctopn 14363

ctg 14379 ℂ_fldccnfld 17821 TopOnctopon 18502

ccld 18623

cdv 21341

clog 22009 arcsincasin 22260

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 4406 ax-sep 4416 ax-nul 4424 ax-pow 4473 ax-pr 4534 ax-un 6375 ax-inf2 7850 ax-cnex 9341 ax-resscn 9342 ax-1cn 9343 ax-icn 9344 ax-addcl 9345 ax-addrcl 9346 ax-mulcl 9347 ax-mulrcl 9348 ax-mulcom 9349 ax-addass 9350 ax-mulass 9351 ax-distr 9352 ax-i2m1 9353 ax-1ne0 9354 ax-1rid 9355 ax-rnegex 9356 ax-rrecex 9357 ax-cnre 9358 ax-pre-lttri 9359 ax-pre-lttrn 9360 ax-pre-ltadd 9361 ax-pre-mulgt0 9362 ax-pre-sup 9363 ax-addf 9364 ax-mulf 9365

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 2571 df-ne 2611 df-nel 2612 df-ral 2723 df-rex 2724 df-reu 2725 df-rmo 2726 df-rab 2727 df-v 2977 df-sbc 3190 df-csb 3292 df-dif 3334 df-un 3336 df-in 3338 df-ss 3345 df-pss 3347 df-nul 3641 df-if 3795 df-pw 3865 df-sn 3881 df-pr 3883 df-tp 3885 df-op 3887 df-uni 4095 df-int 4132 df-iun 4176 df-iin 4177 df-br 4296 df-opab 4354 df-mpt 4355 df-tr 4389 df-eprel 4635 df-id 4639 df-po 4644 df-so 4645 df-fr 4682 df-se 4683 df-we 4684 df-ord 4725 df-on 4726 df-lim 4727 df-suc 4728 df-xp 4849 df-rel 4850 df-cnv 4851 df-co 4852 df-dm 4853 df-rn 4854 df-res 4855 df-ima 4856 df-iota 5384 df-fun 5423 df-fn 5424 df-f 5425 df-f1 5426 df-fo 5427 df-f1o 5428 df-fv 5429 df-isom 5430 df-riota 6055 df-ov 6097 df-oprab 6098 df-mpt2 6099 df-of 6323 df-om 6480 df-1st 6580 df-2nd 6581 df-supp 6694 df-recs 6835 df-rdg 6869 df-1o 6923 df-2o 6924 df-oadd 6927 df-er 7104 df-map 7219 df-pm 7220 df-ixp 7267 df-en 7314 df-dom 7315 df-sdom 7316 df-fin 7317 df-fsupp 7624 df-fi 7664 df-sup 7694 df-oi 7727 df-card 8112 df-cda 8340 df-pnf 9423 df-mnf 9424 df-xr 9425 df-ltxr 9426 df-le 9427 df-sub 9600 df-neg 9601 df-div 9997 df-nn 10326 df-2 10383 df-3 10384 df-4 10385 df-5 10386 df-6 10387 df-7 10388 df-8 10389 df-9 10390 df-10 10391 df-n0 10583 df-z 10650 df-dec 10759 df-uz 10865 df-q 10957 df-rp 10995 df-xneg 11092 df-xadd 11093 df-xmul 11094 df-ioo 11307 df-ioc 11308 df-ico 11309 df-icc 11310 df-fz 11441 df-fzo 11552 df-fl 11645 df-mod 11712 df-seq 11810 df-exp 11869 df-fac 12055 df-bc 12082 df-hash 12107 df-shft 12559 df-cj 12591 df-re 12592 df-im 12593 df-sqr 12727 df-abs 12728 df-limsup 12952 df-clim 12969 df-rlim 12970 df-sum 13167 df-ef 13356 df-sin 13358 df-cos 13359 df-tan 13360 df-pi 13361 df-struct 14179 df-ndx 14180 df-slot 14181 df-base 14182 df-sets 14183 df-ress 14184 df-plusg 14254 df-mulr 14255 df-starv 14256 df-sca 14257 df-vsca 14258 df-ip 14259 df-tset 14260 df-ple 14261 df-ds 14263 df-unif 14264 df-hom 14265 df-cco 14266 df-rest 14364 df-topn 14365 df-0g 14383 df-gsum 14384 df-topgen 14385 df-pt 14386 df-prds 14389 df-xrs 14443 df-qtop 14448 df-imas 14449 df-xps 14451 df-mre 14527 df-mrc 14528 df-acs 14530 df-mnd 15418 df-submnd 15468 df-mulg 15551 df-cntz 15838 df-cmn 16282 df-psmet 17812 df-xmet 17813 df-met 17814 df-bl 17815 df-mopn 17816 df-fbas 17817 df-fg 17818 df-cnfld 17822 df-top 18506 df-bases 18508 df-topon 18509 df-topsp 18510 df-cld 18626 df-ntr 18627 df-cls 18628 df-nei 18705 df-lp 18743 df-perf 18744 df-cn 18834 df-cnp 18835 df-haus 18922 df-cmp 18993 df-tx 19138 df-hmeo 19331 df-fil 19422 df-fm 19514 df-flim 19515 df-flf 19516 df-xms 19898 df-ms 19899 df-tms 19900 df-cncf 20457 df-limc 21344 df-dv 21345 df-log 22011 df-cxp 22012 df-asin 22263

This theorem is referenced by: dvacos 28484 dvreasin 28485

W3C validator