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 33496

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 24592	. . . . 5 arcsin
2	1	reseq1i 5392	. . . 4 arcsin
3		dvasin.d	. . . . . 6 $\$
4		difss 3737	. . . . . 6 $\$
5	3, 4	eqsstri 3635	. . . . 5
6		resmpt 5449	. . . . 5
7	5, 6	ax-mp 5	. . . 4
8	2, 7	eqtri 2644	. . 3 arcsin
9	8	oveq2i 6661	. 2 arcsin
10		cnelprrecn 10029	. . . . 5
11	10	a1i 11	. . . 4
12	5	sseli 3599	. . . . . . 7
13		ax-icn 9995	. . . . . . . . 9
14		mulcl 10020	. . . . . . . . 9 $/\$
15	13, 14	mpan 706	. . . . . . . 8
16		ax-1cn 9994	. . . . . . . . . 10
17		sqcl 12925	. . . . . . . . . 10
18		subcl 10280	. . . . . . . . . 10 $/\$
19	16, 17, 18	sylancr 695	. . . . . . . . 9
20	19	sqrtcld 14176	. . . . . . . 8
21	15, 20	addcld 10059	. . . . . . 7
22	12, 21	syl 17	. . . . . 6
23		asinlem 24595	. . . . . . 7
24	12, 23	syl 17	. . . . . 6
25	22, 24	logcld 24317	. . . . 5
26	25	adantl 482	. . . 4 $/\$
27		ovexd 6680	. . . 4 $/\$
28		simpr 477	. . . . . . . . . . . . . . . 16 $/\$
29		asinlem3 24598	. . . . . . . . . . . . . . . . 17
30		rere 13862	. . . . . . . . . . . . . . . . . . 19
31	30	breq2d 4665	. . . . . . . . . . . . . . . . . 18
32	31	biimpac 503	. . . . . . . . . . . . . . . . 17 $/\$
33	29, 32	sylan 488	. . . . . . . . . . . . . . . 16 $/\$
34	23	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
35	28, 33, 34	ne0gt0d 10174	. . . . . . . . . . . . . . 15 $/\$
36		0re 10040	. . . . . . . . . . . . . . . . 17
37		ltnle 10117	. . . . . . . . . . . . . . . . 17 $/\$
38	36, 37	mpan 706	. . . . . . . . . . . . . . . 16
39	38	adantl 482	. . . . . . . . . . . . . . 15 $/\$
40	35, 39	mpbid 222	. . . . . . . . . . . . . 14 $/\$
41	40	ex 450	. . . . . . . . . . . . 13
42	12, 41	syl 17	. . . . . . . . . . . 12
43		imor 428	. . . . . . . . . . . 12 $\/$
44	42, 43	sylib 208	. . . . . . . . . . 11 $\/$
45	44	orcomd 403	. . . . . . . . . 10 $\/$
46	45	olcd 408	. . . . . . . . 9 $\/$ $\/$
47		3ianor 1055	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $\/$
48		3orrot 1044	. . . . . . . . . . 11 $\/$ $\/$ $\/$ $\/$
49		3orass 1040	. . . . . . . . . . 11 $\/$ $\/$ $\/$ $\/$
50	47, 48, 49	3bitrri 287	. . . . . . . . . 10 $\/$ $\/$ $/\$ $/\$
51		mnfxr 10096	. . . . . . . . . . 11
52		elioc2 12236	. . . . . . . . . . 11 $/\$ $/\$ $/\$
53	51, 36, 52	mp2an 708	. . . . . . . . . 10 $/\$ $/\$
54	50, 53	xchbinxr 325	. . . . . . . . 9 $\/$ $\/$
55	46, 54	sylib 208	. . . . . . . 8
56	22, 55	eldifd 3585	. . . . . . 7 $\$
57	56	adantl 482	. . . . . 6 $/\$ $\$
58		ovexd 6680	. . . . . 6 $/\$
59		eldifi 3732	. . . . . . . 8 $\$
60		eldifn 3733	. . . . . . . . 9 $\$
61		0xr 10086	. . . . . . . . . . . 12
62		mnflt0 11959	. . . . . . . . . . . 12
63		ubioc1 12227	. . . . . . . . . . . 12 $/\$ $/\$
64	51, 61, 62, 63	mp3an 1424	. . . . . . . . . . 11
65		eleq1 2689	. . . . . . . . . . 11
66	64, 65	mpbiri 248	. . . . . . . . . 10
67	66	necon3bi 2820	. . . . . . . . 9
68	60, 67	syl 17	. . . . . . . 8 $\$
69	59, 68	logcld 24317	. . . . . . 7 $\$
70	69	adantl 482	. . . . . 6 $/\$ $\$
71		ovexd 6680	. . . . . 6 $/\$ $\$
72	13	a1i 11	. . . . . . . . . 10
73	72, 12	mulcld 10060	. . . . . . . . 9
74	73	adantl 482	. . . . . . . 8 $/\$
75	13	a1i 11	. . . . . . . 8 $/\$
76	12	adantl 482	. . . . . . . . . 10 $/\$
77		1cnd 10056	. . . . . . . . . 10 $/\$
78		simpr 477	. . . . . . . . . . 11 $/\$
79		1cnd 10056	. . . . . . . . . . 11 $/\$
80	11	dvmptid 23720	. . . . . . . . . . 11
81	5	a1i 11	. . . . . . . . . . 11
82		eqid 2622	. . . . . . . . . . . . . 14 ℂ_fld ℂ_fld
83	82	cnfldtopon 22586	. . . . . . . . . . . . 13 ℂ_fld TopOn
84	83	toponunii 20721	. . . . . . . . . . . . . 14 ℂ_fld
85	84	restid 16094	. . . . . . . . . . . . 13 ℂ_fld TopOn ℂ_fld ↾_t ℂ_fld
86	83, 85	ax-mp 5	. . . . . . . . . . . 12 ℂ_fld ↾_t ℂ_fld
87	86	eqcomi 2631	. . . . . . . . . . 11 ℂ_fld ℂ_fld ↾_t
88	82	recld2 22617	. . . . . . . . . . . . . . 15 ℂ_fld
89		neg1rr 11125	. . . . . . . . . . . . . . . . . 18
90		iocmnfcld 22572	. . . . . . . . . . . . . . . . . 18
91	89, 90	ax-mp 5	. . . . . . . . . . . . . . . . 17
92		1re 10039	. . . . . . . . . . . . . . . . . 18
93		icopnfcld 22571	. . . . . . . . . . . . . . . . . 18
94	92, 93	ax-mp 5	. . . . . . . . . . . . . . . . 17
95		uncld 20845	. . . . . . . . . . . . . . . . 17 $/\$
96	91, 94, 95	mp2an 708	. . . . . . . . . . . . . . . 16
97	82	tgioo2 22606	. . . . . . . . . . . . . . . . 17 ℂ_fld ↾_t
98	97	fveq2i 6194	. . . . . . . . . . . . . . . 16 ℂ_fld ↾_t
99	96, 98	eleqtri 2699	. . . . . . . . . . . . . . 15 ℂ_fld ↾_t
100		restcldr 20978	. . . . . . . . . . . . . . 15 ℂ_fld $/\$ ℂ_fld ↾_t ℂ_fld
101	88, 99, 100	mp2an 708	. . . . . . . . . . . . . 14 ℂ_fld
102	84	cldopn 20835	. . . . . . . . . . . . . 14 ℂ_fld $\$ ℂ_fld
103	101, 102	ax-mp 5	. . . . . . . . . . . . 13 $\$ ℂ_fld
104	3, 103	eqeltri 2697	. . . . . . . . . . . 12 ℂ_fld
105	104	a1i 11	. . . . . . . . . . 11 ℂ_fld
106	11, 78, 79, 80, 81, 87, 82, 105	dvmptres 23726	. . . . . . . . . 10
107	13	a1i 11	. . . . . . . . . 10
108	11, 76, 77, 106, 107	dvmptcmul 23727	. . . . . . . . 9
109	13	mulid1i 10042	. . . . . . . . . 10
110	109	mpteq2i 4741	. . . . . . . . 9
111	108, 110	syl6eq 2672	. . . . . . . 8
112	12	sqcld 13006	. . . . . . . . . . 11
113	16, 112, 18	sylancr 695	. . . . . . . . . 10
114	113	sqrtcld 14176	. . . . . . . . 9
115	114	adantl 482	. . . . . . . 8 $/\$
116		ovexd 6680	. . . . . . . 8 $/\$
117		elin 3796	. . . . . . . . . . . . . . 15 $/\$
118	3	asindmre 33495	. . . . . . . . . . . . . . . . 17
119	118	eqimssi 3659	. . . . . . . . . . . . . . . 16
120	119	sseli 3599	. . . . . . . . . . . . . . 15
121	117, 120	sylbir 225	. . . . . . . . . . . . . 14 $/\$
122		incom 3805	. . . . . . . . . . . . . . . 16
123		pnfxr 10092	. . . . . . . . . . . . . . . . 17
124		df-ioc 12180	. . . . . . . . . . . . . . . . . 18 $/\$
125		df-ioo 12179	. . . . . . . . . . . . . . . . . 18 $/\$
126		xrltnle 10105	. . . . . . . . . . . . . . . . . 18 $/\$
127	124, 125, 126	ixxdisj 12190	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
128	51, 61, 123, 127	mp3an 1424	. . . . . . . . . . . . . . . 16
129	122, 128	eqtri 2644	. . . . . . . . . . . . . . 15
130		elioore 12205	. . . . . . . . . . . . . . . . . . 19
131	130	resqcld 13035	. . . . . . . . . . . . . . . . . 18
132		resubcl 10345	. . . . . . . . . . . . . . . . . 18 $/\$
133	92, 131, 132	sylancr 695	. . . . . . . . . . . . . . . . 17
134	89	rexri 10097	. . . . . . . . . . . . . . . . . . 19
135	92	rexri 10097	. . . . . . . . . . . . . . . . . . 19
136		elioo2 12216	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
137	134, 135, 136	mp2an 708	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
138		recn 10026	. . . . . . . . . . . . . . . . . . . . . . 23
139	138	abscld 14175	. . . . . . . . . . . . . . . . . . . . . 22
140	138	absge0d 14183	. . . . . . . . . . . . . . . . . . . . . 22
141		0le1 10551	. . . . . . . . . . . . . . . . . . . . . . 23
142		lt2sq 12937	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
143	92, 141, 142	mpanr12 721	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
144	139, 140, 143	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21
145		abslt 14054	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
146	92, 145	mpan2 707	. . . . . . . . . . . . . . . . . . . . 21 $/\$
147		absresq 14042	. . . . . . . . . . . . . . . . . . . . . . 23
148		sq1 12958	. . . . . . . . . . . . . . . . . . . . . . . 24
149	148	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
150	147, 149	breq12d 4666	. . . . . . . . . . . . . . . . . . . . . 22
151		resqcl 12931	. . . . . . . . . . . . . . . . . . . . . . 23
152		posdif 10521	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
153	151, 92, 152	sylancl 694	. . . . . . . . . . . . . . . . . . . . . 22
154	150, 153	bitrd 268	. . . . . . . . . . . . . . . . . . . . 21
155	144, 146, 154	3bitr3d 298	. . . . . . . . . . . . . . . . . . . 20 $/\$
156	155	biimpd 219	. . . . . . . . . . . . . . . . . . 19 $/\$
157	156	3impib 1262	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
158	137, 157	sylbi 207	. . . . . . . . . . . . . . . . 17
159	133, 158	elrpd 11869	. . . . . . . . . . . . . . . 16
160		ioorp 12251	. . . . . . . . . . . . . . . 16
161	159, 160	syl6eleqr 2712	. . . . . . . . . . . . . . 15
162		disjel 4023	. . . . . . . . . . . . . . 15 $/\$
163	129, 161, 162	sylancr 695	. . . . . . . . . . . . . 14
164	121, 163	syl 17	. . . . . . . . . . . . 13 $/\$
165		elioc2 12236	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
166	51, 36, 165	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
167	166	biimpi 206	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
168	167	simp1d 1073	. . . . . . . . . . . . . . . . . . . . 21
169		resubcl 10345	. . . . . . . . . . . . . . . . . . . . 21 $/\$
170	92, 168, 169	sylancr 695	. . . . . . . . . . . . . . . . . . . 20
171		nncan 10310	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
172	16, 171	mpan 706	. . . . . . . . . . . . . . . . . . . . . 22
173	172	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . 21
174	173	biimpa 501	. . . . . . . . . . . . . . . . . . . 20 $/\$
175	170, 174	sylan2 491	. . . . . . . . . . . . . . . . . . 19 $/\$
176	168	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
177	167	simp3d 1075	. . . . . . . . . . . . . . . . . . . . . . 23
178	177	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
179		letr 10131	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
180	36, 92, 179	mp3an23 1416	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
181	141, 180	mpan2i 713	. . . . . . . . . . . . . . . . . . . . . 22
182	176, 178, 181	sylc 65	. . . . . . . . . . . . . . . . . . . . 21 $/\$
183		subge0 10541	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
184	92, 176, 183	sylancr 695	. . . . . . . . . . . . . . . . . . . . 21 $/\$
185	182, 184	mpbird 247	. . . . . . . . . . . . . . . . . . . 20 $/\$
186	172	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
187	185, 186	breqtrd 4679	. . . . . . . . . . . . . . . . . . 19 $/\$
188	175, 187	resqrtcld 14156	. . . . . . . . . . . . . . . . . 18 $/\$
189	17, 188	sylan 488	. . . . . . . . . . . . . . . . 17 $/\$
190		eleq1 2689	. . . . . . . . . . . . . . . . 17
191	189, 190	syl5ibrcom 237	. . . . . . . . . . . . . . . 16 $/\$
192	189	renegcld 10457	. . . . . . . . . . . . . . . . 17 $/\$
193		eleq1 2689	. . . . . . . . . . . . . . . . 17
194	192, 193	syl5ibrcom 237	. . . . . . . . . . . . . . . 16 $/\$
195		eqid 2622	. . . . . . . . . . . . . . . . . 18
196		eqsqrtor 14106	. . . . . . . . . . . . . . . . . . 19 $/\$ $\/$
197	17, 196	mpdan 702	. . . . . . . . . . . . . . . . . 18 $\/$
198	195, 197	mpbii 223	. . . . . . . . . . . . . . . . 17 $\/$
199	198	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $\/$
200	191, 194, 199	mpjaod 396	. . . . . . . . . . . . . . 15 $/\$
201	200	stoic1a 1697	. . . . . . . . . . . . . 14 $/\$
202	12, 201	sylan 488	. . . . . . . . . . . . 13 $/\$
203	164, 202	pm2.61dan 832	. . . . . . . . . . . 12
204	113, 203	eldifd 3585	. . . . . . . . . . 11 $\$
205	204	adantl 482	. . . . . . . . . 10 $/\$ $\$
206		2cnd 11093	. . . . . . . . . . . . . 14
207		id 22	. . . . . . . . . . . . . 14
208	206, 207	mulcld 10060	. . . . . . . . . . . . 13
209	208	negcld 10379	. . . . . . . . . . . 12
210	209	adantl 482	. . . . . . . . . . 11 $/\$
211	12, 210	sylan2 491	. . . . . . . . . 10 $/\$
212	59	sqrtcld 14176	. . . . . . . . . . 11 $\$
213	212	adantl 482	. . . . . . . . . 10 $/\$ $\$
214		ovexd 6680	. . . . . . . . . 10 $/\$ $\$
215	19	adantl 482	. . . . . . . . . . 11 $/\$
216	36	a1i 11	. . . . . . . . . . . . 13 $/\$
217		1cnd 10056	. . . . . . . . . . . . . 14
218	11, 217	dvmptc 23721	. . . . . . . . . . . . 13
219	17	adantl 482	. . . . . . . . . . . . 13 $/\$
220		2cn 11091	. . . . . . . . . . . . . . 15
221		mulcl 10020	. . . . . . . . . . . . . . 15 $/\$
222	220, 221	mpan 706	. . . . . . . . . . . . . 14
223	222	adantl 482	. . . . . . . . . . . . 13 $/\$
224		2nn 11185	. . . . . . . . . . . . . . . 16
225		dvexp 23716	. . . . . . . . . . . . . . . 16
226	224, 225	ax-mp 5	. . . . . . . . . . . . . . 15
227		2m1e1 11135	. . . . . . . . . . . . . . . . . . 19
228	227	oveq2i 6661	. . . . . . . . . . . . . . . . . 18
229		exp1 12866	. . . . . . . . . . . . . . . . . 18
230	228, 229	syl5eq 2668	. . . . . . . . . . . . . . . . 17
231	230	oveq2d 6666	. . . . . . . . . . . . . . . 16
232	231	mpteq2ia 4740	. . . . . . . . . . . . . . 15
233	226, 232	eqtri 2644	. . . . . . . . . . . . . 14
234	233	a1i 11	. . . . . . . . . . . . 13
235	11, 79, 216, 218, 219, 223, 234	dvmptsub 23730	. . . . . . . . . . . 12
236		df-neg 10269	. . . . . . . . . . . . 13
237	236	mpteq2i 4741	. . . . . . . . . . . 12
238	235, 237	syl6eqr 2674	. . . . . . . . . . 11
239	11, 215, 210, 238, 81, 87, 82, 105	dvmptres 23726	. . . . . . . . . 10
240		eqid 2622	. . . . . . . . . . . 12 $\$ $\$
241	240	dvcnsqrt 24485	. . . . . . . . . . 11 $\$ $\$
242	241	a1i 11	. . . . . . . . . 10 $\$ $\$
243		fveq2 6191	. . . . . . . . . 10
244	243	oveq2d 6666	. . . . . . . . . . 11
245	244	oveq2d 6666	. . . . . . . . . 10
246	11, 11, 205, 211, 213, 214, 239, 242, 243, 245	dvmptco 23735	. . . . . . . . 9
247		mulneg2 10467	. . . . . . . . . . . . 13 $/\$
248	220, 12, 247	sylancr 695	. . . . . . . . . . . 12
249	248	oveq1d 6665	. . . . . . . . . . 11
250	12	negcld 10379	. . . . . . . . . . . 12
251		eldifn 3733	. . . . . . . . . . . . . . 15 $\$
252	251, 3	eleq2s 2719	. . . . . . . . . . . . . 14
253		id 22	. . . . . . . . . . . . . . . . . 18
254		mnflt 11957	. . . . . . . . . . . . . . . . . . . 20
255	89, 254	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
256		ubioc1 12227	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
257	51, 134, 255, 256	mp3an 1424	. . . . . . . . . . . . . . . . . 18
258	253, 257	syl6eqel 2709	. . . . . . . . . . . . . . . . 17
259		id 22	. . . . . . . . . . . . . . . . . 18
260		ltpnf 11954	. . . . . . . . . . . . . . . . . . . 20
261	92, 260	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
262		lbico1 12228	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
263	135, 123, 261, 262	mp3an 1424	. . . . . . . . . . . . . . . . . 18
264	259, 263	syl6eqel 2709	. . . . . . . . . . . . . . . . 17
265	258, 264	orim12i 538	. . . . . . . . . . . . . . . 16 $\/$ $\/$
266	265	orcoms 404	. . . . . . . . . . . . . . 15 $\/$ $\/$
267		elun 3753	. . . . . . . . . . . . . . 15 $\/$
268	266, 267	sylibr 224	. . . . . . . . . . . . . 14 $\/$
269	252, 268	nsyl 135	. . . . . . . . . . . . 13 $\/$
270		1cnd 10056	. . . . . . . . . . . . . . . . . 18 $/\$
271	17	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
272	19	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$
273		simpr 477	. . . . . . . . . . . . . . . . . . 19 $/\$
274	272, 273	sqr00d 14180	. . . . . . . . . . . . . . . . . 18 $/\$
275	270, 271, 274	subeq0d 10400	. . . . . . . . . . . . . . . . 17 $/\$
276	148, 275	syl5req 2669	. . . . . . . . . . . . . . . 16 $/\$
277	276	ex 450	. . . . . . . . . . . . . . 15
278		sqeqor 12978	. . . . . . . . . . . . . . . 16 $/\$ $\/$
279	16, 278	mpan2 707	. . . . . . . . . . . . . . 15 $\/$
280	277, 279	sylibd 229	. . . . . . . . . . . . . 14 $\/$
281	280	necon3bd 2808	. . . . . . . . . . . . 13 $\/$
282	12, 269, 281	sylc 65	. . . . . . . . . . . 12
283		2cnne0 11242	. . . . . . . . . . . . 13 $/\$
284		divcan5 10727	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
285	283, 284	mp3an3 1413	. . . . . . . . . . . 12 $/\$ $/\$
286	250, 114, 282, 285	syl12anc 1324	. . . . . . . . . . 11
287	220, 12, 221	sylancr 695	. . . . . . . . . . . . 13
288	287	negcld 10379	. . . . . . . . . . . 12
289		mulcl 10020	. . . . . . . . . . . . 13 $/\$
290	220, 114, 289	sylancr 695	. . . . . . . . . . . 12
291		mulne0 10669	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
292	283, 291	mpan 706	. . . . . . . . . . . . 13 $/\$
293	114, 282, 292	syl2anc 693	. . . . . . . . . . . 12
294	288, 290, 293	divrec2d 10805	. . . . . . . . . . 11
295	249, 286, 294	3eqtr3rd 2665	. . . . . . . . . 10
296	295	mpteq2ia 4740	. . . . . . . . 9
297	246, 296	syl6eq 2672	. . . . . . . 8
298	11, 74, 75, 111, 115, 116, 297	dvmptadd 23723	. . . . . . 7
299		mulcl 10020	. . . . . . . . . . . 12 $/\$
300	13, 20, 299	sylancr 695	. . . . . . . . . . 11
301	12, 300	syl 17	. . . . . . . . . 10
302	301, 250, 114, 282	divdird 10839	. . . . . . . . 9
303		ixi 10656	. . . . . . . . . . . . . . . 16
304	303	eqcomi 2631	. . . . . . . . . . . . . . 15
305	304	oveq1i 6660	. . . . . . . . . . . . . 14
306		mulm1 10471	. . . . . . . . . . . . . 14
307		mulass 10024	. . . . . . . . . . . . . . 15 $/\$ $/\$
308	13, 13, 307	mp3an12 1414	. . . . . . . . . . . . . 14
309	305, 306, 308	3eqtr3a 2680	. . . . . . . . . . . . 13
310	309	oveq1d 6665	. . . . . . . . . . . 12
311		negcl 10281	. . . . . . . . . . . . 13
312	300, 311	addcomd 10238	. . . . . . . . . . . 12
313	13	a1i 11	. . . . . . . . . . . . 13
314	313, 15, 20	adddid 10064	. . . . . . . . . . . 12
315	310, 312, 314	3eqtr4d 2666	. . . . . . . . . . 11
316	12, 315	syl 17	. . . . . . . . . 10
317	316	oveq1d 6665	. . . . . . . . 9
318	72, 114, 282	divcan4d 10807	. . . . . . . . . 10
319	318	oveq1d 6665	. . . . . . . . 9
320	302, 317, 319	3eqtr3rd 2665	. . . . . . . 8
321	320	mpteq2ia 4740	. . . . . . 7
322	298, 321	syl6eq 2672	. . . . . 6
323	240	dvlog 24397	. . . . . . 7 $\$ $\$
324		logf1o 24311	. . . . . . . . . 10 $\$
325		f1of 6137	. . . . . . . . . 10 $\$ $\$
326	324, 325	mp1i 13	. . . . . . . . 9 $\$
327		snssi 4339	. . . . . . . . . . 11
328	64, 327	ax-mp 5	. . . . . . . . . 10
329		sscon 3744	. . . . . . . . . 10 $\$ $\$
330	328, 329	mp1i 13	. . . . . . . . 9 $\$ $\$
331	326, 330	feqresmpt 6250	. . . . . . . 8 $\$ $\$
332	331	oveq2d 6666	. . . . . . 7 $\$ $\$
333	323, 332	syl5reqr 2671	. . . . . 6 $\$ $\$
334		fveq2 6191	. . . . . 6
335		oveq2 6658	. . . . . 6
336	11, 11, 57, 58, 70, 71, 322, 333, 334, 335	dvmptco 23735	. . . . 5
337	22, 24	reccld 10794	. . . . . . . 8
338		mulcl 10020	. . . . . . . . . 10 $/\$
339	13, 21, 338	sylancr 695	. . . . . . . . 9
340	12, 339	syl 17	. . . . . . . 8
341	337, 340, 114, 282	divassd 10836	. . . . . . 7
342	340, 22, 24	divrec2d 10805	. . . . . . . . 9
343	72, 22, 24	divcan4d 10807	. . . . . . . . 9
344	342, 343	eqtr3d 2658	. . . . . . . 8
345	344	oveq1d 6665	. . . . . . 7
346	341, 345	eqtr3d 2658	. . . . . 6
347	346	mpteq2ia 4740	. . . . 5
348	336, 347	syl6eq 2672	. . . 4
349		negicn 10282	. . . . 5
350	349	a1i 11	. . . 4
351	11, 26, 27, 348, 350	dvmptcmul 23727	. . 3
352	351	trud 1493	. 2
353	13, 13	mulneg1i 10476	. . . . . 6
354	303	negeqi 10274	. . . . . 6
355		negneg1e1 11128	. . . . . 6
356	353, 354, 355	3eqtri 2648	. . . . 5
357	356	oveq1i 6660	. . . 4
358		divass 10703	. . . . . 6 $/\$ $/\$ $/\$
359	349, 13, 358	mp3an12 1414	. . . . 5 $/\$
360	114, 282, 359	syl2anc 693	. . . 4
361	357, 360	syl5reqr 2671	. . 3
362	361	mpteq2ia 4740	. 2
363	9, 352, 362	3eqtri 2648	1 arcsin

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384 $\/$ w3o 1036 $/\$ w3a 1037

