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 30269

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 23312	. . . . 5 arcsin
2	1	reseq1i 5182	. . . 4 arcsin
3		dvasin.d	. . . . . 6 $\$
4		difss 3545	. . . . . 6 $\$
5	3, 4	eqsstri 3447	. . . . 5
6		resmpt 5235	. . . . 5
7	5, 6	ax-mp 5	. . . 4
8	2, 7	eqtri 2411	. . 3 arcsin
9	8	oveq2i 6207	. 2 arcsin
10		cnelprrecn 9496	. . . . 5
11	10	a1i 11	. . . 4
12	5	sseli 3413	. . . . . . 7
13		ax-icn 9462	. . . . . . . . 9
14		mulcl 9487	. . . . . . . . 9 $/\$
15	13, 14	mpan 668	. . . . . . . 8
16		ax-1cn 9461	. . . . . . . . . 10
17		sqcl 12133	. . . . . . . . . 10
18		subcl 9732	. . . . . . . . . 10 $/\$
19	16, 17, 18	sylancr 661	. . . . . . . . 9
20	19	sqrtcld 13270	. . . . . . . 8
21	15, 20	addcld 9526	. . . . . . 7
22	12, 21	syl 16	. . . . . 6
23		asinlem 23315	. . . . . . 7
24	12, 23	syl 16	. . . . . 6
25	22, 24	logcld 23043	. . . . 5
26	25	adantl 464	. . . 4 $/\$
27		ovex 6224	. . . . 5
28	27	a1i 11	. . . 4 $/\$
29		simpr 459	. . . . . . . . . . . . . . . 16 $/\$
30		asinlem3 23318	. . . . . . . . . . . . . . . . 17
31		rere 12957	. . . . . . . . . . . . . . . . . . 19
32	31	breq2d 4379	. . . . . . . . . . . . . . . . . 18
33	32	biimpac 484	. . . . . . . . . . . . . . . . 17 $/\$
34	30, 33	sylan 469	. . . . . . . . . . . . . . . 16 $/\$
35	23	adantr 463	. . . . . . . . . . . . . . . 16 $/\$
36	29, 34, 35	ne0gt0d 9633	. . . . . . . . . . . . . . 15 $/\$
37		0re 9507	. . . . . . . . . . . . . . . . 17
38		ltnle 9575	. . . . . . . . . . . . . . . . 17 $/\$
39	37, 38	mpan 668	. . . . . . . . . . . . . . . 16
40	39	adantl 464	. . . . . . . . . . . . . . 15 $/\$
41	36, 40	mpbid 210	. . . . . . . . . . . . . 14 $/\$
42	41	ex 432	. . . . . . . . . . . . 13
43	12, 42	syl 16	. . . . . . . . . . . 12
44		imor 410	. . . . . . . . . . . 12 $\/$
45	43, 44	sylib 196	. . . . . . . . . . 11 $\/$
46	45	orcomd 386	. . . . . . . . . 10 $\/$
47	46	olcd 391	. . . . . . . . 9 $\/$ $\/$
48		3ianor 988	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $\/$
49		3orrot 977	. . . . . . . . . . 11 $\/$ $\/$ $\/$ $\/$
50		3orass 974	. . . . . . . . . . 11 $\/$ $\/$ $\/$ $\/$
51	48, 49, 50	3bitrri 272	. . . . . . . . . 10 $\/$ $\/$ $/\$ $/\$
52		mnfxr 11244	. . . . . . . . . . 11
53		elioc2 11508	. . . . . . . . . . 11 $/\$ $/\$ $/\$
54	52, 37, 53	mp2an 670	. . . . . . . . . 10 $/\$ $/\$
55	51, 54	xchbinxr 309	. . . . . . . . 9 $\/$ $\/$
56	47, 55	sylib 196	. . . . . . . 8
57	22, 56	eldifd 3400	. . . . . . 7 $\$
58	57	adantl 464	. . . . . 6 $/\$ $\$
59		ovex 6224	. . . . . . 7
60	59	a1i 11	. . . . . 6 $/\$
61		eldifi 3540	. . . . . . . 8 $\$
62		eldifn 3541	. . . . . . . . 9 $\$
63		0xr 9551	. . . . . . . . . . . 12
64		mnflt0 11255	. . . . . . . . . . . 12
65		ubioc1 11499	. . . . . . . . . . . 12 $/\$ $/\$
66	52, 63, 64, 65	mp3an 1322	. . . . . . . . . . 11
67		eleq1 2454	. . . . . . . . . . 11
68	66, 67	mpbiri 233	. . . . . . . . . 10
69	68	necon3bi 2611	. . . . . . . . 9
70	62, 69	syl 16	. . . . . . . 8 $\$
71	61, 70	logcld 23043	. . . . . . 7 $\$
72	71	adantl 464	. . . . . 6 $/\$ $\$
73		ovex 6224	. . . . . . 7
74	73	a1i 11	. . . . . 6 $/\$ $\$
75	13	a1i 11	. . . . . . . . . 10
76	75, 12	mulcld 9527	. . . . . . . . 9
77	76	adantl 464	. . . . . . . 8 $/\$
78	13	a1i 11	. . . . . . . 8 $/\$
79	12	adantl 464	. . . . . . . . . 10 $/\$
80		1cnd 9523	. . . . . . . . . 10 $/\$
81		simpr 459	. . . . . . . . . . 11 $/\$
82		1cnd 9523	. . . . . . . . . . 11 $/\$
83	11	dvmptid 22445	. . . . . . . . . . 11
84	5	a1i 11	. . . . . . . . . . 11
85		eqid 2382	. . . . . . . . . . . . . 14 ℂ_fld ℂ_fld
86	85	cnfldtopon 21375	. . . . . . . . . . . . 13 ℂ_fld TopOn
87	86	toponunii 19518	. . . . . . . . . . . . . 14 ℂ_fld
88	87	restid 14841	. . . . . . . . . . . . 13 ℂ_fld TopOn ℂ_fld ↾_t ℂ_fld
89	86, 88	ax-mp 5	. . . . . . . . . . . 12 ℂ_fld ↾_t ℂ_fld
90	89	eqcomi 2395	. . . . . . . . . . 11 ℂ_fld ℂ_fld ↾_t
91	85	recld2 21404	. . . . . . . . . . . . . . 15 ℂ_fld
92		neg1rr 10557	. . . . . . . . . . . . . . . . . 18
93		iocmnfcld 21361	. . . . . . . . . . . . . . . . . 18
94	92, 93	ax-mp 5	. . . . . . . . . . . . . . . . 17
95		1re 9506	. . . . . . . . . . . . . . . . . 18
96		icopnfcld 21360	. . . . . . . . . . . . . . . . . 18
97	95, 96	ax-mp 5	. . . . . . . . . . . . . . . . 17
98		uncld 19627	. . . . . . . . . . . . . . . . 17 $/\$
99	94, 97, 98	mp2an 670	. . . . . . . . . . . . . . . 16
100	85	tgioo2 21393	. . . . . . . . . . . . . . . . 17 ℂ_fld ↾_t
101	100	fveq2i 5777	. . . . . . . . . . . . . . . 16 ℂ_fld ↾_t
102	99, 101	eleqtri 2468	. . . . . . . . . . . . . . 15 ℂ_fld ↾_t
103		restcldr 19761	. . . . . . . . . . . . . . 15 ℂ_fld $/\$ ℂ_fld ↾_t ℂ_fld
104	91, 102, 103	mp2an 670	. . . . . . . . . . . . . 14 ℂ_fld
105	87	cldopn 19617	. . . . . . . . . . . . . 14 ℂ_fld $\$ ℂ_fld
106	104, 105	ax-mp 5	. . . . . . . . . . . . 13 $\$ ℂ_fld
107	3, 106	eqeltri 2466	. . . . . . . . . . . 12 ℂ_fld
108	107	a1i 11	. . . . . . . . . . 11 ℂ_fld
109	11, 81, 82, 83, 84, 90, 85, 108	dvmptres 22451	. . . . . . . . . 10
110	13	a1i 11	. . . . . . . . . 10
111	11, 79, 80, 109, 110	dvmptcmul 22452	. . . . . . . . 9
112	13	mulid1i 9509	. . . . . . . . . 10
113	112	mpteq2i 4450	. . . . . . . . 9
114	111, 113	syl6eq 2439	. . . . . . . 8
115	12	sqcld 12210	. . . . . . . . . . 11
116	16, 115, 18	sylancr 661	. . . . . . . . . 10
117	116	sqrtcld 13270	. . . . . . . . 9
118	117	adantl 464	. . . . . . . 8 $/\$
119		ovex 6224	. . . . . . . . 9
120	119	a1i 11	. . . . . . . 8 $/\$
121		elin 3601	. . . . . . . . . . . . . . 15 $/\$
122	3	asindmre 30268	. . . . . . . . . . . . . . . . 17
123	122	eqimssi 3471	. . . . . . . . . . . . . . . 16
124	123	sseli 3413	. . . . . . . . . . . . . . 15
125	121, 124	sylbir 213	. . . . . . . . . . . . . 14 $/\$
126		incom 3605	. . . . . . . . . . . . . . . 16
127		pnfxr 11242	. . . . . . . . . . . . . . . . 17
128		df-ioc 11455	. . . . . . . . . . . . . . . . . 18 $/\$
129		df-ioo 11454	. . . . . . . . . . . . . . . . . 18 $/\$
130		xrltnle 9564	. . . . . . . . . . . . . . . . . 18 $/\$
131	128, 129, 130	ixxdisj 11465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
132	52, 63, 127, 131	mp3an 1322	. . . . . . . . . . . . . . . 16
133	126, 132	eqtri 2411	. . . . . . . . . . . . . . 15
134		elioore 11480	. . . . . . . . . . . . . . . . . . 19
135	134	resqcld 12238	. . . . . . . . . . . . . . . . . 18
136		resubcl 9796	. . . . . . . . . . . . . . . . . 18 $/\$
137	95, 135, 136	sylancr 661	. . . . . . . . . . . . . . . . 17
138	92	rexri 9557	. . . . . . . . . . . . . . . . . . 19
139	95	rexri 9557	. . . . . . . . . . . . . . . . . . 19
140		elioo2 11491	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
141	138, 139, 140	mp2an 670	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
142		recn 9493	. . . . . . . . . . . . . . . . . . . . . . 23
143	142	abscld 13269	. . . . . . . . . . . . . . . . . . . . . 22
144	142	absge0d 13277	. . . . . . . . . . . . . . . . . . . . . 22
145		0le1 9993	. . . . . . . . . . . . . . . . . . . . . . 23
146		lt2sq 12144	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
147	95, 145, 146	mpanr12 683	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
148	143, 144, 147	syl2anc 659	. . . . . . . . . . . . . . . . . . . . 21
149		abslt 13149	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
150	95, 149	mpan2 669	. . . . . . . . . . . . . . . . . . . . 21 $/\$
151		absresq 13137	. . . . . . . . . . . . . . . . . . . . . . 23
152		sq1 12165	. . . . . . . . . . . . . . . . . . . . . . . 24
153	152	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
154	151, 153	breq12d 4380	. . . . . . . . . . . . . . . . . . . . . 22
155		resqcl 12138	. . . . . . . . . . . . . . . . . . . . . . 23
156		posdif 9963	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
157	155, 95, 156	sylancl 660	. . . . . . . . . . . . . . . . . . . . . 22
158	154, 157	bitrd 253	. . . . . . . . . . . . . . . . . . . . 21
159	148, 150, 158	3bitr3d 283	. . . . . . . . . . . . . . . . . . . 20 $/\$
160	159	biimpd 207	. . . . . . . . . . . . . . . . . . 19 $/\$
161	160	3impib 1192	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
162	141, 161	sylbi 195	. . . . . . . . . . . . . . . . 17
163	137, 162	elrpd 11174	. . . . . . . . . . . . . . . 16
164		ioorp 11523	. . . . . . . . . . . . . . . 16
165	163, 164	syl6eleqr 2481	. . . . . . . . . . . . . . 15
166		disjel 3789	. . . . . . . . . . . . . . 15 $/\$
167	133, 165, 166	sylancr 661	. . . . . . . . . . . . . 14
168	125, 167	syl 16	. . . . . . . . . . . . 13 $/\$
169		elioc2 11508	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
170	52, 37, 169	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
171	170	biimpi 194	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
172	171	simp1d 1006	. . . . . . . . . . . . . . . . . . . . 21
173		resubcl 9796	. . . . . . . . . . . . . . . . . . . . 21 $/\$
174	95, 172, 173	sylancr 661	. . . . . . . . . . . . . . . . . . . 20
175		nncan 9761	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
176	16, 175	mpan 668	. . . . . . . . . . . . . . . . . . . . . 22
177	176	eleq1d 2451	. . . . . . . . . . . . . . . . . . . . 21
178	177	biimpa 482	. . . . . . . . . . . . . . . . . . . 20 $/\$
179	174, 178	sylan2 472	. . . . . . . . . . . . . . . . . . 19 $/\$
180	172	adantl 464	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
181	171	simp3d 1008	. . . . . . . . . . . . . . . . . . . . . . 23
182	181	adantl 464	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
183		letr 9589	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
184	37, 95, 183	mp3an23 1314	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
185	145, 184	mpan2i 675	. . . . . . . . . . . . . . . . . . . . . 22
186	180, 182, 185	sylc 60	. . . . . . . . . . . . . . . . . . . . 21 $/\$
187		subge0 9983	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
188	95, 180, 187	sylancr 661	. . . . . . . . . . . . . . . . . . . . 21 $/\$
189	186, 188	mpbird 232	. . . . . . . . . . . . . . . . . . . 20 $/\$
190	176	adantr 463	. . . . . . . . . . . . . . . . . . . 20 $/\$
191	189, 190	breqtrd 4391	. . . . . . . . . . . . . . . . . . 19 $/\$
192	179, 191	resqrtcld 13251	. . . . . . . . . . . . . . . . . 18 $/\$
193	17, 192	sylan 469	. . . . . . . . . . . . . . . . 17 $/\$
194		eleq1 2454	. . . . . . . . . . . . . . . . 17
195	193, 194	syl5ibrcom 222	. . . . . . . . . . . . . . . 16 $/\$
196	193	renegcld 9904	. . . . . . . . . . . . . . . . 17 $/\$
197		eleq1 2454	. . . . . . . . . . . . . . . . 17
198	196, 197	syl5ibrcom 222	. . . . . . . . . . . . . . . 16 $/\$
199		eqid 2382	. . . . . . . . . . . . . . . . . 18
200		eqsqrtor 13201	. . . . . . . . . . . . . . . . . . 19 $/\$ $\/$
201	17, 200	mpdan 666	. . . . . . . . . . . . . . . . . 18 $\/$
202	199, 201	mpbii 211	. . . . . . . . . . . . . . . . 17 $\/$
203	202	adantr 463	. . . . . . . . . . . . . . . 16 $/\$ $\/$
204	195, 198, 203	mpjaod 379	. . . . . . . . . . . . . . 15 $/\$
205	204	stoic1a 1612	. . . . . . . . . . . . . 14 $/\$
206	12, 205	sylan 469	. . . . . . . . . . . . 13 $/\$
207	168, 206	pm2.61dan 789	. . . . . . . . . . . 12
208	116, 207	eldifd 3400	. . . . . . . . . . 11 $\$
209	208	adantl 464	. . . . . . . . . 10 $/\$ $\$
210		2cnd 10525	. . . . . . . . . . . . . 14
211		id 22	. . . . . . . . . . . . . 14
212	210, 211	mulcld 9527	. . . . . . . . . . . . 13
213	212	negcld 9831	. . . . . . . . . . . 12
214	213	adantl 464	. . . . . . . . . . 11 $/\$
215	12, 214	sylan2 472	. . . . . . . . . 10 $/\$
216	61	sqrtcld 13270	. . . . . . . . . . 11 $\$
217	216	adantl 464	. . . . . . . . . 10 $/\$ $\$
218		ovex 6224	. . . . . . . . . . 11
219	218	a1i 11	. . . . . . . . . 10 $/\$ $\$
220	19	adantl 464	. . . . . . . . . . 11 $/\$
221	37	a1i 11	. . . . . . . . . . . . 13 $/\$
222		1cnd 9523	. . . . . . . . . . . . . 14
223	11, 222	dvmptc 22446	. . . . . . . . . . . . 13
224	17	adantl 464	. . . . . . . . . . . . 13 $/\$
225		2cn 10523	. . . . . . . . . . . . . . 15
226		mulcl 9487	. . . . . . . . . . . . . . 15 $/\$
227	225, 226	mpan 668	. . . . . . . . . . . . . 14
228	227	adantl 464	. . . . . . . . . . . . 13 $/\$
229		2nn 10610	. . . . . . . . . . . . . . . 16
230		dvexp 22441	. . . . . . . . . . . . . . . 16
231	229, 230	ax-mp 5	. . . . . . . . . . . . . . 15
232		2m1e1 10567	. . . . . . . . . . . . . . . . . . 19
233	232	oveq2i 6207	. . . . . . . . . . . . . . . . . 18
234		exp1 12075	. . . . . . . . . . . . . . . . . 18
235	233, 234	syl5eq 2435	. . . . . . . . . . . . . . . . 17
236	235	oveq2d 6212	. . . . . . . . . . . . . . . 16
237	236	mpteq2ia 4449	. . . . . . . . . . . . . . 15
238	231, 237	eqtri 2411	. . . . . . . . . . . . . 14
239	238	a1i 11	. . . . . . . . . . . . 13
240	11, 82, 221, 223, 224, 228, 239	dvmptsub 22455	. . . . . . . . . . . 12
241		df-neg 9721	. . . . . . . . . . . . 13
242	241	mpteq2i 4450	. . . . . . . . . . . 12
243	240, 242	syl6eqr 2441	. . . . . . . . . . 11
244	11, 220, 214, 243, 84, 90, 85, 108	dvmptres 22451	. . . . . . . . . 10
245		eqid 2382	. . . . . . . . . . . 12 $\$ $\$
246	245	dvcnsqrt 30267	. . . . . . . . . . 11 $\$ $\$
247	246	a1i 11	. . . . . . . . . 10 $\$ $\$
248		fveq2 5774	. . . . . . . . . 10
249	248	oveq2d 6212	. . . . . . . . . . 11
250	249	oveq2d 6212	. . . . . . . . . 10
251	11, 11, 209, 215, 217, 219, 244, 247, 248, 250	dvmptco 22460	. . . . . . . . 9
252		mulneg2 9912	. . . . . . . . . . . . 13 $/\$
253	225, 12, 252	sylancr 661	. . . . . . . . . . . 12
254	253	oveq1d 6211	. . . . . . . . . . 11
255	12	negcld 9831	. . . . . . . . . . . 12
256		eldifn 3541	. . . . . . . . . . . . . . 15 $\$
257	256, 3	eleq2s 2490	. . . . . . . . . . . . . 14
258		id 22	. . . . . . . . . . . . . . . . . 18
259		mnflt 11254	. . . . . . . . . . . . . . . . . . . 20
260	92, 259	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
261		ubioc1 11499	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
262	52, 138, 260, 261	mp3an 1322	. . . . . . . . . . . . . . . . . 18
263	258, 262	syl6eqel 2478	. . . . . . . . . . . . . . . . 17
264		id 22	. . . . . . . . . . . . . . . . . 18
265		ltpnf 11252	. . . . . . . . . . . . . . . . . . . 20
266	95, 265	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
267		lbico1 11500	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
268	139, 127, 266, 267	mp3an 1322	. . . . . . . . . . . . . . . . . 18
269	264, 268	syl6eqel 2478	. . . . . . . . . . . . . . . . 17
270	263, 269	orim12i 514	. . . . . . . . . . . . . . . 16 $\/$ $\/$
271	270	orcoms 387	. . . . . . . . . . . . . . 15 $\/$ $\/$
272		elun 3559	. . . . . . . . . . . . . . 15 $\/$
273	271, 272	sylibr 212	. . . . . . . . . . . . . 14 $\/$
274	257, 273	nsyl 121	. . . . . . . . . . . . 13 $\/$
275		1cnd 9523	. . . . . . . . . . . . . . . . . 18 $/\$
276	17	adantr 463	. . . . . . . . . . . . . . . . . 18 $/\$
277	19	adantr 463	. . . . . . . . . . . . . . . . . . 19 $/\$
278		simpr 459	. . . . . . . . . . . . . . . . . . 19 $/\$
279	277, 278	sqr00d 13274	. . . . . . . . . . . . . . . . . 18 $/\$
280	275, 276, 279	subeq0d 9852	. . . . . . . . . . . . . . . . 17 $/\$
281	152, 280	syl5req 2436	. . . . . . . . . . . . . . . 16 $/\$
282	281	ex 432	. . . . . . . . . . . . . . 15
283		sqeqor 12184	. . . . . . . . . . . . . . . 16 $/\$ $\/$
284	16, 283	mpan2 669	. . . . . . . . . . . . . . 15 $\/$
285	282, 284	sylibd 214	. . . . . . . . . . . . . 14 $\/$
286	285	necon3bd 2594	. . . . . . . . . . . . 13 $\/$
287	12, 274, 286	sylc 60	. . . . . . . . . . . 12
288		2cnne0 10667	. . . . . . . . . . . . 13 $/\$
289		divcan5 10163	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
290	288, 289	mp3an3 1311	. . . . . . . . . . . 12 $/\$ $/\$
291	255, 117, 287, 290	syl12anc 1224	. . . . . . . . . . 11
292	225, 12, 226	sylancr 661	. . . . . . . . . . . . 13
293	292	negcld 9831	. . . . . . . . . . . 12
294		mulcl 9487	. . . . . . . . . . . . 13 $/\$
295	225, 117, 294	sylancr 661	. . . . . . . . . . . 12
296		mulne0 10108	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
297	288, 296	mpan 668	. . . . . . . . . . . . 13 $/\$
298	117, 287, 297	syl2anc 659	. . . . . . . . . . . 12
299	293, 295, 298	divrec2d 10241	. . . . . . . . . . 11
300	254, 291, 299	3eqtr3rd 2432	. . . . . . . . . 10
301	300	mpteq2ia 4449	. . . . . . . . 9
302	251, 301	syl6eq 2439	. . . . . . . 8
303	11, 77, 78, 114, 118, 120, 302	dvmptadd 22448	. . . . . . 7
304		mulcl 9487	. . . . . . . . . . . 12 $/\$
305	13, 20, 304	sylancr 661	. . . . . . . . . . 11
306	12, 305	syl 16	. . . . . . . . . 10
307	306, 255, 117, 287	divdird 10275	. . . . . . . . 9
308		ixi 10095	. . . . . . . . . . . . . . . 16
309	308	eqcomi 2395	. . . . . . . . . . . . . . 15
310	309	oveq1i 6206	. . . . . . . . . . . . . 14
311		mulm1 9916	. . . . . . . . . . . . . 14
312		mulass 9491	. . . . . . . . . . . . . . 15 $/\$ $/\$
313	13, 13, 312	mp3an12 1312	. . . . . . . . . . . . . 14
314	310, 311, 313	3eqtr3a 2447	. . . . . . . . . . . . 13
315	314	oveq1d 6211	. . . . . . . . . . . 12
316		negcl 9733	. . . . . . . . . . . . 13
317	305, 316	addcomd 9693	. . . . . . . . . . . 12
318	13	a1i 11	. . . . . . . . . . . . 13
319	318, 15, 20	adddid 9531	. . . . . . . . . . . 12
320	315, 317, 319	3eqtr4d 2433	. . . . . . . . . . 11
321	12, 320	syl 16	. . . . . . . . . 10
322	321	oveq1d 6211	. . . . . . . . 9
323	75, 117, 287	divcan4d 10243	. . . . . . . . . 10
324	323	oveq1d 6211	. . . . . . . . 9
325	307, 322, 324	3eqtr3rd 2432	. . . . . . . 8
326	325	mpteq2ia 4449	. . . . . . 7
327	303, 326	syl6eq 2439	. . . . . 6
328	245	dvlog 23119	. . . . . . 7 $\$ $\$
329		logf1o 23037	. . . . . . . . . 10 $\$
330		f1of 5724	. . . . . . . . . 10 $\$ $\$
331	329, 330	mp1i 12	. . . . . . . . 9 $\$
332		snssi 4088	. . . . . . . . . . 11
333	66, 332	ax-mp 5	. . . . . . . . . 10
334		sscon 3552	. . . . . . . . . 10 $\$ $\$
335	333, 334	mp1i 12	. . . . . . . . 9 $\$ $\$
336	331, 335	feqresmpt 5828	. . . . . . . 8 $\$ $\$
337	336	oveq2d 6212	. . . . . . 7 $\$ $\$
338	328, 337	syl5reqr 2438	. . . . . 6 $\$ $\$
339		fveq2 5774	. . . . . 6
340		oveq2 6204	. . . . . 6
341	11, 11, 58, 60, 72, 74, 327, 338, 339, 340	dvmptco 22460	. . . . 5
342	22, 24	reccld 10230	. . . . . . . 8
343		mulcl 9487	. . . . . . . . . 10 $/\$
344	13, 21, 343	sylancr 661	. . . . . . . . 9
345	12, 344	syl 16	. . . . . . . 8
346	342, 345, 117, 287	divassd 10272	. . . . . . 7
347	345, 22, 24	divrec2d 10241	. . . . . . . . 9
348	75, 22, 24	divcan4d 10243	. . . . . . . . 9
349	347, 348	eqtr3d 2425	. . . . . . . 8
350	349	oveq1d 6211	. . . . . . 7
351	346, 350	eqtr3d 2425	. . . . . 6
352	351	mpteq2ia 4449	. . . . 5
353	341, 352	syl6eq 2439	. . . 4
354		negicn 9734	. . . . 5
355	354	a1i 11	. . . 4
356	11, 26, 28, 353, 355	dvmptcmul 22452	. . 3
357	356	trud 1408	. 2
358	13, 13	mulneg1i 9920	. . . . . 6
359	308	negeqi 9726	. . . . . 6
360		negneg1e1 10560	. . . . . 6
361	358, 359, 360	3eqtri 2415	. . . . 5
362	361	oveq1i 6206	. . . 4
363		divass 10142	. . . . . 6 $/\$ $/\$ $/\$
364	354, 13, 363	mp3an12 1312	. . . . 5 $/\$
365	117, 287, 364	syl2anc 659	. . . 4
366	362, 365	syl5reqr 2438	. . 3
367	366	mpteq2ia 4449	. 2
368	9, 357, 367	3eqtri 2415	1 arcsin

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 366 $/\$ wa 367 $\/$ w3o 970 $/\$ w3a 971

