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 31935

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 23728	. . . . 5 arcsin
2	1	reseq1i 5058	. . . 4 arcsin
3		dvasin.d	. . . . . 6 $\$
4		difss 3530	. . . . . 6 $\$
5	3, 4	eqsstri 3432	. . . . 5
6		resmpt 5111	. . . . 5
7	5, 6	ax-mp 5	. . . 4
8	2, 7	eqtri 2445	. . 3 arcsin
9	8	oveq2i 6255	. 2 arcsin
10		cnelprrecn 9578	. . . . 5
11	10	a1i 11	. . . 4
12	5	sseli 3398	. . . . . . 7
13		ax-icn 9544	. . . . . . . . 9
14		mulcl 9569	. . . . . . . . 9 $/\$
15	13, 14	mpan 674	. . . . . . . 8
16		ax-1cn 9543	. . . . . . . . . 10
17		sqcl 12282	. . . . . . . . . 10
18		subcl 9820	. . . . . . . . . 10 $/\$
19	16, 17, 18	sylancr 667	. . . . . . . . 9
20	19	sqrtcld 13437	. . . . . . . 8
21	15, 20	addcld 9608	. . . . . . 7
22	12, 21	syl 17	. . . . . 6
23		asinlem 23731	. . . . . . 7
24	12, 23	syl 17	. . . . . 6
25	22, 24	logcld 23457	. . . . 5
26	25	adantl 467	. . . 4 $/\$
27		ovex 6272	. . . . 5
28	27	a1i 11	. . . 4 $/\$
29		simpr 462	. . . . . . . . . . . . . . . 16 $/\$
30		asinlem3 23734	. . . . . . . . . . . . . . . . 17
31		rere 13124	. . . . . . . . . . . . . . . . . . 19
32	31	breq2d 4373	. . . . . . . . . . . . . . . . . 18
33	32	biimpac 488	. . . . . . . . . . . . . . . . 17 $/\$
34	30, 33	sylan 473	. . . . . . . . . . . . . . . 16 $/\$
35	23	adantr 466	. . . . . . . . . . . . . . . 16 $/\$
36	29, 34, 35	ne0gt0d 9718	. . . . . . . . . . . . . . 15 $/\$
37		0re 9589	. . . . . . . . . . . . . . . . 17
38		ltnle 9659	. . . . . . . . . . . . . . . . 17 $/\$
39	37, 38	mpan 674	. . . . . . . . . . . . . . . 16
40	39	adantl 467	. . . . . . . . . . . . . . 15 $/\$
41	36, 40	mpbid 213	. . . . . . . . . . . . . 14 $/\$
42	41	ex 435	. . . . . . . . . . . . 13
43	12, 42	syl 17	. . . . . . . . . . . 12
44		imor 413	. . . . . . . . . . . 12 $\/$
45	43, 44	sylib 199	. . . . . . . . . . 11 $\/$
46	45	orcomd 389	. . . . . . . . . 10 $\/$
47	46	olcd 394	. . . . . . . . 9 $\/$ $\/$
48		3ianor 999	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $\/$
49		3orrot 988	. . . . . . . . . . 11 $\/$ $\/$ $\/$ $\/$
50		3orass 985	. . . . . . . . . . 11 $\/$ $\/$ $\/$ $\/$
51	48, 49, 50	3bitrri 275	. . . . . . . . . 10 $\/$ $\/$ $/\$ $/\$
52		mnfxr 11360	. . . . . . . . . . 11
53		elioc2 11643	. . . . . . . . . . 11 $/\$ $/\$ $/\$
54	52, 37, 53	mp2an 676	. . . . . . . . . 10 $/\$ $/\$
55	51, 54	xchbinxr 312	. . . . . . . . 9 $\/$ $\/$
56	47, 55	sylib 199	. . . . . . . 8
57	22, 56	eldifd 3385	. . . . . . 7 $\$
58	57	adantl 467	. . . . . 6 $/\$ $\$
59		ovex 6272	. . . . . . 7
60	59	a1i 11	. . . . . 6 $/\$
61		eldifi 3525	. . . . . . . 8 $\$
62		eldifn 3526	. . . . . . . . 9 $\$
63		0xr 9633	. . . . . . . . . . . 12
64		mnflt0 11373	. . . . . . . . . . . 12
65		ubioc1 11634	. . . . . . . . . . . 12 $/\$ $/\$
66	52, 63, 64, 65	mp3an 1360	. . . . . . . . . . 11
67		eleq1 2489	. . . . . . . . . . 11
68	66, 67	mpbiri 236	. . . . . . . . . 10
69	68	necon3bi 2622	. . . . . . . . 9
70	62, 69	syl 17	. . . . . . . 8 $\$
71	61, 70	logcld 23457	. . . . . . 7 $\$
72	71	adantl 467	. . . . . 6 $/\$ $\$
73		ovex 6272	. . . . . . 7
74	73	a1i 11	. . . . . 6 $/\$ $\$
75	13	a1i 11	. . . . . . . . . 10
76	75, 12	mulcld 9609	. . . . . . . . 9
77	76	adantl 467	. . . . . . . 8 $/\$
78	13	a1i 11	. . . . . . . 8 $/\$
79	12	adantl 467	. . . . . . . . . 10 $/\$
80		1cnd 9605	. . . . . . . . . 10 $/\$
81		simpr 462	. . . . . . . . . . 11 $/\$
82		1cnd 9605	. . . . . . . . . . 11 $/\$
83	11	dvmptid 22848	. . . . . . . . . . 11
84	5	a1i 11	. . . . . . . . . . 11
85		eqid 2423	. . . . . . . . . . . . . 14 ℂ_fld ℂ_fld
86	85	cnfldtopon 21740	. . . . . . . . . . . . 13 ℂ_fld TopOn
87	86	toponunii 19884	. . . . . . . . . . . . . 14 ℂ_fld
88	87	restid 15270	. . . . . . . . . . . . 13 ℂ_fld TopOn ℂ_fld ↾_t ℂ_fld
89	86, 88	ax-mp 5	. . . . . . . . . . . 12 ℂ_fld ↾_t ℂ_fld
90	89	eqcomi 2432	. . . . . . . . . . 11 ℂ_fld ℂ_fld ↾_t
91	85	recld2 21769	. . . . . . . . . . . . . . 15 ℂ_fld
92		neg1rr 10660	. . . . . . . . . . . . . . . . . 18
93		iocmnfcld 21726	. . . . . . . . . . . . . . . . . 18
94	92, 93	ax-mp 5	. . . . . . . . . . . . . . . . 17
95		1re 9588	. . . . . . . . . . . . . . . . . 18
96		icopnfcld 21725	. . . . . . . . . . . . . . . . . 18
97	95, 96	ax-mp 5	. . . . . . . . . . . . . . . . 17
98		uncld 19993	. . . . . . . . . . . . . . . . 17 $/\$
99	94, 97, 98	mp2an 676	. . . . . . . . . . . . . . . 16
100	85	tgioo2 21758	. . . . . . . . . . . . . . . . 17 ℂ_fld ↾_t
101	100	fveq2i 5823	. . . . . . . . . . . . . . . 16 ℂ_fld ↾_t
102	99, 101	eleqtri 2499	. . . . . . . . . . . . . . 15 ℂ_fld ↾_t
103		restcldr 20127	. . . . . . . . . . . . . . 15 ℂ_fld $/\$ ℂ_fld ↾_t ℂ_fld
104	91, 102, 103	mp2an 676	. . . . . . . . . . . . . 14 ℂ_fld
105	87	cldopn 19983	. . . . . . . . . . . . . 14 ℂ_fld $\$ ℂ_fld
106	104, 105	ax-mp 5	. . . . . . . . . . . . 13 $\$ ℂ_fld
107	3, 106	eqeltri 2497	. . . . . . . . . . . 12 ℂ_fld
108	107	a1i 11	. . . . . . . . . . 11 ℂ_fld
109	11, 81, 82, 83, 84, 90, 85, 108	dvmptres 22854	. . . . . . . . . 10
110	13	a1i 11	. . . . . . . . . 10
111	11, 79, 80, 109, 110	dvmptcmul 22855	. . . . . . . . 9
112	13	mulid1i 9591	. . . . . . . . . 10
113	112	mpteq2i 4445	. . . . . . . . 9
114	111, 113	syl6eq 2473	. . . . . . . 8
115	12	sqcld 12359	. . . . . . . . . . 11
116	16, 115, 18	sylancr 667	. . . . . . . . . 10
117	116	sqrtcld 13437	. . . . . . . . 9
118	117	adantl 467	. . . . . . . 8 $/\$
119		ovex 6272	. . . . . . . . 9
120	119	a1i 11	. . . . . . . 8 $/\$
121		elin 3587	. . . . . . . . . . . . . . 15 $/\$
122	3	asindmre 31934	. . . . . . . . . . . . . . . . 17
123	122	eqimssi 3456	. . . . . . . . . . . . . . . 16
124	123	sseli 3398	. . . . . . . . . . . . . . 15
125	121, 124	sylbir 216	. . . . . . . . . . . . . 14 $/\$
126		incom 3593	. . . . . . . . . . . . . . . 16
127		pnfxr 11358	. . . . . . . . . . . . . . . . 17
128		df-ioc 11586	. . . . . . . . . . . . . . . . . 18 $/\$
129		df-ioo 11585	. . . . . . . . . . . . . . . . . 18 $/\$
130		xrltnle 9647	. . . . . . . . . . . . . . . . . 18 $/\$
131	128, 129, 130	ixxdisj 11596	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
132	52, 63, 127, 131	mp3an 1360	. . . . . . . . . . . . . . . 16
133	126, 132	eqtri 2445	. . . . . . . . . . . . . . 15
134		elioore 11612	. . . . . . . . . . . . . . . . . . 19
135	134	resqcld 12387	. . . . . . . . . . . . . . . . . 18
136		resubcl 9884	. . . . . . . . . . . . . . . . . 18 $/\$
137	95, 135, 136	sylancr 667	. . . . . . . . . . . . . . . . 17
138	92	rexri 9639	. . . . . . . . . . . . . . . . . . 19
139	95	rexri 9639	. . . . . . . . . . . . . . . . . . 19
140		elioo2 11623	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
141	138, 139, 140	mp2an 676	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
142		recn 9575	. . . . . . . . . . . . . . . . . . . . . . 23
143	142	abscld 13436	. . . . . . . . . . . . . . . . . . . . . 22
144	142	absge0d 13444	. . . . . . . . . . . . . . . . . . . . . 22
145		0le1 10083	. . . . . . . . . . . . . . . . . . . . . . 23
146		lt2sq 12293	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
147	95, 145, 146	mpanr12 689	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
148	143, 144, 147	syl2anc 665	. . . . . . . . . . . . . . . . . . . . 21
149		abslt 13316	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
150	95, 149	mpan2 675	. . . . . . . . . . . . . . . . . . . . 21 $/\$
151		absresq 13304	. . . . . . . . . . . . . . . . . . . . . . 23
152		sq1 12314	. . . . . . . . . . . . . . . . . . . . . . . 24
153	152	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
154	151, 153	breq12d 4374	. . . . . . . . . . . . . . . . . . . . . 22
155		resqcl 12287	. . . . . . . . . . . . . . . . . . . . . . 23
156		posdif 10053	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
157	155, 95, 156	sylancl 666	. . . . . . . . . . . . . . . . . . . . . 22
158	154, 157	bitrd 256	. . . . . . . . . . . . . . . . . . . . 21
159	148, 150, 158	3bitr3d 286	. . . . . . . . . . . . . . . . . . . 20 $/\$
160	159	biimpd 210	. . . . . . . . . . . . . . . . . . 19 $/\$
161	160	3impib 1203	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
162	141, 161	sylbi 198	. . . . . . . . . . . . . . . . 17
163	137, 162	elrpd 11284	. . . . . . . . . . . . . . . 16
164		ioorp 11658	. . . . . . . . . . . . . . . 16
165	163, 164	syl6eleqr 2512	. . . . . . . . . . . . . . 15
166		disjel 3779	. . . . . . . . . . . . . . 15 $/\$
167	133, 165, 166	sylancr 667	. . . . . . . . . . . . . 14
168	125, 167	syl 17	. . . . . . . . . . . . 13 $/\$
169		elioc2 11643	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
170	52, 37, 169	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
171	170	biimpi 197	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
172	171	simp1d 1017	. . . . . . . . . . . . . . . . . . . . 21
173		resubcl 9884	. . . . . . . . . . . . . . . . . . . . 21 $/\$
174	95, 172, 173	sylancr 667	. . . . . . . . . . . . . . . . . . . 20
175		nncan 9849	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
176	16, 175	mpan 674	. . . . . . . . . . . . . . . . . . . . . 22
177	176	eleq1d 2485	. . . . . . . . . . . . . . . . . . . . 21
178	177	biimpa 486	. . . . . . . . . . . . . . . . . . . 20 $/\$
179	174, 178	sylan2 476	. . . . . . . . . . . . . . . . . . 19 $/\$
180	172	adantl 467	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
181	171	simp3d 1019	. . . . . . . . . . . . . . . . . . . . . . 23
182	181	adantl 467	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
183		letr 9673	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
184	37, 95, 183	mp3an23 1352	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
185	145, 184	mpan2i 681	. . . . . . . . . . . . . . . . . . . . . 22
186	180, 182, 185	sylc 62	. . . . . . . . . . . . . . . . . . . . 21 $/\$
187		subge0 10073	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
188	95, 180, 187	sylancr 667	. . . . . . . . . . . . . . . . . . . . 21 $/\$
189	186, 188	mpbird 235	. . . . . . . . . . . . . . . . . . . 20 $/\$
190	176	adantr 466	. . . . . . . . . . . . . . . . . . . 20 $/\$
191	189, 190	breqtrd 4386	. . . . . . . . . . . . . . . . . . 19 $/\$
192	179, 191	resqrtcld 13418	. . . . . . . . . . . . . . . . . 18 $/\$
193	17, 192	sylan 473	. . . . . . . . . . . . . . . . 17 $/\$
194		eleq1 2489	. . . . . . . . . . . . . . . . 17
195	193, 194	syl5ibrcom 225	. . . . . . . . . . . . . . . 16 $/\$
196	193	renegcld 9992	. . . . . . . . . . . . . . . . 17 $/\$
197		eleq1 2489	. . . . . . . . . . . . . . . . 17
198	196, 197	syl5ibrcom 225	. . . . . . . . . . . . . . . 16 $/\$
199		eqid 2423	. . . . . . . . . . . . . . . . . 18
200		eqsqrtor 13368	. . . . . . . . . . . . . . . . . . 19 $/\$ $\/$
201	17, 200	mpdan 672	. . . . . . . . . . . . . . . . . 18 $\/$
202	199, 201	mpbii 214	. . . . . . . . . . . . . . . . 17 $\/$
203	202	adantr 466	. . . . . . . . . . . . . . . 16 $/\$ $\/$
204	195, 198, 203	mpjaod 382	. . . . . . . . . . . . . . 15 $/\$
205	204	stoic1a 1649	. . . . . . . . . . . . . 14 $/\$
206	12, 205	sylan 473	. . . . . . . . . . . . 13 $/\$
207	168, 206	pm2.61dan 798	. . . . . . . . . . . 12
208	116, 207	eldifd 3385	. . . . . . . . . . 11 $\$
209	208	adantl 467	. . . . . . . . . 10 $/\$ $\$
210		2cnd 10628	. . . . . . . . . . . . . 14
211		id 22	. . . . . . . . . . . . . 14
212	210, 211	mulcld 9609	. . . . . . . . . . . . 13
213	212	negcld 9919	. . . . . . . . . . . 12
214	213	adantl 467	. . . . . . . . . . 11 $/\$
215	12, 214	sylan2 476	. . . . . . . . . 10 $/\$
216	61	sqrtcld 13437	. . . . . . . . . . 11 $\$
217	216	adantl 467	. . . . . . . . . 10 $/\$ $\$
218		ovex 6272	. . . . . . . . . . 11
219	218	a1i 11	. . . . . . . . . 10 $/\$ $\$
220	19	adantl 467	. . . . . . . . . . 11 $/\$
221	37	a1i 11	. . . . . . . . . . . . 13 $/\$
222		1cnd 9605	. . . . . . . . . . . . . 14
223	11, 222	dvmptc 22849	. . . . . . . . . . . . 13
224	17	adantl 467	. . . . . . . . . . . . 13 $/\$
225		2cn 10626	. . . . . . . . . . . . . . 15
226		mulcl 9569	. . . . . . . . . . . . . . 15 $/\$
227	225, 226	mpan 674	. . . . . . . . . . . . . 14
228	227	adantl 467	. . . . . . . . . . . . 13 $/\$
229		2nn 10713	. . . . . . . . . . . . . . . 16
230		dvexp 22844	. . . . . . . . . . . . . . . 16
231	229, 230	ax-mp 5	. . . . . . . . . . . . . . 15
232		2m1e1 10670	. . . . . . . . . . . . . . . . . . 19
233	232	oveq2i 6255	. . . . . . . . . . . . . . . . . 18
234		exp1 12223	. . . . . . . . . . . . . . . . . 18
235	233, 234	syl5eq 2469	. . . . . . . . . . . . . . . . 17
236	235	oveq2d 6260	. . . . . . . . . . . . . . . 16
237	236	mpteq2ia 4444	. . . . . . . . . . . . . . 15
238	231, 237	eqtri 2445	. . . . . . . . . . . . . 14
239	238	a1i 11	. . . . . . . . . . . . 13
240	11, 82, 221, 223, 224, 228, 239	dvmptsub 22858	. . . . . . . . . . . 12
241		df-neg 9809	. . . . . . . . . . . . 13
242	241	mpteq2i 4445	. . . . . . . . . . . 12
243	240, 242	syl6eqr 2475	. . . . . . . . . . 11
244	11, 220, 214, 243, 84, 90, 85, 108	dvmptres 22854	. . . . . . . . . 10
245		eqid 2423	. . . . . . . . . . . 12 $\$ $\$
246	245	dvcnsqrt 23621	. . . . . . . . . . 11 $\$ $\$
247	246	a1i 11	. . . . . . . . . 10 $\$ $\$
248		fveq2 5820	. . . . . . . . . 10
249	248	oveq2d 6260	. . . . . . . . . . 11
250	249	oveq2d 6260	. . . . . . . . . 10
251	11, 11, 209, 215, 217, 219, 244, 247, 248, 250	dvmptco 22863	. . . . . . . . 9
252		mulneg2 10002	. . . . . . . . . . . . 13 $/\$
253	225, 12, 252	sylancr 667	. . . . . . . . . . . 12
254	253	oveq1d 6259	. . . . . . . . . . 11
255	12	negcld 9919	. . . . . . . . . . . 12
256		eldifn 3526	. . . . . . . . . . . . . . 15 $\$
257	256, 3	eleq2s 2519	. . . . . . . . . . . . . 14
258		id 22	. . . . . . . . . . . . . . . . . 18
259		mnflt 11371	. . . . . . . . . . . . . . . . . . . 20
260	92, 259	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
261		ubioc1 11634	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
262	52, 138, 260, 261	mp3an 1360	. . . . . . . . . . . . . . . . . 18
263	258, 262	syl6eqel 2509	. . . . . . . . . . . . . . . . 17
264		id 22	. . . . . . . . . . . . . . . . . 18
265		ltpnf 11368	. . . . . . . . . . . . . . . . . . . 20
266	95, 265	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
267		lbico1 11635	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
268	139, 127, 266, 267	mp3an 1360	. . . . . . . . . . . . . . . . . 18
269	264, 268	syl6eqel 2509	. . . . . . . . . . . . . . . . 17
270	263, 269	orim12i 518	. . . . . . . . . . . . . . . 16 $\/$ $\/$
271	270	orcoms 390	. . . . . . . . . . . . . . 15 $\/$ $\/$
272		elun 3544	. . . . . . . . . . . . . . 15 $\/$
273	271, 272	sylibr 215	. . . . . . . . . . . . . 14 $\/$
274	257, 273	nsyl 124	. . . . . . . . . . . . 13 $\/$
275		1cnd 9605	. . . . . . . . . . . . . . . . . 18 $/\$
276	17	adantr 466	. . . . . . . . . . . . . . . . . 18 $/\$
277	19	adantr 466	. . . . . . . . . . . . . . . . . . 19 $/\$
278		simpr 462	. . . . . . . . . . . . . . . . . . 19 $/\$
279	277, 278	sqr00d 13441	. . . . . . . . . . . . . . . . . 18 $/\$
280	275, 276, 279	subeq0d 9940	. . . . . . . . . . . . . . . . 17 $/\$
281	152, 280	syl5req 2470	. . . . . . . . . . . . . . . 16 $/\$
282	281	ex 435	. . . . . . . . . . . . . . 15
283		sqeqor 12333	. . . . . . . . . . . . . . . 16 $/\$ $\/$
284	16, 283	mpan2 675	. . . . . . . . . . . . . . 15 $\/$
285	282, 284	sylibd 217	. . . . . . . . . . . . . 14 $\/$
286	285	necon3bd 2610	. . . . . . . . . . . . 13 $\/$
287	12, 274, 286	sylc 62	. . . . . . . . . . . 12
288		2cnne0 10770	. . . . . . . . . . . . 13 $/\$
289		divcan5 10255	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
290	288, 289	mp3an3 1349	. . . . . . . . . . . 12 $/\$ $/\$
291	255, 117, 287, 290	syl12anc 1262	. . . . . . . . . . 11
292	225, 12, 226	sylancr 667	. . . . . . . . . . . . 13
293	292	negcld 9919	. . . . . . . . . . . 12
294		mulcl 9569	. . . . . . . . . . . . 13 $/\$
295	225, 117, 294	sylancr 667	. . . . . . . . . . . 12
296		mulne0 10200	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
297	288, 296	mpan 674	. . . . . . . . . . . . 13 $/\$
298	117, 287, 297	syl2anc 665	. . . . . . . . . . . 12
299	293, 295, 298	divrec2d 10333	. . . . . . . . . . 11
300	254, 291, 299	3eqtr3rd 2466	. . . . . . . . . 10
301	300	mpteq2ia 4444	. . . . . . . . 9
302	251, 301	syl6eq 2473	. . . . . . . 8
303	11, 77, 78, 114, 118, 120, 302	dvmptadd 22851	. . . . . . 7
304		mulcl 9569	. . . . . . . . . . . 12 $/\$
305	13, 20, 304	sylancr 667	. . . . . . . . . . 11
306	12, 305	syl 17	. . . . . . . . . 10
307	306, 255, 117, 287	divdird 10367	. . . . . . . . 9
308		ixi 10187	. . . . . . . . . . . . . . . 16
309	308	eqcomi 2432	. . . . . . . . . . . . . . 15
310	309	oveq1i 6254	. . . . . . . . . . . . . 14
311		mulm1 10006	. . . . . . . . . . . . . 14
312		mulass 9573	. . . . . . . . . . . . . . 15 $/\$ $/\$
313	13, 13, 312	mp3an12 1350	. . . . . . . . . . . . . 14
314	310, 311, 313	3eqtr3a 2481	. . . . . . . . . . . . 13
315	314	oveq1d 6259	. . . . . . . . . . . 12
316		negcl 9821	. . . . . . . . . . . . 13
317	305, 316	addcomd 9781	. . . . . . . . . . . 12
318	13	a1i 11	. . . . . . . . . . . . 13
319	318, 15, 20	adddid 9613	. . . . . . . . . . . 12
320	315, 317, 319	3eqtr4d 2467	. . . . . . . . . . 11
321	12, 320	syl 17	. . . . . . . . . 10
322	321	oveq1d 6259	. . . . . . . . 9
323	75, 117, 287	divcan4d 10335	. . . . . . . . . 10
324	323	oveq1d 6259	. . . . . . . . 9
325	307, 322, 324	3eqtr3rd 2466	. . . . . . . 8
326	325	mpteq2ia 4444	. . . . . . 7
327	303, 326	syl6eq 2473	. . . . . 6
328	245	dvlog 23533	. . . . . . 7 $\$ $\$
329		logf1o 23451	. . . . . . . . . 10 $\$
330		f1of 5769	. . . . . . . . . 10 $\$ $\$
331	329, 330	mp1i 13	. . . . . . . . 9 $\$
332		snssi 4082	. . . . . . . . . . 11
333	66, 332	ax-mp 5	. . . . . . . . . 10
334		sscon 3537	. . . . . . . . . 10 $\$ $\$
335	333, 334	mp1i 13	. . . . . . . . 9 $\$ $\$
336	331, 335	feqresmpt 5874	. . . . . . . 8 $\$ $\$
337	336	oveq2d 6260	. . . . . . 7 $\$ $\$
338	328, 337	syl5reqr 2472	. . . . . 6 $\$ $\$
339		fveq2 5820	. . . . . 6
340		oveq2 6252	. . . . . 6
341	11, 11, 58, 60, 72, 74, 327, 338, 339, 340	dvmptco 22863	. . . . 5
342	22, 24	reccld 10322	. . . . . . . 8
343		mulcl 9569	. . . . . . . . . 10 $/\$
344	13, 21, 343	sylancr 667	. . . . . . . . 9
345	12, 344	syl 17	. . . . . . . 8
346	342, 345, 117, 287	divassd 10364	. . . . . . 7
347	345, 22, 24	divrec2d 10333	. . . . . . . . 9
348	75, 22, 24	divcan4d 10335	. . . . . . . . 9
349	347, 348	eqtr3d 2459	. . . . . . . 8
350	349	oveq1d 6259	. . . . . . 7
351	346, 350	eqtr3d 2459	. . . . . 6
352	351	mpteq2ia 4444	. . . . 5
353	341, 352	syl6eq 2473	. . . 4
354		negicn 9822	. . . . 5
355	354	a1i 11	. . . 4
356	11, 26, 28, 353, 355	dvmptcmul 22855	. . 3
357	356	trud 1446	. 2
358	13, 13	mulneg1i 10010	. . . . . 6
359	308	negeqi 9814	. . . . . 6
360		negneg1e1 10663	. . . . . 6
361	358, 359, 360	3eqtri 2449	. . . . 5
362	361	oveq1i 6254	. . . 4
363		divass 10234	. . . . . 6 $/\$ $/\$ $/\$
364	354, 13, 363	mp3an12 1350	. . . . 5 $/\$
365	117, 287, 364	syl2anc 665	. . . 4
366	362, 365	syl5reqr 2472	. . 3
367	366	mpteq2ia 4444	. 2
368	9, 357, 367	3eqtri 2449	1 arcsin

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $\/$ wo 369 $/\$ wa 370 $\/$ w3o 981 $/\$ w3a 982

