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 28423

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 22229	. . . . 5 arcsin
2	1	reseq1i 5098	. . . 4 arcsin
3		dvasin.d	. . . . . 6 $\$
4		difss 3476	. . . . . 6 $\$
5	3, 4	eqsstri 3379	. . . . 5
6		resmpt 5149	. . . . 5
7	5, 6	ax-mp 5	. . . 4
8	2, 7	eqtri 2457	. . 3 arcsin
9	8	oveq2i 6097	. 2 arcsin
10		cnelprrecn 9367	. . . . 5
11	10	a1i 11	. . . 4
12	5	sseli 3345	. . . . . . 7
13		ax-icn 9333	. . . . . . . . 9
14		mulcl 9358	. . . . . . . . 9 $/\$
15	13, 14	mpan 670	. . . . . . . 8
16		ax-1cn 9332	. . . . . . . . . 10
17		sqcl 11920	. . . . . . . . . 10
18		subcl 9601	. . . . . . . . . 10 $/\$
19	16, 17, 18	sylancr 663	. . . . . . . . 9
20	19	sqrcld 12915	. . . . . . . 8
21	15, 20	addcld 9397	. . . . . . 7
22	12, 21	syl 16	. . . . . 6
23		asinlem 22232	. . . . . . 7
24	12, 23	syl 16	. . . . . 6
25	22, 24	logcld 21991	. . . . 5
26	25	adantl 466	. . . 4 $/\$
27		ovex 6111	. . . . 5
28	27	a1i 11	. . . 4 $/\$
29		simpr 461	. . . . . . . . . . . . . . . 16 $/\$
30		asinlem3 22235	. . . . . . . . . . . . . . . . 17
31		rere 12603	. . . . . . . . . . . . . . . . . . 19
32	31	breq2d 4297	. . . . . . . . . . . . . . . . . 18
33	32	biimpac 486	. . . . . . . . . . . . . . . . 17 $/\$
34	30, 33	sylan 471	. . . . . . . . . . . . . . . 16 $/\$
35	23	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
36	29, 34, 35	ne0gt0d 9503	. . . . . . . . . . . . . . 15 $/\$
37		0re 9378	. . . . . . . . . . . . . . . . 17
38		ltnle 9446	. . . . . . . . . . . . . . . . 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 11086	. . . . . . . . . . 11
53		elioc2 11350	. . . . . . . . . . 11 $/\$ $/\$ $/\$
54	52, 37, 53	mp2an 672	. . . . . . . . . 10 $/\$ $/\$
55	51, 54	xchbinxr 311	. . . . . . . . 9 $\/$ $\/$
56	47, 55	sylib 196	. . . . . . . 8
57	22, 56	eldifd 3332	. . . . . . 7 $\$
58	57	adantl 466	. . . . . 6 $/\$ $\$
59		ovex 6111	. . . . . . 7
60	59	a1i 11	. . . . . 6 $/\$
61		eldifi 3471	. . . . . . . 8 $\$
62		eldifn 3472	. . . . . . . . 9 $\$
63		0xr 9422	. . . . . . . . . . . 12
64		mnflt0 11097	. . . . . . . . . . . 12
65		ubioc1 11341	. . . . . . . . . . . 12 $/\$ $/\$
66	52, 63, 64, 65	mp3an 1314	. . . . . . . . . . 11
67		eleq1 2497	. . . . . . . . . . 11
68	66, 67	mpbiri 233	. . . . . . . . . 10
69	68	necon3bi 2646	. . . . . . . . 9
70	62, 69	syl 16	. . . . . . . 8 $\$
71	61, 70	logcld 21991	. . . . . . 7 $\$
72	71	adantl 466	. . . . . 6 $/\$ $\$
73		ovex 6111	. . . . . . 7
74	73	a1i 11	. . . . . 6 $/\$ $\$
75	13	a1i 11	. . . . . . . . . 10
76	75, 12	mulcld 9398	. . . . . . . . 9
77	76	adantl 466	. . . . . . . 8 $/\$
78	13	a1i 11	. . . . . . . 8 $/\$
79	12	adantl 466	. . . . . . . . . 10 $/\$
80		1cnd 9394	. . . . . . . . . 10 $/\$
81		simpr 461	. . . . . . . . . . 11 $/\$
82		1cnd 9394	. . . . . . . . . . 11 $/\$
83	11	dvmptid 21400	. . . . . . . . . . 11
84	5	a1i 11	. . . . . . . . . . 11
85		eqid 2437	. . . . . . . . . . . . . 14 ℂ_fld ℂ_fld
86	85	cnfldtopon 20331	. . . . . . . . . . . . 13 ℂ_fld TopOn
87	86	toponunii 18506	. . . . . . . . . . . . . 14 ℂ_fld
88	87	restid 14364	. . . . . . . . . . . . 13 ℂ_fld TopOn ℂ_fld ↾_t ℂ_fld
89	86, 88	ax-mp 5	. . . . . . . . . . . 12 ℂ_fld ↾_t ℂ_fld
90	89	eqcomi 2441	. . . . . . . . . . 11 ℂ_fld ℂ_fld ↾_t
91	85	recld2 20360	. . . . . . . . . . . . . . 15 ℂ_fld
92		neg1rr 10418	. . . . . . . . . . . . . . . . . 18
93		iocmnfcld 20317	. . . . . . . . . . . . . . . . . 18
94	92, 93	ax-mp 5	. . . . . . . . . . . . . . . . 17
95		1re 9377	. . . . . . . . . . . . . . . . . 18
96		icopnfcld 20316	. . . . . . . . . . . . . . . . . 18
97	95, 96	ax-mp 5	. . . . . . . . . . . . . . . . 17
98		uncld 18614	. . . . . . . . . . . . . . . . 17 $/\$
99	94, 97, 98	mp2an 672	. . . . . . . . . . . . . . . 16
100	85	tgioo2 20349	. . . . . . . . . . . . . . . . 17 ℂ_fld ↾_t
101	100	fveq2i 5687	. . . . . . . . . . . . . . . 16 ℂ_fld ↾_t
102	99, 101	eleqtri 2509	. . . . . . . . . . . . . . 15 ℂ_fld ↾_t
103		restcldr 18747	. . . . . . . . . . . . . . 15 ℂ_fld $/\$ ℂ_fld ↾_t ℂ_fld
104	91, 102, 103	mp2an 672	. . . . . . . . . . . . . 14 ℂ_fld
105	87	cldopn 18604	. . . . . . . . . . . . . 14 ℂ_fld $\$ ℂ_fld
106	104, 105	ax-mp 5	. . . . . . . . . . . . 13 $\$ ℂ_fld
107	3, 106	eqeltri 2507	. . . . . . . . . . . 12 ℂ_fld
108	107	a1i 11	. . . . . . . . . . 11 ℂ_fld
109	11, 81, 82, 83, 84, 90, 85, 108	dvmptres 21406	. . . . . . . . . 10
110	13	a1i 11	. . . . . . . . . 10
111	11, 79, 80, 109, 110	dvmptcmul 21407	. . . . . . . . 9
112	13	mulid1i 9380	. . . . . . . . . 10
113	112	mpteq2i 4368	. . . . . . . . 9
114	111, 113	syl6eq 2485	. . . . . . . 8
115	12	sqcld 11998	. . . . . . . . . . 11
116	16, 115, 18	sylancr 663	. . . . . . . . . 10
117	116	sqrcld 12915	. . . . . . . . 9
118	117	adantl 466	. . . . . . . 8 $/\$
119		ovex 6111	. . . . . . . . 9
120	119	a1i 11	. . . . . . . 8 $/\$
121		elin 3532	. . . . . . . . . . . . . . 15 $/\$
122	3	asindmre 28422	. . . . . . . . . . . . . . . . 17
123	122	eqimssi 3403	. . . . . . . . . . . . . . . 16
124	123	sseli 3345	. . . . . . . . . . . . . . 15
125	121, 124	sylbir 213	. . . . . . . . . . . . . 14 $/\$
126		incom 3536	. . . . . . . . . . . . . . . 16
127		pnfxr 11084	. . . . . . . . . . . . . . . . 17
128		df-ioc 11297	. . . . . . . . . . . . . . . . . 18 $/\$
129		df-ioo 11296	. . . . . . . . . . . . . . . . . 18 $/\$
130		xrltnle 9435	. . . . . . . . . . . . . . . . . 18 $/\$
131	128, 129, 130	ixxdisj 11307	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
132	52, 63, 127, 131	mp3an 1314	. . . . . . . . . . . . . . . 16
133	126, 132	eqtri 2457	. . . . . . . . . . . . . . 15
134		elioore 11322	. . . . . . . . . . . . . . . . . . 19
135	134	resqcld 12026	. . . . . . . . . . . . . . . . . 18
136		resubcl 9665	. . . . . . . . . . . . . . . . . 18 $/\$
137	95, 135, 136	sylancr 663	. . . . . . . . . . . . . . . . 17
138	92	rexri 9428	. . . . . . . . . . . . . . . . . . 19
139	95	rexri 9428	. . . . . . . . . . . . . . . . . . 19
140		elioo2 11333	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
141	138, 139, 140	mp2an 672	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
142		recn 9364	. . . . . . . . . . . . . . . . . . . . . . 23
143	142	abscld 12914	. . . . . . . . . . . . . . . . . . . . . 22
144	142	absge0d 12922	. . . . . . . . . . . . . . . . . . . . . 22
145		0le1 9855	. . . . . . . . . . . . . . . . . . . . . . 23
146		lt2sq 11931	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
147	95, 145, 146	mpanr12 685	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
148	143, 144, 147	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21
149		abslt 12794	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
150	95, 149	mpan2 671	. . . . . . . . . . . . . . . . . . . . 21 $/\$
151		absresq 12783	. . . . . . . . . . . . . . . . . . . . . . 23
152		sq1 11952	. . . . . . . . . . . . . . . . . . . . . . . 24
153	152	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
154	151, 153	breq12d 4298	. . . . . . . . . . . . . . . . . . . . . 22
155		resqcl 11925	. . . . . . . . . . . . . . . . . . . . . . 23
156		posdif 9824	. . . . . . . . . . . . . . . . . . . . . . 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 11017	. . . . . . . . . . . . . . . 16
164		ioorp 11365	. . . . . . . . . . . . . . . 16
165	163, 164	syl6eleqr 2528	. . . . . . . . . . . . . . 15
166		disjel 3718	. . . . . . . . . . . . . . 15 $/\$
167	133, 165, 166	sylancr 663	. . . . . . . . . . . . . 14
168	125, 167	syl 16	. . . . . . . . . . . . 13 $/\$
169		elioc2 11350	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
170	52, 37, 169	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
171	170	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
172	171	simp1d 1000	. . . . . . . . . . . . . . . . . . . . . 22
173		resubcl 9665	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
174	95, 172, 173	sylancr 663	. . . . . . . . . . . . . . . . . . . . 21
175		nncan 9630	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
176	16, 175	mpan 670	. . . . . . . . . . . . . . . . . . . . . . 23
177	176	eleq1d 2503	. . . . . . . . . . . . . . . . . . . . . 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 9460	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
184	37, 95, 183	mp3an23 1306	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
185	145, 184	mpan2i 677	. . . . . . . . . . . . . . . . . . . . . . 23
186	180, 182, 185	sylc 60	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
187		subge0 9844	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
188	95, 180, 187	sylancr 663	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
189	186, 188	mpbird 232	. . . . . . . . . . . . . . . . . . . . 21 $/\$
190	176	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 $/\$
191	189, 190	breqtrd 4309	. . . . . . . . . . . . . . . . . . . 20 $/\$
192	179, 191	resqrcld 12896	. . . . . . . . . . . . . . . . . . 19 $/\$
193	17, 192	sylan 471	. . . . . . . . . . . . . . . . . 18 $/\$
194		eleq1 2497	. . . . . . . . . . . . . . . . . 18
195	193, 194	syl5ibrcom 222	. . . . . . . . . . . . . . . . 17 $/\$
196	193	renegcld 9767	. . . . . . . . . . . . . . . . . 18 $/\$
197		eleq1 2497	. . . . . . . . . . . . . . . . . 18
198	196, 197	syl5ibrcom 222	. . . . . . . . . . . . . . . . 17 $/\$
199		eqid 2437	. . . . . . . . . . . . . . . . . . 19
200		eqsqror 12846	. . . . . . . . . . . . . . . . . . . 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 3332	. . . . . . . . . . 11 $\$
210	209	adantl 466	. . . . . . . . . 10 $/\$ $\$
211		2cnd 10386	. . . . . . . . . . . . . 14
212		id 22	. . . . . . . . . . . . . 14
213	211, 212	mulcld 9398	. . . . . . . . . . . . 13
214	213	negcld 9698	. . . . . . . . . . . 12
215	214	adantl 466	. . . . . . . . . . 11 $/\$
216	12, 215	sylan2 474	. . . . . . . . . 10 $/\$
217	61	sqrcld 12915	. . . . . . . . . . 11 $\$
218	217	adantl 466	. . . . . . . . . 10 $/\$ $\$
219		ovex 6111	. . . . . . . . . . 11
220	219	a1i 11	. . . . . . . . . 10 $/\$ $\$
221	19	adantl 466	. . . . . . . . . . 11 $/\$
222	37	a1i 11	. . . . . . . . . . . . 13 $/\$
223		1cnd 9394	. . . . . . . . . . . . . 14
224	11, 223	dvmptc 21401	. . . . . . . . . . . . 13
225	17	adantl 466	. . . . . . . . . . . . 13 $/\$
226		2cn 10384	. . . . . . . . . . . . . . 15
227		mulcl 9358	. . . . . . . . . . . . . . 15 $/\$
228	226, 227	mpan 670	. . . . . . . . . . . . . 14
229	228	adantl 466	. . . . . . . . . . . . 13 $/\$
230		2nn 10471	. . . . . . . . . . . . . . . 16
231		dvexp 21396	. . . . . . . . . . . . . . . 16
232	230, 231	ax-mp 5	. . . . . . . . . . . . . . 15
233		2m1e1 10428	. . . . . . . . . . . . . . . . . . 19
234	233	oveq2i 6097	. . . . . . . . . . . . . . . . . 18
235		exp1 11863	. . . . . . . . . . . . . . . . . 18
236	234, 235	syl5eq 2481	. . . . . . . . . . . . . . . . 17
237	236	oveq2d 6102	. . . . . . . . . . . . . . . 16
238	237	mpteq2ia 4367	. . . . . . . . . . . . . . 15
239	232, 238	eqtri 2457	. . . . . . . . . . . . . 14
240	239	a1i 11	. . . . . . . . . . . . 13
241	11, 82, 222, 224, 225, 229, 240	dvmptsub 21410	. . . . . . . . . . . 12
242		df-neg 9590	. . . . . . . . . . . . 13
243	242	mpteq2i 4368	. . . . . . . . . . . 12
244	241, 243	syl6eqr 2487	. . . . . . . . . . 11
245	11, 221, 215, 244, 84, 90, 85, 108	dvmptres 21406	. . . . . . . . . 10
246		eqid 2437	. . . . . . . . . . . 12 $\$ $\$
247	246	dvcnsqr 28421	. . . . . . . . . . 11 $\$ $\$
248	247	a1i 11	. . . . . . . . . 10 $\$ $\$
249		fveq2 5684	. . . . . . . . . 10
250	249	oveq2d 6102	. . . . . . . . . . 11
251	250	oveq2d 6102	. . . . . . . . . 10
252	11, 11, 210, 216, 218, 220, 245, 248, 249, 251	dvmptco 21415	. . . . . . . . 9
253		mulneg2 9774	. . . . . . . . . . . . 13 $/\$
254	226, 12, 253	sylancr 663	. . . . . . . . . . . 12
255	254	oveq1d 6101	. . . . . . . . . . 11
256	12	negcld 9698	. . . . . . . . . . . 12
257		eldifn 3472	. . . . . . . . . . . . . . 15 $\$
258	257, 3	eleq2s 2529	. . . . . . . . . . . . . 14
259		id 22	. . . . . . . . . . . . . . . . . 18
260		mnflt 11096	. . . . . . . . . . . . . . . . . . . 20
261	92, 260	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
262		ubioc1 11341	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
263	52, 138, 261, 262	mp3an 1314	. . . . . . . . . . . . . . . . . 18
264	259, 263	syl6eqel 2525	. . . . . . . . . . . . . . . . 17
265		id 22	. . . . . . . . . . . . . . . . . 18
266		ltpnf 11094	. . . . . . . . . . . . . . . . . . . 20
267	95, 266	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
268		lbico1 11342	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
269	139, 127, 267, 268	mp3an 1314	. . . . . . . . . . . . . . . . . 18
270	265, 269	syl6eqel 2525	. . . . . . . . . . . . . . . . 17
271	264, 270	orim12i 516	. . . . . . . . . . . . . . . 16 $\/$ $\/$
272	271	orcoms 389	. . . . . . . . . . . . . . 15 $\/$ $\/$
273		elun 3490	. . . . . . . . . . . . . . 15 $\/$
274	272, 273	sylibr 212	. . . . . . . . . . . . . 14 $\/$
275	258, 274	nsyl 121	. . . . . . . . . . . . 13 $\/$
276		1cnd 9394	. . . . . . . . . . . . . . . . . 18 $/\$
277	17	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
278	19	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
279		simpr 461	. . . . . . . . . . . . . . . . . . 19 $/\$
280	278, 279	sqr00d 12919	. . . . . . . . . . . . . . . . . 18 $/\$
281	276, 277, 280	subeq0d 9719	. . . . . . . . . . . . . . . . 17 $/\$
282	152, 281	syl5req 2482	. . . . . . . . . . . . . . . 16 $/\$
283	282	ex 434	. . . . . . . . . . . . . . 15
284		sqeqor 11972	. . . . . . . . . . . . . . . 16 $/\$ $\/$
285	16, 284	mpan2 671	. . . . . . . . . . . . . . 15 $\/$
286	283, 285	sylibd 214	. . . . . . . . . . . . . 14 $\/$
287	286	necon3bd 2639	. . . . . . . . . . . . 13 $\/$
288	12, 275, 287	sylc 60	. . . . . . . . . . . 12
289		2cnne0 10528	. . . . . . . . . . . . 13 $/\$
290		divcan5 10025	. . . . . . . . . . . . 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 9698	. . . . . . . . . . . 12
295		mulcl 9358	. . . . . . . . . . . . 13 $/\$
296	226, 117, 295	sylancr 663	. . . . . . . . . . . 12
297		mulne0 9970	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
298	289, 297	mpan 670	. . . . . . . . . . . . 13 $/\$
299	117, 288, 298	syl2anc 661	. . . . . . . . . . . 12
300	294, 296, 299	divrec2d 10103	. . . . . . . . . . 11
301	255, 292, 300	3eqtr3rd 2478	. . . . . . . . . 10
302	301	mpteq2ia 4367	. . . . . . . . 9
303	252, 302	syl6eq 2485	. . . . . . . 8
304	11, 77, 78, 114, 118, 120, 303	dvmptadd 21403	. . . . . . 7
305		mulcl 9358	. . . . . . . . . . . 12 $/\$
306	13, 20, 305	sylancr 663	. . . . . . . . . . 11
307	12, 306	syl 16	. . . . . . . . . 10
308	307, 256, 117, 288	divdird 10137	. . . . . . . . 9
309		ixi 9957	. . . . . . . . . . . . . . . 16
310	309	eqcomi 2441	. . . . . . . . . . . . . . 15
311	310	oveq1i 6096	. . . . . . . . . . . . . 14
312		mulm1 9778	. . . . . . . . . . . . . 14
313		mulass 9362	. . . . . . . . . . . . . . 15 $/\$ $/\$
314	13, 13, 313	mp3an12 1304	. . . . . . . . . . . . . 14
315	311, 312, 314	3eqtr3a 2493	. . . . . . . . . . . . 13
316	315	oveq1d 6101	. . . . . . . . . . . 12
317		negcl 9602	. . . . . . . . . . . . 13
318	306, 317	addcomd 9563	. . . . . . . . . . . 12
319	13	a1i 11	. . . . . . . . . . . . 13
320	319, 15, 20	adddid 9402	. . . . . . . . . . . 12
321	316, 318, 320	3eqtr4d 2479	. . . . . . . . . . 11
322	12, 321	syl 16	. . . . . . . . . 10
323	322	oveq1d 6101	. . . . . . . . 9
324	75, 117, 288	divcan4d 10105	. . . . . . . . . 10
325	324	oveq1d 6101	. . . . . . . . 9
326	308, 323, 325	3eqtr3rd 2478	. . . . . . . 8
327	326	mpteq2ia 4367	. . . . . . 7
328	304, 327	syl6eq 2485	. . . . . 6
329	246	dvlog 22065	. . . . . . 7 $\$ $\$
330		logf1o 21985	. . . . . . . . . 10 $\$
331		f1of 5634	. . . . . . . . . 10 $\$ $\$
332	330, 331	mp1i 12	. . . . . . . . 9 $\$
333		snssi 4010	. . . . . . . . . . 11
334	66, 333	ax-mp 5	. . . . . . . . . 10
335		sscon 3483	. . . . . . . . . 10 $\$ $\$
336	334, 335	mp1i 12	. . . . . . . . 9 $\$ $\$
337	332, 336	feqresmpt 5738	. . . . . . . 8 $\$ $\$
338	337	oveq2d 6102	. . . . . . 7 $\$ $\$
339	329, 338	syl5reqr 2484	. . . . . 6 $\$ $\$
340		fveq2 5684	. . . . . 6
341		oveq2 6094	. . . . . 6
342	11, 11, 58, 60, 72, 74, 328, 339, 340, 341	dvmptco 21415	. . . . 5
343	22, 24	reccld 10092	. . . . . . . 8
344		mulcl 9358	. . . . . . . . . 10 $/\$
345	13, 21, 344	sylancr 663	. . . . . . . . 9
346	12, 345	syl 16	. . . . . . . 8
347	343, 346, 117, 288	divassd 10134	. . . . . . 7
348	346, 22, 24	divrec2d 10103	. . . . . . . . 9
349	75, 22, 24	divcan4d 10105	. . . . . . . . 9
350	348, 349	eqtr3d 2471	. . . . . . . 8
351	350	oveq1d 6101	. . . . . . 7
352	347, 351	eqtr3d 2471	. . . . . 6
353	352	mpteq2ia 4367	. . . . 5
354	342, 353	syl6eq 2485	. . . 4
355		negicn 9603	. . . . 5
356	355	a1i 11	. . . 4
357	11, 26, 28, 354, 356	dvmptcmul 21407	. . 3
358	357	trud 1378	. 2
359	13, 13	mulneg1i 9782	. . . . . 6
360	309	negeqi 9595	. . . . . 6
361		negneg1e1 10421	. . . . . 6
362	359, 360, 361	3eqtri 2461	. . . . 5
363	362	oveq1i 6096	. . . 4
364		divass 10004	. . . . . 6 $/\$ $/\$ $/\$
365	355, 13, 364	mp3an12 1304	. . . . 5 $/\$
366	117, 288, 365	syl2anc 661	. . . 4
367	363, 366	syl5reqr 2484	. . 3
368	367	mpteq2ia 4367	. 2
369	9, 358, 368	3eqtri 2461	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 2600

