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 30078

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 23068	. . . . 5 arcsin
2	1	reseq1i 5259	. . . 4 arcsin
3		dvasin.d	. . . . . 6 $\$
4		difss 3616	. . . . . 6 $\$
5	3, 4	eqsstri 3519	. . . . 5
6		resmpt 5313	. . . . 5
7	5, 6	ax-mp 5	. . . 4
8	2, 7	eqtri 2472	. . 3 arcsin
9	8	oveq2i 6292	. 2 arcsin
10		cnelprrecn 9588	. . . . 5
11	10	a1i 11	. . . 4
12	5	sseli 3485	. . . . . . 7
13		ax-icn 9554	. . . . . . . . 9
14		mulcl 9579	. . . . . . . . 9 $/\$
15	13, 14	mpan 670	. . . . . . . 8
16		ax-1cn 9553	. . . . . . . . . 10
17		sqcl 12209	. . . . . . . . . 10
18		subcl 9824	. . . . . . . . . 10 $/\$
19	16, 17, 18	sylancr 663	. . . . . . . . 9
20	19	sqrtcld 13247	. . . . . . . 8
21	15, 20	addcld 9618	. . . . . . 7
22	12, 21	syl 16	. . . . . 6
23		asinlem 23071	. . . . . . 7
24	12, 23	syl 16	. . . . . 6
25	22, 24	logcld 22830	. . . . 5
26	25	adantl 466	. . . 4 $/\$
27		ovex 6309	. . . . 5
28	27	a1i 11	. . . 4 $/\$
29		simpr 461	. . . . . . . . . . . . . . . 16 $/\$
30		asinlem3 23074	. . . . . . . . . . . . . . . . 17
31		rere 12934	. . . . . . . . . . . . . . . . . . 19
32	31	breq2d 4449	. . . . . . . . . . . . . . . . . 18
33	32	biimpac 486	. . . . . . . . . . . . . . . . 17 $/\$
34	30, 33	sylan 471	. . . . . . . . . . . . . . . 16 $/\$
35	23	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
36	29, 34, 35	ne0gt0d 9725	. . . . . . . . . . . . . . 15 $/\$
37		0re 9599	. . . . . . . . . . . . . . . . 17
38		ltnle 9667	. . . . . . . . . . . . . . . . 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 991	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $\/$
49		3orrot 980	. . . . . . . . . . 11 $\/$ $\/$ $\/$ $\/$
50		3orass 977	. . . . . . . . . . 11 $\/$ $\/$ $\/$ $\/$
51	48, 49, 50	3bitrri 272	. . . . . . . . . 10 $\/$ $\/$ $/\$ $/\$
52		mnfxr 11332	. . . . . . . . . . 11
53		elioc2 11596	. . . . . . . . . . 11 $/\$ $/\$ $/\$
54	52, 37, 53	mp2an 672	. . . . . . . . . 10 $/\$ $/\$
55	51, 54	xchbinxr 311	. . . . . . . . 9 $\/$ $\/$
56	47, 55	sylib 196	. . . . . . . 8
57	22, 56	eldifd 3472	. . . . . . 7 $\$
58	57	adantl 466	. . . . . 6 $/\$ $\$
59		ovex 6309	. . . . . . 7
60	59	a1i 11	. . . . . 6 $/\$
61		eldifi 3611	. . . . . . . 8 $\$
62		eldifn 3612	. . . . . . . . 9 $\$
63		0xr 9643	. . . . . . . . . . . 12
64		mnflt0 11343	. . . . . . . . . . . 12
65		ubioc1 11587	. . . . . . . . . . . 12 $/\$ $/\$
66	52, 63, 64, 65	mp3an 1325	. . . . . . . . . . 11
67		eleq1 2515	. . . . . . . . . . 11
68	66, 67	mpbiri 233	. . . . . . . . . 10
69	68	necon3bi 2672	. . . . . . . . 9
70	62, 69	syl 16	. . . . . . . 8 $\$
71	61, 70	logcld 22830	. . . . . . 7 $\$
72	71	adantl 466	. . . . . 6 $/\$ $\$
73		ovex 6309	. . . . . . 7
74	73	a1i 11	. . . . . 6 $/\$ $\$
75	13	a1i 11	. . . . . . . . . 10
76	75, 12	mulcld 9619	. . . . . . . . 9
77	76	adantl 466	. . . . . . . 8 $/\$
78	13	a1i 11	. . . . . . . 8 $/\$
79	12	adantl 466	. . . . . . . . . 10 $/\$
80		1cnd 9615	. . . . . . . . . 10 $/\$
81		simpr 461	. . . . . . . . . . 11 $/\$
82		1cnd 9615	. . . . . . . . . . 11 $/\$
83	11	dvmptid 22233	. . . . . . . . . . 11
84	5	a1i 11	. . . . . . . . . . 11
85		eqid 2443	. . . . . . . . . . . . . 14 ℂ_fld ℂ_fld
86	85	cnfldtopon 21163	. . . . . . . . . . . . 13 ℂ_fld TopOn
87	86	toponunii 19306	. . . . . . . . . . . . . 14 ℂ_fld
88	87	restid 14708	. . . . . . . . . . . . 13 ℂ_fld TopOn ℂ_fld ↾_t ℂ_fld
89	86, 88	ax-mp 5	. . . . . . . . . . . 12 ℂ_fld ↾_t ℂ_fld
90	89	eqcomi 2456	. . . . . . . . . . 11 ℂ_fld ℂ_fld ↾_t
91	85	recld2 21192	. . . . . . . . . . . . . . 15 ℂ_fld
92		neg1rr 10646	. . . . . . . . . . . . . . . . . 18
93		iocmnfcld 21149	. . . . . . . . . . . . . . . . . 18
94	92, 93	ax-mp 5	. . . . . . . . . . . . . . . . 17
95		1re 9598	. . . . . . . . . . . . . . . . . 18
96		icopnfcld 21148	. . . . . . . . . . . . . . . . . 18
97	95, 96	ax-mp 5	. . . . . . . . . . . . . . . . 17
98		uncld 19415	. . . . . . . . . . . . . . . . 17 $/\$
99	94, 97, 98	mp2an 672	. . . . . . . . . . . . . . . 16
100	85	tgioo2 21181	. . . . . . . . . . . . . . . . 17 ℂ_fld ↾_t
101	100	fveq2i 5859	. . . . . . . . . . . . . . . 16 ℂ_fld ↾_t
102	99, 101	eleqtri 2529	. . . . . . . . . . . . . . 15 ℂ_fld ↾_t
103		restcldr 19548	. . . . . . . . . . . . . . 15 ℂ_fld $/\$ ℂ_fld ↾_t ℂ_fld
104	91, 102, 103	mp2an 672	. . . . . . . . . . . . . 14 ℂ_fld
105	87	cldopn 19405	. . . . . . . . . . . . . 14 ℂ_fld $\$ ℂ_fld
106	104, 105	ax-mp 5	. . . . . . . . . . . . 13 $\$ ℂ_fld
107	3, 106	eqeltri 2527	. . . . . . . . . . . 12 ℂ_fld
108	107	a1i 11	. . . . . . . . . . 11 ℂ_fld
109	11, 81, 82, 83, 84, 90, 85, 108	dvmptres 22239	. . . . . . . . . 10
110	13	a1i 11	. . . . . . . . . 10
111	11, 79, 80, 109, 110	dvmptcmul 22240	. . . . . . . . 9
112	13	mulid1i 9601	. . . . . . . . . 10
113	112	mpteq2i 4520	. . . . . . . . 9
114	111, 113	syl6eq 2500	. . . . . . . 8
115	12	sqcld 12287	. . . . . . . . . . 11
116	16, 115, 18	sylancr 663	. . . . . . . . . 10
117	116	sqrtcld 13247	. . . . . . . . 9
118	117	adantl 466	. . . . . . . 8 $/\$
119		ovex 6309	. . . . . . . . 9
120	119	a1i 11	. . . . . . . 8 $/\$
121		elin 3672	. . . . . . . . . . . . . . 15 $/\$
122	3	asindmre 30077	. . . . . . . . . . . . . . . . 17
123	122	eqimssi 3543	. . . . . . . . . . . . . . . 16
124	123	sseli 3485	. . . . . . . . . . . . . . 15
125	121, 124	sylbir 213	. . . . . . . . . . . . . 14 $/\$
126		incom 3676	. . . . . . . . . . . . . . . 16
127		pnfxr 11330	. . . . . . . . . . . . . . . . 17
128		df-ioc 11543	. . . . . . . . . . . . . . . . . 18 $/\$
129		df-ioo 11542	. . . . . . . . . . . . . . . . . 18 $/\$
130		xrltnle 9656	. . . . . . . . . . . . . . . . . 18 $/\$
131	128, 129, 130	ixxdisj 11553	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
132	52, 63, 127, 131	mp3an 1325	. . . . . . . . . . . . . . . 16
133	126, 132	eqtri 2472	. . . . . . . . . . . . . . 15
134		elioore 11568	. . . . . . . . . . . . . . . . . . 19
135	134	resqcld 12315	. . . . . . . . . . . . . . . . . 18
136		resubcl 9888	. . . . . . . . . . . . . . . . . 18 $/\$
137	95, 135, 136	sylancr 663	. . . . . . . . . . . . . . . . 17
138	92	rexri 9649	. . . . . . . . . . . . . . . . . . 19
139	95	rexri 9649	. . . . . . . . . . . . . . . . . . 19
140		elioo2 11579	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
141	138, 139, 140	mp2an 672	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
142		recn 9585	. . . . . . . . . . . . . . . . . . . . . . 23
143	142	abscld 13246	. . . . . . . . . . . . . . . . . . . . . 22
144	142	absge0d 13254	. . . . . . . . . . . . . . . . . . . . . 22
145		0le1 10082	. . . . . . . . . . . . . . . . . . . . . . 23
146		lt2sq 12220	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
147	95, 145, 146	mpanr12 685	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
148	143, 144, 147	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21
149		abslt 13126	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
150	95, 149	mpan2 671	. . . . . . . . . . . . . . . . . . . . 21 $/\$
151		absresq 13114	. . . . . . . . . . . . . . . . . . . . . . 23
152		sq1 12241	. . . . . . . . . . . . . . . . . . . . . . . 24
153	152	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
154	151, 153	breq12d 4450	. . . . . . . . . . . . . . . . . . . . . 22
155		resqcl 12214	. . . . . . . . . . . . . . . . . . . . . . 23
156		posdif 10051	. . . . . . . . . . . . . . . . . . . . . . 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 1195	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
162	141, 161	sylbi 195	. . . . . . . . . . . . . . . . 17
163	137, 162	elrpd 11263	. . . . . . . . . . . . . . . 16
164		ioorp 11611	. . . . . . . . . . . . . . . 16
165	163, 164	syl6eleqr 2542	. . . . . . . . . . . . . . 15
166		disjel 3859	. . . . . . . . . . . . . . 15 $/\$
167	133, 165, 166	sylancr 663	. . . . . . . . . . . . . 14
168	125, 167	syl 16	. . . . . . . . . . . . 13 $/\$
169		elioc2 11596	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
170	52, 37, 169	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
171	170	biimpi 194	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
172	171	simp1d 1009	. . . . . . . . . . . . . . . . . . . . 21
173		resubcl 9888	. . . . . . . . . . . . . . . . . . . . 21 $/\$
174	95, 172, 173	sylancr 663	. . . . . . . . . . . . . . . . . . . 20
175		nncan 9853	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
176	16, 175	mpan 670	. . . . . . . . . . . . . . . . . . . . . 22
177	176	eleq1d 2512	. . . . . . . . . . . . . . . . . . . . 21
178	177	biimpa 484	. . . . . . . . . . . . . . . . . . . 20 $/\$
179	174, 178	sylan2 474	. . . . . . . . . . . . . . . . . . 19 $/\$
180	172	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
181	171	simp3d 1011	. . . . . . . . . . . . . . . . . . . . . . 23
182	181	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
183		letr 9681	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
184	37, 95, 183	mp3an23 1317	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
185	145, 184	mpan2i 677	. . . . . . . . . . . . . . . . . . . . . 22
186	180, 182, 185	sylc 60	. . . . . . . . . . . . . . . . . . . . 21 $/\$
187		subge0 10071	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
188	95, 180, 187	sylancr 663	. . . . . . . . . . . . . . . . . . . . 21 $/\$
189	186, 188	mpbird 232	. . . . . . . . . . . . . . . . . . . 20 $/\$
190	176	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$
191	189, 190	breqtrd 4461	. . . . . . . . . . . . . . . . . . 19 $/\$
192	179, 191	resqrtcld 13228	. . . . . . . . . . . . . . . . . 18 $/\$
193	17, 192	sylan 471	. . . . . . . . . . . . . . . . 17 $/\$
194		eleq1 2515	. . . . . . . . . . . . . . . . 17
195	193, 194	syl5ibrcom 222	. . . . . . . . . . . . . . . 16 $/\$
196	193	renegcld 9992	. . . . . . . . . . . . . . . . 17 $/\$
197		eleq1 2515	. . . . . . . . . . . . . . . . 17
198	196, 197	syl5ibrcom 222	. . . . . . . . . . . . . . . 16 $/\$
199		eqid 2443	. . . . . . . . . . . . . . . . . 18
200		eqsqrtor 13178	. . . . . . . . . . . . . . . . . . 19 $/\$ $\/$
201	17, 200	mpdan 668	. . . . . . . . . . . . . . . . . 18 $\/$
202	199, 201	mpbii 211	. . . . . . . . . . . . . . . . 17 $\/$
203	202	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $\/$
204	195, 198, 203	mpjaod 381	. . . . . . . . . . . . . . 15 $/\$
205	204	stoic1a 1592	. . . . . . . . . . . . . 14 $/\$
206	12, 205	sylan 471	. . . . . . . . . . . . 13 $/\$
207	168, 206	pm2.61dan 791	. . . . . . . . . . . 12
208	116, 207	eldifd 3472	. . . . . . . . . . 11 $\$
209	208	adantl 466	. . . . . . . . . 10 $/\$ $\$
210		2cnd 10614	. . . . . . . . . . . . . 14
211		id 22	. . . . . . . . . . . . . 14
212	210, 211	mulcld 9619	. . . . . . . . . . . . 13
213	212	negcld 9923	. . . . . . . . . . . 12
214	213	adantl 466	. . . . . . . . . . 11 $/\$
215	12, 214	sylan2 474	. . . . . . . . . 10 $/\$
216	61	sqrtcld 13247	. . . . . . . . . . 11 $\$
217	216	adantl 466	. . . . . . . . . 10 $/\$ $\$
218		ovex 6309	. . . . . . . . . . 11
219	218	a1i 11	. . . . . . . . . 10 $/\$ $\$
220	19	adantl 466	. . . . . . . . . . 11 $/\$
221	37	a1i 11	. . . . . . . . . . . . 13 $/\$
222		1cnd 9615	. . . . . . . . . . . . . 14
223	11, 222	dvmptc 22234	. . . . . . . . . . . . 13
224	17	adantl 466	. . . . . . . . . . . . 13 $/\$
225		2cn 10612	. . . . . . . . . . . . . . 15
226		mulcl 9579	. . . . . . . . . . . . . . 15 $/\$
227	225, 226	mpan 670	. . . . . . . . . . . . . 14
228	227	adantl 466	. . . . . . . . . . . . 13 $/\$
229		2nn 10699	. . . . . . . . . . . . . . . 16
230		dvexp 22229	. . . . . . . . . . . . . . . 16
231	229, 230	ax-mp 5	. . . . . . . . . . . . . . 15
232		2m1e1 10656	. . . . . . . . . . . . . . . . . . 19
233	232	oveq2i 6292	. . . . . . . . . . . . . . . . . 18
234		exp1 12151	. . . . . . . . . . . . . . . . . 18
235	233, 234	syl5eq 2496	. . . . . . . . . . . . . . . . 17
236	235	oveq2d 6297	. . . . . . . . . . . . . . . 16
237	236	mpteq2ia 4519	. . . . . . . . . . . . . . 15
238	231, 237	eqtri 2472	. . . . . . . . . . . . . 14
239	238	a1i 11	. . . . . . . . . . . . 13
240	11, 82, 221, 223, 224, 228, 239	dvmptsub 22243	. . . . . . . . . . . 12
241		df-neg 9813	. . . . . . . . . . . . 13
242	241	mpteq2i 4520	. . . . . . . . . . . 12
243	240, 242	syl6eqr 2502	. . . . . . . . . . 11
244	11, 220, 214, 243, 84, 90, 85, 108	dvmptres 22239	. . . . . . . . . 10
245		eqid 2443	. . . . . . . . . . . 12 $\$ $\$
246	245	dvcnsqrt 30076	. . . . . . . . . . 11 $\$ $\$
247	246	a1i 11	. . . . . . . . . 10 $\$ $\$
248		fveq2 5856	. . . . . . . . . 10
249	248	oveq2d 6297	. . . . . . . . . . 11
250	249	oveq2d 6297	. . . . . . . . . 10
251	11, 11, 209, 215, 217, 219, 244, 247, 248, 250	dvmptco 22248	. . . . . . . . 9
252		mulneg2 10000	. . . . . . . . . . . . 13 $/\$
253	225, 12, 252	sylancr 663	. . . . . . . . . . . 12
254	253	oveq1d 6296	. . . . . . . . . . 11
255	12	negcld 9923	. . . . . . . . . . . 12
256		eldifn 3612	. . . . . . . . . . . . . . 15 $\$
257	256, 3	eleq2s 2551	. . . . . . . . . . . . . 14
258		id 22	. . . . . . . . . . . . . . . . . 18
259		mnflt 11342	. . . . . . . . . . . . . . . . . . . 20
260	92, 259	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
261		ubioc1 11587	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
262	52, 138, 260, 261	mp3an 1325	. . . . . . . . . . . . . . . . . 18
263	258, 262	syl6eqel 2539	. . . . . . . . . . . . . . . . 17
264		id 22	. . . . . . . . . . . . . . . . . 18
265		ltpnf 11340	. . . . . . . . . . . . . . . . . . . 20
266	95, 265	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
267		lbico1 11588	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
268	139, 127, 266, 267	mp3an 1325	. . . . . . . . . . . . . . . . . 18
269	264, 268	syl6eqel 2539	. . . . . . . . . . . . . . . . 17
270	263, 269	orim12i 516	. . . . . . . . . . . . . . . 16 $\/$ $\/$
271	270	orcoms 389	. . . . . . . . . . . . . . 15 $\/$ $\/$
272		elun 3630	. . . . . . . . . . . . . . 15 $\/$
273	271, 272	sylibr 212	. . . . . . . . . . . . . 14 $\/$
274	257, 273	nsyl 121	. . . . . . . . . . . . 13 $\/$
275		1cnd 9615	. . . . . . . . . . . . . . . . . 18 $/\$
276	17	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
277	19	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
278		simpr 461	. . . . . . . . . . . . . . . . . . 19 $/\$
279	277, 278	sqr00d 13251	. . . . . . . . . . . . . . . . . 18 $/\$
280	275, 276, 279	subeq0d 9944	. . . . . . . . . . . . . . . . 17 $/\$
281	152, 280	syl5req 2497	. . . . . . . . . . . . . . . 16 $/\$
282	281	ex 434	. . . . . . . . . . . . . . 15
283		sqeqor 12261	. . . . . . . . . . . . . . . 16 $/\$ $\/$
284	16, 283	mpan2 671	. . . . . . . . . . . . . . 15 $\/$
285	282, 284	sylibd 214	. . . . . . . . . . . . . 14 $\/$
286	285	necon3bd 2655	. . . . . . . . . . . . 13 $\/$
287	12, 274, 286	sylc 60	. . . . . . . . . . . 12
288		2cnne0 10756	. . . . . . . . . . . . 13 $/\$
289		divcan5 10252	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
290	288, 289	mp3an3 1314	. . . . . . . . . . . 12 $/\$ $/\$
291	255, 117, 287, 290	syl12anc 1227	. . . . . . . . . . 11
292	225, 12, 226	sylancr 663	. . . . . . . . . . . . 13
293	292	negcld 9923	. . . . . . . . . . . 12
294		mulcl 9579	. . . . . . . . . . . . 13 $/\$
295	225, 117, 294	sylancr 663	. . . . . . . . . . . 12
296		mulne0 10197	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
297	288, 296	mpan 670	. . . . . . . . . . . . 13 $/\$
298	117, 287, 297	syl2anc 661	. . . . . . . . . . . 12
299	293, 295, 298	divrec2d 10330	. . . . . . . . . . 11
300	254, 291, 299	3eqtr3rd 2493	. . . . . . . . . 10
301	300	mpteq2ia 4519	. . . . . . . . 9
302	251, 301	syl6eq 2500	. . . . . . . 8
303	11, 77, 78, 114, 118, 120, 302	dvmptadd 22236	. . . . . . 7
304		mulcl 9579	. . . . . . . . . . . 12 $/\$
305	13, 20, 304	sylancr 663	. . . . . . . . . . 11
306	12, 305	syl 16	. . . . . . . . . 10
307	306, 255, 117, 287	divdird 10364	. . . . . . . . 9
308		ixi 10184	. . . . . . . . . . . . . . . 16
309	308	eqcomi 2456	. . . . . . . . . . . . . . 15
310	309	oveq1i 6291	. . . . . . . . . . . . . 14
311		mulm1 10004	. . . . . . . . . . . . . 14
312		mulass 9583	. . . . . . . . . . . . . . 15 $/\$ $/\$
313	13, 13, 312	mp3an12 1315	. . . . . . . . . . . . . 14
314	310, 311, 313	3eqtr3a 2508	. . . . . . . . . . . . 13
315	314	oveq1d 6296	. . . . . . . . . . . 12
316		negcl 9825	. . . . . . . . . . . . 13
317	305, 316	addcomd 9785	. . . . . . . . . . . 12
318	13	a1i 11	. . . . . . . . . . . . 13
319	318, 15, 20	adddid 9623	. . . . . . . . . . . 12
320	315, 317, 319	3eqtr4d 2494	. . . . . . . . . . 11
321	12, 320	syl 16	. . . . . . . . . 10
322	321	oveq1d 6296	. . . . . . . . 9
323	75, 117, 287	divcan4d 10332	. . . . . . . . . 10
324	323	oveq1d 6296	. . . . . . . . 9
325	307, 322, 324	3eqtr3rd 2493	. . . . . . . 8
326	325	mpteq2ia 4519	. . . . . . 7
327	303, 326	syl6eq 2500	. . . . . 6
328	245	dvlog 22904	. . . . . . 7 $\$ $\$
329		logf1o 22824	. . . . . . . . . 10 $\$
330		f1of 5806	. . . . . . . . . 10 $\$ $\$
331	329, 330	mp1i 12	. . . . . . . . 9 $\$
332		snssi 4159	. . . . . . . . . . 11
333	66, 332	ax-mp 5	. . . . . . . . . 10
334		sscon 3623	. . . . . . . . . 10 $\$ $\$
335	333, 334	mp1i 12	. . . . . . . . 9 $\$ $\$
336	331, 335	feqresmpt 5912	. . . . . . . 8 $\$ $\$
337	336	oveq2d 6297	. . . . . . 7 $\$ $\$
338	328, 337	syl5reqr 2499	. . . . . 6 $\$ $\$
339		fveq2 5856	. . . . . 6
340		oveq2 6289	. . . . . 6
341	11, 11, 58, 60, 72, 74, 327, 338, 339, 340	dvmptco 22248	. . . . 5
342	22, 24	reccld 10319	. . . . . . . 8
343		mulcl 9579	. . . . . . . . . 10 $/\$
344	13, 21, 343	sylancr 663	. . . . . . . . 9
345	12, 344	syl 16	. . . . . . . 8
346	342, 345, 117, 287	divassd 10361	. . . . . . 7
347	345, 22, 24	divrec2d 10330	. . . . . . . . 9
348	75, 22, 24	divcan4d 10332	. . . . . . . . 9
349	347, 348	eqtr3d 2486	. . . . . . . 8
350	349	oveq1d 6296	. . . . . . 7
351	346, 350	eqtr3d 2486	. . . . . 6
352	351	mpteq2ia 4519	. . . . 5
353	341, 352	syl6eq 2500	. . . 4
354		negicn 9826	. . . . 5
355	354	a1i 11	. . . 4
356	11, 26, 28, 353, 355	dvmptcmul 22240	. . 3
357	356	trud 1392	. 2
358	13, 13	mulneg1i 10008	. . . . . 6
359	308	negeqi 9818	. . . . . 6
360		negneg1e1 10649	. . . . . 6
361	358, 359, 360	3eqtri 2476	. . . . 5
362	361	oveq1i 6291	. . . 4
363		divass 10231	. . . . . 6 $/\$ $/\$ $/\$
364	354, 13, 363	mp3an12 1315	. . . . 5 $/\$
365	117, 287, 364	syl2anc 661	. . . 4
366	362, 365	syl5reqr 2499	. . 3
367	366	mpteq2ia 4519	. 2
368	9, 357, 367	3eqtri 2476	1 arcsin

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369 $\/$ w3o 973 $/\$ w3a 974

