dvasin - Mathbox for Brendan Leahy

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

Theorem dvasin 32092

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 23870	. . . . 5 arcsin
2	1	reseq1i 5107	. . . 4 arcsin
3		dvasin.d	. . . . . 6 $\$
4		difss 3549	. . . . . 6 $\$
5	3, 4	eqsstri 3448	. . . . 5
6		resmpt 5160	. . . . 5
7	5, 6	ax-mp 5	. . . 4
8	2, 7	eqtri 2493	. . 3 arcsin
9	8	oveq2i 6319	. 2 arcsin
10		cnelprrecn 9650	. . . . 5
11	10	a1i 11	. . . 4
12	5	sseli 3414	. . . . . . 7
13		ax-icn 9616	. . . . . . . . 9
14		mulcl 9641	. . . . . . . . 9 $/\$
15	13, 14	mpan 684	. . . . . . . 8
16		ax-1cn 9615	. . . . . . . . . 10
17		sqcl 12375	. . . . . . . . . 10
18		subcl 9894	. . . . . . . . . 10 $/\$
19	16, 17, 18	sylancr 676	. . . . . . . . 9
20	19	sqrtcld 13576	. . . . . . . 8
21	15, 20	addcld 9680	. . . . . . 7
22	12, 21	syl 17	. . . . . 6
23		asinlem 23873	. . . . . . 7
24	12, 23	syl 17	. . . . . 6
25	22, 24	logcld 23599	. . . . 5
26	25	adantl 473	. . . 4 $/\$
27		ovex 6336	. . . . 5
28	27	a1i 11	. . . 4 $/\$
29		simpr 468	. . . . . . . . . . . . . . . 16 $/\$
30		asinlem3 23876	. . . . . . . . . . . . . . . . 17
31		rere 13262	. . . . . . . . . . . . . . . . . . 19
32	31	breq2d 4407	. . . . . . . . . . . . . . . . . 18
33	32	biimpac 494	. . . . . . . . . . . . . . . . 17 $/\$
34	30, 33	sylan 479	. . . . . . . . . . . . . . . 16 $/\$
35	23	adantr 472	. . . . . . . . . . . . . . . 16 $/\$
36	29, 34, 35	ne0gt0d 9789	. . . . . . . . . . . . . . 15 $/\$
37		0re 9661	. . . . . . . . . . . . . . . . 17
38		ltnle 9731	. . . . . . . . . . . . . . . . 17 $/\$
39	37, 38	mpan 684	. . . . . . . . . . . . . . . 16
40	39	adantl 473	. . . . . . . . . . . . . . 15 $/\$
41	36, 40	mpbid 215	. . . . . . . . . . . . . 14 $/\$
42	41	ex 441	. . . . . . . . . . . . 13
43	12, 42	syl 17	. . . . . . . . . . . 12
44		imor 419	. . . . . . . . . . . 12 $\/$
45	43, 44	sylib 201	. . . . . . . . . . 11 $\/$
46	45	orcomd 395	. . . . . . . . . 10 $\/$
47	46	olcd 400	. . . . . . . . 9 $\/$ $\/$
48		3ianor 1024	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $\/$
49		3orrot 1013	. . . . . . . . . . 11 $\/$ $\/$ $\/$ $\/$
50		3orass 1010	. . . . . . . . . . 11 $\/$ $\/$ $\/$ $\/$
51	48, 49, 50	3bitrri 280	. . . . . . . . . 10 $\/$ $\/$ $/\$ $/\$
52		mnfxr 11437	. . . . . . . . . . 11
53		elioc2 11722	. . . . . . . . . . 11 $/\$ $/\$ $/\$
54	52, 37, 53	mp2an 686	. . . . . . . . . 10 $/\$ $/\$
55	51, 54	xchbinxr 318	. . . . . . . . 9 $\/$ $\/$
56	47, 55	sylib 201	. . . . . . . 8
57	22, 56	eldifd 3401	. . . . . . 7 $\$
58	57	adantl 473	. . . . . 6 $/\$ $\$
59		ovex 6336	. . . . . . 7
60	59	a1i 11	. . . . . 6 $/\$
61		eldifi 3544	. . . . . . . 8 $\$
62		eldifn 3545	. . . . . . . . 9 $\$
63		0xr 9705	. . . . . . . . . . . 12
64		mnflt0 11450	. . . . . . . . . . . 12
65		ubioc1 11713	. . . . . . . . . . . 12 $/\$ $/\$
66	52, 63, 64, 65	mp3an 1390	. . . . . . . . . . 11
67		eleq1 2537	. . . . . . . . . . 11
68	66, 67	mpbiri 241	. . . . . . . . . 10
69	68	necon3bi 2669	. . . . . . . . 9
70	62, 69	syl 17	. . . . . . . 8 $\$
71	61, 70	logcld 23599	. . . . . . 7 $\$
72	71	adantl 473	. . . . . 6 $/\$ $\$
73		ovex 6336	. . . . . . 7
74	73	a1i 11	. . . . . 6 $/\$ $\$
75	13	a1i 11	. . . . . . . . . 10
76	75, 12	mulcld 9681	. . . . . . . . 9
77	76	adantl 473	. . . . . . . 8 $/\$
78	13	a1i 11	. . . . . . . 8 $/\$
79	12	adantl 473	. . . . . . . . . 10 $/\$
80		1cnd 9677	. . . . . . . . . 10 $/\$
81		simpr 468	. . . . . . . . . . 11 $/\$
82		1cnd 9677	. . . . . . . . . . 11 $/\$
83	11	dvmptid 22990	. . . . . . . . . . 11
84	5	a1i 11	. . . . . . . . . . 11
85		eqid 2471	. . . . . . . . . . . . . 14 ℂ_fld ℂ_fld
86	85	cnfldtopon 21881	. . . . . . . . . . . . 13 ℂ_fld TopOn
87	86	toponunii 20024	. . . . . . . . . . . . . 14 ℂ_fld
88	87	restid 15410	. . . . . . . . . . . . 13 ℂ_fld TopOn ℂ_fld ↾_t ℂ_fld
89	86, 88	ax-mp 5	. . . . . . . . . . . 12 ℂ_fld ↾_t ℂ_fld
90	89	eqcomi 2480	. . . . . . . . . . 11 ℂ_fld ℂ_fld ↾_t
91	85	recld2 21910	. . . . . . . . . . . . . . 15 ℂ_fld
92		neg1rr 10736	. . . . . . . . . . . . . . . . . 18
93		iocmnfcld 21867	. . . . . . . . . . . . . . . . . 18
94	92, 93	ax-mp 5	. . . . . . . . . . . . . . . . 17
95		1re 9660	. . . . . . . . . . . . . . . . . 18
96		icopnfcld 21866	. . . . . . . . . . . . . . . . . 18
97	95, 96	ax-mp 5	. . . . . . . . . . . . . . . . 17
98		uncld 20133	. . . . . . . . . . . . . . . . 17 $/\$
99	94, 97, 98	mp2an 686	. . . . . . . . . . . . . . . 16
100	85	tgioo2 21899	. . . . . . . . . . . . . . . . 17 ℂ_fld ↾_t
101	100	fveq2i 5882	. . . . . . . . . . . . . . . 16 ℂ_fld ↾_t
102	99, 101	eleqtri 2547	. . . . . . . . . . . . . . 15 ℂ_fld ↾_t
103		restcldr 20267	. . . . . . . . . . . . . . 15 ℂ_fld $/\$ ℂ_fld ↾_t ℂ_fld
104	91, 102, 103	mp2an 686	. . . . . . . . . . . . . 14 ℂ_fld
105	87	cldopn 20123	. . . . . . . . . . . . . 14 ℂ_fld $\$ ℂ_fld
106	104, 105	ax-mp 5	. . . . . . . . . . . . 13 $\$ ℂ_fld
107	3, 106	eqeltri 2545	. . . . . . . . . . . 12 ℂ_fld
108	107	a1i 11	. . . . . . . . . . 11 ℂ_fld
109	11, 81, 82, 83, 84, 90, 85, 108	dvmptres 22996	. . . . . . . . . 10
110	13	a1i 11	. . . . . . . . . 10
111	11, 79, 80, 109, 110	dvmptcmul 22997	. . . . . . . . 9
112	13	mulid1i 9663	. . . . . . . . . 10
113	112	mpteq2i 4479	. . . . . . . . 9
114	111, 113	syl6eq 2521	. . . . . . . 8
115	12	sqcld 12452	. . . . . . . . . . 11
116	16, 115, 18	sylancr 676	. . . . . . . . . 10
117	116	sqrtcld 13576	. . . . . . . . 9
118	117	adantl 473	. . . . . . . 8 $/\$
119		ovex 6336	. . . . . . . . 9
120	119	a1i 11	. . . . . . . 8 $/\$
121		elin 3608	. . . . . . . . . . . . . . 15 $/\$
122	3	asindmre 32091	. . . . . . . . . . . . . . . . 17
123	122	eqimssi 3472	. . . . . . . . . . . . . . . 16
124	123	sseli 3414	. . . . . . . . . . . . . . 15
125	121, 124	sylbir 218	. . . . . . . . . . . . . 14 $/\$
126		incom 3616	. . . . . . . . . . . . . . . 16
127		pnfxr 11435	. . . . . . . . . . . . . . . . 17
128		df-ioc 11665	. . . . . . . . . . . . . . . . . 18 $/\$
129		df-ioo 11664	. . . . . . . . . . . . . . . . . 18 $/\$
130		xrltnle 9719	. . . . . . . . . . . . . . . . . 18 $/\$
131	128, 129, 130	ixxdisj 11675	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
132	52, 63, 127, 131	mp3an 1390	. . . . . . . . . . . . . . . 16
133	126, 132	eqtri 2493	. . . . . . . . . . . . . . 15
134		elioore 11691	. . . . . . . . . . . . . . . . . . 19
135	134	resqcld 12480	. . . . . . . . . . . . . . . . . 18
136		resubcl 9958	. . . . . . . . . . . . . . . . . 18 $/\$
137	95, 135, 136	sylancr 676	. . . . . . . . . . . . . . . . 17
138	92	rexri 9711	. . . . . . . . . . . . . . . . . . 19
139	95	rexri 9711	. . . . . . . . . . . . . . . . . . 19
140		elioo2 11702	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
141	138, 139, 140	mp2an 686	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
142		recn 9647	. . . . . . . . . . . . . . . . . . . . . . 23
143	142	abscld 13575	. . . . . . . . . . . . . . . . . . . . . 22
144	142	absge0d 13583	. . . . . . . . . . . . . . . . . . . . . 22
145		0le1 10158	. . . . . . . . . . . . . . . . . . . . . . 23
146		lt2sq 12386	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
147	95, 145, 146	mpanr12 699	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
148	143, 144, 147	syl2anc 673	. . . . . . . . . . . . . . . . . . . . 21
149		abslt 13454	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
150	95, 149	mpan2 685	. . . . . . . . . . . . . . . . . . . . 21 $/\$
151		absresq 13442	. . . . . . . . . . . . . . . . . . . . . . 23
152		sq1 12407	. . . . . . . . . . . . . . . . . . . . . . . 24
153	152	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
154	151, 153	breq12d 4408	. . . . . . . . . . . . . . . . . . . . . 22
155		resqcl 12380	. . . . . . . . . . . . . . . . . . . . . . 23
156		posdif 10128	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
157	155, 95, 156	sylancl 675	. . . . . . . . . . . . . . . . . . . . . 22
158	154, 157	bitrd 261	. . . . . . . . . . . . . . . . . . . . 21
159	148, 150, 158	3bitr3d 291	. . . . . . . . . . . . . . . . . . . 20 $/\$
160	159	biimpd 212	. . . . . . . . . . . . . . . . . . 19 $/\$
161	160	3impib 1229	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
162	141, 161	sylbi 200	. . . . . . . . . . . . . . . . 17
163	137, 162	elrpd 11361	. . . . . . . . . . . . . . . 16
164		ioorp 11737	. . . . . . . . . . . . . . . 16
165	163, 164	syl6eleqr 2560	. . . . . . . . . . . . . . 15
166		disjel 3815	. . . . . . . . . . . . . . 15 $/\$
167	133, 165, 166	sylancr 676	. . . . . . . . . . . . . 14
168	125, 167	syl 17	. . . . . . . . . . . . 13 $/\$
169		elioc2 11722	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
170	52, 37, 169	mp2an 686	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
171	170	biimpi 199	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
172	171	simp1d 1042	. . . . . . . . . . . . . . . . . . . . 21
173		resubcl 9958	. . . . . . . . . . . . . . . . . . . . 21 $/\$
174	95, 172, 173	sylancr 676	. . . . . . . . . . . . . . . . . . . 20
175		nncan 9923	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
176	16, 175	mpan 684	. . . . . . . . . . . . . . . . . . . . . 22
177	176	eleq1d 2533	. . . . . . . . . . . . . . . . . . . . 21
178	177	biimpa 492	. . . . . . . . . . . . . . . . . . . 20 $/\$
179	174, 178	sylan2 482	. . . . . . . . . . . . . . . . . . 19 $/\$
180	172	adantl 473	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
181	171	simp3d 1044	. . . . . . . . . . . . . . . . . . . . . . 23
182	181	adantl 473	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
183		letr 9745	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
184	37, 95, 183	mp3an23 1382	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
185	145, 184	mpan2i 691	. . . . . . . . . . . . . . . . . . . . . 22
186	180, 182, 185	sylc 61	. . . . . . . . . . . . . . . . . . . . 21 $/\$
187		subge0 10148	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
188	95, 180, 187	sylancr 676	. . . . . . . . . . . . . . . . . . . . 21 $/\$
189	186, 188	mpbird 240	. . . . . . . . . . . . . . . . . . . 20 $/\$
190	176	adantr 472	. . . . . . . . . . . . . . . . . . . 20 $/\$
191	189, 190	breqtrd 4420	. . . . . . . . . . . . . . . . . . 19 $/\$
192	179, 191	resqrtcld 13556	. . . . . . . . . . . . . . . . . 18 $/\$
193	17, 192	sylan 479	. . . . . . . . . . . . . . . . 17 $/\$
194		eleq1 2537	. . . . . . . . . . . . . . . . 17
195	193, 194	syl5ibrcom 230	. . . . . . . . . . . . . . . 16 $/\$
196	193	renegcld 10067	. . . . . . . . . . . . . . . . 17 $/\$
197		eleq1 2537	. . . . . . . . . . . . . . . . 17
198	196, 197	syl5ibrcom 230	. . . . . . . . . . . . . . . 16 $/\$
199		eqid 2471	. . . . . . . . . . . . . . . . . 18
200		eqsqrtor 13506	. . . . . . . . . . . . . . . . . . 19 $/\$ $\/$
201	17, 200	mpdan 681	. . . . . . . . . . . . . . . . . 18 $\/$
202	199, 201	mpbii 216	. . . . . . . . . . . . . . . . 17 $\/$
203	202	adantr 472	. . . . . . . . . . . . . . . 16 $/\$ $\/$
204	195, 198, 203	mpjaod 388	. . . . . . . . . . . . . . 15 $/\$
205	204	stoic1a 1663	. . . . . . . . . . . . . 14 $/\$
206	12, 205	sylan 479	. . . . . . . . . . . . 13 $/\$
207	168, 206	pm2.61dan 808	. . . . . . . . . . . 12
208	116, 207	eldifd 3401	. . . . . . . . . . 11 $\$
209	208	adantl 473	. . . . . . . . . 10 $/\$ $\$
210		2cnd 10704	. . . . . . . . . . . . . 14
211		id 22	. . . . . . . . . . . . . 14
212	210, 211	mulcld 9681	. . . . . . . . . . . . 13
213	212	negcld 9992	. . . . . . . . . . . 12
214	213	adantl 473	. . . . . . . . . . 11 $/\$
215	12, 214	sylan2 482	. . . . . . . . . 10 $/\$
216	61	sqrtcld 13576	. . . . . . . . . . 11 $\$
217	216	adantl 473	. . . . . . . . . 10 $/\$ $\$
218		ovex 6336	. . . . . . . . . . 11
219	218	a1i 11	. . . . . . . . . 10 $/\$ $\$
220	19	adantl 473	. . . . . . . . . . 11 $/\$
221	37	a1i 11	. . . . . . . . . . . . 13 $/\$
222		1cnd 9677	. . . . . . . . . . . . . 14
223	11, 222	dvmptc 22991	. . . . . . . . . . . . 13
224	17	adantl 473	. . . . . . . . . . . . 13 $/\$
225		2cn 10702	. . . . . . . . . . . . . . 15
226		mulcl 9641	. . . . . . . . . . . . . . 15 $/\$
227	225, 226	mpan 684	. . . . . . . . . . . . . 14
228	227	adantl 473	. . . . . . . . . . . . 13 $/\$
229		2nn 10790	. . . . . . . . . . . . . . . 16
230		dvexp 22986	. . . . . . . . . . . . . . . 16
231	229, 230	ax-mp 5	. . . . . . . . . . . . . . 15
232		2m1e1 10746	. . . . . . . . . . . . . . . . . . 19
233	232	oveq2i 6319	. . . . . . . . . . . . . . . . . 18
234		exp1 12316	. . . . . . . . . . . . . . . . . 18
235	233, 234	syl5eq 2517	. . . . . . . . . . . . . . . . 17
236	235	oveq2d 6324	. . . . . . . . . . . . . . . 16
237	236	mpteq2ia 4478	. . . . . . . . . . . . . . 15
238	231, 237	eqtri 2493	. . . . . . . . . . . . . 14
239	238	a1i 11	. . . . . . . . . . . . 13
240	11, 82, 221, 223, 224, 228, 239	dvmptsub 23000	. . . . . . . . . . . 12
241		df-neg 9883	. . . . . . . . . . . . 13
242	241	mpteq2i 4479	. . . . . . . . . . . 12
243	240, 242	syl6eqr 2523	. . . . . . . . . . 11
244	11, 220, 214, 243, 84, 90, 85, 108	dvmptres 22996	. . . . . . . . . 10
245		eqid 2471	. . . . . . . . . . . 12 $\$ $\$
246	245	dvcnsqrt 23763	. . . . . . . . . . 11 $\$ $\$
247	246	a1i 11	. . . . . . . . . 10 $\$ $\$
248		fveq2 5879	. . . . . . . . . 10
249	248	oveq2d 6324	. . . . . . . . . . 11
250	249	oveq2d 6324	. . . . . . . . . 10
251	11, 11, 209, 215, 217, 219, 244, 247, 248, 250	dvmptco 23005	. . . . . . . . 9
252		mulneg2 10077	. . . . . . . . . . . . 13 $/\$
253	225, 12, 252	sylancr 676	. . . . . . . . . . . 12
254	253	oveq1d 6323	. . . . . . . . . . 11
255	12	negcld 9992	. . . . . . . . . . . 12
256		eldifn 3545	. . . . . . . . . . . . . . 15 $\$
257	256, 3	eleq2s 2567	. . . . . . . . . . . . . 14
258		id 22	. . . . . . . . . . . . . . . . . 18
259		mnflt 11448	. . . . . . . . . . . . . . . . . . . 20
260	92, 259	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
261		ubioc1 11713	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
262	52, 138, 260, 261	mp3an 1390	. . . . . . . . . . . . . . . . . 18
263	258, 262	syl6eqel 2557	. . . . . . . . . . . . . . . . 17
264		id 22	. . . . . . . . . . . . . . . . . 18
265		ltpnf 11445	. . . . . . . . . . . . . . . . . . . 20
266	95, 265	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
267		lbico1 11714	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
268	139, 127, 266, 267	mp3an 1390	. . . . . . . . . . . . . . . . . 18
269	264, 268	syl6eqel 2557	. . . . . . . . . . . . . . . . 17
270	263, 269	orim12i 525	. . . . . . . . . . . . . . . 16 $\/$ $\/$
271	270	orcoms 396	. . . . . . . . . . . . . . 15 $\/$ $\/$
272		elun 3565	. . . . . . . . . . . . . . 15 $\/$
273	271, 272	sylibr 217	. . . . . . . . . . . . . 14 $\/$
274	257, 273	nsyl 125	. . . . . . . . . . . . 13 $\/$
275		1cnd 9677	. . . . . . . . . . . . . . . . . 18 $/\$
276	17	adantr 472	. . . . . . . . . . . . . . . . . 18 $/\$
277	19	adantr 472	. . . . . . . . . . . . . . . . . . 19 $/\$
278		simpr 468	. . . . . . . . . . . . . . . . . . 19 $/\$
279	277, 278	sqr00d 13580	. . . . . . . . . . . . . . . . . 18 $/\$
280	275, 276, 279	subeq0d 10013	. . . . . . . . . . . . . . . . 17 $/\$
281	152, 280	syl5req 2518	. . . . . . . . . . . . . . . 16 $/\$
282	281	ex 441	. . . . . . . . . . . . . . 15
283		sqeqor 12426	. . . . . . . . . . . . . . . 16 $/\$ $\/$
284	16, 283	mpan2 685	. . . . . . . . . . . . . . 15 $\/$
285	282, 284	sylibd 222	. . . . . . . . . . . . . 14 $\/$
286	285	necon3bd 2657	. . . . . . . . . . . . 13 $\/$
287	12, 274, 286	sylc 61	. . . . . . . . . . . 12
288		2cnne0 10847	. . . . . . . . . . . . 13 $/\$
289		divcan5 10331	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
290	288, 289	mp3an3 1379	. . . . . . . . . . . 12 $/\$ $/\$
291	255, 117, 287, 290	syl12anc 1290	. . . . . . . . . . 11
292	225, 12, 226	sylancr 676	. . . . . . . . . . . . 13
293	292	negcld 9992	. . . . . . . . . . . 12
294		mulcl 9641	. . . . . . . . . . . . 13 $/\$
295	225, 117, 294	sylancr 676	. . . . . . . . . . . 12
296		mulne0 10276	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
297	288, 296	mpan 684	. . . . . . . . . . . . 13 $/\$
298	117, 287, 297	syl2anc 673	. . . . . . . . . . . 12
299	293, 295, 298	divrec2d 10409	. . . . . . . . . . 11
300	254, 291, 299	3eqtr3rd 2514	. . . . . . . . . 10
301	300	mpteq2ia 4478	. . . . . . . . 9
302	251, 301	syl6eq 2521	. . . . . . . 8
303	11, 77, 78, 114, 118, 120, 302	dvmptadd 22993	. . . . . . 7
304		mulcl 9641	. . . . . . . . . . . 12 $/\$
305	13, 20, 304	sylancr 676	. . . . . . . . . . 11
306	12, 305	syl 17	. . . . . . . . . 10
307	306, 255, 117, 287	divdird 10443	. . . . . . . . 9
308		ixi 10263	. . . . . . . . . . . . . . . 16
309	308	eqcomi 2480	. . . . . . . . . . . . . . 15
310	309	oveq1i 6318	. . . . . . . . . . . . . 14
311		mulm1 10081	. . . . . . . . . . . . . 14
312		mulass 9645	. . . . . . . . . . . . . . 15 $/\$ $/\$
313	13, 13, 312	mp3an12 1380	. . . . . . . . . . . . . 14
314	310, 311, 313	3eqtr3a 2529	. . . . . . . . . . . . 13
315	314	oveq1d 6323	. . . . . . . . . . . 12
316		negcl 9895	. . . . . . . . . . . . 13
317	305, 316	addcomd 9853	. . . . . . . . . . . 12
318	13	a1i 11	. . . . . . . . . . . . 13
319	318, 15, 20	adddid 9685	. . . . . . . . . . . 12
320	315, 317, 319	3eqtr4d 2515	. . . . . . . . . . 11
321	12, 320	syl 17	. . . . . . . . . 10
322	321	oveq1d 6323	. . . . . . . . 9
323	75, 117, 287	divcan4d 10411	. . . . . . . . . 10
324	323	oveq1d 6323	. . . . . . . . 9
325	307, 322, 324	3eqtr3rd 2514	. . . . . . . 8
326	325	mpteq2ia 4478	. . . . . . 7
327	303, 326	syl6eq 2521	. . . . . 6
328	245	dvlog 23675	. . . . . . 7 $\$ $\$
329		logf1o 23593	. . . . . . . . . 10 $\$
330		f1of 5828	. . . . . . . . . 10 $\$ $\$
331	329, 330	mp1i 13	. . . . . . . . 9 $\$
332		snssi 4107	. . . . . . . . . . 11
333	66, 332	ax-mp 5	. . . . . . . . . 10
334		sscon 3556	. . . . . . . . . 10 $\$ $\$
335	333, 334	mp1i 13	. . . . . . . . 9 $\$ $\$
336	331, 335	feqresmpt 5933	. . . . . . . 8 $\$ $\$
337	336	oveq2d 6324	. . . . . . 7 $\$ $\$
338	328, 337	syl5reqr 2520	. . . . . 6 $\$ $\$
339		fveq2 5879	. . . . . 6
340		oveq2 6316	. . . . . 6
341	11, 11, 58, 60, 72, 74, 327, 338, 339, 340	dvmptco 23005	. . . . 5
342	22, 24	reccld 10398	. . . . . . . 8
343		mulcl 9641	. . . . . . . . . 10 $/\$
344	13, 21, 343	sylancr 676	. . . . . . . . 9
345	12, 344	syl 17	. . . . . . . 8
346	342, 345, 117, 287	divassd 10440	. . . . . . 7
347	345, 22, 24	divrec2d 10409	. . . . . . . . 9
348	75, 22, 24	divcan4d 10411	. . . . . . . . 9
349	347, 348	eqtr3d 2507	. . . . . . . 8
350	349	oveq1d 6323	. . . . . . 7
351	346, 350	eqtr3d 2507	. . . . . 6
352	351	mpteq2ia 4478	. . . . 5
353	341, 352	syl6eq 2521	. . . 4
354		negicn 9896	. . . . 5
355	354	a1i 11	. . . 4
356	11, 26, 28, 353, 355	dvmptcmul 22997	. . 3
357	356	trud 1461	. 2
358	13, 13	mulneg1i 10085	. . . . . 6
359	308	negeqi 9888	. . . . . 6
360		negneg1e1 10739	. . . . . 6
361	358, 359, 360	3eqtri 2497	. . . . 5
362	361	oveq1i 6318	. . . 4
363		divass 10310	. . . . . 6 $/\$ $/\$ $/\$
364	354, 13, 363	mp3an12 1380	. . . . 5 $/\$
365	117, 287, 364	syl2anc 673	. . . 4
366	362, 365	syl5reqr 2520	. . 3
367	366	mpteq2ia 4478	. 2
368	9, 357, 367	3eqtri 2497	1 arcsin

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $\/$ wo 375 $/\$ wa 376 $\/$ w3o 1006 $/\$ w3a 1007

