Theorem areacirclem1 30083

Description: Antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 28-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.)

Assertion

Ref	Expression
areacirclem1	|- ( R e. RR+ -> ( RR _D ( t e. ( -u R (,) R ) |-> ( ( R ^ 2 ) x. ( (arcsin ` ( t / R ) ) + ( ( t / R ) x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) ) ) ) = ( t e. ( -u R (,) R ) |-> ( 2 x. ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )

Distinct variable group:   t, R

Proof of Theorem areacirclem1

Dummy variables u v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		reelprrecn 9587	. . . 4 |- RR e. { RR , CC }
2	1	a1i 11	. . 3 |- ( R e. RR+ -> RR e. { RR , CC } )
3		elioore 11570	. . . . . . . 8 |- ( t e. ( -u R (,) R ) -> t e. RR )
4	3	recnd 9625	. . . . . . 7 |- ( t e. ( -u R (,) R ) -> t e. CC )
5	4	adantl 466	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> t e. CC )
6		rpcn 11239	. . . . . . 7 |- ( R e. RR+ -> R e. CC )
7	6	adantr 465	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> R e. CC )
8		rpne0 11246	. . . . . . 7 |- ( R e. RR+ -> R =/= 0 )
9	8	adantr 465	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> R =/= 0 )
10	5, 7, 9	divcld 10327	. . . . 5 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( t / R ) e. CC )
11		asincl 23182	. . . . 5 |- ( ( t / R ) e. CC -> (arcsin ` ( t / R ) ) e. CC )
12	10, 11	syl 16	. . . 4 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> (arcsin ` ( t / R ) ) e. CC )
13		1cnd 9615	. . . . . . 7 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 1 e. CC )
14	10	sqcld 12290	. . . . . . 7 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) ^ 2 ) e. CC )
15	13, 14	subcld 9936	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 1 - ( ( t / R ) ^ 2 ) ) e. CC )
16	15	sqrtcld 13250	. . . . 5 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) e. CC )
17	10, 16	mulcld 9619	. . . 4 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. CC )
18	12, 17	addcld 9618	. . 3 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( (arcsin ` ( t / R ) ) + ( ( t / R ) x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) e. CC )
19		ovex 6309	. . . 4 |- ( ( 2 x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) x. ( 1 / R ) ) e. _V
20	19	a1i 11	. . 3 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( 2 x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) x. ( 1 / R ) ) e. _V )
21		rpre 11237	. . . . . . . . . 10 |- ( R e. RR+ -> R e. RR )
22	21	renegcld 9993	. . . . . . . . 9 |- ( R e. RR+ -> -u R e. RR )
23	22	rexrd 9646	. . . . . . . 8 |- ( R e. RR+ -> -u R e. RR* )
24		rpxr 11238	. . . . . . . 8 |- ( R e. RR+ -> R e. RR* )
25		elioo2 11581	. . . . . . . 8 |- ( ( -u R e. RR* /\ R e. RR* ) -> ( t e. ( -u R (,) R ) <-> ( t e. RR /\ -u R < t /\ t < R ) ) )
26	23, 24, 25	syl2anc 661	. . . . . . 7 |- ( R e. RR+ -> ( t e. ( -u R (,) R ) <-> ( t e. RR /\ -u R < t /\ t < R ) ) )
27		simpr 461	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. RR ) -> t e. RR )
28	21	adantr 465	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. RR ) -> R e. RR )
29	8	adantr 465	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. RR ) -> R =/= 0 )
30	27, 28, 29	redivcld 10379	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. RR ) -> ( t / R ) e. RR )
31	30	a1d 25	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) -> ( t / R ) e. RR ) )
32	6	mulm1d 10015	. . . . . . . . . . . . . . 15 |- ( R e. RR+ -> ( -u 1 x. R ) = -u R )
33	32	adantr 465	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. RR ) -> ( -u 1 x. R ) = -u R )
34	33	breq1d 4447	. . . . . . . . . . . . 13 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u 1 x. R ) < t <-> -u R < t ) )
35		neg1rr 10647	. . . . . . . . . . . . . . 15 |- -u 1 e. RR
36	35	a1i 11	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. RR ) -> -u 1 e. RR )
37		simpl 457	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. RR ) -> R e. RR+ )
38	36, 27, 37	ltmuldivd 11310	. . . . . . . . . . . . 13 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u 1 x. R ) < t <-> -u 1 < ( t / R ) ) )
39	34, 38	bitr3d 255	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. RR ) -> ( -u R < t <-> -u 1 < ( t / R ) ) )
40	39	biimpd 207	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. RR ) -> ( -u R < t -> -u 1 < ( t / R ) ) )
41	40	adantrd 468	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) -> -u 1 < ( t / R ) ) )
42		1red 9614	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. RR ) -> 1 e. RR )
43	27, 42, 37	ltdivmuld 11314	. . . . . . . . . . . . 13 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( t / R ) < 1 <-> t < ( R x. 1 ) ) )
44	6	mulid1d 9616	. . . . . . . . . . . . . . 15 |- ( R e. RR+ -> ( R x. 1 ) = R )
45	44	adantr 465	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. RR ) -> ( R x. 1 ) = R )
46	45	breq2d 4449	. . . . . . . . . . . . 13 |- ( ( R e. RR+ /\ t e. RR ) -> ( t < ( R x. 1 ) <-> t < R ) )
47	43, 46	bitr2d 254	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. RR ) -> ( t < R <-> ( t / R ) < 1 ) )
48	47	biimpd 207	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. RR ) -> ( t < R -> ( t / R ) < 1 ) )
49	48	adantld 467	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) -> ( t / R ) < 1 ) )
50	31, 41, 49	3jcad 1178	. . . . . . . . 9 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) -> ( ( t / R ) e. RR /\ -u 1 < ( t / R ) /\ ( t / R ) < 1 ) ) )
51	50	exp4b 607	. . . . . . . 8 |- ( R e. RR+ -> ( t e. RR -> ( -u R < t -> ( t < R -> ( ( t / R ) e. RR /\ -u 1 < ( t / R ) /\ ( t / R ) < 1 ) ) ) ) )
52	51	3impd 1211	. . . . . . 7 |- ( R e. RR+ -> ( ( t e. RR /\ -u R < t /\ t < R ) -> ( ( t / R ) e. RR /\ -u 1 < ( t / R ) /\ ( t / R ) < 1 ) ) )
53	26, 52	sylbid 215	. . . . . 6 |- ( R e. RR+ -> ( t e. ( -u R (,) R ) -> ( ( t / R ) e. RR /\ -u 1 < ( t / R ) /\ ( t / R ) < 1 ) ) )
54	53	imp 429	. . . . 5 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) e. RR /\ -u 1 < ( t / R ) /\ ( t / R ) < 1 ) )
55	35	rexri 9649	. . . . . 6 |- -u 1 e. RR*
56		1re 9598	. . . . . . 7 |- 1 e. RR
57	56	rexri 9649	. . . . . 6 |- 1 e. RR*
58		elioo2 11581	. . . . . 6 |- ( ( -u 1 e. RR* /\ 1 e. RR* ) -> ( ( t / R ) e. ( -u 1 (,) 1 ) <-> ( ( t / R ) e. RR /\ -u 1 < ( t / R ) /\ ( t / R ) < 1 ) ) )
59	55, 57, 58	mp2an 672	. . . . 5 |- ( ( t / R ) e. ( -u 1 (,) 1 ) <-> ( ( t / R ) e. RR /\ -u 1 < ( t / R ) /\ ( t / R ) < 1 ) )
60	54, 59	sylibr 212	. . . 4 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( t / R ) e. ( -u 1 (,) 1 ) )
61		ovex 6309	. . . . 5 |- ( 1 / R ) e. _V
62	61	a1i 11	. . . 4 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 1 / R ) e. _V )
63		elioore 11570	. . . . . . 7 |- ( u e. ( -u 1 (,) 1 ) -> u e. RR )
64	63	recnd 9625	. . . . . 6 |- ( u e. ( -u 1 (,) 1 ) -> u e. CC )
65		asincl 23182	. . . . . . 7 |- ( u e. CC -> (arcsin ` u ) e. CC )
66		id 22	. . . . . . . 8 |- ( u e. CC -> u e. CC )
67		1cnd 9615	. . . . . . . . . 10 |- ( u e. CC -> 1 e. CC )
68		sqcl 12212	. . . . . . . . . 10 |- ( u e. CC -> ( u ^ 2 ) e. CC )
69	67, 68	subcld 9936	. . . . . . . . 9 |- ( u e. CC -> ( 1 - ( u ^ 2 ) ) e. CC )
70	69	sqrtcld 13250	. . . . . . . 8 |- ( u e. CC -> ( sqr ` ( 1 - ( u ^ 2 ) ) ) e. CC )
71	66, 70	mulcld 9619	. . . . . . 7 |- ( u e. CC -> ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
72	65, 71	addcld 9618	. . . . . 6 |- ( u e. CC -> ( (arcsin ` u ) + ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) e. CC )
73	64, 72	syl 16	. . . . 5 |- ( u e. ( -u 1 (,) 1 ) -> ( (arcsin ` u ) + ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) e. CC )
74	73	adantl 466	. . . 4 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( (arcsin ` u ) + ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) e. CC )
75		ovex 6309	. . . . 5 |- ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. _V
76	75	a1i 11	. . . 4 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. _V )
77		recn 9585	. . . . . . 7 |- ( t e. RR -> t e. CC )
78	77	adantl 466	. . . . . 6 |- ( ( R e. RR+ /\ t e. RR ) -> t e. CC )
79		1cnd 9615	. . . . . 6 |- ( ( R e. RR+ /\ t e. RR ) -> 1 e. CC )
80	2	dvmptid 22338	. . . . . 6 |- ( R e. RR+ -> ( RR _D ( t e. RR |-> t ) ) = ( t e. RR |-> 1 ) )
81		ioossre 11597	. . . . . . 7 |- ( -u R (,) R ) C_ RR
82	81	a1i 11	. . . . . 6 |- ( R e. RR+ -> ( -u R (,) R ) C_ RR )
83		eqid 2443	. . . . . . 7 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
84	83	tgioo2 21286	. . . . . 6 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
85		iooretop 21251	. . . . . . 7 |- ( -u R (,) R ) e. ( topGen ` ran (,) )
86	85	a1i 11	. . . . . 6 |- ( R e. RR+ -> ( -u R (,) R ) e. ( topGen ` ran (,) ) )
87	2, 78, 79, 80, 82, 84, 83, 86	dvmptres 22344	. . . . 5 |- ( R e. RR+ -> ( RR _D ( t e. ( -u R (,) R ) |-> t ) ) = ( t e. ( -u R (,) R ) |-> 1 ) )
88	2, 5, 13, 87, 6, 8	dvmptdivc 22346	. . . 4 |- ( R e. RR+ -> ( RR _D ( t e. ( -u R (,) R ) |-> ( t / R ) ) ) = ( t e. ( -u R (,) R ) |-> ( 1 / R ) ) )
89	64, 65	syl 16	. . . . . . 7 |- ( u e. ( -u 1 (,) 1 ) -> (arcsin ` u ) e. CC )
90	89	adantl 466	. . . . . 6 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> (arcsin ` u ) e. CC )
91		ovex 6309	. . . . . . 7 |- ( 1 / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. _V
92	91	a1i 11	. . . . . 6 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( 1 / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. _V )
93		dvreasin 30081	. . . . . . 7 |- ( RR _D (arcsin |` ( -u 1 (,) 1 ) ) ) = ( u e. ( -u 1 (,) 1 ) |-> ( 1 / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
94		asinf 23181	. . . . . . . . . 10 |- arcsin : CC --> CC
95	94	a1i 11	. . . . . . . . 9 |- ( R e. RR+ -> arcsin : CC --> CC )
96		ioossre 11597	. . . . . . . . . . 11 |- ( -u 1 (,) 1 ) C_ RR
97		ax-resscn 9552	. . . . . . . . . . 11 |- RR C_ CC
98	96, 97	sstri 3498	. . . . . . . . . 10 |- ( -u 1 (,) 1 ) C_ CC
99	98	a1i 11	. . . . . . . . 9 |- ( R e. RR+ -> ( -u 1 (,) 1 ) C_ CC )
100	95, 99	feqresmpt 5912	. . . . . . . 8 |- ( R e. RR+ -> (arcsin |` ( -u 1 (,) 1 ) ) = ( u e. ( -u 1 (,) 1 ) |-> (arcsin ` u ) ) )
101	100	oveq2d 6297	. . . . . . 7 |- ( R e. RR+ -> ( RR _D (arcsin |` ( -u 1 (,) 1 ) ) ) = ( RR _D ( u e. ( -u 1 (,) 1 ) |-> (arcsin ` u ) ) ) )
102	93, 101	syl5reqr 2499	. . . . . 6 |- ( R e. RR+ -> ( RR _D ( u e. ( -u 1 (,) 1 ) |-> (arcsin ` u ) ) ) = ( u e. ( -u 1 (,) 1 ) |-> ( 1 / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) )
103	64, 71	syl 16	. . . . . . 7 |- ( u e. ( -u 1 (,) 1 ) -> ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
104	103	adantl 466	. . . . . 6 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
105		ovex 6309	. . . . . . 7 |- ( ( 1 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( -u u / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) x. u ) ) e. _V
106	105	a1i 11	. . . . . 6 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( ( 1 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( -u u / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) x. u ) ) e. _V )
107	64	adantl 466	. . . . . . 7 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> u e. CC )
108		1cnd 9615	. . . . . . 7 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> 1 e. CC )
109		recn 9585	. . . . . . . . 9 |- ( u e. RR -> u e. CC )
110	109	adantl 466	. . . . . . . 8 |- ( ( R e. RR+ /\ u e. RR ) -> u e. CC )
111		1cnd 9615	. . . . . . . 8 |- ( ( R e. RR+ /\ u e. RR ) -> 1 e. CC )
112	2	dvmptid 22338	. . . . . . . 8 |- ( R e. RR+ -> ( RR _D ( u e. RR |-> u ) ) = ( u e. RR |-> 1 ) )
113	96	a1i 11	. . . . . . . 8 |- ( R e. RR+ -> ( -u 1 (,) 1 ) C_ RR )
114		iooretop 21251	. . . . . . . . 9 |- ( -u 1 (,) 1 ) e. ( topGen ` ran (,) )
115	114	a1i 11	. . . . . . . 8 |- ( R e. RR+ -> ( -u 1 (,) 1 ) e. ( topGen ` ran (,) ) )
116	2, 110, 111, 112, 113, 84, 83, 115	dvmptres 22344	. . . . . . 7 |- ( R e. RR+ -> ( RR _D ( u e. ( -u 1 (,) 1 ) |-> u ) ) = ( u e. ( -u 1 (,) 1 ) |-> 1 ) )
117	64, 70	syl 16	. . . . . . . 8 |- ( u e. ( -u 1 (,) 1 ) -> ( sqr ` ( 1 - ( u ^ 2 ) ) ) e. CC )
118	117	adantl 466	. . . . . . 7 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( sqr ` ( 1 - ( u ^ 2 ) ) ) e. CC )
119		ovex 6309	. . . . . . . 8 |- ( -u u / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. _V
120	119	a1i 11	. . . . . . 7 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( -u u / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. _V )
121		1red 9614	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> 1 e. RR )
122	63	resqcld 12318	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> ( u ^ 2 ) e. RR )
123	121, 122	resubcld 9994	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> ( 1 - ( u ^ 2 ) ) e. RR )
124		elioo2 11581	. . . . . . . . . . . . 13 |- ( ( -u 1 e. RR* /\ 1 e. RR* ) -> ( u e. ( -u 1 (,) 1 ) <-> ( u e. RR /\ -u 1 < u /\ u < 1 ) ) )
125	55, 57, 124	mp2an 672	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) <-> ( u e. RR /\ -u 1 < u /\ u < 1 ) )
126		id 22	. . . . . . . . . . . . . . . 16 |- ( u e. RR -> u e. RR )
127		1red 9614	. . . . . . . . . . . . . . . 16 |- ( u e. RR -> 1 e. RR )
128	126, 127	absltd 13243	. . . . . . . . . . . . . . 15 |- ( u e. RR -> ( ( abs ` u ) < 1 <-> ( -u 1 < u /\ u < 1 ) ) )
129	109	abscld 13249	. . . . . . . . . . . . . . . . 17 |- ( u e. RR -> ( abs ` u ) e. RR )
130	109	absge0d 13257	. . . . . . . . . . . . . . . . 17 |- ( u e. RR -> 0 <_ ( abs ` u ) )
131		0le1 10083	. . . . . . . . . . . . . . . . . 18 |- 0 <_ 1
132	131	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( u e. RR -> 0 <_ 1 )
133	129, 127, 130, 132	lt2sqd 12326	. . . . . . . . . . . . . . . 16 |- ( u e. RR -> ( ( abs ` u ) < 1 <-> ( ( abs ` u ) ^ 2 ) < ( 1 ^ 2 ) ) )
134		absresq 13117	. . . . . . . . . . . . . . . . 17 |- ( u e. RR -> ( ( abs ` u ) ^ 2 ) = ( u ^ 2 ) )
135		sq1 12244	. . . . . . . . . . . . . . . . . 18 |- ( 1 ^ 2 ) = 1
136	135	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( u e. RR -> ( 1 ^ 2 ) = 1 )
137	134, 136	breq12d 4450	. . . . . . . . . . . . . . . 16 |- ( u e. RR -> ( ( ( abs ` u ) ^ 2 ) < ( 1 ^ 2 ) <-> ( u ^ 2 ) < 1 ) )
138		resqcl 12217	. . . . . . . . . . . . . . . . 17 |- ( u e. RR -> ( u ^ 2 ) e. RR )
139	138, 127	posdifd 10146	. . . . . . . . . . . . . . . 16 |- ( u e. RR -> ( ( u ^ 2 ) < 1 <-> 0 < ( 1 - ( u ^ 2 ) ) ) )
140	133, 137, 139	3bitrd 279	. . . . . . . . . . . . . . 15 |- ( u e. RR -> ( ( abs ` u ) < 1 <-> 0 < ( 1 - ( u ^ 2 ) ) ) )
141	128, 140	bitr3d 255	. . . . . . . . . . . . . 14 |- ( u e. RR -> ( ( -u 1 < u /\ u < 1 ) <-> 0 < ( 1 - ( u ^ 2 ) ) ) )
142	141	biimpd 207	. . . . . . . . . . . . 13 |- ( u e. RR -> ( ( -u 1 < u /\ u < 1 ) -> 0 < ( 1 - ( u ^ 2 ) ) ) )
143	142	3impib 1195	. . . . . . . . . . . 12 |- ( ( u e. RR /\ -u 1 < u /\ u < 1 ) -> 0 < ( 1 - ( u ^ 2 ) ) )
144	125, 143	sylbi 195	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> 0 < ( 1 - ( u ^ 2 ) ) )
145	123, 144	elrpd 11265	. . . . . . . . . 10 |- ( u e. ( -u 1 (,) 1 ) -> ( 1 - ( u ^ 2 ) ) e. RR+ )
146	145	adantl 466	. . . . . . . . 9 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( 1 - ( u ^ 2 ) ) e. RR+ )
147		negex 9823	. . . . . . . . . 10 |- -u ( 2 x. u ) e. _V
148	147	a1i 11	. . . . . . . . 9 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> -u ( 2 x. u ) e. _V )
149		rpcn 11239	. . . . . . . . . . 11 |- ( v e. RR+ -> v e. CC )
150	149	sqrtcld 13250	. . . . . . . . . 10 |- ( v e. RR+ -> ( sqr ` v ) e. CC )
151	150	adantl 466	. . . . . . . . 9 |- ( ( R e. RR+ /\ v e. RR+ ) -> ( sqr ` v ) e. CC )
152		ovex 6309	. . . . . . . . . 10 |- ( 1 / ( 2 x. ( sqr ` v ) ) ) e. _V
153	152	a1i 11	. . . . . . . . 9 |- ( ( R e. RR+ /\ v e. RR+ ) -> ( 1 / ( 2 x. ( sqr ` v ) ) ) e. _V )
154		1cnd 9615	. . . . . . . . . . . 12 |- ( u e. RR -> 1 e. CC )
155	109	sqcld 12290	. . . . . . . . . . . 12 |- ( u e. RR -> ( u ^ 2 ) e. CC )
156	154, 155	subcld 9936	. . . . . . . . . . 11 |- ( u e. RR -> ( 1 - ( u ^ 2 ) ) e. CC )
157	156	adantl 466	. . . . . . . . . 10 |- ( ( R e. RR+ /\ u e. RR ) -> ( 1 - ( u ^ 2 ) ) e. CC )
158	147	a1i 11	. . . . . . . . . 10 |- ( ( R e. RR+ /\ u e. RR ) -> -u ( 2 x. u ) e. _V )
159		0red 9600	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ u e. RR ) -> 0 e. RR )
160		1cnd 9615	. . . . . . . . . . . . 13 |- ( R e. RR+ -> 1 e. CC )
161	2, 160	dvmptc 22339	. . . . . . . . . . . 12 |- ( R e. RR+ -> ( RR _D ( u e. RR |-> 1 ) ) = ( u e. RR |-> 0 ) )
162	155	adantl 466	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ u e. RR ) -> ( u ^ 2 ) e. CC )
163		ovex 6309	. . . . . . . . . . . . 13 |- ( 2 x. u ) e. _V
164	163	a1i 11	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ u e. RR ) -> ( 2 x. u ) e. _V )
165	83	cnfldtopon 21268	. . . . . . . . . . . . . 14 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
166		toponmax 19407	. . . . . . . . . . . . . 14 |- ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) -> CC e. ( TopOpen ` ℂfld ) )
167	165, 166	mp1i 12	. . . . . . . . . . . . 13 |- ( R e. RR+ -> CC e. ( TopOpen ` ℂfld ) )
168		df-ss 3475	. . . . . . . . . . . . . . 15 |- ( RR C_ CC <-> ( RR i^i CC ) = RR )
169	97, 168	mpbi 208	. . . . . . . . . . . . . 14 |- ( RR i^i CC ) = RR
170	169	a1i 11	. . . . . . . . . . . . 13 |- ( R e. RR+ -> ( RR i^i CC ) = RR )
171	68	adantl 466	. . . . . . . . . . . . 13 |- ( ( R e. RR+ /\ u e. CC ) -> ( u ^ 2 ) e. CC )
172	163	a1i 11	. . . . . . . . . . . . 13 |- ( ( R e. RR+ /\ u e. CC ) -> ( 2 x. u ) e. _V )
173		2nn 10700	. . . . . . . . . . . . . . . 16 |- 2 e. NN
174		dvexp 22334	. . . . . . . . . . . . . . . 16 |- ( 2 e. NN -> ( CC _D ( u e. CC |-> ( u ^ 2 ) ) ) = ( u e. CC |-> ( 2 x. ( u ^ ( 2 - 1 ) ) ) ) )
175	173, 174	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( CC _D ( u e. CC |-> ( u ^ 2 ) ) ) = ( u e. CC |-> ( 2 x. ( u ^ ( 2 - 1 ) ) ) )
176		2m1e1 10657	. . . . . . . . . . . . . . . . . . 19 |- ( 2 - 1 ) = 1
177	176	oveq2i 6292	. . . . . . . . . . . . . . . . . 18 |- ( u ^ ( 2 - 1 ) ) = ( u ^ 1 )
178		exp1 12154	. . . . . . . . . . . . . . . . . 18 |- ( u e. CC -> ( u ^ 1 ) = u )
179	177, 178	syl5eq 2496	. . . . . . . . . . . . . . . . 17 |- ( u e. CC -> ( u ^ ( 2 - 1 ) ) = u )
180	179	oveq2d 6297	. . . . . . . . . . . . . . . 16 |- ( u e. CC -> ( 2 x. ( u ^ ( 2 - 1 ) ) ) = ( 2 x. u ) )
181	180	mpteq2ia 4519	. . . . . . . . . . . . . . 15 |- ( u e. CC |-> ( 2 x. ( u ^ ( 2 - 1 ) ) ) ) = ( u e. CC |-> ( 2 x. u ) )
182	175, 181	eqtri 2472	. . . . . . . . . . . . . 14 |- ( CC _D ( u e. CC |-> ( u ^ 2 ) ) ) = ( u e. CC |-> ( 2 x. u ) )
183	182	a1i 11	. . . . . . . . . . . . 13 |- ( R e. RR+ -> ( CC _D ( u e. CC |-> ( u ^ 2 ) ) ) = ( u e. CC |-> ( 2 x. u ) ) )
184	83, 2, 167, 170, 171, 172, 183	dvmptres3 22337	. . . . . . . . . . . 12 |- ( R e. RR+ -> ( RR _D ( u e. RR |-> ( u ^ 2 ) ) ) = ( u e. RR |-> ( 2 x. u ) ) )
185	2, 111, 159, 161, 162, 164, 184	dvmptsub 22348	. . . . . . . . . . 11 |- ( R e. RR+ -> ( RR _D ( u e. RR |-> ( 1 - ( u ^ 2 ) ) ) ) = ( u e. RR |-> ( 0 - ( 2 x. u ) ) ) )
186		df-neg 9813	. . . . . . . . . . . 12 |- -u ( 2 x. u ) = ( 0 - ( 2 x. u ) )
187	186	mpteq2i 4520	. . . . . . . . . . 11 |- ( u e. RR |-> -u ( 2 x. u ) ) = ( u e. RR |-> ( 0 - ( 2 x. u ) ) )
188	185, 187	syl6eqr 2502	. . . . . . . . . 10 |- ( R e. RR+ -> ( RR _D ( u e. RR |-> ( 1 - ( u ^ 2 ) ) ) ) = ( u e. RR |-> -u ( 2 x. u ) ) )
189	2, 157, 158, 188, 113, 84, 83, 115	dvmptres 22344	. . . . . . . . 9 |- ( R e. RR+ -> ( RR _D ( u e. ( -u 1 (,) 1 ) |-> ( 1 - ( u ^ 2 ) ) ) ) = ( u e. ( -u 1 (,) 1 ) |-> -u ( 2 x. u ) ) )
190		dvsqrt 23096	. . . . . . . . . 10 |- ( RR _D ( v e. RR+ |-> ( sqr ` v ) ) ) = ( v e. RR+ |-> ( 1 / ( 2 x. ( sqr ` v ) ) ) )
191	190	a1i 11	. . . . . . . . 9 |- ( R e. RR+ -> ( RR _D ( v e. RR+ |-> ( sqr ` v ) ) ) = ( v e. RR+ |-> ( 1 / ( 2 x. ( sqr ` v ) ) ) ) )
192		fveq2 5856	. . . . . . . . 9 |- ( v = ( 1 - ( u ^ 2 ) ) -> ( sqr ` v ) = ( sqr ` ( 1 - ( u ^ 2 ) ) ) )
193	192	oveq2d 6297	. . . . . . . . . 10 |- ( v = ( 1 - ( u ^ 2 ) ) -> ( 2 x. ( sqr ` v ) ) = ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
194	193	oveq2d 6297	. . . . . . . . 9 |- ( v = ( 1 - ( u ^ 2 ) ) -> ( 1 / ( 2 x. ( sqr ` v ) ) ) = ( 1 / ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) )
195	2, 2, 146, 148, 151, 153, 189, 191, 192, 194	dvmptco 22353	. . . . . . . 8 |- ( R e. RR+ -> ( RR _D ( u e. ( -u 1 (,) 1 ) |-> ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) = ( u e. ( -u 1 (,) 1 ) |-> ( ( 1 / ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) x. -u ( 2 x. u ) ) ) )
196		2cnd 10615	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> 2 e. CC )
197	196, 64	mulneg2d 10017	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> ( 2 x. -u u ) = -u ( 2 x. u ) )
198	197	oveq1d 6296	. . . . . . . . . 10 |- ( u e. ( -u 1 (,) 1 ) -> ( ( 2 x. -u u ) / ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) = ( -u ( 2 x. u ) / ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) )
199	64	negcld 9923	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> -u u e. CC )
200	144	gt0ne0d 10124	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> ( 1 - ( u ^ 2 ) ) =/= 0 )
201	64, 69	syl 16	. . . . . . . . . . . . . . . 16 |- ( u e. ( -u 1 (,) 1 ) -> ( 1 - ( u ^ 2 ) ) e. CC )
202	201	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( u e. ( -u 1 (,) 1 ) /\ ( sqr ` ( 1 - ( u ^ 2 ) ) ) = 0 ) -> ( 1 - ( u ^ 2 ) ) e. CC )
203		simpr 461	. . . . . . . . . . . . . . 15 |- ( ( u e. ( -u 1 (,) 1 ) /\ ( sqr ` ( 1 - ( u ^ 2 ) ) ) = 0 ) -> ( sqr ` ( 1 - ( u ^ 2 ) ) ) = 0 )
204	202, 203	sqr00d 13254	. . . . . . . . . . . . . 14 |- ( ( u e. ( -u 1 (,) 1 ) /\ ( sqr ` ( 1 - ( u ^ 2 ) ) ) = 0 ) -> ( 1 - ( u ^ 2 ) ) = 0 )
205	204	ex 434	. . . . . . . . . . . . 13 |- ( u e. ( -u 1 (,) 1 ) -> ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) = 0 -> ( 1 - ( u ^ 2 ) ) = 0 ) )
206	205	necon3d 2667	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> ( ( 1 - ( u ^ 2 ) ) =/= 0 -> ( sqr ` ( 1 - ( u ^ 2 ) ) ) =/= 0 ) )
207	200, 206	mpd 15	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> ( sqr ` ( 1 - ( u ^ 2 ) ) ) =/= 0 )
208		2ne0 10635	. . . . . . . . . . . 12 |- 2 =/= 0
209	208	a1i 11	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> 2 =/= 0 )
210	199, 117, 196, 207, 209	divcan5d 10353	. . . . . . . . . 10 |- ( u e. ( -u 1 (,) 1 ) -> ( ( 2 x. -u u ) / ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) = ( -u u / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
211	196, 64	mulcld 9619	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> ( 2 x. u ) e. CC )
212	211	negcld 9923	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> -u ( 2 x. u ) e. CC )
213	196, 117	mulcld 9619	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
214	196, 117, 209, 207	mulne0d 10208	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) =/= 0 )
215	212, 213, 214	divrec2d 10331	. . . . . . . . . 10 |- ( u e. ( -u 1 (,) 1 ) -> ( -u ( 2 x. u ) / ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) = ( ( 1 / ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) x. -u ( 2 x. u ) ) )
216	198, 210, 215	3eqtr3rd 2493	. . . . . . . . 9 |- ( u e. ( -u 1 (,) 1 ) -> ( ( 1 / ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) x. -u ( 2 x. u ) ) = ( -u u / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
217	216	mpteq2ia 4519	. . . . . . . 8 |- ( u e. ( -u 1 (,) 1 ) |-> ( ( 1 / ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) x. -u ( 2 x. u ) ) ) = ( u e. ( -u 1 (,) 1 ) |-> ( -u u / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
218	195, 217	syl6eq 2500	. . . . . . 7 |- ( R e. RR+ -> ( RR _D ( u e. ( -u 1 (,) 1 ) |-> ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) = ( u e. ( -u 1 (,) 1 ) |-> ( -u u / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) )
219	2, 107, 108, 116, 118, 120, 218	dvmptmul 22342	. . . . . 6 |- ( R e. RR+ -> ( RR _D ( u e. ( -u 1 (,) 1 ) |-> ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) ) = ( u e. ( -u 1 (,) 1 ) |-> ( ( 1 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( -u u / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) x. u ) ) ) )
220	2, 90, 92, 102, 104, 106, 219	dvmptadd 22341	. . . . 5 |- ( R e. RR+ -> ( RR _D ( u e. ( -u 1 (,) 1 ) |-> ( (arcsin ` u ) + ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) ) ) = ( u e. ( -u 1 (,) 1 ) |-> ( ( 1 / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( 1 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( -u u / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) x. u ) ) ) ) )
221	117	mulid2d 9617	. . . . . . . . . 10 |- ( u e. ( -u 1 (,) 1 ) -> ( 1 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) = ( sqr ` ( 1 - ( u ^ 2 ) ) ) )
222	199, 117, 207	divcld 10327	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> ( -u u / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
223	222, 64	mulcomd 9620	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> ( ( -u u / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) x. u ) = ( u x. ( -u u / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) )
224	64, 199, 117, 207	divassd 10362	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> ( ( u x. -u u ) / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) = ( u x. ( -u u / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) )
225	64, 64	mulneg2d 10017	. . . . . . . . . . . . 13 |- ( u e. ( -u 1 (,) 1 ) -> ( u x. -u u ) = -u ( u x. u ) )
226	64	sqvald 12289	. . . . . . . . . . . . . 14 |- ( u e. ( -u 1 (,) 1 ) -> ( u ^ 2 ) = ( u x. u ) )
227	226	negeqd 9819	. . . . . . . . . . . . 13 |- ( u e. ( -u 1 (,) 1 ) -> -u ( u ^ 2 ) = -u ( u x. u ) )
228	225, 227	eqtr4d 2487	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> ( u x. -u u ) = -u ( u ^ 2 ) )
229	228	oveq1d 6296	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> ( ( u x. -u u ) / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) = ( -u ( u ^ 2 ) / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
230	223, 224, 229	3eqtr2d 2490	. . . . . . . . . 10 |- ( u e. ( -u 1 (,) 1 ) -> ( ( -u u / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) x. u ) = ( -u ( u ^ 2 ) / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
231	221, 230	oveq12d 6299	. . . . . . . . 9 |- ( u e. ( -u 1 (,) 1 ) -> ( ( 1 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( -u u / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) x. u ) ) = ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) + ( -u ( u ^ 2 ) / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) )
232	64	sqcld 12290	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> ( u ^ 2 ) e. CC )
233	232	negcld 9923	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> -u ( u ^ 2 ) e. CC )
234	233, 117, 207	divcld 10327	. . . . . . . . . 10 |- ( u e. ( -u 1 (,) 1 ) -> ( -u ( u ^ 2 ) / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
235	117, 234	addcomd 9785	. . . . . . . . 9 |- ( u e. ( -u 1 (,) 1 ) -> ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) + ( -u ( u ^ 2 ) / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) = ( ( -u ( u ^ 2 ) / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
236	231, 235	eqtrd 2484	. . . . . . . 8 |- ( u e. ( -u 1 (,) 1 ) -> ( ( 1 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( -u u / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) x. u ) ) = ( ( -u ( u ^ 2 ) / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
237	236	oveq2d 6297	. . . . . . 7 |- ( u e. ( -u 1 (,) 1 ) -> ( ( 1 / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( 1 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( -u u / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) x. u ) ) ) = ( ( 1 / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( -u ( u ^ 2 ) / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) )
238	117	2timesd 10788	. . . . . . . 8 |- ( u e. ( -u 1 (,) 1 ) -> ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) = ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) + ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
239	67, 68	negsubd 9942	. . . . . . . . . . . . 13 |- ( u e. CC -> ( 1 + -u ( u ^ 2 ) ) = ( 1 - ( u ^ 2 ) ) )
240	69	sqsqrtd 13252	. . . . . . . . . . . . 13 |- ( u e. CC -> ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) ^ 2 ) = ( 1 - ( u ^ 2 ) ) )
241	70	sqvald 12289	. . . . . . . . . . . . 13 |- ( u e. CC -> ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) ^ 2 ) = ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
242	239, 240, 241	3eqtr2d 2490	. . . . . . . . . . . 12 |- ( u e. CC -> ( 1 + -u ( u ^ 2 ) ) = ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
243	64, 242	syl 16	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> ( 1 + -u ( u ^ 2 ) ) = ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
244	243	oveq1d 6296	. . . . . . . . . 10 |- ( u e. ( -u 1 (,) 1 ) -> ( ( 1 + -u ( u ^ 2 ) ) / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) = ( ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
245		1cnd 9615	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> 1 e. CC )
246	245, 233, 117, 207	divdird 10365	. . . . . . . . . 10 |- ( u e. ( -u 1 (,) 1 ) -> ( ( 1 + -u ( u ^ 2 ) ) / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) = ( ( 1 / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( -u ( u ^ 2 ) / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) )
247	117, 117, 207	divcan3d 10332	. . . . . . . . . 10 |- ( u e. ( -u 1 (,) 1 ) -> ( ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) = ( sqr ` ( 1 - ( u ^ 2 ) ) ) )
248	244, 246, 247	3eqtr3rd 2493	. . . . . . . . 9 |- ( u e. ( -u 1 (,) 1 ) -> ( sqr ` ( 1 - ( u ^ 2 ) ) ) = ( ( 1 / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( -u ( u ^ 2 ) / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) )
249	248	oveq1d 6296	. . . . . . . 8 |- ( u e. ( -u 1 (,) 1 ) -> ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) + ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) = ( ( ( 1 / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( -u ( u ^ 2 ) / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) + ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
250	117, 207	reccld 10320	. . . . . . . . 9 |- ( u e. ( -u 1 (,) 1 ) -> ( 1 / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
251	250, 234, 117	addassd 9621	. . . . . . . 8 |- ( u e. ( -u 1 (,) 1 ) -> ( ( ( 1 / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( -u ( u ^ 2 ) / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) + ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) = ( ( 1 / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( -u ( u ^ 2 ) / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) )
252	238, 249, 251	3eqtrrd 2489	. . . . . . 7 |- ( u e. ( -u 1 (,) 1 ) -> ( ( 1 / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( -u ( u ^ 2 ) / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) = ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
253	237, 252	eqtrd 2484	. . . . . 6 |- ( u e. ( -u 1 (,) 1 ) -> ( ( 1 / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( 1 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( -u u / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) x. u ) ) ) = ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
254	253	mpteq2ia 4519	. . . . 5 |- ( u e. ( -u 1 (,) 1 ) |-> ( ( 1 / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( 1 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( -u u / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) x. u ) ) ) ) = ( u e. ( -u 1 (,) 1 ) |-> ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
255	220, 254	syl6eq 2500	. . . 4 |- ( R e. RR+ -> ( RR _D ( u e. ( -u 1 (,) 1 ) |-> ( (arcsin ` u ) + ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) ) ) = ( u e. ( -u 1 (,) 1 ) |-> ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) )
256		fveq2 5856	. . . . 5 |- ( u = ( t / R ) -> (arcsin ` u ) = (arcsin ` ( t / R ) ) )
257		id 22	. . . . . 6 |- ( u = ( t / R ) -> u = ( t / R ) )
258		oveq1 6288	. . . . . . . 8 |- ( u = ( t / R ) -> ( u ^ 2 ) = ( ( t / R ) ^ 2 ) )
259	258	oveq2d 6297	. . . . . . 7 |- ( u = ( t / R ) -> ( 1 - ( u ^ 2 ) ) = ( 1 - ( ( t / R ) ^ 2 ) ) )
260	259	fveq2d 5860	. . . . . 6 |- ( u = ( t / R ) -> ( sqr ` ( 1 - ( u ^ 2 ) ) ) = ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) )
261	257, 260	oveq12d 6299	. . . . 5 |- ( u = ( t / R ) -> ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) = ( ( t / R ) x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) )
262	256, 261	oveq12d 6299	. . . 4 |- ( u = ( t / R ) -> ( (arcsin ` u ) + ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) = ( (arcsin ` ( t / R ) ) + ( ( t / R ) x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) )
263	260	oveq2d 6297	. . . 4 |- ( u = ( t / R ) -> ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) = ( 2 x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) )
264	2, 2, 60, 62, 74, 76, 88, 255, 262, 263	dvmptco 22353	. . 3 |- ( R e. RR+ -> ( RR _D ( t e. ( -u R (,) R ) |-> ( (arcsin ` ( t / R ) ) + ( ( t / R ) x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) ) ) = ( t e. ( -u R (,) R ) |-> ( ( 2 x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) x. ( 1 / R ) ) ) )
265	6	sqcld 12290	. . 3 |- ( R e. RR+ -> ( R ^ 2 ) e. CC )
266	2, 18, 20, 264, 265	dvmptcmul 22345	. 2 |- ( R e. RR+ -> ( RR _D ( t e. ( -u R (,) R ) |-> ( ( R ^ 2 ) x. ( (arcsin ` ( t / R ) ) + ( ( t / R ) x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) ) ) ) = ( t e. ( -u R (,) R ) |-> ( ( R ^ 2 ) x. ( ( 2 x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) x. ( 1 / R ) ) ) ) )
267		2cnd 10615	. . . . . . 7 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 2 e. CC )
268	267, 16	mulcld 9619	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 2 x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. CC )
269	6, 8	reccld 10320	. . . . . . 7 |- ( R e. RR+ -> ( 1 / R ) e. CC )
270	269	adantr 465	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 1 / R ) e. CC )
271	268, 270	mulcomd 9620	. . . . 5 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( 2 x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) x. ( 1 / R ) ) = ( ( 1 / R ) x. ( 2 x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) )
272	271	oveq2d 6297	. . . 4 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( ( 2 x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) x. ( 1 / R ) ) ) = ( ( R ^ 2 ) x. ( ( 1 / R ) x. ( 2 x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) ) )
273	265	adantr 465	. . . . 5 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( R ^ 2 ) e. CC )
274	273, 270, 268	mulassd 9622	. . . 4 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( ( R ^ 2 ) x. ( 1 / R ) ) x. ( 2 x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) = ( ( R ^ 2 ) x. ( ( 1 / R ) x. ( 2 x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) ) )
275	6	sqvald 12289	. . . . . . . . 9 |- ( R e. RR+ -> ( R ^ 2 ) = ( R x. R ) )
276	275	oveq1d 6296	. . . . . . . 8 |- ( R e. RR+ -> ( ( R ^ 2 ) / R ) = ( ( R x. R ) / R ) )
277	265, 6, 8	divrecd 10330	. . . . . . . 8 |- ( R e. RR+ -> ( ( R ^ 2 ) / R ) = ( ( R ^ 2 ) x. ( 1 / R ) ) )
278	6, 6, 8	divcan3d 10332	. . . . . . . 8 |- ( R e. RR+ -> ( ( R x. R ) / R ) = R )
279	276, 277, 278	3eqtr3d 2492	. . . . . . 7 |- ( R e. RR+ -> ( ( R ^ 2 ) x. ( 1 / R ) ) = R )
280	279	adantr 465	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( 1 / R ) ) = R )
281	280	oveq1d 6296	. . . . 5 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( ( R ^ 2 ) x. ( 1 / R ) ) x. ( 2 x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) = ( R x. ( 2 x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) )
282	7, 267, 16	mul12d 9792	. . . . 5 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( R x. ( 2 x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) = ( 2 x. ( R x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) )
283	21	resqcld 12318	. . . . . . . . 9 |- ( R e. RR+ -> ( R ^ 2 ) e. RR )
284	283	adantr 465	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( R ^ 2 ) e. RR )
285	21	sqge0d 12319	. . . . . . . . 9 |- ( R e. RR+ -> 0 <_ ( R ^ 2 ) )
286	285	adantr 465	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 <_ ( R ^ 2 ) )
287		1red 9614	. . . . . . . . 9 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 1 e. RR )
288	3	adantl 466	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> t e. RR )
289	21	adantr 465	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> R e. RR )
290	288, 289, 9	redivcld 10379	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( t / R ) e. RR )
291	290	resqcld 12318	. . . . . . . . 9 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) ^ 2 ) e. RR )
292	287, 291	resubcld 9994	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 1 - ( ( t / R ) ^ 2 ) ) e. RR )
293		0red 9600	. . . . . . . . 9 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 e. RR )
294	27, 28	absltd 13243	. . . . . . . . . . . . . . 15 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) < R <-> ( -u R < t /\ t < R ) ) )
295	77	abscld 13249	. . . . . . . . . . . . . . . . . 18 |- ( t e. RR -> ( abs ` t ) e. RR )
296	295	adantl 466	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> ( abs ` t ) e. RR )
297	77	absge0d 13257	. . . . . . . . . . . . . . . . . 18 |- ( t e. RR -> 0 <_ ( abs ` t ) )
298	297	adantl 466	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> 0 <_ ( abs ` t ) )
299		rpge0 11243	. . . . . . . . . . . . . . . . . 18 |- ( R e. RR+ -> 0 <_ R )
300	299	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> 0 <_ R )
301	296, 28, 298, 300	lt2sqd 12326	. . . . . . . . . . . . . . . 16 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) < R <-> ( ( abs ` t ) ^ 2 ) < ( R ^ 2 ) ) )
302		absresq 13117	. . . . . . . . . . . . . . . . . 18 |- ( t e. RR -> ( ( abs ` t ) ^ 2 ) = ( t ^ 2 ) )
303	302	adantl 466	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) ^ 2 ) = ( t ^ 2 ) )
304	265	adantr 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( R e. RR+ /\ t e. RR ) -> ( R ^ 2 ) e. CC )
305	304	mulid1d 9616	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( R ^ 2 ) x. 1 ) = ( R ^ 2 ) )
306	305	eqcomd 2451	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> ( R ^ 2 ) = ( ( R ^ 2 ) x. 1 ) )
307	303, 306	breq12d 4450	. . . . . . . . . . . . . . . 16 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( ( abs ` t ) ^ 2 ) < ( R ^ 2 ) <-> ( t ^ 2 ) < ( ( R ^ 2 ) x. 1 ) ) )
308	6	adantr 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( R e. RR+ /\ t e. RR ) -> R e. CC )
309	78, 308, 29	sqdivd 12305	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( t / R ) ^ 2 ) = ( ( t ^ 2 ) / ( R ^ 2 ) ) )
310	309	breq1d 4447	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( ( t / R ) ^ 2 ) < 1 <-> ( ( t ^ 2 ) / ( R ^ 2 ) ) < 1 ) )
311	30	resqcld 12318	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( t / R ) ^ 2 ) e. RR )
312	311, 42	posdifd 10146	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( ( t / R ) ^ 2 ) < 1 <-> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
313		resqcl 12217	. . . . . . . . . . . . . . . . . . 19 |- ( t e. RR -> ( t ^ 2 ) e. RR )
314	313	adantl 466	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR+ /\ t e. RR ) -> ( t ^ 2 ) e. RR )
315		rpgt0 11242	. . . . . . . . . . . . . . . . . . . . 21 |- ( R e. RR+ -> 0 < R )
316		0red 9600	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( R e. RR+ -> 0 e. RR )
317		0le0 10632	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 0 <_ 0
318	317	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( R e. RR+ -> 0 <_ 0 )
319	316, 21, 318, 299	lt2sqd 12326	. . . . . . . . . . . . . . . . . . . . . 22 |- ( R e. RR+ -> ( 0 < R <-> ( 0 ^ 2 ) < ( R ^ 2 ) ) )
320		sq0 12241	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 0 ^ 2 ) = 0
321	320	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( R e. RR+ -> ( 0 ^ 2 ) = 0 )
322	321	breq1d 4447	. . . . . . . . . . . . . . . . . . . . . 22 |- ( R e. RR+ -> ( ( 0 ^ 2 ) < ( R ^ 2 ) <-> 0 < ( R ^ 2 ) ) )
323	319, 322	bitrd 253	. . . . . . . . . . . . . . . . . . . . 21 |- ( R e. RR+ -> ( 0 < R <-> 0 < ( R ^ 2 ) ) )
324	315, 323	mpbid 210	. . . . . . . . . . . . . . . . . . . 20 |- ( R e. RR+ -> 0 < ( R ^ 2 ) )
325	283, 324	elrpd 11265	. . . . . . . . . . . . . . . . . . 19 |- ( R e. RR+ -> ( R ^ 2 ) e. RR+ )
326	325	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR+ /\ t e. RR ) -> ( R ^ 2 ) e. RR+ )
327	314, 42, 326	ltdivmuld 11314	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( ( t ^ 2 ) / ( R ^ 2 ) ) < 1 <-> ( t ^ 2 ) < ( ( R ^ 2 ) x. 1 ) ) )
328	310, 312, 327	3bitr3rd 284	. . . . . . . . . . . . . . . 16 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( t ^ 2 ) < ( ( R ^ 2 ) x. 1 ) <-> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
329	301, 307, 328	3bitrd 279	. . . . . . . . . . . . . . 15 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) < R <-> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
330	294, 329	bitr3d 255	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) <-> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
331	330	biimpd 207	. . . . . . . . . . . . 13 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) -> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
332	331	exp4b 607	. . . . . . . . . . . 12 |- ( R e. RR+ -> ( t e. RR -> ( -u R < t -> ( t < R -> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) )
333	332	3impd 1211	. . . . . . . . . . 11 |- ( R e. RR+ -> ( ( t e. RR /\ -u R < t /\ t < R ) -> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
334	26, 333	sylbid 215	. . . . . . . . . 10 |- ( R e. RR+ -> ( t e. ( -u R (,) R ) -> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
335	334	imp 429	. . . . . . . . 9 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) )
336	293, 292, 335	ltled 9736	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 <_ ( 1 - ( ( t / R ) ^ 2 ) ) )
337	284, 286, 292, 336	sqrtmuld 13238	. . . . . . 7 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( sqr ` ( ( R ^ 2 ) x. ( 1 - ( ( t / R ) ^ 2 ) ) ) ) = ( ( sqr ` ( R ^ 2 ) ) x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) )
338	273, 13, 14	subdid 10019	. . . . . . . . 9 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( 1 - ( ( t / R ) ^ 2 ) ) ) = ( ( ( R ^ 2 ) x. 1 ) - ( ( R ^ 2 ) x. ( ( t / R ) ^ 2 ) ) ) )
339	273	mulid1d 9616	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. 1 ) = ( R ^ 2 ) )
340	5, 7, 9	sqdivd 12305	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) ^ 2 ) = ( ( t ^ 2 ) / ( R ^ 2 ) ) )
341	340	oveq2d 6297	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( ( t / R ) ^ 2 ) ) = ( ( R ^ 2 ) x. ( ( t ^ 2 ) / ( R ^ 2 ) ) ) )
342	4	sqcld 12290	. . . . . . . . . . . . 13 |- ( t e. ( -u R (,) R ) -> ( t ^ 2 ) e. CC )
343	342	adantl 466	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( t ^ 2 ) e. CC )
344		sqne0 12216	. . . . . . . . . . . . . . 15 |- ( R e. CC -> ( ( R ^ 2 ) =/= 0 <-> R =/= 0 ) )
345	6, 344	syl 16	. . . . . . . . . . . . . 14 |- ( R e. RR+ -> ( ( R ^ 2 ) =/= 0 <-> R =/= 0 ) )
346	8, 345	mpbird 232	. . . . . . . . . . . . 13 |- ( R e. RR+ -> ( R ^ 2 ) =/= 0 )
347	346	adantr 465	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( R ^ 2 ) =/= 0 )
348	343, 273, 347	divcan2d 10329	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( ( t ^ 2 ) / ( R ^ 2 ) ) ) = ( t ^ 2 ) )
349	341, 348	eqtrd 2484	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( ( t / R ) ^ 2 ) ) = ( t ^ 2 ) )
350	339, 349	oveq12d 6299	. . . . . . . . 9 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( ( R ^ 2 ) x. 1 ) - ( ( R ^ 2 ) x. ( ( t / R ) ^ 2 ) ) ) = ( ( R ^ 2 ) - ( t ^ 2 ) ) )
351	338, 350	eqtrd 2484	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( 1 - ( ( t / R ) ^ 2 ) ) ) = ( ( R ^ 2 ) - ( t ^ 2 ) ) )
352	351	fveq2d 5860	. . . . . . 7 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( sqr ` ( ( R ^ 2 ) x. ( 1 - ( ( t / R ) ^ 2 ) ) ) ) = ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
353	21, 299	sqrtsqd 13233	. . . . . . . . 9 |- ( R e. RR+ -> ( sqr ` ( R ^ 2 ) ) = R )
354	353	adantr 465	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( sqr ` ( R ^ 2 ) ) = R )
355	354	oveq1d 6296	. . . . . . 7 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( sqr ` ( R ^ 2 ) ) x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) = ( R x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) )
356	337, 352, 355	3eqtr3rd 2493	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( R x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) = ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
357	356	oveq2d 6297	. . . . 5 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 2 x. ( R x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) = ( 2 x. ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
358	281, 282, 357	3eqtrd 2488	. . . 4 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( ( R ^ 2 ) x. ( 1 / R ) ) x. ( 2 x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) = ( 2 x. ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
359	272, 274, 358	3eqtr2d 2490	. . 3 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( ( 2 x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) x. ( 1 / R ) ) ) = ( 2 x. ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
360	359	mpteq2dva 4523	. 2 |- ( R e. RR+ -> ( t e. ( -u R (,) R ) |-> ( ( R ^ 2 ) x. ( ( 2 x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) x. ( 1 / R ) ) ) ) = ( t e. ( -u R (,) R ) |-> ( 2 x. ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
361	266, 360	eqtrd 2484	1 |- ( R e. RR+ -> ( RR _D ( t e. ( -u R (,) R ) |-> ( ( R ^ 2 ) x. ( (arcsin ` ( t / R ) ) + ( ( t / R ) x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) ) ) ) = ( t e. ( -u R (,) R ) |-> ( 2 x. ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 974   = wceq 1383   e. wcel 1804   =/= wne 2638   _Vcvv 3095   i^i cin 3460   C_ wss 3461   {cpr 4016   class class class wbr 4437   |-> cmpt 4495   ran crn 4990   |` cres 4991   -->wf 5574   ` cfv 5578  (class class class)co 6281   CCcc 9493   RRcr 9494   0cc0 9495   1c1 9496   + caddc 9498   x. cmul 9500   RR*cxr 9630   < clt 9631   <_ cle 9632   - cmin 9810   -ucneg 9811   / cdiv 10213   NNcn 10543   2c2 10592   RR+crp 11231   (,)cioo 11540   ^cexp 12148   sqrcsqrt 13048   abscabs 13049   TopOpenctopn 14801   topGenctg 14817  ℂ_fldccnfld 18399  TopOnctopon 19373   _D cdv 22245  arcsincasin 23171

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 10214  df-nn 10544  df-2 10601  df-3 10602  df-4 10603  df-5 10604  df-6 10605  df-7 10606  df-8 10607  df-9 10608  df-10 10609  df-n0 10803  df-z 10872  df-dec 10987  df-uz 11093  df-q 11194  df-rp 11232  df-xneg 11329  df-xadd 11330  df-xmul 11331  df-ioo 11544  df-ioc 11545  df-ico 11546  df-icc 11547  df-fz 11684  df-fzo 11807  df-fl 11911  df-mod 11979  df-seq 12090  df-exp 12149  df-fac 12336  df-bc 12363  df-hash 12388  df-shft 12882  df-cj 12914  df-re 12915  df-im 12916  df-sqrt 13050  df-abs 13051  df-limsup 13276  df-clim 13293  df-rlim 13294  df-sum 13491  df-ef 13785  df-sin 13787  df-cos 13788  df-tan 13789  df-pi 13790  df-struct 14616  df-ndx 14617  df-slot 14618  df-base 14619  df-sets 14620  df-ress 14621  df-plusg 14692  df-mulr 14693  df-starv 14694  df-sca 14695  df-vsca 14696  df-ip 14697  df-tset 14698  df-ple 14699  df-ds 14701  df-unif 14702  df-hom 14703  df-cco 14704  df-rest 14802  df-topn 14803  df-0g 14821  df-gsum 14822  df-topgen 14823  df-pt 14824  df-prds 14827  df-xrs 14881  df-qtop 14886  df-imas 14887  df-xps 14889  df-mre 14965  df-mrc 14966  df-acs 14968  df-mgm 15851  df-sgrp 15890  df-mnd 15900  df-submnd 15946  df-mulg 16039  df-cntz 16334  df-cmn 16779  df-psmet 18390  df-xmet 18391  df-met 18392  df-bl 18393  df-mopn 18394  df-fbas 18395  df-fg 18396  df-cnfld 18400  df-top 19377  df-bases 19379  df-topon 19380  df-topsp 19381  df-cld 19498  df-ntr 19499  df-cls 19500  df-nei 19577  df-lp 19615  df-perf 19616  df-cn 19706  df-cnp 19707  df-haus 19794  df-cmp 19865  df-tx 20041  df-hmeo 20234  df-fil 20325  df-fm 20417  df-flim 20418  df-flf 20419  df-xms 20801  df-ms 20802  df-tms 20803  df-cncf 21360  df-limc 22248  df-dv 22249  df-log 22922  df-cxp 22923  df-asin 23174

This theorem is referenced by:  areacirc  30088