wceq 1383

wtru 1384

wcel 1804

wne 2638

cvv 3095 $\$ cdif 3458

cun 3459

cin 3460

wss 3461

c0 3770

csn 4014

cpr 4016 class class class wbr 4437

cmpt 4495

crn 4990

cres 4991

wf 5574

wf1o 5577

cfv 5578 (class class class)co 6281

cc 9493

cr 9494

cc0 9495

c1 9496

ci 9497

caddc 9498

cmul 9500

cpnf 9628

cmnf 9629

cxr 9630

clt 9631

cle 9632

cmin 9810

cneg 9811

cdiv 10212

cn 10542

c2 10591

crp 11229

cioo 11538

cioc 11539

cico 11540

cexp 12145

cre 12909

csqrt 13045

cabs 13046 ↾_t crest 14695

ctopn 14696

ctg 14712 ℂ_fldccnfld 18294 TopOnctopon 19268

ccld 19390

cdv 22140

clog 22814 arcsincasin 23065

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1605 ax-4 1618 ax-5 1691 ax-6 1734 ax-7 1776 ax-8 1806 ax-9 1808 ax-10 1823 ax-11 1828 ax-12 1840 ax-13 1985 ax-ext 2421 ax-rep 4548 ax-sep 4558 ax-nul 4566 ax-pow 4615 ax-pr 4676 ax-un 6577 ax-inf2 8061 ax-cnex 9551 ax-resscn 9552 ax-1cn 9553 ax-icn 9554 ax-addcl 9555 ax-addrcl 9556 ax-mulcl 9557 ax-mulrcl 9558 ax-mulcom 9559 ax-addass 9560 ax-mulass 9561 ax-distr 9562 ax-i2m1 9563 ax-1ne0 9564 ax-1rid 9565 ax-rnegex 9566 ax-rrecex 9567 ax-cnre 9568 ax-pre-lttri 9569 ax-pre-lttrn 9570 ax-pre-ltadd 9571 ax-pre-mulgt0 9572 ax-pre-sup 9573 ax-addf 9574 ax-mulf 9575

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 975 df-3an 976 df-tru 1386 df-fal 1389 df-ex 1600 df-nf 1604 df-sb 1727 df-eu 2272 df-mo 2273 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2593 df-ne 2640 df-nel 2641 df-ral 2798 df-rex 2799 df-reu 2800 df-rmo 2801 df-rab 2802 df-v 3097 df-sbc 3314 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3771 df-if 3927 df-pw 3999 df-sn 4015 df-pr 4017 df-tp 4019 df-op 4021 df-uni 4235 df-int 4272 df-iun 4317 df-iin 4318 df-br 4438 df-opab 4496 df-mpt 4497 df-tr 4531 df-eprel 4781 df-id 4785 df-po 4790 df-so 4791 df-fr 4828 df-se 4829 df-we 4830 df-ord 4871 df-on 4872 df-lim 4873 df-suc 4874 df-xp 4995 df-rel 4996 df-cnv 4997 df-co 4998 df-dm 4999 df-rn 5000 df-res 5001 df-ima 5002 df-iota 5541 df-fun 5580 df-fn 5581 df-f 5582 df-f1 5583 df-fo 5584 df-f1o 5585 df-fv 5586 df-isom 5587 df-riota 6242 df-ov 6284 df-oprab 6285 df-mpt2 6286 df-of 6525 df-om 6686 df-1st 6785 df-2nd 6786 df-supp 6904 df-recs 7044 df-rdg 7078 df-1o 7132 df-2o 7133 df-oadd 7136 df-er 7313 df-map 7424 df-pm 7425 df-ixp 7472 df-en 7519 df-dom 7520 df-sdom 7521 df-fin 7522 df-fsupp 7832 df-fi 7873 df-sup 7903 df-oi 7938 df-card 8323 df-cda 8551 df-pnf 9633 df-mnf 9634 df-xr 9635 df-ltxr 9636 df-le 9637 df-sub 9812 df-neg 9813 df-div 10213 df-nn 10543 df-2 10600 df-3 10601 df-4 10602 df-5 10603 df-6 10604 df-7 10605 df-8 10606 df-9 10607 df-10 10608 df-n0 10802 df-z 10871 df-dec 10985 df-uz 11091 df-q 11192 df-rp 11230 df-xneg 11327 df-xadd 11328 df-xmul 11329 df-ioo 11542 df-ioc 11543 df-ico 11544 df-icc 11545 df-fz 11682 df-fzo 11804 df-fl 11908 df-mod 11976 df-seq 12087 df-exp 12146 df-fac 12333 df-bc 12360 df-hash 12385 df-shft 12879 df-cj 12911 df-re 12912 df-im 12913 df-sqrt 13047 df-abs 13048 df-limsup 13273 df-clim 13290 df-rlim 13291 df-sum 13488 df-ef 13681 df-sin 13683 df-cos 13684 df-tan 13685 df-pi 13686 df-struct 14511 df-ndx 14512 df-slot 14513 df-base 14514 df-sets 14515 df-ress 14516 df-plusg 14587 df-mulr 14588 df-starv 14589 df-sca 14590 df-vsca 14591 df-ip 14592 df-tset 14593 df-ple 14594 df-ds 14596 df-unif 14597 df-hom 14598 df-cco 14599 df-rest 14697 df-topn 14698 df-0g 14716 df-gsum 14717 df-topgen 14718 df-pt 14719 df-prds 14722 df-xrs 14776 df-qtop 14781 df-imas 14782 df-xps 14784 df-mre 14860 df-mrc 14861 df-acs 14863 df-mgm 15746 df-sgrp 15785 df-mnd 15795 df-submnd 15841 df-mulg 15934 df-cntz 16229 df-cmn 16674 df-psmet 18285 df-xmet 18286 df-met 18287 df-bl 18288 df-mopn 18289 df-fbas 18290 df-fg 18291 df-cnfld 18295 df-top 19272 df-bases 19274 df-topon 19275 df-topsp 19276 df-cld 19393 df-ntr 19394 df-cls 19395 df-nei 19472 df-lp 19510 df-perf 19511 df-cn 19601 df-cnp 19602 df-haus 19689 df-cmp 19760 df-tx 19936 df-hmeo 20129 df-fil 20220 df-fm 20312 df-flim 20313 df-flf 20314 df-xms 20696 df-ms 20697 df-tms 20698 df-cncf 21255 df-limc 22143 df-dv 22144 df-log 22816 df-cxp 22817 df-asin 23068

This theorem is referenced by: dvacos 30079 dvreasin 30080

W3C validator