Theorem areacirclem1 32096

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 9649	. . . 4 |- RR e. { RR , CC }
2	1	a1i 11	. . 3 |- ( R e. RR+ -> RR e. { RR , CC } )
3		elioore 11691	. . . . . . . 8 |- ( t e. ( -u R (,) R ) -> t e. RR )
4	3	recnd 9687	. . . . . . 7 |- ( t e. ( -u R (,) R ) -> t e. CC )
5	4	adantl 473	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> t e. CC )
6		rpcn 11333	. . . . . . 7 |- ( R e. RR+ -> R e. CC )
7	6	adantr 472	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> R e. CC )
8		rpne0 11340	. . . . . . 7 |- ( R e. RR+ -> R =/= 0 )
9	8	adantr 472	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> R =/= 0 )
10	5, 7, 9	divcld 10405	. . . . 5 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( t / R ) e. CC )
11		asincl 23878	. . . . 5 |- ( ( t / R ) e. CC -> (arcsin ` ( t / R ) ) e. CC )
12	10, 11	syl 17	. . . 4 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> (arcsin ` ( t / R ) ) e. CC )
13		1cnd 9677	. . . . . . 7 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 1 e. CC )
14	10	sqcld 12452	. . . . . . 7 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) ^ 2 ) e. CC )
15	13, 14	subcld 10005	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 1 - ( ( t / R ) ^ 2 ) ) e. CC )
16	15	sqrtcld 13576	. . . . 5 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) e. CC )
17	10, 16	mulcld 9681	. . . 4 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. CC )
18	12, 17	addcld 9680	. . 3 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( (arcsin ` ( t / R ) ) + ( ( t / R ) x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) e. CC )
19		ovex 6336	. . . 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 11331	. . . . . . . . . 10 |- ( R e. RR+ -> R e. RR )
22	21	renegcld 10067	. . . . . . . . 9 |- ( R e. RR+ -> -u R e. RR )
23	22	rexrd 9708	. . . . . . . 8 |- ( R e. RR+ -> -u R e. RR* )
24		rpxr 11332	. . . . . . . 8 |- ( R e. RR+ -> R e. RR* )
25		elioo2 11702	. . . . . . . 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 673	. . . . . . 7 |- ( R e. RR+ -> ( t e. ( -u R (,) R ) <-> ( t e. RR /\ -u R < t /\ t < R ) ) )
27		simpr 468	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. RR ) -> t e. RR )
28	21	adantr 472	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. RR ) -> R e. RR )
29	8	adantr 472	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. RR ) -> R =/= 0 )
30	27, 28, 29	redivcld 10457	. . . . . . . . . . 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 10091	. . . . . . . . . . . . . . 15 |- ( R e. RR+ -> ( -u 1 x. R ) = -u R )
33	32	adantr 472	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. RR ) -> ( -u 1 x. R ) = -u R )
34	33	breq1d 4405	. . . . . . . . . . . . 13 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u 1 x. R ) < t <-> -u R < t ) )
35		neg1rr 10736	. . . . . . . . . . . . . . 15 |- -u 1 e. RR
36	35	a1i 11	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. RR ) -> -u 1 e. RR )
37		simpl 464	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. RR ) -> R e. RR+ )
38	36, 27, 37	ltmuldivd 11408	. . . . . . . . . . . . 13 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u 1 x. R ) < t <-> -u 1 < ( t / R ) ) )
39	34, 38	bitr3d 263	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. RR ) -> ( -u R < t <-> -u 1 < ( t / R ) ) )
40	39	biimpd 212	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. RR ) -> ( -u R < t -> -u 1 < ( t / R ) ) )
41	40	adantrd 475	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) -> -u 1 < ( t / R ) ) )
42		1red 9676	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. RR ) -> 1 e. RR )
43	27, 42, 37	ltdivmuld 11412	. . . . . . . . . . . . 13 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( t / R ) < 1 <-> t < ( R x. 1 ) ) )
44	6	mulid1d 9678	. . . . . . . . . . . . . . 15 |- ( R e. RR+ -> ( R x. 1 ) = R )
45	44	adantr 472	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. RR ) -> ( R x. 1 ) = R )
46	45	breq2d 4407	. . . . . . . . . . . . 13 |- ( ( R e. RR+ /\ t e. RR ) -> ( t < ( R x. 1 ) <-> t < R ) )
47	43, 46	bitr2d 262	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. RR ) -> ( t < R <-> ( t / R ) < 1 ) )
48	47	biimpd 212	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. RR ) -> ( t < R -> ( t / R ) < 1 ) )
49	48	adantld 474	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) -> ( t / R ) < 1 ) )
50	31, 41, 49	3jcad 1211	. . . . . . . . 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 618	. . . . . . . 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 1247	. . . . . . 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 223	. . . . . 6 |- ( R e. RR+ -> ( t e. ( -u R (,) R ) -> ( ( t / R ) e. RR /\ -u 1 < ( t / R ) /\ ( t / R ) < 1 ) ) )
54	53	imp 436	. . . . 5 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) e. RR /\ -u 1 < ( t / R ) /\ ( t / R ) < 1 ) )
55	35	rexri 9711	. . . . . 6 |- -u 1 e. RR*
56		1re 9660	. . . . . . 7 |- 1 e. RR
57	56	rexri 9711	. . . . . 6 |- 1 e. RR*
58		elioo2 11702	. . . . . 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 686	. . . . 5 |- ( ( t / R ) e. ( -u 1 (,) 1 ) <-> ( ( t / R ) e. RR /\ -u 1 < ( t / R ) /\ ( t / R ) < 1 ) )
60	54, 59	sylibr 217	. . . 4 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( t / R ) e. ( -u 1 (,) 1 ) )
61		ovex 6336	. . . . 5 |- ( 1 / R ) e. _V
62	61	a1i 11	. . . 4 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 1 / R ) e. _V )
63		elioore 11691	. . . . . . 7 |- ( u e. ( -u 1 (,) 1 ) -> u e. RR )
64	63	recnd 9687	. . . . . 6 |- ( u e. ( -u 1 (,) 1 ) -> u e. CC )
65		asincl 23878	. . . . . . 7 |- ( u e. CC -> (arcsin ` u ) e. CC )
66		id 22	. . . . . . . 8 |- ( u e. CC -> u e. CC )
67		1cnd 9677	. . . . . . . . . 10 |- ( u e. CC -> 1 e. CC )
68		sqcl 12375	. . . . . . . . . 10 |- ( u e. CC -> ( u ^ 2 ) e. CC )
69	67, 68	subcld 10005	. . . . . . . . 9 |- ( u e. CC -> ( 1 - ( u ^ 2 ) ) e. CC )
70	69	sqrtcld 13576	. . . . . . . 8 |- ( u e. CC -> ( sqr ` ( 1 - ( u ^ 2 ) ) ) e. CC )
71	66, 70	mulcld 9681	. . . . . . 7 |- ( u e. CC -> ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
72	65, 71	addcld 9680	. . . . . 6 |- ( u e. CC -> ( (arcsin ` u ) + ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) e. CC )
73	64, 72	syl 17	. . . . 5 |- ( u e. ( -u 1 (,) 1 ) -> ( (arcsin ` u ) + ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) e. CC )
74	73	adantl 473	. . . 4 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( (arcsin ` u ) + ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) e. CC )
75		ovex 6336	. . . . 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 9647	. . . . . . 7 |- ( t e. RR -> t e. CC )
78	77	adantl 473	. . . . . 6 |- ( ( R e. RR+ /\ t e. RR ) -> t e. CC )
79		1cnd 9677	. . . . . 6 |- ( ( R e. RR+ /\ t e. RR ) -> 1 e. CC )
80	2	dvmptid 22990	. . . . . 6 |- ( R e. RR+ -> ( RR _D ( t e. RR |-> t ) ) = ( t e. RR |-> 1 ) )
81		ioossre 11721	. . . . . . 7 |- ( -u R (,) R ) C_ RR
82	81	a1i 11	. . . . . 6 |- ( R e. RR+ -> ( -u R (,) R ) C_ RR )
83		eqid 2471	. . . . . . 7 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
84	83	tgioo2 21899	. . . . . 6 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
85		iooretop 21864	. . . . . . 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 22996	. . . . 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 22998	. . . 4 |- ( R e. RR+ -> ( RR _D ( t e. ( -u R (,) R ) |-> ( t / R ) ) ) = ( t e. ( -u R (,) R ) |-> ( 1 / R ) ) )
89	64, 65	syl 17	. . . . . . 7 |- ( u e. ( -u 1 (,) 1 ) -> (arcsin ` u ) e. CC )
90	89	adantl 473	. . . . . 6 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> (arcsin ` u ) e. CC )
91		ovex 6336	. . . . . . 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 32094	. . . . . . 7 |- ( RR _D (arcsin |` ( -u 1 (,) 1 ) ) ) = ( u e. ( -u 1 (,) 1 ) |-> ( 1 / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
94		asinf 23877	. . . . . . . . . 10 |- arcsin : CC --> CC
95	94	a1i 11	. . . . . . . . 9 |- ( R e. RR+ -> arcsin : CC --> CC )
96		ioossre 11721	. . . . . . . . . . 11 |- ( -u 1 (,) 1 ) C_ RR
97		ax-resscn 9614	. . . . . . . . . . 11 |- RR C_ CC
98	96, 97	sstri 3427	. . . . . . . . . 10 |- ( -u 1 (,) 1 ) C_ CC
99	98	a1i 11	. . . . . . . . 9 |- ( R e. RR+ -> ( -u 1 (,) 1 ) C_ CC )
100	95, 99	feqresmpt 5933	. . . . . . . 8 |- ( R e. RR+ -> (arcsin |` ( -u 1 (,) 1 ) ) = ( u e. ( -u 1 (,) 1 ) |-> (arcsin ` u ) ) )
101	100	oveq2d 6324	. . . . . . 7 |- ( R e. RR+ -> ( RR _D (arcsin |` ( -u 1 (,) 1 ) ) ) = ( RR _D ( u e. ( -u 1 (,) 1 ) |-> (arcsin ` u ) ) ) )
102	93, 101	syl5reqr 2520	. . . . . 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 17	. . . . . . 7 |- ( u e. ( -u 1 (,) 1 ) -> ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
104	103	adantl 473	. . . . . 6 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
105		ovex 6336	. . . . . . 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 473	. . . . . . 7 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> u e. CC )
108		1cnd 9677	. . . . . . 7 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> 1 e. CC )
109		recn 9647	. . . . . . . . 9 |- ( u e. RR -> u e. CC )
110	109	adantl 473	. . . . . . . 8 |- ( ( R e. RR+ /\ u e. RR ) -> u e. CC )
111		1cnd 9677	. . . . . . . 8 |- ( ( R e. RR+ /\ u e. RR ) -> 1 e. CC )
112	2	dvmptid 22990	. . . . . . . 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 21864	. . . . . . . . 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 22996	. . . . . . 7 |- ( R e. RR+ -> ( RR _D ( u e. ( -u 1 (,) 1 ) |-> u ) ) = ( u e. ( -u 1 (,) 1 ) |-> 1 ) )
117	64, 70	syl 17	. . . . . . . 8 |- ( u e. ( -u 1 (,) 1 ) -> ( sqr ` ( 1 - ( u ^ 2 ) ) ) e. CC )
118	117	adantl 473	. . . . . . 7 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( sqr ` ( 1 - ( u ^ 2 ) ) ) e. CC )
119		ovex 6336	. . . . . . . 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 9676	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> 1 e. RR )
122	63	resqcld 12480	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> ( u ^ 2 ) e. RR )
123	121, 122	resubcld 10068	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> ( 1 - ( u ^ 2 ) ) e. RR )
124		elioo2 11702	. . . . . . . . . . . . 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 686	. . . . . . . . . . . 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 9676	. . . . . . . . . . . . . . . 16 |- ( u e. RR -> 1 e. RR )
128	126, 127	absltd 13568	. . . . . . . . . . . . . . 15 |- ( u e. RR -> ( ( abs ` u ) < 1 <-> ( -u 1 < u /\ u < 1 ) ) )
129	109	abscld 13575	. . . . . . . . . . . . . . . . 17 |- ( u e. RR -> ( abs ` u ) e. RR )
130	109	absge0d 13583	. . . . . . . . . . . . . . . . 17 |- ( u e. RR -> 0 <_ ( abs ` u ) )
131		0le1 10158	. . . . . . . . . . . . . . . . . 18 |- 0 <_ 1
132	131	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( u e. RR -> 0 <_ 1 )
133	129, 127, 130, 132	lt2sqd 12488	. . . . . . . . . . . . . . . 16 |- ( u e. RR -> ( ( abs ` u ) < 1 <-> ( ( abs ` u ) ^ 2 ) < ( 1 ^ 2 ) ) )
134		absresq 13442	. . . . . . . . . . . . . . . . 17 |- ( u e. RR -> ( ( abs ` u ) ^ 2 ) = ( u ^ 2 ) )
135		sq1 12407	. . . . . . . . . . . . . . . . . 18 |- ( 1 ^ 2 ) = 1
136	135	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( u e. RR -> ( 1 ^ 2 ) = 1 )
137	134, 136	breq12d 4408	. . . . . . . . . . . . . . . 16 |- ( u e. RR -> ( ( ( abs ` u ) ^ 2 ) < ( 1 ^ 2 ) <-> ( u ^ 2 ) < 1 ) )
138		resqcl 12380	. . . . . . . . . . . . . . . . 17 |- ( u e. RR -> ( u ^ 2 ) e. RR )
139	138, 127	posdifd 10221	. . . . . . . . . . . . . . . 16 |- ( u e. RR -> ( ( u ^ 2 ) < 1 <-> 0 < ( 1 - ( u ^ 2 ) ) ) )
140	133, 137, 139	3bitrd 287	. . . . . . . . . . . . . . 15 |- ( u e. RR -> ( ( abs ` u ) < 1 <-> 0 < ( 1 - ( u ^ 2 ) ) ) )
141	128, 140	bitr3d 263	. . . . . . . . . . . . . 14 |- ( u e. RR -> ( ( -u 1 < u /\ u < 1 ) <-> 0 < ( 1 - ( u ^ 2 ) ) ) )
142	141	biimpd 212	. . . . . . . . . . . . 13 |- ( u e. RR -> ( ( -u 1 < u /\ u < 1 ) -> 0 < ( 1 - ( u ^ 2 ) ) ) )
143	142	3impib 1229	. . . . . . . . . . . 12 |- ( ( u e. RR /\ -u 1 < u /\ u < 1 ) -> 0 < ( 1 - ( u ^ 2 ) ) )
144	125, 143	sylbi 200	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> 0 < ( 1 - ( u ^ 2 ) ) )
145	123, 144	elrpd 11361	. . . . . . . . . 10 |- ( u e. ( -u 1 (,) 1 ) -> ( 1 - ( u ^ 2 ) ) e. RR+ )
146	145	adantl 473	. . . . . . . . 9 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( 1 - ( u ^ 2 ) ) e. RR+ )
147		negex 9893	. . . . . . . . . 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 11333	. . . . . . . . . . 11 |- ( v e. RR+ -> v e. CC )
150	149	sqrtcld 13576	. . . . . . . . . 10 |- ( v e. RR+ -> ( sqr ` v ) e. CC )
151	150	adantl 473	. . . . . . . . 9 |- ( ( R e. RR+ /\ v e. RR+ ) -> ( sqr ` v ) e. CC )
152		ovex 6336	. . . . . . . . . 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 9677	. . . . . . . . . . . 12 |- ( u e. RR -> 1 e. CC )
155	109	sqcld 12452	. . . . . . . . . . . 12 |- ( u e. RR -> ( u ^ 2 ) e. CC )
156	154, 155	subcld 10005	. . . . . . . . . . 11 |- ( u e. RR -> ( 1 - ( u ^ 2 ) ) e. CC )
157	156	adantl 473	. . . . . . . . . 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 9662	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ u e. RR ) -> 0 e. RR )
160		1cnd 9677	. . . . . . . . . . . . 13 |- ( R e. RR+ -> 1 e. CC )
161	2, 160	dvmptc 22991	. . . . . . . . . . . 12 |- ( R e. RR+ -> ( RR _D ( u e. RR |-> 1 ) ) = ( u e. RR |-> 0 ) )
162	155	adantl 473	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ u e. RR ) -> ( u ^ 2 ) e. CC )
163		ovex 6336	. . . . . . . . . . . . 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 21881	. . . . . . . . . . . . . 14 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
166		toponmax 20020	. . . . . . . . . . . . . 14 |- ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) -> CC e. ( TopOpen ` ℂfld ) )
167	165, 166	mp1i 13	. . . . . . . . . . . . 13 |- ( R e. RR+ -> CC e. ( TopOpen ` ℂfld ) )
168		df-ss 3404	. . . . . . . . . . . . . . 15 |- ( RR C_ CC <-> ( RR i^i CC ) = RR )
169	97, 168	mpbi 213	. . . . . . . . . . . . . 14 |- ( RR i^i CC ) = RR
170	169	a1i 11	. . . . . . . . . . . . 13 |- ( R e. RR+ -> ( RR i^i CC ) = RR )
171	68	adantl 473	. . . . . . . . . . . . 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 10790	. . . . . . . . . . . . . . . 16 |- 2 e. NN
174		dvexp 22986	. . . . . . . . . . . . . . . 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 10746	. . . . . . . . . . . . . . . . . . 19 |- ( 2 - 1 ) = 1
177	176	oveq2i 6319	. . . . . . . . . . . . . . . . . 18 |- ( u ^ ( 2 - 1 ) ) = ( u ^ 1 )
178		exp1 12316	. . . . . . . . . . . . . . . . . 18 |- ( u e. CC -> ( u ^ 1 ) = u )
179	177, 178	syl5eq 2517	. . . . . . . . . . . . . . . . 17 |- ( u e. CC -> ( u ^ ( 2 - 1 ) ) = u )
180	179	oveq2d 6324	. . . . . . . . . . . . . . . 16 |- ( u e. CC -> ( 2 x. ( u ^ ( 2 - 1 ) ) ) = ( 2 x. u ) )
181	180	mpteq2ia 4478	. . . . . . . . . . . . . . 15 |- ( u e. CC |-> ( 2 x. ( u ^ ( 2 - 1 ) ) ) ) = ( u e. CC |-> ( 2 x. u ) )
182	175, 181	eqtri 2493	. . . . . . . . . . . . . 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 22989	. . . . . . . . . . . 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 23000	. . . . . . . . . . 11 |- ( R e. RR+ -> ( RR _D ( u e. RR |-> ( 1 - ( u ^ 2 ) ) ) ) = ( u e. RR |-> ( 0 - ( 2 x. u ) ) ) )
186		df-neg 9883	. . . . . . . . . . . 12 |- -u ( 2 x. u ) = ( 0 - ( 2 x. u ) )
187	186	mpteq2i 4479	. . . . . . . . . . 11 |- ( u e. RR |-> -u ( 2 x. u ) ) = ( u e. RR |-> ( 0 - ( 2 x. u ) ) )
188	185, 187	syl6eqr 2523	. . . . . . . . . 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 22996	. . . . . . . . 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 23761	. . . . . . . . . 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 5879	. . . . . . . . 9 |- ( v = ( 1 - ( u ^ 2 ) ) -> ( sqr ` v ) = ( sqr ` ( 1 - ( u ^ 2 ) ) ) )
193	192	oveq2d 6324	. . . . . . . . . 10 |- ( v = ( 1 - ( u ^ 2 ) ) -> ( 2 x. ( sqr ` v ) ) = ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
194	193	oveq2d 6324	. . . . . . . . 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 23005	. . . . . . . 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 10704	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> 2 e. CC )
197	196, 64	mulneg2d 10093	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> ( 2 x. -u u ) = -u ( 2 x. u ) )
198	197	oveq1d 6323	. . . . . . . . . 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 9992	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> -u u e. CC )
200	144	gt0ne0d 10199	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> ( 1 - ( u ^ 2 ) ) =/= 0 )
201	64, 69	syl 17	. . . . . . . . . . . . . . . 16 |- ( u e. ( -u 1 (,) 1 ) -> ( 1 - ( u ^ 2 ) ) e. CC )
202	201	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( u e. ( -u 1 (,) 1 ) /\ ( sqr ` ( 1 - ( u ^ 2 ) ) ) = 0 ) -> ( 1 - ( u ^ 2 ) ) e. CC )
203		simpr 468	. . . . . . . . . . . . . . 15 |- ( ( u e. ( -u 1 (,) 1 ) /\ ( sqr ` ( 1 - ( u ^ 2 ) ) ) = 0 ) -> ( sqr ` ( 1 - ( u ^ 2 ) ) ) = 0 )
204	202, 203	sqr00d 13580	. . . . . . . . . . . . . 14 |- ( ( u e. ( -u 1 (,) 1 ) /\ ( sqr ` ( 1 - ( u ^ 2 ) ) ) = 0 ) -> ( 1 - ( u ^ 2 ) ) = 0 )
205	204	ex 441	. . . . . . . . . . . . 13 |- ( u e. ( -u 1 (,) 1 ) -> ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) = 0 -> ( 1 - ( u ^ 2 ) ) = 0 ) )
206	205	necon3d 2664	. . . . . . . . . . . 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 10724	. . . . . . . . . . . 12 |- 2 =/= 0
209	208	a1i 11	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> 2 =/= 0 )
210	199, 117, 196, 207, 209	divcan5d 10431	. . . . . . . . . 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 9681	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> ( 2 x. u ) e. CC )
212	211	negcld 9992	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> -u ( 2 x. u ) e. CC )
213	196, 117	mulcld 9681	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
214	196, 117, 209, 207	mulne0d 10286	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) =/= 0 )
215	212, 213, 214	divrec2d 10409	. . . . . . . . . 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 2514	. . . . . . . . 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 4478	. . . . . . . 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 2521	. . . . . . 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 22994	. . . . . 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 22993	. . . . 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 9679	. . . . . . . . . 10 |- ( u e. ( -u 1 (,) 1 ) -> ( 1 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) = ( sqr ` ( 1 - ( u ^ 2 ) ) ) )
222	199, 117, 207	divcld 10405	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> ( -u u / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
223	222, 64	mulcomd 9682	. . . . . . . . . . 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 10440	. . . . . . . . . . 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 10093	. . . . . . . . . . . . 13 |- ( u e. ( -u 1 (,) 1 ) -> ( u x. -u u ) = -u ( u x. u ) )
226	64	sqvald 12451	. . . . . . . . . . . . . 14 |- ( u e. ( -u 1 (,) 1 ) -> ( u ^ 2 ) = ( u x. u ) )
227	226	negeqd 9889	. . . . . . . . . . . . 13 |- ( u e. ( -u 1 (,) 1 ) -> -u ( u ^ 2 ) = -u ( u x. u ) )
228	225, 227	eqtr4d 2508	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> ( u x. -u u ) = -u ( u ^ 2 ) )
229	228	oveq1d 6323	. . . . . . . . . . 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 2511	. . . . . . . . . 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 6326	. . . . . . . . 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 12452	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> ( u ^ 2 ) e. CC )
233	232	negcld 9992	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> -u ( u ^ 2 ) e. CC )
234	233, 117, 207	divcld 10405	. . . . . . . . . 10 |- ( u e. ( -u 1 (,) 1 ) -> ( -u ( u ^ 2 ) / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
235	117, 234	addcomd 9853	. . . . . . . . 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 2505	. . . . . . . 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 6324	. . . . . . 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 10878	. . . . . . . 8 |- ( u e. ( -u 1 (,) 1 ) -> ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) = ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) + ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
239	67, 68	negsubd 10011	. . . . . . . . . . . . 13 |- ( u e. CC -> ( 1 + -u ( u ^ 2 ) ) = ( 1 - ( u ^ 2 ) ) )
240	69	sqsqrtd 13578	. . . . . . . . . . . . 13 |- ( u e. CC -> ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) ^ 2 ) = ( 1 - ( u ^ 2 ) ) )
241	70	sqvald 12451	. . . . . . . . . . . . 13 |- ( u e. CC -> ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) ^ 2 ) = ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
242	239, 240, 241	3eqtr2d 2511	. . . . . . . . . . . 12 |- ( u e. CC -> ( 1 + -u ( u ^ 2 ) ) = ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
243	64, 242	syl 17	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> ( 1 + -u ( u ^ 2 ) ) = ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
244	243	oveq1d 6323	. . . . . . . . . 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 9677	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> 1 e. CC )
246	245, 233, 117, 207	divdird 10443	. . . . . . . . . 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 10410	. . . . . . . . . 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 2514	. . . . . . . . 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 6323	. . . . . . . 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 10398	. . . . . . . . 9 |- ( u e. ( -u 1 (,) 1 ) -> ( 1 / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
251	250, 234, 117	addassd 9683	. . . . . . . 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 2510	. . . . . . 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 2505	. . . . . 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 4478	. . . . 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 2521	. . . 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 5879	. . . . 5 |- ( u = ( t / R ) -> (arcsin ` u ) = (arcsin ` ( t / R ) ) )
257		id 22	. . . . . 6 |- ( u = ( t / R ) -> u = ( t / R ) )
258		oveq1 6315	. . . . . . . 8 |- ( u = ( t / R ) -> ( u ^ 2 ) = ( ( t / R ) ^ 2 ) )
259	258	oveq2d 6324	. . . . . . 7 |- ( u = ( t / R ) -> ( 1 - ( u ^ 2 ) ) = ( 1 - ( ( t / R ) ^ 2 ) ) )
260	259	fveq2d 5883	. . . . . 6 |- ( u = ( t / R ) -> ( sqr ` ( 1 - ( u ^ 2 ) ) ) = ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) )
261	257, 260	oveq12d 6326	. . . . 5 |- ( u = ( t / R ) -> ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) = ( ( t / R ) x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) )
262	256, 261	oveq12d 6326	. . . 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 6324	. . . 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 23005	. . 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 12452	. . 3 |- ( R e. RR+ -> ( R ^ 2 ) e. CC )
266	2, 18, 20, 264, 265	dvmptcmul 22997	. 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 10704	. . . . . . 7 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 2 e. CC )
268	267, 16	mulcld 9681	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 2 x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. CC )
269	6, 8	reccld 10398	. . . . . . 7 |- ( R e. RR+ -> ( 1 / R ) e. CC )
270	269	adantr 472	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 1 / R ) e. CC )
271	268, 270	mulcomd 9682	. . . . 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 6324	. . . 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 472	. . . . 5 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( R ^ 2 ) e. CC )
274	273, 270, 268	mulassd 9684	. . . 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 12451	. . . . . . . . 9 |- ( R e. RR+ -> ( R ^ 2 ) = ( R x. R ) )
276	275	oveq1d 6323	. . . . . . . 8 |- ( R e. RR+ -> ( ( R ^ 2 ) / R ) = ( ( R x. R ) / R ) )
277	265, 6, 8	divrecd 10408	. . . . . . . 8 |- ( R e. RR+ -> ( ( R ^ 2 ) / R ) = ( ( R ^ 2 ) x. ( 1 / R ) ) )
278	6, 6, 8	divcan3d 10410	. . . . . . . 8 |- ( R e. RR+ -> ( ( R x. R ) / R ) = R )
279	276, 277, 278	3eqtr3d 2513	. . . . . . 7 |- ( R e. RR+ -> ( ( R ^ 2 ) x. ( 1 / R ) ) = R )
280	279	adantr 472	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( 1 / R ) ) = R )
281	280	oveq1d 6323	. . . . 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 9860	. . . . 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 12480	. . . . . . . . 9 |- ( R e. RR+ -> ( R ^ 2 ) e. RR )
284	283	adantr 472	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( R ^ 2 ) e. RR )
285	21	sqge0d 12481	. . . . . . . . 9 |- ( R e. RR+ -> 0 <_ ( R ^ 2 ) )
286	285	adantr 472	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 <_ ( R ^ 2 ) )
287		1red 9676	. . . . . . . . 9 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 1 e. RR )
288	3	adantl 473	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> t e. RR )
289	21	adantr 472	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> R e. RR )
290	288, 289, 9	redivcld 10457	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( t / R ) e. RR )
291	290	resqcld 12480	. . . . . . . . 9 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) ^ 2 ) e. RR )
292	287, 291	resubcld 10068	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 1 - ( ( t / R ) ^ 2 ) ) e. RR )
293		0red 9662	. . . . . . . . 9 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 e. RR )
294	27, 28	absltd 13568	. . . . . . . . . . . . . . 15 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) < R <-> ( -u R < t /\ t < R ) ) )
295	77	abscld 13575	. . . . . . . . . . . . . . . . . 18 |- ( t e. RR -> ( abs ` t ) e. RR )
296	295	adantl 473	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> ( abs ` t ) e. RR )
297	77	absge0d 13583	. . . . . . . . . . . . . . . . . 18 |- ( t e. RR -> 0 <_ ( abs ` t ) )
298	297	adantl 473	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> 0 <_ ( abs ` t ) )
299		rpge0 11337	. . . . . . . . . . . . . . . . . 18 |- ( R e. RR+ -> 0 <_ R )
300	299	adantr 472	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> 0 <_ R )
301	296, 28, 298, 300	lt2sqd 12488	. . . . . . . . . . . . . . . 16 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) < R <-> ( ( abs ` t ) ^ 2 ) < ( R ^ 2 ) ) )
302		absresq 13442	. . . . . . . . . . . . . . . . . 18 |- ( t e. RR -> ( ( abs ` t ) ^ 2 ) = ( t ^ 2 ) )
303	302	adantl 473	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) ^ 2 ) = ( t ^ 2 ) )
304	265	adantr 472	. . . . . . . . . . . . . . . . . . 19 |- ( ( R e. RR+ /\ t e. RR ) -> ( R ^ 2 ) e. CC )
305	304	mulid1d 9678	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( R ^ 2 ) x. 1 ) = ( R ^ 2 ) )
306	305	eqcomd 2477	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> ( R ^ 2 ) = ( ( R ^ 2 ) x. 1 ) )
307	303, 306	breq12d 4408	. . . . . . . . . . . . . . . 16 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( ( abs ` t ) ^ 2 ) < ( R ^ 2 ) <-> ( t ^ 2 ) < ( ( R ^ 2 ) x. 1 ) ) )
308	6	adantr 472	. . . . . . . . . . . . . . . . . . 19 |- ( ( R e. RR+ /\ t e. RR ) -> R e. CC )
309	78, 308, 29	sqdivd 12467	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( t / R ) ^ 2 ) = ( ( t ^ 2 ) / ( R ^ 2 ) ) )
310	309	breq1d 4405	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( ( t / R ) ^ 2 ) < 1 <-> ( ( t ^ 2 ) / ( R ^ 2 ) ) < 1 ) )
311	30	resqcld 12480	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( t / R ) ^ 2 ) e. RR )
312	311, 42	posdifd 10221	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( ( t / R ) ^ 2 ) < 1 <-> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
313		resqcl 12380	. . . . . . . . . . . . . . . . . . 19 |- ( t e. RR -> ( t ^ 2 ) e. RR )
314	313	adantl 473	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR+ /\ t e. RR ) -> ( t ^ 2 ) e. RR )
315		rpgt0 11336	. . . . . . . . . . . . . . . . . . . . 21 |- ( R e. RR+ -> 0 < R )
316		0red 9662	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( R e. RR+ -> 0 e. RR )
317		0le0 10721	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 0 <_ 0
318	317	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( R e. RR+ -> 0 <_ 0 )
319	316, 21, 318, 299	lt2sqd 12488	. . . . . . . . . . . . . . . . . . . . . 22 |- ( R e. RR+ -> ( 0 < R <-> ( 0 ^ 2 ) < ( R ^ 2 ) ) )
320		sq0 12404	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 0 ^ 2 ) = 0
321	320	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( R e. RR+ -> ( 0 ^ 2 ) = 0 )
322	321	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . 22 |- ( R e. RR+ -> ( ( 0 ^ 2 ) < ( R ^ 2 ) <-> 0 < ( R ^ 2 ) ) )
323	319, 322	bitrd 261	. . . . . . . . . . . . . . . . . . . . 21 |- ( R e. RR+ -> ( 0 < R <-> 0 < ( R ^ 2 ) ) )
324	315, 323	mpbid 215	. . . . . . . . . . . . . . . . . . . 20 |- ( R e. RR+ -> 0 < ( R ^ 2 ) )
325	283, 324	elrpd 11361	. . . . . . . . . . . . . . . . . . 19 |- ( R e. RR+ -> ( R ^ 2 ) e. RR+ )
326	325	adantr 472	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR+ /\ t e. RR ) -> ( R ^ 2 ) e. RR+ )
327	314, 42, 326	ltdivmuld 11412	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( ( t ^ 2 ) / ( R ^ 2 ) ) < 1 <-> ( t ^ 2 ) < ( ( R ^ 2 ) x. 1 ) ) )
328	310, 312, 327	3bitr3rd 292	. . . . . . . . . . . . . . . 16 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( t ^ 2 ) < ( ( R ^ 2 ) x. 1 ) <-> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
329	301, 307, 328	3bitrd 287	. . . . . . . . . . . . . . 15 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) < R <-> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
330	294, 329	bitr3d 263	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) <-> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
331	330	biimpd 212	. . . . . . . . . . . . 13 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) -> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
332	331	exp4b 618	. . . . . . . . . . . 12 |- ( R e. RR+ -> ( t e. RR -> ( -u R < t -> ( t < R -> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) )
333	332	3impd 1247	. . . . . . . . . . 11 |- ( R e. RR+ -> ( ( t e. RR /\ -u R < t /\ t < R ) -> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
334	26, 333	sylbid 223	. . . . . . . . . 10 |- ( R e. RR+ -> ( t e. ( -u R (,) R ) -> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
335	334	imp 436	. . . . . . . . 9 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) )
336	293, 292, 335	ltled 9800	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 <_ ( 1 - ( ( t / R ) ^ 2 ) ) )
337	284, 286, 292, 336	sqrtmuld 13563	. . . . . . 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 10095	. . . . . . . . 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 9678	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. 1 ) = ( R ^ 2 ) )
340	5, 7, 9	sqdivd 12467	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) ^ 2 ) = ( ( t ^ 2 ) / ( R ^ 2 ) ) )
341	340	oveq2d 6324	. . . . . . . . . . 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 12452	. . . . . . . . . . . . 13 |- ( t e. ( -u R (,) R ) -> ( t ^ 2 ) e. CC )
343	342	adantl 473	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( t ^ 2 ) e. CC )
344		sqne0 12379	. . . . . . . . . . . . . . 15 |- ( R e. CC -> ( ( R ^ 2 ) =/= 0 <-> R =/= 0 ) )
345	6, 344	syl 17	. . . . . . . . . . . . . 14 |- ( R e. RR+ -> ( ( R ^ 2 ) =/= 0 <-> R =/= 0 ) )
346	8, 345	mpbird 240	. . . . . . . . . . . . 13 |- ( R e. RR+ -> ( R ^ 2 ) =/= 0 )
347	346	adantr 472	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( R ^ 2 ) =/= 0 )
348	343, 273, 347	divcan2d 10407	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( ( t ^ 2 ) / ( R ^ 2 ) ) ) = ( t ^ 2 ) )
349	341, 348	eqtrd 2505	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( ( t / R ) ^ 2 ) ) = ( t ^ 2 ) )
350	339, 349	oveq12d 6326	. . . . . . . . 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 2505	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( 1 - ( ( t / R ) ^ 2 ) ) ) = ( ( R ^ 2 ) - ( t ^ 2 ) ) )
352	351	fveq2d 5883	. . . . . . 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 13558	. . . . . . . . 9 |- ( R e. RR+ -> ( sqr ` ( R ^ 2 ) ) = R )
354	353	adantr 472	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( sqr ` ( R ^ 2 ) ) = R )
355	354	oveq1d 6323	. . . . . . 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 2514	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( R x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) = ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
357	356	oveq2d 6324	. . . . 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 2509	. . . 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 2511	. . 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 4482	. 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 2505	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 189   /\ wa 376   /\ w3a 1007   = wceq 1452   e. wcel 1904   =/= wne 2641   _Vcvv 3031   i^i cin 3389   C_ wss 3390   {cpr 3961   class class class wbr 4395   |-> cmpt 4454   ran crn 4840   |` cres 4841   -->wf 5585   ` cfv 5589  (class class class)co 6308   CCcc 9555   RRcr 9556   0cc0 9557   1c1 9558   + caddc 9560   x. cmul 9562   RR*cxr 9692   < clt 9693   <_ cle 9694   - cmin 9880   -ucneg 9881   / cdiv 10291   NNcn 10631   2c2 10681   RR+crp 11325   (,)cioo 11660   ^cexp 12310   sqrcsqrt 13373   abscabs 13374   TopOpenctopn 15398   topGenctg 15414  ℂ_fldccnfld 19047  TopOnctopon 19995   _D cdv 22897  arcsincasin 23867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635  ax-addf 9636  ax-mulf 9637

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-iin 4272  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-of 6550  df-om 6712  df-1st 6812  df-2nd 6813  df-supp 6934  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-2o 7201  df-oadd 7204  df-er 7381  df-map 7492  df-pm 7493  df-ixp 7541  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-fsupp 7902  df-fi 7943  df-sup 7974  df-inf 7975  df-oi 8043  df-card 8391  df-cda 8616  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-3 10691  df-4 10692  df-5 10693  df-6 10694  df-7 10695  df-8 10696  df-9 10697  df-10 10698  df-n0 10894  df-z 10962  df-dec 11075  df-uz 11183  df-q 11288  df-rp 11326  df-xneg 11432  df-xadd 11433  df-xmul 11434  df-ioo 11664  df-ioc 11665  df-ico 11666  df-icc 11667  df-fz 11811  df-fzo 11943  df-fl 12061  df-mod 12130  df-seq 12252  df-exp 12311  df-fac 12498  df-bc 12526  df-hash 12554  df-shft 13207  df-cj 13239  df-re 13240  df-im 13241  df-sqrt 13375  df-abs 13376  df-limsup 13603  df-clim 13629  df-rlim 13630  df-sum 13830  df-ef 14198  df-sin 14200  df-cos 14201  df-tan 14202  df-pi 14203  df-struct 15201  df-ndx 15202  df-slot 15203  df-base 15204  df-sets 15205  df-ress 15206  df-plusg 15281  df-mulr 15282  df-starv 15283  df-sca 15284  df-vsca 15285  df-ip 15286  df-tset 15287  df-ple 15288  df-ds 15290  df-unif 15291  df-hom 15292  df-cco 15293  df-rest 15399  df-topn 15400  df-0g 15418  df-gsum 15419  df-topgen 15420  df-pt 15421  df-prds 15424  df-xrs 15478  df-qtop 15484  df-imas 15485  df-xps 15488  df-mre 15570  df-mrc 15571  df-acs 15573  df-mgm 16566  df-sgrp 16605  df-mnd 16615  df-submnd 16661  df-mulg 16754  df-cntz 17049  df-cmn 17510  df-psmet 19039  df-xmet 19040  df-met 19041  df-bl 19042  df-mopn 19043  df-fbas 19044  df-fg 19045  df-cnfld 19048  df-top 19998  df-bases 19999  df-topon 20000  df-topsp 20001  df-cld 20111  df-ntr 20112  df-cls 20113  df-nei 20191  df-lp 20229  df-perf 20230  df-cn 20320  df-cnp 20321  df-haus 20408  df-cmp 20479  df-tx 20654  df-hmeo 20847  df-fil 20939  df-fm 21031  df-flim 21032  df-flf 21033  df-xms 21413  df-ms 21414  df-tms 21415  df-cncf 21988  df-limc 22900  df-dv 22901  df-log 23585  df-cxp 23586  df-asin 23870

This theorem is referenced by:  areacirc  32101