areacirclem5 - Mathbox for Brendan Leahy

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

Theorem areacirclem5 26185

Description: Endpoint-inclusive continuity of antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 31-Aug-2017.)

**Assertion**
Ref	Expression
areacirclem5	arcsin

Distinct variable group:

**Proof of Theorem areacirclem5**
Step	Hyp	Ref	Expression
1		eqid 2404	. 2 ℂ_fld ℂ_fld
2	1	mulcn 18850	. . 3 ℂ_fld ℂ_fld ℂ_fld
3	2	a1i 11	. 2 ℂ_fld ℂ_fld ℂ_fld
4		rpcn 10576	. . . 4
5	4	sqcld 11476	. . 3
6		rpre 10574	. . . . . 6
7	6	renegcld 9420	. . . . 5
8		iccssre 10948	. . . . 5 $/\$
9	7, 6, 8	syl2anc 643	. . . 4
10		ax-resscn 9003	. . . 4
11	9, 10	syl6ss 3320	. . 3
12		ssid 3327	. . . 4
13	12	a1i 11	. . 3
14		cncfmptc 18894	. . 3 $/\$ $/\$
15	5, 11, 13, 14	syl3anc 1184	. 2
16	1	addcn 18848	. . . 4 ℂ_fld ℂ_fld ℂ_fld
17	16	a1i 11	. . 3 ℂ_fld ℂ_fld ℂ_fld
18	11	sselda 3308	. . . . . . . 8 $/\$
19	4	adantr 452	. . . . . . . 8 $/\$
20		rpne0 10583	. . . . . . . . 9
21	20	adantr 452	. . . . . . . 8 $/\$
22	18, 19, 21	divcld 9746	. . . . . . 7 $/\$
23		asinval 20675	. . . . . . 7 arcsin
24	22, 23	syl 16	. . . . . 6 $/\$ arcsin
25		ax-icn 9005	. . . . . . . . . . . 12
26	25	a1i 11	. . . . . . . . . . 11 $/\$
27	26, 22	mulcld 9064	. . . . . . . . . 10 $/\$
28		ax-1cn 9004	. . . . . . . . . . . . 13
29	28	a1i 11	. . . . . . . . . . . 12 $/\$
30	22	sqcld 11476	. . . . . . . . . . . 12 $/\$
31	29, 30	subcld 9367	. . . . . . . . . . 11 $/\$
32	31	sqrcld 12194	. . . . . . . . . 10 $/\$
33	27, 32	addcld 9063	. . . . . . . . 9 $/\$
34		0lt1 9506	. . . . . . . . . . . . . . 15
35		simp3 959	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
36	35	oveq1d 6055	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
37	4, 20	div0d 9745	. . . . . . . . . . . . . . . . . . . . . . 23
38	37	3ad2ant1 978	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
39	36, 38	eqtrd 2436	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
40	39	oveq2d 6056	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
41	25	mul01i 9212	. . . . . . . . . . . . . . . . . . . 20
42	40, 41	syl6eq 2452	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
43	39	oveq1d 6055	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
44	43	oveq2d 6056	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
45	44	fveq2d 5691	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
46		sq0 11428	. . . . . . . . . . . . . . . . . . . . . . . 24
47	46	oveq2i 6051	. . . . . . . . . . . . . . . . . . . . . . 23
48	28	subid1i 9328	. . . . . . . . . . . . . . . . . . . . . . 23
49	47, 48	eqtri 2424	. . . . . . . . . . . . . . . . . . . . . 22
50	49	fveq2i 5690	. . . . . . . . . . . . . . . . . . . . 21
51		sqr1 12032	. . . . . . . . . . . . . . . . . . . . 21
52	50, 51	eqtri 2424	. . . . . . . . . . . . . . . . . . . 20
53	45, 52	syl6eq 2452	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
54	42, 53	oveq12d 6058	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
55		0p1e1 10049	. . . . . . . . . . . . . . . . . 18
56	54, 55	syl6eq 2452	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
57	56	breq2d 4184	. . . . . . . . . . . . . . . 16 $/\$ $/\$
58		0re 9047	. . . . . . . . . . . . . . . . . 18
59	58	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
60		1re 9046	. . . . . . . . . . . . . . . . . . 19
61	60	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
62	56, 61	eqeltrd 2478	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
63	59, 62	ltnled 9176	. . . . . . . . . . . . . . . 16 $/\$ $/\$
64	57, 63	bitr3d 247	. . . . . . . . . . . . . . 15 $/\$ $/\$
65	34, 64	mpbii 203	. . . . . . . . . . . . . 14 $/\$ $/\$
66	65	3expa 1153	. . . . . . . . . . . . 13 $/\$ $/\$
67	66	olcd 383	. . . . . . . . . . . 12 $/\$ $/\$ $\/$
68		inelr 9946	. . . . . . . . . . . . . 14
69	27, 32	pncand 9368	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
70	69	3adant3 977	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
71	70	oveq1d 6055	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
72	25	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
73	22	3adant3 977	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
74	4	3ad2ant1 978	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
75	18	3adant3 977	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
76		simp3 959	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
77	74, 75, 76	divcld 9746	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
78	72, 73, 77	mulassd 9067	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
79	71, 78	eqtrd 2436	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
80	20	3ad2ant1 978	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
81	75, 74, 76, 80	divcan6d 9765	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
82	81	oveq2d 6056	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
83	72	mulid1d 9061	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
84	79, 82, 83	3eqtrrd 2441	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
85	84	adantr 452	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
86		simpr 448	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
87	60	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
88	9	sselda 3308	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
89	6	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
90	88, 89, 21	redivcld 9798	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
91	90	resqcld 11504	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
92	87, 91	resubcld 9421	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
93		elicc2 10931	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
94	7, 6, 93	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
95	60	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
96		simpr 448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
97	6	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
98	20	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
99	96, 97, 98	redivcld 9798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
100	99	resqcld 11504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
101	95, 100	subge0d 9572	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
102		recn 9036	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
103	102	adantl 453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
104	4	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
105	103, 104, 98	sqdivd 11491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
106	105	breq1d 4182	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
107		resqcl 11404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
108	107	adantl 453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
109	6	resqcld 11504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
110		rpgt0 10579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
111	58	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
112		0le0 10037	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
113	112	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
114		rpge0 10580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
115	111, 6, 113, 114	lt2sqd 11512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
116	46	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
117	116	breq1d 4182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
118	115, 117	bitrd 245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
119	110, 118	mpbid 202	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
120	109, 119	elrpd 10602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
121	120	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
122	108, 95, 121	ledivmuld 10653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
123		absresq 12062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
124	123	eqcomd 2409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
125	5	mulid1d 9061	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
126	124, 125	breqan12rd 4188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
127	102	abscld 12193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
128	127	adantl 453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
129	102	absge0d 12201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
130	129	adantl 453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
131	114	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
132	128, 97, 130, 131	le2sqd 11513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
133	96, 97	absled 12188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
134	126, 132, 133	3bitr2d 273	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
135	122, 134	bitrd 245	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
136	101, 106, 135	3bitrrd 272	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
137	136	biimpd 199	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
138	137	exp4b 591	. . . . . . . . . . . . . . . . . . . . . . . . 25
139	138	3impd 1167	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
140	94, 139	sylbid 207	. . . . . . . . . . . . . . . . . . . . . . 23
141	140	imp 419	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
142	92, 141	resqrcld 12175	. . . . . . . . . . . . . . . . . . . . 21 $/\$
143	142	3adant3 977	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
144	143	adantr 452	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
145	86, 144	resubcld 9421	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
146	6	3ad2ant1 978	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
147	88	3adant3 977	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
148	146, 147, 76	redivcld 9798	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
149	148	adantr 452	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
150	145, 149	remulcld 9072	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
151	85, 150	eqeltrd 2478	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
152	151	ex 424	. . . . . . . . . . . . . . 15 $/\$ $/\$
153	152	3expa 1153	. . . . . . . . . . . . . 14 $/\$ $/\$
154	68, 153	mtoi 171	. . . . . . . . . . . . 13 $/\$ $/\$
155	154	orcd 382	. . . . . . . . . . . 12 $/\$ $/\$ $\/$
156	67, 155	pm2.61dane 2645	. . . . . . . . . . 11 $/\$ $\/$
157		ianor 475	. . . . . . . . . . 11 $/\$ $\/$
158	156, 157	sylibr 204	. . . . . . . . . 10 $/\$ $/\$
159		mnfxr 10670	. . . . . . . . . . . 12
160		elioc2 10929	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
161	159, 58, 160	mp2an 654	. . . . . . . . . . 11 $/\$ $/\$
162		3simpb 955	. . . . . . . . . . 11 $/\$ $/\$ $/\$
163	161, 162	sylbi 188	. . . . . . . . . 10 $/\$
164	158, 163	nsyl 115	. . . . . . . . 9 $/\$
165	33, 164	eldifd 3291	. . . . . . . 8 $/\$ $\$
166		fvres 5704	. . . . . . . 8 $\$ $\$
167	165, 166	syl 16	. . . . . . 7 $/\$ $\$
168	167	oveq2d 6056	. . . . . 6 $/\$ $\$
169	24, 168	eqtr4d 2439	. . . . 5 $/\$ arcsin $\$
170	169	mpteq2dva 4255	. . . 4 arcsin $\$
171	25	negcli 9324	. . . . . . 7
172	171	a1i 11	. . . . . 6
173		cncfmptc 18894	. . . . . 6 $/\$ $/\$
174	172, 11, 13, 173	syl3anc 1184	. . . . 5
175	1	cnfldtopon 18770	. . . . . . . . 9 ℂ_fld TopOn
176	175	a1i 11	. . . . . . . 8 ℂ_fld TopOn
177		resttopon 17179	. . . . . . . 8 ℂ_fld TopOn $/\$ ℂ_fld ↾_t TopOn
178	176, 11, 177	syl2anc 643	. . . . . . 7 ℂ_fld ↾_t TopOn
179		eqid 2404	. . . . . . . . . 10
180	165, 179	fmptd 5852	. . . . . . . . 9 $\$
181		difssd 3435	. . . . . . . . . 10 $\$
182	18, 19, 21	divrec2d 9750	. . . . . . . . . . . . . . 15 $/\$
183	182	oveq2d 6056	. . . . . . . . . . . . . 14 $/\$
184	4, 20	reccld 9739	. . . . . . . . . . . . . . . 16
185	184	adantr 452	. . . . . . . . . . . . . . 15 $/\$
186	26, 185, 18	mulassd 9067	. . . . . . . . . . . . . 14 $/\$
187	183, 186	eqtr4d 2439	. . . . . . . . . . . . 13 $/\$
188	187	mpteq2dva 4255	. . . . . . . . . . . 12
189	25	a1i 11	. . . . . . . . . . . . . . 15
190	189, 184	mulcld 9064	. . . . . . . . . . . . . 14
191		cncfmptc 18894	. . . . . . . . . . . . . 14 $/\$ $/\$
192	190, 11, 13, 191	syl3anc 1184	. . . . . . . . . . . . 13
193		cncfmptid 18895	. . . . . . . . . . . . . 14 $/\$
194	11, 13, 193	syl2anc 643	. . . . . . . . . . . . 13
195	1, 3, 192, 194	cncfmpt2f 18897	. . . . . . . . . . . 12
196	188, 195	eqeltrd 2478	. . . . . . . . . . 11
197	19, 32	mulcld 9064	. . . . . . . . . . . . . . 15 $/\$
198	197, 19, 21	divrec2d 9750	. . . . . . . . . . . . . 14 $/\$
199	32, 19, 21	divcan3d 9751	. . . . . . . . . . . . . 14 $/\$
200	109	adantr 452	. . . . . . . . . . . . . . . . 17 $/\$
201	6	sqge0d 11505	. . . . . . . . . . . . . . . . . 18
202	201	adantr 452	. . . . . . . . . . . . . . . . 17 $/\$
203	200, 202, 92, 141	sqrmuld 12182	. . . . . . . . . . . . . . . 16 $/\$
204	5	adantr 452	. . . . . . . . . . . . . . . . . . 19 $/\$
205	204, 29, 30	subdid 9445	. . . . . . . . . . . . . . . . . 18 $/\$
206	204	mulid1d 9061	. . . . . . . . . . . . . . . . . . 19 $/\$
207	18, 19, 21	sqdivd 11491	. . . . . . . . . . . . . . . . . . . . 21 $/\$
208	207	oveq2d 6056	. . . . . . . . . . . . . . . . . . . 20 $/\$
209	18	sqcld 11476	. . . . . . . . . . . . . . . . . . . . 21 $/\$
210		sqne0 11403	. . . . . . . . . . . . . . . . . . . . . . . 24
211	4, 210	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23
212	20, 211	mpbird 224	. . . . . . . . . . . . . . . . . . . . . 22
213	212	adantr 452	. . . . . . . . . . . . . . . . . . . . 21 $/\$
214	209, 204, 213	divcan2d 9748	. . . . . . . . . . . . . . . . . . . 20 $/\$
215	208, 214	eqtrd 2436	. . . . . . . . . . . . . . . . . . 19 $/\$
216	206, 215	oveq12d 6058	. . . . . . . . . . . . . . . . . 18 $/\$
217	205, 216	eqtrd 2436	. . . . . . . . . . . . . . . . 17 $/\$
218	217	fveq2d 5691	. . . . . . . . . . . . . . . 16 $/\$
219	114	adantr 452	. . . . . . . . . . . . . . . . . 18 $/\$
220	89, 219	sqrsqd 12177	. . . . . . . . . . . . . . . . 17 $/\$
221	220	oveq1d 6055	. . . . . . . . . . . . . . . 16 $/\$
222	203, 218, 221	3eqtr3rd 2445	. . . . . . . . . . . . . . 15 $/\$
223	222	oveq2d 6056	. . . . . . . . . . . . . 14 $/\$
224	198, 199, 223	3eqtr3d 2444	. . . . . . . . . . . . 13 $/\$
225	224	mpteq2dva 4255	. . . . . . . . . . . 12
226		cncfmptc 18894	. . . . . . . . . . . . . 14 $/\$ $/\$
227	184, 11, 13, 226	syl3anc 1184	. . . . . . . . . . . . 13
228		areacirclem4 26183	. . . . . . . . . . . . . 14 $/\$
229	6, 114, 228	syl2anc 643	. . . . . . . . . . . . 13
230	1, 3, 227, 229	cncfmpt2f 18897	. . . . . . . . . . . 12
231	225, 230	eqeltrd 2478	. . . . . . . . . . 11
232	1, 17, 196, 231	cncfmpt2f 18897	. . . . . . . . . 10
233		cncffvrn 18881	. . . . . . . . . 10 $\$ $/\$ $\$ $\$
234	181, 232, 233	syl2anc 643	. . . . . . . . 9 $\$ $\$
235	180, 234	mpbird 224	. . . . . . . 8 $\$
236		eqid 2404	. . . . . . . . . 10 ℂ_fld ↾_t ℂ_fld ↾_t
237		eqid 2404	. . . . . . . . . 10 ℂ_fld ↾_t $\$ ℂ_fld ↾_t $\$
238	1, 236, 237	cncfcn 18892	. . . . . . . . 9 $/\$ $\$ $\$ ℂ_fld ↾_t ℂ_fld ↾_t $\$
239	11, 181, 238	syl2anc 643	. . . . . . . 8 $\$ ℂ_fld ↾_t ℂ_fld ↾_t $\$
240	235, 239	eleqtrd 2480	. . . . . . 7 ℂ_fld ↾_t ℂ_fld ↾_t $\$
241		eqid 2404	. . . . . . . . . 10 $\$ $\$
242	241	logcn 20491	. . . . . . . . 9 $\$ $\$
243		difss 3434	. . . . . . . . . 10 $\$
244		eqid 2404	. . . . . . . . . . 11 ℂ_fld ↾_t ℂ_fld ↾_t
245	1, 237, 244	cncfcn 18892	. . . . . . . . . 10 $\$ $/\$ $\$ ℂ_fld ↾_t $\$ ℂ_fld ↾_t
246	243, 12, 245	mp2an 654	. . . . . . . . 9 $\$ ℂ_fld ↾_t $\$ ℂ_fld ↾_t
247	242, 246	eleqtri 2476	. . . . . . . 8 $\$ ℂ_fld ↾_t $\$ ℂ_fld ↾_t
248	247	a1i 11	. . . . . . 7 $\$ ℂ_fld ↾_t $\$ ℂ_fld ↾_t
249	178, 240, 248	cnmpt11f 17649	. . . . . 6 $\$ ℂ_fld ↾_t ℂ_fld ↾_t
250	1, 236, 244	cncfcn 18892	. . . . . . 7 $/\$ ℂ_fld ↾_t ℂ_fld ↾_t
251	11, 13, 250	syl2anc 643	. . . . . 6 ℂ_fld ↾_t ℂ_fld ↾_t
252	249, 251	eleqtrrd 2481	. . . . 5 $\$
253	1, 3, 174, 252	cncfmpt2f 18897	. . . 4 $\$
254	170, 253	eqeltrd 2478	. . 3 arcsin
255	224	oveq2d 6056	. . . . . 6 $/\$
256	204, 209	subcld 9367	. . . . . . . 8 $/\$
257	256	sqrcld 12194	. . . . . . 7 $/\$
258	22, 185, 257	mulassd 9067	. . . . . 6 $/\$
259	18, 19, 21	divrecd 9749	. . . . . . . . 9 $/\$
260	259	oveq1d 6055	. . . . . . . 8 $/\$
261	18, 185, 185	mulassd 9067	. . . . . . . 8 $/\$
262	260, 261	eqtrd 2436	. . . . . . 7 $/\$
263	262	oveq1d 6055	. . . . . 6 $/\$
264	255, 258, 263	3eqtr2d 2442	. . . . 5 $/\$
265	264	mpteq2dva 4255	. . . 4
266	184, 184	mulcld 9064	. . . . . . 7
267		cncfmptc 18894	. . . . . . 7 $/\$ $/\$
268	266, 11, 13, 267	syl3anc 1184	. . . . . 6
269	1, 3, 194, 268	cncfmpt2f 18897	. . . . 5
270	1, 3, 269, 229	cncfmpt2f 18897	. . . 4
271	265, 270	eqeltrd 2478	. . 3
272	1, 17, 254, 271	cncfmpt2f 18897	. 2 arcsin
273	1, 3, 15, 272	cncfmpt2f 18897	1 arcsin

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $\/$ wo 358 $/\$ wa 359 $/\$ w3a 936