cvv 2966 $\$ cdif 3318

cun 3319

cin 3320

wss 3321

c0 3630

csn 3870

cpr 3872 class class class wbr 4285

cmpt 4343

crn 4833

cres 4834

wf 5407

wf1o 5410

cfv 5411 (class class class)co 6086

cc 9272

cr 9273

cc0 9274

c1 9275

ci 9276

caddc 9277

cmul 9279

cpnf 9407

cmnf 9408

cxr 9409

clt 9410

cle 9411

cmin 9587

cneg 9588

cdiv 9985

cn 10314

c2 10363

crp 10983

cioo 11292

cioc 11293

cico 11294

cexp 11857

cre 12578

csqr 12714

cabs 12715 ↾_t crest 14351

ctopn 14352

ctg 14368 ℂ_fldccnfld 17787 TopOnctopon 18468

ccld 18589

cdv 21307

clog 21975 arcsincasin 22226

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 2418 ax-rep 4396 ax-sep 4406 ax-nul 4414 ax-pow 4463 ax-pr 4524 ax-un 6367 ax-inf2 7839 ax-cnex 9330 ax-resscn 9331 ax-1cn 9332 ax-icn 9333 ax-addcl 9334 ax-addrcl 9335 ax-mulcl 9336 ax-mulrcl 9337 ax-mulcom 9338 ax-addass 9339 ax-mulass 9340 ax-distr 9341 ax-i2m1 9342 ax-1ne0 9343 ax-1rid 9344 ax-rnegex 9345 ax-rrecex 9346 ax-cnre 9347 ax-pre-lttri 9348 ax-pre-lttrn 9349 ax-pre-ltadd 9350 ax-pre-mulgt0 9351 ax-pre-sup 9352 ax-addf 9353 ax-mulf 9354

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 2256 df-mo 2257 df-clab 2424 df-cleq 2430 df-clel 2433 df-nfc 2562 df-ne 2602 df-nel 2603 df-ral 2714 df-rex 2715 df-reu 2716 df-rmo 2717 df-rab 2718 df-v 2968 df-sbc 3180 df-csb 3282 df-dif 3324 df-un 3326 df-in 3328 df-ss 3335 df-pss 3337 df-nul 3631 df-if 3785 df-pw 3855 df-sn 3871 df-pr 3873 df-tp 3875 df-op 3877 df-uni 4085 df-int 4122 df-iun 4166 df-iin 4167 df-br 4286 df-opab 4344 df-mpt 4345 df-tr 4379 df-eprel 4624 df-id 4628 df-po 4633 df-so 4634 df-fr 4671 df-se 4672 df-we 4673 df-ord 4714 df-on 4715 df-lim 4716 df-suc 4717 df-xp 4838 df-rel 4839 df-cnv 4840 df-co 4841 df-dm 4842 df-rn 4843 df-res 4844 df-ima 4845 df-iota 5374 df-fun 5413 df-fn 5414 df-f 5415 df-f1 5416 df-fo 5417 df-f1o 5418 df-fv 5419 df-isom 5420 df-riota 6045 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-of 6315 df-om 6472 df-1st 6572 df-2nd 6573 df-supp 6686 df-recs 6824 df-rdg 6858 df-1o 6912 df-2o 6913 df-oadd 6916 df-er 7093 df-map 7208 df-pm 7209 df-ixp 7256 df-en 7303 df-dom 7304 df-sdom 7305 df-fin 7306 df-fsupp 7613 df-fi 7653 df-sup 7683 df-oi 7716 df-card 8101 df-cda 8329 df-pnf 9412 df-mnf 9413 df-xr 9414 df-ltxr 9415 df-le 9416 df-sub 9589 df-neg 9590 df-div 9986 df-nn 10315 df-2 10372 df-3 10373 df-4 10374 df-5 10375 df-6 10376 df-7 10377 df-8 10378 df-9 10379 df-10 10380 df-n0 10572 df-z 10639 df-dec 10748 df-uz 10854 df-q 10946 df-rp 10984 df-xneg 11081 df-xadd 11082 df-xmul 11083 df-ioo 11296 df-ioc 11297 df-ico 11298 df-icc 11299 df-fz 11430 df-fzo 11541 df-fl 11634 df-mod 11701 df-seq 11799 df-exp 11858 df-fac 12044 df-bc 12071 df-hash 12096 df-shft 12548 df-cj 12580 df-re 12581 df-im 12582 df-sqr 12716 df-abs 12717 df-limsup 12941 df-clim 12958 df-rlim 12959 df-sum 13156 df-ef 13345 df-sin 13347 df-cos 13348 df-tan 13349 df-pi 13350 df-struct 14168 df-ndx 14169 df-slot 14170 df-base 14171 df-sets 14172 df-ress 14173 df-plusg 14243 df-mulr 14244 df-starv 14245 df-sca 14246 df-vsca 14247 df-ip 14248 df-tset 14249 df-ple 14250 df-ds 14252 df-unif 14253 df-hom 14254 df-cco 14255 df-rest 14353 df-topn 14354 df-0g 14372 df-gsum 14373 df-topgen 14374 df-pt 14375 df-prds 14378 df-xrs 14432 df-qtop 14437 df-imas 14438 df-xps 14440 df-mre 14516 df-mrc 14517 df-acs 14519 df-mnd 15407 df-submnd 15457 df-mulg 15537 df-cntz 15824 df-cmn 16268 df-psmet 17778 df-xmet 17779 df-met 17780 df-bl 17781 df-mopn 17782 df-fbas 17783 df-fg 17784 df-cnfld 17788 df-top 18472 df-bases 18474 df-topon 18475 df-topsp 18476 df-cld 18592 df-ntr 18593 df-cls 18594 df-nei 18671 df-lp 18709 df-perf 18710 df-cn 18800 df-cnp 18801 df-haus 18888 df-cmp 18959 df-tx 19104 df-hmeo 19297 df-fil 19388 df-fm 19480 df-flim 19481 df-flf 19482 df-xms 19864 df-ms 19865 df-tms 19866 df-cncf 20423 df-limc 21310 df-dv 21311 df-log 21977 df-cxp 21978 df-asin 22229

This theorem is referenced by: dvacos 28424 dvreasin 28425

W3C validator