wceq 1452

wtru 1453

wcel 1904

wne 2641

cvv 3031 $\$ cdif 3387

cun 3388

cin 3389

wss 3390

c0 3722

csn 3959

cpr 3961 class class class wbr 4395

cmpt 4454

crn 4840

cres 4841

wf 5585

wf1o 5588

cfv 5589 (class class class)co 6308

cc 9555

cr 9556

cc0 9557

c1 9558

ci 9559

caddc 9560

cmul 9562

cpnf 9690

cmnf 9691

cxr 9692

clt 9693

cle 9694

cmin 9880

cneg 9881

cdiv 10291

cn 10631

c2 10681

crp 11325

cioo 11660

cioc 11661

cico 11662

cexp 12310

cre 13237

csqrt 13373

cabs 13374 ↾_t crest 15397

ctopn 15398

ctg 15414 ℂ_fldccnfld 19047 TopOnctopon 19995

ccld 20108

cdv 22897

clog 23583 arcsincasin 23867

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635 ax-addf 9636 ax-mulf 9637

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-iin 4272 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-of 6550 df-om 6712 df-1st 6812 df-2nd 6813 df-supp 6934 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-er 7381 df-map 7492 df-pm 7493 df-ixp 7541 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-fsupp 7902 df-fi 7943 df-sup 7974 df-inf 7975 df-oi 8043 df-card 8391 df-cda 8616 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-4 10692 df-5 10693 df-6 10694 df-7 10695 df-8 10696 df-9 10697 df-10 10698 df-n0 10894 df-z 10962 df-dec 11075 df-uz 11183 df-q 11288 df-rp 11326 df-xneg 11432 df-xadd 11433 df-xmul 11434 df-ioo 11664 df-ioc 11665 df-ico 11666 df-icc 11667 df-fz 11811 df-fzo 11943 df-fl 12061 df-mod 12130 df-seq 12252 df-exp 12311 df-fac 12498 df-bc 12526 df-hash 12554 df-shft 13207 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-limsup 13603 df-clim 13629 df-rlim 13630 df-sum 13830 df-ef 14198 df-sin 14200 df-cos 14201 df-tan 14202 df-pi 14203 df-struct 15201 df-ndx 15202 df-slot 15203 df-base 15204 df-sets 15205 df-ress 15206 df-plusg 15281 df-mulr 15282 df-starv 15283 df-sca 15284 df-vsca 15285 df-ip 15286 df-tset 15287 df-ple 15288 df-ds 15290 df-unif 15291 df-hom 15292 df-cco 15293 df-rest 15399 df-topn 15400 df-0g 15418 df-gsum 15419 df-topgen 15420 df-pt 15421 df-prds 15424 df-xrs 15478 df-qtop 15484 df-imas 15485 df-xps 15488 df-mre 15570 df-mrc 15571 df-acs 15573 df-mgm 16566 df-sgrp 16605 df-mnd 16615 df-submnd 16661 df-mulg 16754 df-cntz 17049 df-cmn 17510 df-psmet 19039 df-xmet 19040 df-met 19041 df-bl 19042 df-mopn 19043 df-fbas 19044 df-fg 19045 df-cnfld 19048 df-top 19998 df-bases 19999 df-topon 20000 df-topsp 20001 df-cld 20111 df-ntr 20112 df-cls 20113 df-nei 20191 df-lp 20229 df-perf 20230 df-cn 20320 df-cnp 20321 df-haus 20408 df-cmp 20479 df-tx 20654 df-hmeo 20847 df-fil 20939 df-fm 21031 df-flim 21032 df-flf 21033 df-xms 21413 df-ms 21414 df-tms 21415 df-cncf 21988 df-limc 22900 df-dv 22901 df-log 23585 df-cxp 23586 df-asin 23870

This theorem is referenced by: dvacos 32093 dvreasin 32094

W3C validator