wceq 1437

wtru 1438

wcel 1872

wne 2594

cvv 3017 $\$ cdif 3371

cun 3372

cin 3373

wss 3374

c0 3699

csn 3936

cpr 3938 class class class wbr 4361

cmpt 4420

crn 4792

cres 4793

wf 5535

wf1o 5538

cfv 5539 (class class class)co 6244

cc 9483

cr 9484

cc0 9485

c1 9486

ci 9487

caddc 9488

cmul 9490

cpnf 9618

cmnf 9619

cxr 9620

clt 9621

cle 9622

cmin 9806

cneg 9807

cdiv 10215

cn 10555

c2 10605

crp 11248

cioo 11581

cioc 11582

cico 11583

cexp 12217

cre 13099

csqrt 13235

cabs 13236 ↾_t crest 15257

ctopn 15258

ctg 15274 ℂ_fldccnfld 18908 TopOnctopon 19855

ccld 19968

cdv 22755

clog 23441 arcsincasin 23725

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2058 ax-ext 2403 ax-rep 4474 ax-sep 4484 ax-nul 4493 ax-pow 4540 ax-pr 4598 ax-un 6536 ax-inf2 8094 ax-cnex 9541 ax-resscn 9542 ax-1cn 9543 ax-icn 9544 ax-addcl 9545 ax-addrcl 9546 ax-mulcl 9547 ax-mulrcl 9548 ax-mulcom 9549 ax-addass 9550 ax-mulass 9551 ax-distr 9552 ax-i2m1 9553 ax-1ne0 9554 ax-1rid 9555 ax-rnegex 9556 ax-rrecex 9557 ax-cnre 9558 ax-pre-lttri 9559 ax-pre-lttrn 9560 ax-pre-ltadd 9561 ax-pre-mulgt0 9562 ax-pre-sup 9563 ax-addf 9564 ax-mulf 9565

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2275 df-mo 2276 df-clab 2410 df-cleq 2416 df-clel 2419 df-nfc 2553 df-ne 2596 df-nel 2597 df-ral 2714 df-rex 2715 df-reu 2716 df-rmo 2717 df-rab 2718 df-v 3019 df-sbc 3238 df-csb 3334 df-dif 3377 df-un 3379 df-in 3381 df-ss 3388 df-pss 3390 df-nul 3700 df-if 3850 df-pw 3921 df-sn 3937 df-pr 3939 df-tp 3941 df-op 3943 df-uni 4158 df-int 4194 df-iun 4239 df-iin 4240 df-br 4362 df-opab 4421 df-mpt 4422 df-tr 4457 df-eprel 4702 df-id 4706 df-po 4712 df-so 4713 df-fr 4750 df-se 4751 df-we 4752 df-xp 4797 df-rel 4798 df-cnv 4799 df-co 4800 df-dm 4801 df-rn 4802 df-res 4803 df-ima 4804 df-pred 5337 df-ord 5383 df-on 5384 df-lim 5385 df-suc 5386 df-iota 5503 df-fun 5541 df-fn 5542 df-f 5543 df-f1 5544 df-fo 5545 df-f1o 5546 df-fv 5547 df-isom 5548 df-riota 6206 df-ov 6247 df-oprab 6248 df-mpt2 6249 df-of 6484 df-om 6646 df-1st 6746 df-2nd 6747 df-supp 6865 df-wrecs 6978 df-recs 7040 df-rdg 7078 df-1o 7132 df-2o 7133 df-oadd 7136 df-er 7313 df-map 7424 df-pm 7425 df-ixp 7473 df-en 7520 df-dom 7521 df-sdom 7522 df-fin 7523 df-fsupp 7832 df-fi 7873 df-sup 7904 df-inf 7905 df-oi 7973 df-card 8320 df-cda 8544 df-pnf 9623 df-mnf 9624 df-xr 9625 df-ltxr 9626 df-le 9627 df-sub 9808 df-neg 9809 df-div 10216 df-nn 10556 df-2 10614 df-3 10615 df-4 10616 df-5 10617 df-6 10618 df-7 10619 df-8 10620 df-9 10621 df-10 10622 df-n0 10816 df-z 10884 df-dec 10998 df-uz 11106 df-q 11211 df-rp 11249 df-xneg 11355 df-xadd 11356 df-xmul 11357 df-ioo 11585 df-ioc 11586 df-ico 11587 df-icc 11588 df-fz 11731 df-fzo 11862 df-fl 11973 df-mod 12042 df-seq 12159 df-exp 12218 df-fac 12405 df-bc 12433 df-hash 12461 df-shft 13069 df-cj 13101 df-re 13102 df-im 13103 df-sqrt 13237 df-abs 13238 df-limsup 13464 df-clim 13490 df-rlim 13491 df-sum 13691 df-ef 14059 df-sin 14061 df-cos 14062 df-tan 14063 df-pi 14064 df-struct 15061 df-ndx 15062 df-slot 15063 df-base 15064 df-sets 15065 df-ress 15066 df-plusg 15141 df-mulr 15142 df-starv 15143 df-sca 15144 df-vsca 15145 df-ip 15146 df-tset 15147 df-ple 15148 df-ds 15150 df-unif 15151 df-hom 15152 df-cco 15153 df-rest 15259 df-topn 15260 df-0g 15278 df-gsum 15279 df-topgen 15280 df-pt 15281 df-prds 15284 df-xrs 15338 df-qtop 15344 df-imas 15345 df-xps 15348 df-mre 15430 df-mrc 15431 df-acs 15433 df-mgm 16426 df-sgrp 16465 df-mnd 16475 df-submnd 16521 df-mulg 16614 df-cntz 16909 df-cmn 17370 df-psmet 18900 df-xmet 18901 df-met 18902 df-bl 18903 df-mopn 18904 df-fbas 18905 df-fg 18906 df-cnfld 18909 df-top 19858 df-bases 19859 df-topon 19860 df-topsp 19861 df-cld 19971 df-ntr 19972 df-cls 19973 df-nei 20051 df-lp 20089 df-perf 20090 df-cn 20180 df-cnp 20181 df-haus 20268 df-cmp 20339 df-tx 20514 df-hmeo 20707 df-fil 20798 df-fm 20890 df-flim 20891 df-flf 20892 df-xms 21272 df-ms 21273 df-tms 21274 df-cncf 21847 df-limc 22758 df-dv 22759 df-log 23443 df-cxp 23444 df-asin 23728

This theorem is referenced by: dvacos 31936 dvreasin 31937

W3C validator