wceq 1483

wtru 1484

wcel 1990

wne 2794

cvv 3200 $\$ cdif 3571

cun 3572

cin 3573

wss 3574

c0 3915

csn 4177

cpr 4179 class class class wbr 4653

cmpt 4729

crn 5115

cres 5116

wf 5884

wf1o 5887

cfv 5888 (class class class)co 6650

cc 9934

cr 9935

cc0 9936

c1 9937

ci 9938

caddc 9939

cmul 9941

cpnf 10071

cmnf 10072

cxr 10073

clt 10074

cle 10075

cmin 10266

cneg 10267

cdiv 10684

cn 11020

c2 11070

crp 11832

cioo 12175

cioc 12176

cico 12177

cexp 12860

cre 13837

csqrt 13973

cabs 13974 ↾_t crest 16081

ctopn 16082

ctg 16098 ℂ_fldccnfld 19746 TopOnctopon 20715

ccld 20820

cdv 23627

clog 24301 arcsincasin 24589

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ioc 12180 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-fac 13061 df-bc 13090 df-hash 13118 df-shft 13807 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-limsup 14202 df-clim 14219 df-rlim 14220 df-sum 14417 df-ef 14798 df-sin 14800 df-cos 14801 df-tan 14802 df-pi 14803 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-rest 16083 df-topn 16084 df-0g 16102 df-gsum 16103 df-topgen 16104 df-pt 16105 df-prds 16108 df-xrs 16162 df-qtop 16167 df-imas 16168 df-xps 16170 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-mulg 17541 df-cntz 17750 df-cmn 18195 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-fbas 19743 df-fg 19744 df-cnfld 19747 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-nei 20902 df-lp 20940 df-perf 20941 df-cn 21031 df-cnp 21032 df-haus 21119 df-cmp 21190 df-tx 21365 df-hmeo 21558 df-fil 21650 df-fm 21742 df-flim 21743 df-flf 21744 df-xms 22125 df-ms 22126 df-tms 22127 df-cncf 22681 df-limc 23630 df-dv 23631 df-log 24303 df-cxp 24304 df-asin 24592

This theorem is referenced by: dvacos 33497 dvreasin 33498

W3C validator