wceq 1399

wtru 1400

wcel 1826

wne 2577

cvv 3034 $\$ cdif 3386

cun 3387

cin 3388

wss 3389

c0 3711

csn 3944

cpr 3946 class class class wbr 4367

cmpt 4425

crn 4914

cres 4915

wf 5492

wf1o 5495

cfv 5496 (class class class)co 6196

cc 9401

cr 9402

cc0 9403

c1 9404

ci 9405

caddc 9406

cmul 9408

cpnf 9536

cmnf 9537

cxr 9538

clt 9539

cle 9540

cmin 9718

cneg 9719

cdiv 10123

cn 10452

c2 10502

crp 11139

cioo 11450

cioc 11451

cico 11452

cexp 12069

cre 12932

csqrt 13068

cabs 13069 ↾_t crest 14828

ctopn 14829

ctg 14845 ℂ_fldccnfld 18533 TopOnctopon 19480

ccld 19602

cdv 22352

clog 23027 arcsincasin 23309

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1626 ax-4 1639 ax-5 1712 ax-6 1755 ax-7 1798 ax-8 1828 ax-9 1830 ax-10 1845 ax-11 1850 ax-12 1862 ax-13 2006 ax-ext 2360 ax-rep 4478 ax-sep 4488 ax-nul 4496 ax-pow 4543 ax-pr 4601 ax-un 6491 ax-inf2 7972 ax-cnex 9459 ax-resscn 9460 ax-1cn 9461 ax-icn 9462 ax-addcl 9463 ax-addrcl 9464 ax-mulcl 9465 ax-mulrcl 9466 ax-mulcom 9467 ax-addass 9468 ax-mulass 9469 ax-distr 9470 ax-i2m1 9471 ax-1ne0 9472 ax-1rid 9473 ax-rnegex 9474 ax-rrecex 9475 ax-cnre 9476 ax-pre-lttri 9477 ax-pre-lttrn 9478 ax-pre-ltadd 9479 ax-pre-mulgt0 9480 ax-pre-sup 9481 ax-addf 9482 ax-mulf 9483

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1402 df-fal 1405 df-ex 1621 df-nf 1625 df-sb 1748 df-eu 2222 df-mo 2223 df-clab 2368 df-cleq 2374 df-clel 2377 df-nfc 2532 df-ne 2579 df-nel 2580 df-ral 2737 df-rex 2738 df-reu 2739 df-rmo 2740 df-rab 2741 df-v 3036 df-sbc 3253 df-csb 3349 df-dif 3392 df-un 3394 df-in 3396 df-ss 3403 df-pss 3405 df-nul 3712 df-if 3858 df-pw 3929 df-sn 3945 df-pr 3947 df-tp 3949 df-op 3951 df-uni 4164 df-int 4200 df-iun 4245 df-iin 4246 df-br 4368 df-opab 4426 df-mpt 4427 df-tr 4461 df-eprel 4705 df-id 4709 df-po 4714 df-so 4715 df-fr 4752 df-se 4753 df-we 4754 df-ord 4795 df-on 4796 df-lim 4797 df-suc 4798 df-xp 4919 df-rel 4920 df-cnv 4921 df-co 4922 df-dm 4923 df-rn 4924 df-res 4925 df-ima 4926 df-iota 5460 df-fun 5498 df-fn 5499 df-f 5500 df-f1 5501 df-fo 5502 df-f1o 5503 df-fv 5504 df-isom 5505 df-riota 6158 df-ov 6199 df-oprab 6200 df-mpt2 6201 df-of 6439 df-om 6600 df-1st 6699 df-2nd 6700 df-supp 6818 df-recs 6960 df-rdg 6994 df-1o 7048 df-2o 7049 df-oadd 7052 df-er 7229 df-map 7340 df-pm 7341 df-ixp 7389 df-en 7436 df-dom 7437 df-sdom 7438 df-fin 7439 df-fsupp 7745 df-fi 7786 df-sup 7816 df-oi 7850 df-card 8233 df-cda 8461 df-pnf 9541 df-mnf 9542 df-xr 9543 df-ltxr 9544 df-le 9545 df-sub 9720 df-neg 9721 df-div 10124 df-nn 10453 df-2 10511 df-3 10512 df-4 10513 df-5 10514 df-6 10515 df-7 10516 df-8 10517 df-9 10518 df-10 10519 df-n0 10713 df-z 10782 df-dec 10896 df-uz 11002 df-q 11102 df-rp 11140 df-xneg 11239 df-xadd 11240 df-xmul 11241 df-ioo 11454 df-ioc 11455 df-ico 11456 df-icc 11457 df-fz 11594 df-fzo 11718 df-fl 11828 df-mod 11897 df-seq 12011 df-exp 12070 df-fac 12256 df-bc 12283 df-hash 12308 df-shft 12902 df-cj 12934 df-re 12935 df-im 12936 df-sqrt 13070 df-abs 13071 df-limsup 13296 df-clim 13313 df-rlim 13314 df-sum 13511 df-ef 13805 df-sin 13807 df-cos 13808 df-tan 13809 df-pi 13810 df-struct 14636 df-ndx 14637 df-slot 14638 df-base 14639 df-sets 14640 df-ress 14641 df-plusg 14715 df-mulr 14716 df-starv 14717 df-sca 14718 df-vsca 14719 df-ip 14720 df-tset 14721 df-ple 14722 df-ds 14724 df-unif 14725 df-hom 14726 df-cco 14727 df-rest 14830 df-topn 14831 df-0g 14849 df-gsum 14850 df-topgen 14851 df-pt 14852 df-prds 14855 df-xrs 14909 df-qtop 14914 df-imas 14915 df-xps 14917 df-mre 14993 df-mrc 14994 df-acs 14996 df-mgm 15989 df-sgrp 16028 df-mnd 16038 df-submnd 16084 df-mulg 16177 df-cntz 16472 df-cmn 16917 df-psmet 18524 df-xmet 18525 df-met 18526 df-bl 18527 df-mopn 18528 df-fbas 18529 df-fg 18530 df-cnfld 18534 df-top 19484 df-bases 19486 df-topon 19487 df-topsp 19488 df-cld 19605 df-ntr 19606 df-cls 19607 df-nei 19685 df-lp 19723 df-perf 19724 df-cn 19814 df-cnp 19815 df-haus 19902 df-cmp 19973 df-tx 20148 df-hmeo 20341 df-fil 20432 df-fm 20524 df-flim 20525 df-flf 20526 df-xms 20908 df-ms 20909 df-tms 20910 df-cncf 21467 df-limc 22355 df-dv 22356 df-log 23029 df-cxp 23030 df-asin 23312

This theorem is referenced by: dvacos 30270 dvreasin 30271

W3C validator