Theorem areacirclem1 30309

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 9513	. . . 4 |- RR e. { RR , CC }
2	1	a1i 11	. . 3 |- ( R e. RR+ -> RR e. { RR , CC } )
3		elioore 11498	. . . . . . . 8 |- ( t e. ( -u R (,) R ) -> t e. RR )
4	3	recnd 9551	. . . . . . 7 |- ( t e. ( -u R (,) R ) -> t e. CC )
5	4	adantl 464	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> t e. CC )
6		rpcn 11165	. . . . . . 7 |- ( R e. RR+ -> R e. CC )
7	6	adantr 463	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> R e. CC )
8		rpne0 11172	. . . . . . 7 |- ( R e. RR+ -> R =/= 0 )
9	8	adantr 463	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> R =/= 0 )
10	5, 7, 9	divcld 10255	. . . . 5 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( t / R ) e. CC )
11		asincl 23339	. . . . 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 9541	. . . . . . 7 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 1 e. CC )
14	10	sqcld 12229	. . . . . . 7 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) ^ 2 ) e. CC )
15	13, 14	subcld 9862	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 1 - ( ( t / R ) ^ 2 ) ) e. CC )
16	15	sqrtcld 13289	. . . . 5 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) e. CC )
17	10, 16	mulcld 9545	. . . 4 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. CC )
18	12, 17	addcld 9544	. . 3 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( (arcsin ` ( t / R ) ) + ( ( t / R ) x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) e. CC )
19		ovex 6242	. . . 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 11163	. . . . . . . . . 10 |- ( R e. RR+ -> R e. RR )
22	21	renegcld 9922	. . . . . . . . 9 |- ( R e. RR+ -> -u R e. RR )
23	22	rexrd 9572	. . . . . . . 8 |- ( R e. RR+ -> -u R e. RR* )
24		rpxr 11164	. . . . . . . 8 |- ( R e. RR+ -> R e. RR* )
25		elioo2 11509	. . . . . . . 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 659	. . . . . . 7 |- ( R e. RR+ -> ( t e. ( -u R (,) R ) <-> ( t e. RR /\ -u R < t /\ t < R ) ) )
27		simpr 459	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. RR ) -> t e. RR )
28	21	adantr 463	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. RR ) -> R e. RR )
29	8	adantr 463	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. RR ) -> R =/= 0 )
30	27, 28, 29	redivcld 10307	. . . . . . . . . . 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 9944	. . . . . . . . . . . . . . 15 |- ( R e. RR+ -> ( -u 1 x. R ) = -u R )
33	32	adantr 463	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. RR ) -> ( -u 1 x. R ) = -u R )
34	33	breq1d 4390	. . . . . . . . . . . . 13 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u 1 x. R ) < t <-> -u R < t ) )
35		neg1rr 10575	. . . . . . . . . . . . . . 15 |- -u 1 e. RR
36	35	a1i 11	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. RR ) -> -u 1 e. RR )
37		simpl 455	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. RR ) -> R e. RR+ )
38	36, 27, 37	ltmuldivd 11238	. . . . . . . . . . . . 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 466	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) -> -u 1 < ( t / R ) ) )
42		1red 9540	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. RR ) -> 1 e. RR )
43	27, 42, 37	ltdivmuld 11242	. . . . . . . . . . . . 13 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( t / R ) < 1 <-> t < ( R x. 1 ) ) )
44	6	mulid1d 9542	. . . . . . . . . . . . . . 15 |- ( R e. RR+ -> ( R x. 1 ) = R )
45	44	adantr 463	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. RR ) -> ( R x. 1 ) = R )
46	45	breq2d 4392	. . . . . . . . . . . . 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 465	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) -> ( t / R ) < 1 ) )
50	31, 41, 49	3jcad 1175	. . . . . . . . 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 605	. . . . . . . 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 1208	. . . . . . 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 427	. . . . 5 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) e. RR /\ -u 1 < ( t / R ) /\ ( t / R ) < 1 ) )
55	35	rexri 9575	. . . . . 6 |- -u 1 e. RR*
56		1re 9524	. . . . . . 7 |- 1 e. RR
57	56	rexri 9575	. . . . . 6 |- 1 e. RR*
58		elioo2 11509	. . . . . 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 670	. . . . 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 6242	. . . . 5 |- ( 1 / R ) e. _V
62	61	a1i 11	. . . 4 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 1 / R ) e. _V )
63		elioore 11498	. . . . . . 7 |- ( u e. ( -u 1 (,) 1 ) -> u e. RR )
64	63	recnd 9551	. . . . . 6 |- ( u e. ( -u 1 (,) 1 ) -> u e. CC )
65		asincl 23339	. . . . . . 7 |- ( u e. CC -> (arcsin ` u ) e. CC )
66		id 22	. . . . . . . 8 |- ( u e. CC -> u e. CC )
67		1cnd 9541	. . . . . . . . . 10 |- ( u e. CC -> 1 e. CC )
68		sqcl 12152	. . . . . . . . . 10 |- ( u e. CC -> ( u ^ 2 ) e. CC )
69	67, 68	subcld 9862	. . . . . . . . 9 |- ( u e. CC -> ( 1 - ( u ^ 2 ) ) e. CC )
70	69	sqrtcld 13289	. . . . . . . 8 |- ( u e. CC -> ( sqr ` ( 1 - ( u ^ 2 ) ) ) e. CC )
71	66, 70	mulcld 9545	. . . . . . 7 |- ( u e. CC -> ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
72	65, 71	addcld 9544	. . . . . 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 464	. . . 4 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( (arcsin ` u ) + ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) e. CC )
75		ovex 6242	. . . . 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 9511	. . . . . . 7 |- ( t e. RR -> t e. CC )
78	77	adantl 464	. . . . . 6 |- ( ( R e. RR+ /\ t e. RR ) -> t e. CC )
79		1cnd 9541	. . . . . 6 |- ( ( R e. RR+ /\ t e. RR ) -> 1 e. CC )
80	2	dvmptid 22464	. . . . . 6 |- ( R e. RR+ -> ( RR _D ( t e. RR |-> t ) ) = ( t e. RR |-> 1 ) )
81		ioossre 11525	. . . . . . 7 |- ( -u R (,) R ) C_ RR
82	81	a1i 11	. . . . . 6 |- ( R e. RR+ -> ( -u R (,) R ) C_ RR )
83		eqid 2392	. . . . . . 7 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
84	83	tgioo2 21412	. . . . . 6 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
85		iooretop 21377	. . . . . . 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 22470	. . . . 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 22472	. . . 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 464	. . . . . 6 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> (arcsin ` u ) e. CC )
91		ovex 6242	. . . . . . 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 30307	. . . . . . 7 |- ( RR _D (arcsin |` ( -u 1 (,) 1 ) ) ) = ( u e. ( -u 1 (,) 1 ) |-> ( 1 / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
94		asinf 23338	. . . . . . . . . 10 |- arcsin : CC --> CC
95	94	a1i 11	. . . . . . . . 9 |- ( R e. RR+ -> arcsin : CC --> CC )
96		ioossre 11525	. . . . . . . . . . 11 |- ( -u 1 (,) 1 ) C_ RR
97		ax-resscn 9478	. . . . . . . . . . 11 |- RR C_ CC
98	96, 97	sstri 3439	. . . . . . . . . 10 |- ( -u 1 (,) 1 ) C_ CC
99	98	a1i 11	. . . . . . . . 9 |- ( R e. RR+ -> ( -u 1 (,) 1 ) C_ CC )
100	95, 99	feqresmpt 5841	. . . . . . . 8 |- ( R e. RR+ -> (arcsin |` ( -u 1 (,) 1 ) ) = ( u e. ( -u 1 (,) 1 ) |-> (arcsin ` u ) ) )
101	100	oveq2d 6230	. . . . . . 7 |- ( R e. RR+ -> ( RR _D (arcsin |` ( -u 1 (,) 1 ) ) ) = ( RR _D ( u e. ( -u 1 (,) 1 ) |-> (arcsin ` u ) ) ) )
102	93, 101	syl5reqr 2448	. . . . . 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 464	. . . . . 6 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
105		ovex 6242	. . . . . . 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 464	. . . . . . 7 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> u e. CC )
108		1cnd 9541	. . . . . . 7 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> 1 e. CC )
109		recn 9511	. . . . . . . . 9 |- ( u e. RR -> u e. CC )
110	109	adantl 464	. . . . . . . 8 |- ( ( R e. RR+ /\ u e. RR ) -> u e. CC )
111		1cnd 9541	. . . . . . . 8 |- ( ( R e. RR+ /\ u e. RR ) -> 1 e. CC )
112	2	dvmptid 22464	. . . . . . . 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 21377	. . . . . . . . 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 22470	. . . . . . 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 464	. . . . . . 7 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( sqr ` ( 1 - ( u ^ 2 ) ) ) e. CC )
119		ovex 6242	. . . . . . . 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 9540	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> 1 e. RR )
122	63	resqcld 12257	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> ( u ^ 2 ) e. RR )
123	121, 122	resubcld 9923	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> ( 1 - ( u ^ 2 ) ) e. RR )
124		elioo2 11509	. . . . . . . . . . . . 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 670	. . . . . . . . . . . 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 9540	. . . . . . . . . . . . . . . 16 |- ( u e. RR -> 1 e. RR )
128	126, 127	absltd 13282	. . . . . . . . . . . . . . 15 |- ( u e. RR -> ( ( abs ` u ) < 1 <-> ( -u 1 < u /\ u < 1 ) ) )
129	109	abscld 13288	. . . . . . . . . . . . . . . . 17 |- ( u e. RR -> ( abs ` u ) e. RR )
130	109	absge0d 13296	. . . . . . . . . . . . . . . . 17 |- ( u e. RR -> 0 <_ ( abs ` u ) )
131		0le1 10011	. . . . . . . . . . . . . . . . . 18 |- 0 <_ 1
132	131	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( u e. RR -> 0 <_ 1 )
133	129, 127, 130, 132	lt2sqd 12265	. . . . . . . . . . . . . . . 16 |- ( u e. RR -> ( ( abs ` u ) < 1 <-> ( ( abs ` u ) ^ 2 ) < ( 1 ^ 2 ) ) )
134		absresq 13156	. . . . . . . . . . . . . . . . 17 |- ( u e. RR -> ( ( abs ` u ) ^ 2 ) = ( u ^ 2 ) )
135		sq1 12184	. . . . . . . . . . . . . . . . . 18 |- ( 1 ^ 2 ) = 1
136	135	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( u e. RR -> ( 1 ^ 2 ) = 1 )
137	134, 136	breq12d 4393	. . . . . . . . . . . . . . . 16 |- ( u e. RR -> ( ( ( abs ` u ) ^ 2 ) < ( 1 ^ 2 ) <-> ( u ^ 2 ) < 1 ) )
138		resqcl 12157	. . . . . . . . . . . . . . . . 17 |- ( u e. RR -> ( u ^ 2 ) e. RR )
139	138, 127	posdifd 10074	. . . . . . . . . . . . . . . 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 1192	. . . . . . . . . . . 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 11192	. . . . . . . . . 10 |- ( u e. ( -u 1 (,) 1 ) -> ( 1 - ( u ^ 2 ) ) e. RR+ )
146	145	adantl 464	. . . . . . . . 9 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( 1 - ( u ^ 2 ) ) e. RR+ )
147		negex 9749	. . . . . . . . . 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 11165	. . . . . . . . . . 11 |- ( v e. RR+ -> v e. CC )
150	149	sqrtcld 13289	. . . . . . . . . 10 |- ( v e. RR+ -> ( sqr ` v ) e. CC )
151	150	adantl 464	. . . . . . . . 9 |- ( ( R e. RR+ /\ v e. RR+ ) -> ( sqr ` v ) e. CC )
152		ovex 6242	. . . . . . . . . 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 9541	. . . . . . . . . . . 12 |- ( u e. RR -> 1 e. CC )
155	109	sqcld 12229	. . . . . . . . . . . 12 |- ( u e. RR -> ( u ^ 2 ) e. CC )
156	154, 155	subcld 9862	. . . . . . . . . . 11 |- ( u e. RR -> ( 1 - ( u ^ 2 ) ) e. CC )
157	156	adantl 464	. . . . . . . . . 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 9526	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ u e. RR ) -> 0 e. RR )
160		1cnd 9541	. . . . . . . . . . . . 13 |- ( R e. RR+ -> 1 e. CC )
161	2, 160	dvmptc 22465	. . . . . . . . . . . 12 |- ( R e. RR+ -> ( RR _D ( u e. RR |-> 1 ) ) = ( u e. RR |-> 0 ) )
162	155	adantl 464	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ u e. RR ) -> ( u ^ 2 ) e. CC )
163		ovex 6242	. . . . . . . . . . . . 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 21394	. . . . . . . . . . . . . 14 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
166		toponmax 19533	. . . . . . . . . . . . . 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 3416	. . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . 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 10628	. . . . . . . . . . . . . . . 16 |- 2 e. NN
174		dvexp 22460	. . . . . . . . . . . . . . . 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 10585	. . . . . . . . . . . . . . . . . . 19 |- ( 2 - 1 ) = 1
177	176	oveq2i 6225	. . . . . . . . . . . . . . . . . 18 |- ( u ^ ( 2 - 1 ) ) = ( u ^ 1 )
178		exp1 12094	. . . . . . . . . . . . . . . . . 18 |- ( u e. CC -> ( u ^ 1 ) = u )
179	177, 178	syl5eq 2445	. . . . . . . . . . . . . . . . 17 |- ( u e. CC -> ( u ^ ( 2 - 1 ) ) = u )
180	179	oveq2d 6230	. . . . . . . . . . . . . . . 16 |- ( u e. CC -> ( 2 x. ( u ^ ( 2 - 1 ) ) ) = ( 2 x. u ) )
181	180	mpteq2ia 4462	. . . . . . . . . . . . . . 15 |- ( u e. CC |-> ( 2 x. ( u ^ ( 2 - 1 ) ) ) ) = ( u e. CC |-> ( 2 x. u ) )
182	175, 181	eqtri 2421	. . . . . . . . . . . . . 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 22463	. . . . . . . . . . . 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 22474	. . . . . . . . . . 11 |- ( R e. RR+ -> ( RR _D ( u e. RR |-> ( 1 - ( u ^ 2 ) ) ) ) = ( u e. RR |-> ( 0 - ( 2 x. u ) ) ) )
186		df-neg 9739	. . . . . . . . . . . 12 |- -u ( 2 x. u ) = ( 0 - ( 2 x. u ) )
187	186	mpteq2i 4463	. . . . . . . . . . 11 |- ( u e. RR |-> -u ( 2 x. u ) ) = ( u e. RR |-> ( 0 - ( 2 x. u ) ) )
188	185, 187	syl6eqr 2451	. . . . . . . . . 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 22470	. . . . . . . . 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 23224	. . . . . . . . . 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 5787	. . . . . . . . 9 |- ( v = ( 1 - ( u ^ 2 ) ) -> ( sqr ` v ) = ( sqr ` ( 1 - ( u ^ 2 ) ) ) )
193	192	oveq2d 6230	. . . . . . . . . 10 |- ( v = ( 1 - ( u ^ 2 ) ) -> ( 2 x. ( sqr ` v ) ) = ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
194	193	oveq2d 6230	. . . . . . . . 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 22479	. . . . . . . 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 10543	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> 2 e. CC )
197	196, 64	mulneg2d 9946	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> ( 2 x. -u u ) = -u ( 2 x. u ) )
198	197	oveq1d 6229	. . . . . . . . . 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 9849	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> -u u e. CC )
200	144	gt0ne0d 10052	. . . . . . . . . . . 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 463	. . . . . . . . . . . . . . 15 |- ( ( u e. ( -u 1 (,) 1 ) /\ ( sqr ` ( 1 - ( u ^ 2 ) ) ) = 0 ) -> ( 1 - ( u ^ 2 ) ) e. CC )
203		simpr 459	. . . . . . . . . . . . . . 15 |- ( ( u e. ( -u 1 (,) 1 ) /\ ( sqr ` ( 1 - ( u ^ 2 ) ) ) = 0 ) -> ( sqr ` ( 1 - ( u ^ 2 ) ) ) = 0 )
204	202, 203	sqr00d 13293	. . . . . . . . . . . . . 14 |- ( ( u e. ( -u 1 (,) 1 ) /\ ( sqr ` ( 1 - ( u ^ 2 ) ) ) = 0 ) -> ( 1 - ( u ^ 2 ) ) = 0 )
205	204	ex 432	. . . . . . . . . . . . 13 |- ( u e. ( -u 1 (,) 1 ) -> ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) = 0 -> ( 1 - ( u ^ 2 ) ) = 0 ) )
206	205	necon3d 2616	. . . . . . . . . . . 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 10563	. . . . . . . . . . . 12 |- 2 =/= 0
209	208	a1i 11	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> 2 =/= 0 )
210	199, 117, 196, 207, 209	divcan5d 10281	. . . . . . . . . 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 9545	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> ( 2 x. u ) e. CC )
212	211	negcld 9849	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> -u ( 2 x. u ) e. CC )
213	196, 117	mulcld 9545	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
214	196, 117, 209, 207	mulne0d 10136	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) =/= 0 )
215	212, 213, 214	divrec2d 10259	. . . . . . . . . 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 2442	. . . . . . . . 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 4462	. . . . . . . 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 2449	. . . . . . 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 22468	. . . . . 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 22467	. . . . 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 9543	. . . . . . . . . 10 |- ( u e. ( -u 1 (,) 1 ) -> ( 1 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) = ( sqr ` ( 1 - ( u ^ 2 ) ) ) )
222	199, 117, 207	divcld 10255	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> ( -u u / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
223	222, 64	mulcomd 9546	. . . . . . . . . . 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 10290	. . . . . . . . . . 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 9946	. . . . . . . . . . . . 13 |- ( u e. ( -u 1 (,) 1 ) -> ( u x. -u u ) = -u ( u x. u ) )
226	64	sqvald 12228	. . . . . . . . . . . . . 14 |- ( u e. ( -u 1 (,) 1 ) -> ( u ^ 2 ) = ( u x. u ) )
227	226	negeqd 9745	. . . . . . . . . . . . 13 |- ( u e. ( -u 1 (,) 1 ) -> -u ( u ^ 2 ) = -u ( u x. u ) )
228	225, 227	eqtr4d 2436	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> ( u x. -u u ) = -u ( u ^ 2 ) )
229	228	oveq1d 6229	. . . . . . . . . . 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 2439	. . . . . . . . . 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 6232	. . . . . . . . 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 12229	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> ( u ^ 2 ) e. CC )
233	232	negcld 9849	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> -u ( u ^ 2 ) e. CC )
234	233, 117, 207	divcld 10255	. . . . . . . . . 10 |- ( u e. ( -u 1 (,) 1 ) -> ( -u ( u ^ 2 ) / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
235	117, 234	addcomd 9711	. . . . . . . . 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 2433	. . . . . . . 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 6230	. . . . . . 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 10716	. . . . . . . 8 |- ( u e. ( -u 1 (,) 1 ) -> ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) = ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) + ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
239	67, 68	negsubd 9868	. . . . . . . . . . . . 13 |- ( u e. CC -> ( 1 + -u ( u ^ 2 ) ) = ( 1 - ( u ^ 2 ) ) )
240	69	sqsqrtd 13291	. . . . . . . . . . . . 13 |- ( u e. CC -> ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) ^ 2 ) = ( 1 - ( u ^ 2 ) ) )
241	70	sqvald 12228	. . . . . . . . . . . . 13 |- ( u e. CC -> ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) ^ 2 ) = ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
242	239, 240, 241	3eqtr2d 2439	. . . . . . . . . . . 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 6229	. . . . . . . . . 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 9541	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> 1 e. CC )
246	245, 233, 117, 207	divdird 10293	. . . . . . . . . 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 10260	. . . . . . . . . 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 2442	. . . . . . . . 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 6229	. . . . . . . 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 10248	. . . . . . . . 9 |- ( u e. ( -u 1 (,) 1 ) -> ( 1 / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
251	250, 234, 117	addassd 9547	. . . . . . . 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 2438	. . . . . . 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 2433	. . . . . 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 4462	. . . . 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 2449	. . . 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 5787	. . . . 5 |- ( u = ( t / R ) -> (arcsin ` u ) = (arcsin ` ( t / R ) ) )
257		id 22	. . . . . 6 |- ( u = ( t / R ) -> u = ( t / R ) )
258		oveq1 6221	. . . . . . . 8 |- ( u = ( t / R ) -> ( u ^ 2 ) = ( ( t / R ) ^ 2 ) )
259	258	oveq2d 6230	. . . . . . 7 |- ( u = ( t / R ) -> ( 1 - ( u ^ 2 ) ) = ( 1 - ( ( t / R ) ^ 2 ) ) )
260	259	fveq2d 5791	. . . . . 6 |- ( u = ( t / R ) -> ( sqr ` ( 1 - ( u ^ 2 ) ) ) = ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) )
261	257, 260	oveq12d 6232	. . . . 5 |- ( u = ( t / R ) -> ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) = ( ( t / R ) x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) )
262	256, 261	oveq12d 6232	. . . 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 6230	. . . 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 22479	. . 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 12229	. . 3 |- ( R e. RR+ -> ( R ^ 2 ) e. CC )
266	2, 18, 20, 264, 265	dvmptcmul 22471	. 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 10543	. . . . . . 7 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 2 e. CC )
268	267, 16	mulcld 9545	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 2 x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. CC )
269	6, 8	reccld 10248	. . . . . . 7 |- ( R e. RR+ -> ( 1 / R ) e. CC )
270	269	adantr 463	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 1 / R ) e. CC )
271	268, 270	mulcomd 9546	. . . . 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 6230	. . . 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 463	. . . . 5 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( R ^ 2 ) e. CC )
274	273, 270, 268	mulassd 9548	. . . 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 12228	. . . . . . . . 9 |- ( R e. RR+ -> ( R ^ 2 ) = ( R x. R ) )
276	275	oveq1d 6229	. . . . . . . 8 |- ( R e. RR+ -> ( ( R ^ 2 ) / R ) = ( ( R x. R ) / R ) )
277	265, 6, 8	divrecd 10258	. . . . . . . 8 |- ( R e. RR+ -> ( ( R ^ 2 ) / R ) = ( ( R ^ 2 ) x. ( 1 / R ) ) )
278	6, 6, 8	divcan3d 10260	. . . . . . . 8 |- ( R e. RR+ -> ( ( R x. R ) / R ) = R )
279	276, 277, 278	3eqtr3d 2441	. . . . . . 7 |- ( R e. RR+ -> ( ( R ^ 2 ) x. ( 1 / R ) ) = R )
280	279	adantr 463	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( 1 / R ) ) = R )
281	280	oveq1d 6229	. . . . 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 9718	. . . . 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 12257	. . . . . . . . 9 |- ( R e. RR+ -> ( R ^ 2 ) e. RR )
284	283	adantr 463	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( R ^ 2 ) e. RR )
285	21	sqge0d 12258	. . . . . . . . 9 |- ( R e. RR+ -> 0 <_ ( R ^ 2 ) )
286	285	adantr 463	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 <_ ( R ^ 2 ) )
287		1red 9540	. . . . . . . . 9 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 1 e. RR )
288	3	adantl 464	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> t e. RR )
289	21	adantr 463	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> R e. RR )
290	288, 289, 9	redivcld 10307	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( t / R ) e. RR )
291	290	resqcld 12257	. . . . . . . . 9 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) ^ 2 ) e. RR )
292	287, 291	resubcld 9923	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 1 - ( ( t / R ) ^ 2 ) ) e. RR )
293		0red 9526	. . . . . . . . 9 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 e. RR )
294	27, 28	absltd 13282	. . . . . . . . . . . . . . 15 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) < R <-> ( -u R < t /\ t < R ) ) )
295	77	abscld 13288	. . . . . . . . . . . . . . . . . 18 |- ( t e. RR -> ( abs ` t ) e. RR )
296	295	adantl 464	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> ( abs ` t ) e. RR )
297	77	absge0d 13296	. . . . . . . . . . . . . . . . . 18 |- ( t e. RR -> 0 <_ ( abs ` t ) )
298	297	adantl 464	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> 0 <_ ( abs ` t ) )
299		rpge0 11169	. . . . . . . . . . . . . . . . . 18 |- ( R e. RR+ -> 0 <_ R )
300	299	adantr 463	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> 0 <_ R )
301	296, 28, 298, 300	lt2sqd 12265	. . . . . . . . . . . . . . . 16 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) < R <-> ( ( abs ` t ) ^ 2 ) < ( R ^ 2 ) ) )
302		absresq 13156	. . . . . . . . . . . . . . . . . 18 |- ( t e. RR -> ( ( abs ` t ) ^ 2 ) = ( t ^ 2 ) )
303	302	adantl 464	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) ^ 2 ) = ( t ^ 2 ) )
304	265	adantr 463	. . . . . . . . . . . . . . . . . . 19 |- ( ( R e. RR+ /\ t e. RR ) -> ( R ^ 2 ) e. CC )
305	304	mulid1d 9542	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( R ^ 2 ) x. 1 ) = ( R ^ 2 ) )
306	305	eqcomd 2400	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> ( R ^ 2 ) = ( ( R ^ 2 ) x. 1 ) )
307	303, 306	breq12d 4393	. . . . . . . . . . . . . . . 16 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( ( abs ` t ) ^ 2 ) < ( R ^ 2 ) <-> ( t ^ 2 ) < ( ( R ^ 2 ) x. 1 ) ) )
308	6	adantr 463	. . . . . . . . . . . . . . . . . . 19 |- ( ( R e. RR+ /\ t e. RR ) -> R e. CC )
309	78, 308, 29	sqdivd 12244	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( t / R ) ^ 2 ) = ( ( t ^ 2 ) / ( R ^ 2 ) ) )
310	309	breq1d 4390	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( ( t / R ) ^ 2 ) < 1 <-> ( ( t ^ 2 ) / ( R ^ 2 ) ) < 1 ) )
311	30	resqcld 12257	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( t / R ) ^ 2 ) e. RR )
312	311, 42	posdifd 10074	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( ( t / R ) ^ 2 ) < 1 <-> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
313		resqcl 12157	. . . . . . . . . . . . . . . . . . 19 |- ( t e. RR -> ( t ^ 2 ) e. RR )
314	313	adantl 464	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR+ /\ t e. RR ) -> ( t ^ 2 ) e. RR )
315		rpgt0 11168	. . . . . . . . . . . . . . . . . . . . 21 |- ( R e. RR+ -> 0 < R )
316		0red 9526	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( R e. RR+ -> 0 e. RR )
317		0le0 10560	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 0 <_ 0
318	317	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( R e. RR+ -> 0 <_ 0 )
319	316, 21, 318, 299	lt2sqd 12265	. . . . . . . . . . . . . . . . . . . . . 22 |- ( R e. RR+ -> ( 0 < R <-> ( 0 ^ 2 ) < ( R ^ 2 ) ) )
320		sq0 12181	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 0 ^ 2 ) = 0
321	320	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( R e. RR+ -> ( 0 ^ 2 ) = 0 )
322	321	breq1d 4390	. . . . . . . . . . . . . . . . . . . . . 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 11192	. . . . . . . . . . . . . . . . . . 19 |- ( R e. RR+ -> ( R ^ 2 ) e. RR+ )
326	325	adantr 463	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR+ /\ t e. RR ) -> ( R ^ 2 ) e. RR+ )
327	314, 42, 326	ltdivmuld 11242	. . . . . . . . . . . . . . . . 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 605	. . . . . . . . . . . 12 |- ( R e. RR+ -> ( t e. RR -> ( -u R < t -> ( t < R -> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) )
333	332	3impd 1208	. . . . . . . . . . 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 427	. . . . . . . . 9 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) )
336	293, 292, 335	ltled 9662	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 <_ ( 1 - ( ( t / R ) ^ 2 ) ) )
337	284, 286, 292, 336	sqrtmuld 13277	. . . . . . 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 9948	. . . . . . . . 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 9542	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. 1 ) = ( R ^ 2 ) )
340	5, 7, 9	sqdivd 12244	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) ^ 2 ) = ( ( t ^ 2 ) / ( R ^ 2 ) ) )
341	340	oveq2d 6230	. . . . . . . . . . 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 12229	. . . . . . . . . . . . 13 |- ( t e. ( -u R (,) R ) -> ( t ^ 2 ) e. CC )
343	342	adantl 464	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( t ^ 2 ) e. CC )
344		sqne0 12156	. . . . . . . . . . . . . . 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 463	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( R ^ 2 ) =/= 0 )
348	343, 273, 347	divcan2d 10257	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( ( t ^ 2 ) / ( R ^ 2 ) ) ) = ( t ^ 2 ) )
349	341, 348	eqtrd 2433	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( ( t / R ) ^ 2 ) ) = ( t ^ 2 ) )
350	339, 349	oveq12d 6232	. . . . . . . . 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 2433	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( 1 - ( ( t / R ) ^ 2 ) ) ) = ( ( R ^ 2 ) - ( t ^ 2 ) ) )
352	351	fveq2d 5791	. . . . . . 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 13272	. . . . . . . . 9 |- ( R e. RR+ -> ( sqr ` ( R ^ 2 ) ) = R )
354	353	adantr 463	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( sqr ` ( R ^ 2 ) ) = R )
355	354	oveq1d 6229	. . . . . . 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 2442	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( R x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) = ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
357	356	oveq2d 6230	. . . . 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 2437	. . . 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 2439	. . 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 4466	. 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 2433	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 367   /\ w3a 971   = wceq 1399   e. wcel 1836   =/= wne 2587   _Vcvv 3047   i^i cin 3401   C_ wss 3402   {cpr 3959   class class class wbr 4380   |-> cmpt 4438   ran crn 4927   |` cres 4928   -->wf 5505   ` cfv 5509  (class class class)co 6214   CCcc 9419   RRcr 9420   0cc0 9421   1c1 9422   + caddc 9424   x. cmul 9426   RR*cxr 9556   < clt 9557   <_ cle 9558   - cmin 9736   -ucneg 9737   / cdiv 10141   NNcn 10470   2c2 10520   RR+crp 11157   (,)cioo 11468   ^cexp 12088   sqrcsqrt 13087   abscabs 13088   TopOpenctopn 14848   topGenctg 14864  ℂ_fldccnfld 18552  TopOnctopon 19499   _D cdv 22371  arcsincasin 23328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-rep 4491  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509  ax-inf2 7990  ax-cnex 9477  ax-resscn 9478  ax-1cn 9479  ax-icn 9480  ax-addcl 9481  ax-addrcl 9482  ax-mulcl 9483  ax-mulrcl 9484  ax-mulcom 9485  ax-addass 9486  ax-mulass 9487  ax-distr 9488  ax-i2m1 9489  ax-1ne0 9490  ax-1rid 9491  ax-rnegex 9492  ax-rrecex 9493  ax-cnre 9494  ax-pre-lttri 9495  ax-pre-lttrn 9496  ax-pre-ltadd 9497  ax-pre-mulgt0 9498  ax-pre-sup 9499  ax-addf 9500  ax-mulf 9501

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-fal 1405  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-nel 2590  df-ral 2747  df-rex 2748  df-reu 2749  df-rmo 2750  df-rab 2751  df-v 3049  df-sbc 3266  df-csb 3362  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-pss 3418  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-tp 3962  df-op 3964  df-uni 4177  df-int 4213  df-iun 4258  df-iin 4259  df-br 4381  df-opab 4439  df-mpt 4440  df-tr 4474  df-eprel 4718  df-id 4722  df-po 4727  df-so 4728  df-fr 4765  df-se 4766  df-we 4767  df-ord 4808  df-on 4809  df-lim 4810  df-suc 4811  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-fv 5517  df-isom 5518  df-riota 6176  df-ov 6217  df-oprab 6218  df-mpt2 6219  df-of 6457  df-om 6618  df-1st 6717  df-2nd 6718  df-supp 6836  df-recs 6978  df-rdg 7012  df-1o 7066  df-2o 7067  df-oadd 7070  df-er 7247  df-map 7358  df-pm 7359  df-ixp 7407  df-en 7454  df-dom 7455  df-sdom 7456  df-fin 7457  df-fsupp 7763  df-fi 7804  df-sup 7834  df-oi 7868  df-card 8251  df-cda 8479  df-pnf 9559  df-mnf 9560  df-xr 9561  df-ltxr 9562  df-le 9563  df-sub 9738  df-neg 9739  df-div 10142  df-nn 10471  df-2 10529  df-3 10530  df-4 10531  df-5 10532  df-6 10533  df-7 10534  df-8 10535  df-9 10536  df-10 10537  df-n0 10731  df-z 10800  df-dec 10914  df-uz 11020  df-q 11120  df-rp 11158  df-xneg 11257  df-xadd 11258  df-xmul 11259  df-ioo 11472  df-ioc 11473  df-ico 11474  df-icc 11475  df-fz 11612  df-fzo 11736  df-fl 11847  df-mod 11916  df-seq 12030  df-exp 12089  df-fac 12275  df-bc 12302  df-hash 12327  df-shft 12921  df-cj 12953  df-re 12954  df-im 12955  df-sqrt 13089  df-abs 13090  df-limsup 13315  df-clim 13332  df-rlim 13333  df-sum 13530  df-ef 13824  df-sin 13826  df-cos 13827  df-tan 13828  df-pi 13829  df-struct 14655  df-ndx 14656  df-slot 14657  df-base 14658  df-sets 14659  df-ress 14660  df-plusg 14734  df-mulr 14735  df-starv 14736  df-sca 14737  df-vsca 14738  df-ip 14739  df-tset 14740  df-ple 14741  df-ds 14743  df-unif 14744  df-hom 14745  df-cco 14746  df-rest 14849  df-topn 14850  df-0g 14868  df-gsum 14869  df-topgen 14870  df-pt 14871  df-prds 14874  df-xrs 14928  df-qtop 14933  df-imas 14934  df-xps 14936  df-mre 15012  df-mrc 15013  df-acs 15015  df-mgm 16008  df-sgrp 16047  df-mnd 16057  df-submnd 16103  df-mulg 16196  df-cntz 16491  df-cmn 16936  df-psmet 18543  df-xmet 18544  df-met 18545  df-bl 18546  df-mopn 18547  df-fbas 18548  df-fg 18549  df-cnfld 18553  df-top 19503  df-bases 19505  df-topon 19506  df-topsp 19507  df-cld 19624  df-ntr 19625  df-cls 19626  df-nei 19704  df-lp 19742  df-perf 19743  df-cn 19833  df-cnp 19834  df-haus 19921  df-cmp 19992  df-tx 20167  df-hmeo 20360  df-fil 20451  df-fm 20543  df-flim 20544  df-flf 20545  df-xms 20927  df-ms 20928  df-tms 20929  df-cncf 21486  df-limc 22374  df-dv 22375  df-log 23048  df-cxp 23049  df-asin 23331

This theorem is referenced by:  areacirc  30314