wceq 1649

wcel 1721

wne 2567 $\$ cdif 3277

wss 3280 class class class wbr 4172

cmpt 4226

cres 4839

wf 5409

cfv 5413 (class class class)co 6040

cc 8944

cr 8945

cc0 8946

c1 8947

ci 8948

caddc 8949

cmul 8951

cmnf 9074

cxr 9075

clt 9076

cle 9077

cmin 9247

cneg 9248

cdiv 9633

c2 10005

crp 10568

cioc 10873

cicc 10875

cexp 11337

csqr 11993

cabs 11994 ↾_t crest 13603

ctopn 13604 ℂ_fldccnfld 16658 TopOnctopon 16914

ccn 17242

ctx 17545

ccncf 18859

clog 20405 arcsincasin 20655

This theorem is referenced by: areacirc 26187

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-inf2 7552 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024 ax-addf 9025 ax-mulf 9026

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-iin 4056 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-se 4502 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-of 6264 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-2o 6684 df-oadd 6687 df-er 6864 df-map 6979 df-pm 6980 df-ixp 7023 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-fi 7374 df-sup 7404 df-oi 7435 df-card 7782 df-cda 8004 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-4 10016 df-5 10017 df-6 10018 df-7 10019 df-8 10020 df-9 10021 df-10 10022 df-n0 10178 df-z 10239 df-dec 10339 df-uz 10445 df-q 10531 df-rp 10569 df-xneg 10666 df-xadd 10667 df-xmul 10668 df-ioo 10876 df-ioc 10877 df-ico 10878 df-icc 10879 df-fz 11000 df-fzo 11091 df-fl 11157 df-mod 11206 df-seq 11279 df-exp 11338 df-fac 11522 df-bc 11549 df-hash 11574 df-shft 11837 df-cj 11859 df-re 11860 df-im 11861 df-sqr 11995 df-abs 11996 df-limsup 12220 df-clim 12237 df-rlim 12238 df-sum 12435 df-ef 12625 df-sin 12627 df-cos 12628 df-tan 12629 df-pi 12630 df-struct 13426 df-ndx 13427 df-slot 13428 df-base 13429 df-sets 13430 df-ress 13431 df-plusg 13497 df-mulr 13498 df-starv 13499 df-sca 13500 df-vsca 13501 df-tset 13503 df-ple 13504 df-ds 13506 df-unif 13507 df-hom 13508 df-cco 13509 df-rest 13605 df-topn 13606 df-topgen 13622 df-pt 13623 df-prds 13626 df-xrs 13681 df-0g 13682 df-gsum 13683 df-qtop 13688 df-imas 13689 df-xps 13691 df-mre 13766 df-mrc 13767 df-acs 13769 df-mnd 14645 df-submnd 14694 df-mulg 14770 df-cntz 15071 df-cmn 15369 df-psmet 16649 df-xmet 16650 df-met 16651 df-bl 16652 df-mopn 16653 df-fbas 16654 df-fg 16655 df-cnfld 16659 df-top 16918 df-bases 16920 df-topon 16921 df-topsp 16922 df-cld 17038 df-ntr 17039 df-cls 17040 df-nei 17117 df-lp 17155 df-perf 17156 df-cn 17245 df-cnp 17246 df-haus 17333 df-cmp 17404 df-tx 17547 df-hmeo 17740 df-fil 17831 df-fm 17923 df-flim 17924 df-flf 17925 df-xms 18303 df-ms 18304 df-tms 18305 df-cncf 18861 df-limc 19706 df-dv 19707 df-log 20407 df-cxp 20408 df-asin 20658

W3C validator