Theorem areacirclem1 31990

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 9633	. . . 4 |- RR e. { RR , CC }
2	1	a1i 11	. . 3 |- ( R e. RR+ -> RR e. { RR , CC } )
3		elioore 11668	. . . . . . . 8 |- ( t e. ( -u R (,) R ) -> t e. RR )
4	3	recnd 9671	. . . . . . 7 |- ( t e. ( -u R (,) R ) -> t e. CC )
5	4	adantl 468	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> t e. CC )
6		rpcn 11312	. . . . . . 7 |- ( R e. RR+ -> R e. CC )
7	6	adantr 467	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> R e. CC )
8		rpne0 11319	. . . . . . 7 |- ( R e. RR+ -> R =/= 0 )
9	8	adantr 467	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> R =/= 0 )
10	5, 7, 9	divcld 10385	. . . . 5 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( t / R ) e. CC )
11		asincl 23791	. . . . 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 9661	. . . . . . 7 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 1 e. CC )
14	10	sqcld 12415	. . . . . . 7 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) ^ 2 ) e. CC )
15	13, 14	subcld 9988	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 1 - ( ( t / R ) ^ 2 ) ) e. CC )
16	15	sqrtcld 13492	. . . . 5 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) e. CC )
17	10, 16	mulcld 9665	. . . 4 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. CC )
18	12, 17	addcld 9664	. . 3 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( (arcsin ` ( t / R ) ) + ( ( t / R ) x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) e. CC )
19		ovex 6331	. . . 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 11310	. . . . . . . . . 10 |- ( R e. RR+ -> R e. RR )
22	21	renegcld 10048	. . . . . . . . 9 |- ( R e. RR+ -> -u R e. RR )
23	22	rexrd 9692	. . . . . . . 8 |- ( R e. RR+ -> -u R e. RR* )
24		rpxr 11311	. . . . . . . 8 |- ( R e. RR+ -> R e. RR* )
25		elioo2 11679	. . . . . . . 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 666	. . . . . . 7 |- ( R e. RR+ -> ( t e. ( -u R (,) R ) <-> ( t e. RR /\ -u R < t /\ t < R ) ) )
27		simpr 463	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. RR ) -> t e. RR )
28	21	adantr 467	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. RR ) -> R e. RR )
29	8	adantr 467	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. RR ) -> R =/= 0 )
30	27, 28, 29	redivcld 10437	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. RR ) -> ( t / R ) e. RR )
31	30	a1d 27	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) -> ( t / R ) e. RR ) )
32	6	mulm1d 10072	. . . . . . . . . . . . . . 15 |- ( R e. RR+ -> ( -u 1 x. R ) = -u R )
33	32	adantr 467	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. RR ) -> ( -u 1 x. R ) = -u R )
34	33	breq1d 4431	. . . . . . . . . . . . 13 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u 1 x. R ) < t <-> -u R < t ) )
35		neg1rr 10716	. . . . . . . . . . . . . . 15 |- -u 1 e. RR
36	35	a1i 11	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. RR ) -> -u 1 e. RR )
37		simpl 459	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. RR ) -> R e. RR+ )
38	36, 27, 37	ltmuldivd 11387	. . . . . . . . . . . . 13 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u 1 x. R ) < t <-> -u 1 < ( t / R ) ) )
39	34, 38	bitr3d 259	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. RR ) -> ( -u R < t <-> -u 1 < ( t / R ) ) )
40	39	biimpd 211	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. RR ) -> ( -u R < t -> -u 1 < ( t / R ) ) )
41	40	adantrd 470	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) -> -u 1 < ( t / R ) ) )
42		1red 9660	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. RR ) -> 1 e. RR )
43	27, 42, 37	ltdivmuld 11391	. . . . . . . . . . . . 13 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( t / R ) < 1 <-> t < ( R x. 1 ) ) )
44	6	mulid1d 9662	. . . . . . . . . . . . . . 15 |- ( R e. RR+ -> ( R x. 1 ) = R )
45	44	adantr 467	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. RR ) -> ( R x. 1 ) = R )
46	45	breq2d 4433	. . . . . . . . . . . . 13 |- ( ( R e. RR+ /\ t e. RR ) -> ( t < ( R x. 1 ) <-> t < R ) )
47	43, 46	bitr2d 258	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. RR ) -> ( t < R <-> ( t / R ) < 1 ) )
48	47	biimpd 211	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. RR ) -> ( t < R -> ( t / R ) < 1 ) )
49	48	adantld 469	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) -> ( t / R ) < 1 ) )
50	31, 41, 49	3jcad 1187	. . . . . . . . 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 611	. . . . . . . 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 1220	. . . . . . 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 219	. . . . . 6 |- ( R e. RR+ -> ( t e. ( -u R (,) R ) -> ( ( t / R ) e. RR /\ -u 1 < ( t / R ) /\ ( t / R ) < 1 ) ) )
54	53	imp 431	. . . . 5 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) e. RR /\ -u 1 < ( t / R ) /\ ( t / R ) < 1 ) )
55	35	rexri 9695	. . . . . 6 |- -u 1 e. RR*
56		1re 9644	. . . . . . 7 |- 1 e. RR
57	56	rexri 9695	. . . . . 6 |- 1 e. RR*
58		elioo2 11679	. . . . . 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 677	. . . . 5 |- ( ( t / R ) e. ( -u 1 (,) 1 ) <-> ( ( t / R ) e. RR /\ -u 1 < ( t / R ) /\ ( t / R ) < 1 ) )
60	54, 59	sylibr 216	. . . 4 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( t / R ) e. ( -u 1 (,) 1 ) )
61		ovex 6331	. . . . 5 |- ( 1 / R ) e. _V
62	61	a1i 11	. . . 4 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 1 / R ) e. _V )
63		elioore 11668	. . . . . . 7 |- ( u e. ( -u 1 (,) 1 ) -> u e. RR )
64	63	recnd 9671	. . . . . 6 |- ( u e. ( -u 1 (,) 1 ) -> u e. CC )
65		asincl 23791	. . . . . . 7 |- ( u e. CC -> (arcsin ` u ) e. CC )
66		id 23	. . . . . . . 8 |- ( u e. CC -> u e. CC )
67		1cnd 9661	. . . . . . . . . 10 |- ( u e. CC -> 1 e. CC )
68		sqcl 12338	. . . . . . . . . 10 |- ( u e. CC -> ( u ^ 2 ) e. CC )
69	67, 68	subcld 9988	. . . . . . . . 9 |- ( u e. CC -> ( 1 - ( u ^ 2 ) ) e. CC )
70	69	sqrtcld 13492	. . . . . . . 8 |- ( u e. CC -> ( sqr ` ( 1 - ( u ^ 2 ) ) ) e. CC )
71	66, 70	mulcld 9665	. . . . . . 7 |- ( u e. CC -> ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
72	65, 71	addcld 9664	. . . . . 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 468	. . . 4 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( (arcsin ` u ) + ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) ) e. CC )
75		ovex 6331	. . . . 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 9631	. . . . . . 7 |- ( t e. RR -> t e. CC )
78	77	adantl 468	. . . . . 6 |- ( ( R e. RR+ /\ t e. RR ) -> t e. CC )
79		1cnd 9661	. . . . . 6 |- ( ( R e. RR+ /\ t e. RR ) -> 1 e. CC )
80	2	dvmptid 22903	. . . . . 6 |- ( R e. RR+ -> ( RR _D ( t e. RR |-> t ) ) = ( t e. RR |-> 1 ) )
81		ioossre 11698	. . . . . . 7 |- ( -u R (,) R ) C_ RR
82	81	a1i 11	. . . . . 6 |- ( R e. RR+ -> ( -u R (,) R ) C_ RR )
83		eqid 2423	. . . . . . 7 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
84	83	tgioo2 21813	. . . . . 6 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
85		iooretop 21778	. . . . . . 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 22909	. . . . 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 22911	. . . 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 468	. . . . . 6 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> (arcsin ` u ) e. CC )
91		ovex 6331	. . . . . . 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 31988	. . . . . . 7 |- ( RR _D (arcsin |` ( -u 1 (,) 1 ) ) ) = ( u e. ( -u 1 (,) 1 ) |-> ( 1 / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
94		asinf 23790	. . . . . . . . . 10 |- arcsin : CC --> CC
95	94	a1i 11	. . . . . . . . 9 |- ( R e. RR+ -> arcsin : CC --> CC )
96		ioossre 11698	. . . . . . . . . . 11 |- ( -u 1 (,) 1 ) C_ RR
97		ax-resscn 9598	. . . . . . . . . . 11 |- RR C_ CC
98	96, 97	sstri 3474	. . . . . . . . . 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 6319	. . . . . . 7 |- ( R e. RR+ -> ( RR _D (arcsin |` ( -u 1 (,) 1 ) ) ) = ( RR _D ( u e. ( -u 1 (,) 1 ) |-> (arcsin ` u ) ) ) )
102	93, 101	syl5reqr 2479	. . . . . 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 468	. . . . . 6 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
105		ovex 6331	. . . . . . 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 468	. . . . . . 7 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> u e. CC )
108		1cnd 9661	. . . . . . 7 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> 1 e. CC )
109		recn 9631	. . . . . . . . 9 |- ( u e. RR -> u e. CC )
110	109	adantl 468	. . . . . . . 8 |- ( ( R e. RR+ /\ u e. RR ) -> u e. CC )
111		1cnd 9661	. . . . . . . 8 |- ( ( R e. RR+ /\ u e. RR ) -> 1 e. CC )
112	2	dvmptid 22903	. . . . . . . 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 21778	. . . . . . . . 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 22909	. . . . . . 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 468	. . . . . . 7 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( sqr ` ( 1 - ( u ^ 2 ) ) ) e. CC )
119		ovex 6331	. . . . . . . 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 9660	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> 1 e. RR )
122	63	resqcld 12443	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> ( u ^ 2 ) e. RR )
123	121, 122	resubcld 10049	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> ( 1 - ( u ^ 2 ) ) e. RR )
124		elioo2 11679	. . . . . . . . . . . . 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 677	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) <-> ( u e. RR /\ -u 1 < u /\ u < 1 ) )
126		id 23	. . . . . . . . . . . . . . . 16 |- ( u e. RR -> u e. RR )
127		1red 9660	. . . . . . . . . . . . . . . 16 |- ( u e. RR -> 1 e. RR )
128	126, 127	absltd 13485	. . . . . . . . . . . . . . 15 |- ( u e. RR -> ( ( abs ` u ) < 1 <-> ( -u 1 < u /\ u < 1 ) ) )
129	109	abscld 13491	. . . . . . . . . . . . . . . . 17 |- ( u e. RR -> ( abs ` u ) e. RR )
130	109	absge0d 13499	. . . . . . . . . . . . . . . . 17 |- ( u e. RR -> 0 <_ ( abs ` u ) )
131		0le1 10139	. . . . . . . . . . . . . . . . . 18 |- 0 <_ 1
132	131	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( u e. RR -> 0 <_ 1 )
133	129, 127, 130, 132	lt2sqd 12451	. . . . . . . . . . . . . . . 16 |- ( u e. RR -> ( ( abs ` u ) < 1 <-> ( ( abs ` u ) ^ 2 ) < ( 1 ^ 2 ) ) )
134		absresq 13359	. . . . . . . . . . . . . . . . 17 |- ( u e. RR -> ( ( abs ` u ) ^ 2 ) = ( u ^ 2 ) )
135		sq1 12370	. . . . . . . . . . . . . . . . . 18 |- ( 1 ^ 2 ) = 1
136	135	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( u e. RR -> ( 1 ^ 2 ) = 1 )
137	134, 136	breq12d 4434	. . . . . . . . . . . . . . . 16 |- ( u e. RR -> ( ( ( abs ` u ) ^ 2 ) < ( 1 ^ 2 ) <-> ( u ^ 2 ) < 1 ) )
138		resqcl 12343	. . . . . . . . . . . . . . . . 17 |- ( u e. RR -> ( u ^ 2 ) e. RR )
139	138, 127	posdifd 10202	. . . . . . . . . . . . . . . 16 |- ( u e. RR -> ( ( u ^ 2 ) < 1 <-> 0 < ( 1 - ( u ^ 2 ) ) ) )
140	133, 137, 139	3bitrd 283	. . . . . . . . . . . . . . 15 |- ( u e. RR -> ( ( abs ` u ) < 1 <-> 0 < ( 1 - ( u ^ 2 ) ) ) )
141	128, 140	bitr3d 259	. . . . . . . . . . . . . 14 |- ( u e. RR -> ( ( -u 1 < u /\ u < 1 ) <-> 0 < ( 1 - ( u ^ 2 ) ) ) )
142	141	biimpd 211	. . . . . . . . . . . . 13 |- ( u e. RR -> ( ( -u 1 < u /\ u < 1 ) -> 0 < ( 1 - ( u ^ 2 ) ) ) )
143	142	3impib 1204	. . . . . . . . . . . 12 |- ( ( u e. RR /\ -u 1 < u /\ u < 1 ) -> 0 < ( 1 - ( u ^ 2 ) ) )
144	125, 143	sylbi 199	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> 0 < ( 1 - ( u ^ 2 ) ) )
145	123, 144	elrpd 11340	. . . . . . . . . 10 |- ( u e. ( -u 1 (,) 1 ) -> ( 1 - ( u ^ 2 ) ) e. RR+ )
146	145	adantl 468	. . . . . . . . 9 |- ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( 1 - ( u ^ 2 ) ) e. RR+ )
147		negex 9875	. . . . . . . . . 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 11312	. . . . . . . . . . 11 |- ( v e. RR+ -> v e. CC )
150	149	sqrtcld 13492	. . . . . . . . . 10 |- ( v e. RR+ -> ( sqr ` v ) e. CC )
151	150	adantl 468	. . . . . . . . 9 |- ( ( R e. RR+ /\ v e. RR+ ) -> ( sqr ` v ) e. CC )
152		ovex 6331	. . . . . . . . . 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 9661	. . . . . . . . . . . 12 |- ( u e. RR -> 1 e. CC )
155	109	sqcld 12415	. . . . . . . . . . . 12 |- ( u e. RR -> ( u ^ 2 ) e. CC )
156	154, 155	subcld 9988	. . . . . . . . . . 11 |- ( u e. RR -> ( 1 - ( u ^ 2 ) ) e. CC )
157	156	adantl 468	. . . . . . . . . 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 9646	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ u e. RR ) -> 0 e. RR )
160		1cnd 9661	. . . . . . . . . . . . 13 |- ( R e. RR+ -> 1 e. CC )
161	2, 160	dvmptc 22904	. . . . . . . . . . . 12 |- ( R e. RR+ -> ( RR _D ( u e. RR |-> 1 ) ) = ( u e. RR |-> 0 ) )
162	155	adantl 468	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ u e. RR ) -> ( u ^ 2 ) e. CC )
163		ovex 6331	. . . . . . . . . . . . 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 21795	. . . . . . . . . . . . . 14 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
166		toponmax 19935	. . . . . . . . . . . . . 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 3451	. . . . . . . . . . . . . . 15 |- ( RR C_ CC <-> ( RR i^i CC ) = RR )
169	97, 168	mpbi 212	. . . . . . . . . . . . . 14 |- ( RR i^i CC ) = RR
170	169	a1i 11	. . . . . . . . . . . . 13 |- ( R e. RR+ -> ( RR i^i CC ) = RR )
171	68	adantl 468	. . . . . . . . . . . . 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 10769	. . . . . . . . . . . . . . . 16 |- 2 e. NN
174		dvexp 22899	. . . . . . . . . . . . . . . 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 10726	. . . . . . . . . . . . . . . . . . 19 |- ( 2 - 1 ) = 1
177	176	oveq2i 6314	. . . . . . . . . . . . . . . . . 18 |- ( u ^ ( 2 - 1 ) ) = ( u ^ 1 )
178		exp1 12279	. . . . . . . . . . . . . . . . . 18 |- ( u e. CC -> ( u ^ 1 ) = u )
179	177, 178	syl5eq 2476	. . . . . . . . . . . . . . . . 17 |- ( u e. CC -> ( u ^ ( 2 - 1 ) ) = u )
180	179	oveq2d 6319	. . . . . . . . . . . . . . . 16 |- ( u e. CC -> ( 2 x. ( u ^ ( 2 - 1 ) ) ) = ( 2 x. u ) )
181	180	mpteq2ia 4504	. . . . . . . . . . . . . . 15 |- ( u e. CC |-> ( 2 x. ( u ^ ( 2 - 1 ) ) ) ) = ( u e. CC |-> ( 2 x. u ) )
182	175, 181	eqtri 2452	. . . . . . . . . . . . . 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 22902	. . . . . . . . . . . 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 22913	. . . . . . . . . . 11 |- ( R e. RR+ -> ( RR _D ( u e. RR |-> ( 1 - ( u ^ 2 ) ) ) ) = ( u e. RR |-> ( 0 - ( 2 x. u ) ) ) )
186		df-neg 9865	. . . . . . . . . . . 12 |- -u ( 2 x. u ) = ( 0 - ( 2 x. u ) )
187	186	mpteq2i 4505	. . . . . . . . . . 11 |- ( u e. RR |-> -u ( 2 x. u ) ) = ( u e. RR |-> ( 0 - ( 2 x. u ) ) )
188	185, 187	syl6eqr 2482	. . . . . . . . . 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 22909	. . . . . . . . 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 23674	. . . . . . . . . 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 6319	. . . . . . . . . 10 |- ( v = ( 1 - ( u ^ 2 ) ) -> ( 2 x. ( sqr ` v ) ) = ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
194	193	oveq2d 6319	. . . . . . . . 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 22918	. . . . . . . 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 10684	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> 2 e. CC )
197	196, 64	mulneg2d 10074	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> ( 2 x. -u u ) = -u ( 2 x. u ) )
198	197	oveq1d 6318	. . . . . . . . . 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 9975	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> -u u e. CC )
200	144	gt0ne0d 10180	. . . . . . . . . . . 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 467	. . . . . . . . . . . . . . 15 |- ( ( u e. ( -u 1 (,) 1 ) /\ ( sqr ` ( 1 - ( u ^ 2 ) ) ) = 0 ) -> ( 1 - ( u ^ 2 ) ) e. CC )
203		simpr 463	. . . . . . . . . . . . . . 15 |- ( ( u e. ( -u 1 (,) 1 ) /\ ( sqr ` ( 1 - ( u ^ 2 ) ) ) = 0 ) -> ( sqr ` ( 1 - ( u ^ 2 ) ) ) = 0 )
204	202, 203	sqr00d 13496	. . . . . . . . . . . . . 14 |- ( ( u e. ( -u 1 (,) 1 ) /\ ( sqr ` ( 1 - ( u ^ 2 ) ) ) = 0 ) -> ( 1 - ( u ^ 2 ) ) = 0 )
205	204	ex 436	. . . . . . . . . . . . 13 |- ( u e. ( -u 1 (,) 1 ) -> ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) = 0 -> ( 1 - ( u ^ 2 ) ) = 0 ) )
206	205	necon3d 2649	. . . . . . . . . . . 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 10704	. . . . . . . . . . . 12 |- 2 =/= 0
209	208	a1i 11	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> 2 =/= 0 )
210	199, 117, 196, 207, 209	divcan5d 10411	. . . . . . . . . 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 9665	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> ( 2 x. u ) e. CC )
212	211	negcld 9975	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> -u ( 2 x. u ) e. CC )
213	196, 117	mulcld 9665	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
214	196, 117, 209, 207	mulne0d 10266	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) =/= 0 )
215	212, 213, 214	divrec2d 10389	. . . . . . . . . 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 2473	. . . . . . . . 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 4504	. . . . . . . 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 2480	. . . . . . 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 22907	. . . . . 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 22906	. . . . 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 9663	. . . . . . . . . 10 |- ( u e. ( -u 1 (,) 1 ) -> ( 1 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) = ( sqr ` ( 1 - ( u ^ 2 ) ) ) )
222	199, 117, 207	divcld 10385	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> ( -u u / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
223	222, 64	mulcomd 9666	. . . . . . . . . . 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 10420	. . . . . . . . . . 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 10074	. . . . . . . . . . . . 13 |- ( u e. ( -u 1 (,) 1 ) -> ( u x. -u u ) = -u ( u x. u ) )
226	64	sqvald 12414	. . . . . . . . . . . . . 14 |- ( u e. ( -u 1 (,) 1 ) -> ( u ^ 2 ) = ( u x. u ) )
227	226	negeqd 9871	. . . . . . . . . . . . 13 |- ( u e. ( -u 1 (,) 1 ) -> -u ( u ^ 2 ) = -u ( u x. u ) )
228	225, 227	eqtr4d 2467	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> ( u x. -u u ) = -u ( u ^ 2 ) )
229	228	oveq1d 6318	. . . . . . . . . . 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 2470	. . . . . . . . . 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 6321	. . . . . . . . 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 12415	. . . . . . . . . . . 12 |- ( u e. ( -u 1 (,) 1 ) -> ( u ^ 2 ) e. CC )
233	232	negcld 9975	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> -u ( u ^ 2 ) e. CC )
234	233, 117, 207	divcld 10385	. . . . . . . . . 10 |- ( u e. ( -u 1 (,) 1 ) -> ( -u ( u ^ 2 ) / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
235	117, 234	addcomd 9837	. . . . . . . . 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 2464	. . . . . . . 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 6319	. . . . . . 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 10857	. . . . . . . 8 |- ( u e. ( -u 1 (,) 1 ) -> ( 2 x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) = ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) + ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
239	67, 68	negsubd 9994	. . . . . . . . . . . . 13 |- ( u e. CC -> ( 1 + -u ( u ^ 2 ) ) = ( 1 - ( u ^ 2 ) ) )
240	69	sqsqrtd 13494	. . . . . . . . . . . . 13 |- ( u e. CC -> ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) ^ 2 ) = ( 1 - ( u ^ 2 ) ) )
241	70	sqvald 12414	. . . . . . . . . . . . 13 |- ( u e. CC -> ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) ^ 2 ) = ( ( sqr ` ( 1 - ( u ^ 2 ) ) ) x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) )
242	239, 240, 241	3eqtr2d 2470	. . . . . . . . . . . 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 6318	. . . . . . . . . 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 9661	. . . . . . . . . . 11 |- ( u e. ( -u 1 (,) 1 ) -> 1 e. CC )
246	245, 233, 117, 207	divdird 10423	. . . . . . . . . 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 10390	. . . . . . . . . 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 2473	. . . . . . . . 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 6318	. . . . . . . 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 10378	. . . . . . . . 9 |- ( u e. ( -u 1 (,) 1 ) -> ( 1 / ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
251	250, 234, 117	addassd 9667	. . . . . . . 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 2469	. . . . . . 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 2464	. . . . . 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 4504	. . . . 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 2480	. . . 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 23	. . . . . 6 |- ( u = ( t / R ) -> u = ( t / R ) )
258		oveq1 6310	. . . . . . . 8 |- ( u = ( t / R ) -> ( u ^ 2 ) = ( ( t / R ) ^ 2 ) )
259	258	oveq2d 6319	. . . . . . 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 6321	. . . . 5 |- ( u = ( t / R ) -> ( u x. ( sqr ` ( 1 - ( u ^ 2 ) ) ) ) = ( ( t / R ) x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) )
262	256, 261	oveq12d 6321	. . . 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 6319	. . . 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 22918	. . 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 12415	. . 3 |- ( R e. RR+ -> ( R ^ 2 ) e. CC )
266	2, 18, 20, 264, 265	dvmptcmul 22910	. 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 10684	. . . . . . 7 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 2 e. CC )
268	267, 16	mulcld 9665	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 2 x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. CC )
269	6, 8	reccld 10378	. . . . . . 7 |- ( R e. RR+ -> ( 1 / R ) e. CC )
270	269	adantr 467	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 1 / R ) e. CC )
271	268, 270	mulcomd 9666	. . . . 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 6319	. . . 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 467	. . . . 5 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( R ^ 2 ) e. CC )
274	273, 270, 268	mulassd 9668	. . . 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 12414	. . . . . . . . 9 |- ( R e. RR+ -> ( R ^ 2 ) = ( R x. R ) )
276	275	oveq1d 6318	. . . . . . . 8 |- ( R e. RR+ -> ( ( R ^ 2 ) / R ) = ( ( R x. R ) / R ) )
277	265, 6, 8	divrecd 10388	. . . . . . . 8 |- ( R e. RR+ -> ( ( R ^ 2 ) / R ) = ( ( R ^ 2 ) x. ( 1 / R ) ) )
278	6, 6, 8	divcan3d 10390	. . . . . . . 8 |- ( R e. RR+ -> ( ( R x. R ) / R ) = R )
279	276, 277, 278	3eqtr3d 2472	. . . . . . 7 |- ( R e. RR+ -> ( ( R ^ 2 ) x. ( 1 / R ) ) = R )
280	279	adantr 467	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( 1 / R ) ) = R )
281	280	oveq1d 6318	. . . . 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 9844	. . . . 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 12443	. . . . . . . . 9 |- ( R e. RR+ -> ( R ^ 2 ) e. RR )
284	283	adantr 467	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( R ^ 2 ) e. RR )
285	21	sqge0d 12444	. . . . . . . . 9 |- ( R e. RR+ -> 0 <_ ( R ^ 2 ) )
286	285	adantr 467	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 <_ ( R ^ 2 ) )
287		1red 9660	. . . . . . . . 9 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 1 e. RR )
288	3	adantl 468	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> t e. RR )
289	21	adantr 467	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> R e. RR )
290	288, 289, 9	redivcld 10437	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( t / R ) e. RR )
291	290	resqcld 12443	. . . . . . . . 9 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) ^ 2 ) e. RR )
292	287, 291	resubcld 10049	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 1 - ( ( t / R ) ^ 2 ) ) e. RR )
293		0red 9646	. . . . . . . . 9 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 e. RR )
294	27, 28	absltd 13485	. . . . . . . . . . . . . . 15 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) < R <-> ( -u R < t /\ t < R ) ) )
295	77	abscld 13491	. . . . . . . . . . . . . . . . . 18 |- ( t e. RR -> ( abs ` t ) e. RR )
296	295	adantl 468	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> ( abs ` t ) e. RR )
297	77	absge0d 13499	. . . . . . . . . . . . . . . . . 18 |- ( t e. RR -> 0 <_ ( abs ` t ) )
298	297	adantl 468	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> 0 <_ ( abs ` t ) )
299		rpge0 11316	. . . . . . . . . . . . . . . . . 18 |- ( R e. RR+ -> 0 <_ R )
300	299	adantr 467	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> 0 <_ R )
301	296, 28, 298, 300	lt2sqd 12451	. . . . . . . . . . . . . . . 16 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) < R <-> ( ( abs ` t ) ^ 2 ) < ( R ^ 2 ) ) )
302		absresq 13359	. . . . . . . . . . . . . . . . . 18 |- ( t e. RR -> ( ( abs ` t ) ^ 2 ) = ( t ^ 2 ) )
303	302	adantl 468	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) ^ 2 ) = ( t ^ 2 ) )
304	265	adantr 467	. . . . . . . . . . . . . . . . . . 19 |- ( ( R e. RR+ /\ t e. RR ) -> ( R ^ 2 ) e. CC )
305	304	mulid1d 9662	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( R ^ 2 ) x. 1 ) = ( R ^ 2 ) )
306	305	eqcomd 2431	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> ( R ^ 2 ) = ( ( R ^ 2 ) x. 1 ) )
307	303, 306	breq12d 4434	. . . . . . . . . . . . . . . 16 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( ( abs ` t ) ^ 2 ) < ( R ^ 2 ) <-> ( t ^ 2 ) < ( ( R ^ 2 ) x. 1 ) ) )
308	6	adantr 467	. . . . . . . . . . . . . . . . . . 19 |- ( ( R e. RR+ /\ t e. RR ) -> R e. CC )
309	78, 308, 29	sqdivd 12430	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( t / R ) ^ 2 ) = ( ( t ^ 2 ) / ( R ^ 2 ) ) )
310	309	breq1d 4431	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( ( t / R ) ^ 2 ) < 1 <-> ( ( t ^ 2 ) / ( R ^ 2 ) ) < 1 ) )
311	30	resqcld 12443	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( t / R ) ^ 2 ) e. RR )
312	311, 42	posdifd 10202	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( ( t / R ) ^ 2 ) < 1 <-> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
313		resqcl 12343	. . . . . . . . . . . . . . . . . . 19 |- ( t e. RR -> ( t ^ 2 ) e. RR )
314	313	adantl 468	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR+ /\ t e. RR ) -> ( t ^ 2 ) e. RR )
315		rpgt0 11315	. . . . . . . . . . . . . . . . . . . . 21 |- ( R e. RR+ -> 0 < R )
316		0red 9646	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( R e. RR+ -> 0 e. RR )
317		0le0 10701	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 0 <_ 0
318	317	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( R e. RR+ -> 0 <_ 0 )
319	316, 21, 318, 299	lt2sqd 12451	. . . . . . . . . . . . . . . . . . . . . 22 |- ( R e. RR+ -> ( 0 < R <-> ( 0 ^ 2 ) < ( R ^ 2 ) ) )
320		sq0 12367	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 0 ^ 2 ) = 0
321	320	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( R e. RR+ -> ( 0 ^ 2 ) = 0 )
322	321	breq1d 4431	. . . . . . . . . . . . . . . . . . . . . 22 |- ( R e. RR+ -> ( ( 0 ^ 2 ) < ( R ^ 2 ) <-> 0 < ( R ^ 2 ) ) )
323	319, 322	bitrd 257	. . . . . . . . . . . . . . . . . . . . 21 |- ( R e. RR+ -> ( 0 < R <-> 0 < ( R ^ 2 ) ) )
324	315, 323	mpbid 214	. . . . . . . . . . . . . . . . . . . 20 |- ( R e. RR+ -> 0 < ( R ^ 2 ) )
325	283, 324	elrpd 11340	. . . . . . . . . . . . . . . . . . 19 |- ( R e. RR+ -> ( R ^ 2 ) e. RR+ )
326	325	adantr 467	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR+ /\ t e. RR ) -> ( R ^ 2 ) e. RR+ )
327	314, 42, 326	ltdivmuld 11391	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( ( t ^ 2 ) / ( R ^ 2 ) ) < 1 <-> ( t ^ 2 ) < ( ( R ^ 2 ) x. 1 ) ) )
328	310, 312, 327	3bitr3rd 288	. . . . . . . . . . . . . . . 16 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( t ^ 2 ) < ( ( R ^ 2 ) x. 1 ) <-> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
329	301, 307, 328	3bitrd 283	. . . . . . . . . . . . . . 15 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) < R <-> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
330	294, 329	bitr3d 259	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) <-> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
331	330	biimpd 211	. . . . . . . . . . . . 13 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) -> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
332	331	exp4b 611	. . . . . . . . . . . 12 |- ( R e. RR+ -> ( t e. RR -> ( -u R < t -> ( t < R -> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) )
333	332	3impd 1220	. . . . . . . . . . 11 |- ( R e. RR+ -> ( ( t e. RR /\ -u R < t /\ t < R ) -> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
334	26, 333	sylbid 219	. . . . . . . . . 10 |- ( R e. RR+ -> ( t e. ( -u R (,) R ) -> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
335	334	imp 431	. . . . . . . . 9 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) )
336	293, 292, 335	ltled 9785	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 <_ ( 1 - ( ( t / R ) ^ 2 ) ) )
337	284, 286, 292, 336	sqrtmuld 13480	. . . . . . 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 10076	. . . . . . . . 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 9662	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. 1 ) = ( R ^ 2 ) )
340	5, 7, 9	sqdivd 12430	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) ^ 2 ) = ( ( t ^ 2 ) / ( R ^ 2 ) ) )
341	340	oveq2d 6319	. . . . . . . . . . 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 12415	. . . . . . . . . . . . 13 |- ( t e. ( -u R (,) R ) -> ( t ^ 2 ) e. CC )
343	342	adantl 468	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( t ^ 2 ) e. CC )
344		sqne0 12342	. . . . . . . . . . . . . . 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 236	. . . . . . . . . . . . 13 |- ( R e. RR+ -> ( R ^ 2 ) =/= 0 )
347	346	adantr 467	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( R ^ 2 ) =/= 0 )
348	343, 273, 347	divcan2d 10387	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( ( t ^ 2 ) / ( R ^ 2 ) ) ) = ( t ^ 2 ) )
349	341, 348	eqtrd 2464	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( ( t / R ) ^ 2 ) ) = ( t ^ 2 ) )
350	339, 349	oveq12d 6321	. . . . . . . . 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 2464	. . . . . . . 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 13475	. . . . . . . . 9 |- ( R e. RR+ -> ( sqr ` ( R ^ 2 ) ) = R )
354	353	adantr 467	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( sqr ` ( R ^ 2 ) ) = R )
355	354	oveq1d 6318	. . . . . . 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 2473	. . . . . 6 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( R x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) = ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
357	356	oveq2d 6319	. . . . 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 2468	. . . 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 2470	. . 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 4508	. 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 2464	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 188   /\ wa 371   /\ w3a 983   = wceq 1438   e. wcel 1869   =/= wne 2619   _Vcvv 3082   i^i cin 3436   C_ wss 3437   {cpr 3999   class class class wbr 4421   |-> cmpt 4480   ran crn 4852   |` cres 4853   -->wf 5595   ` cfv 5599  (class class class)co 6303   CCcc 9539   RRcr 9540   0cc0 9541   1c1 9542   + caddc 9544   x. cmul 9546   RR*cxr 9676   < clt 9677   <_ cle 9678   - cmin 9862   -ucneg 9863   / cdiv 10271   NNcn 10611   2c2 10661   RR+crp 11304   (,)cioo 11637   ^cexp 12273   sqrcsqrt 13290   abscabs 13291   TopOpenctopn 15313   topGenctg 15329  ℂ_fldccnfld 18963  TopOnctopon 19910   _D cdv 22810  arcsincasin 23780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-rep 4534  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595  ax-inf2 8150  ax-cnex 9597  ax-resscn 9598  ax-1cn 9599  ax-icn 9600  ax-addcl 9601  ax-addrcl 9602  ax-mulcl 9603  ax-mulrcl 9604  ax-mulcom 9605  ax-addass 9606  ax-mulass 9607  ax-distr 9608  ax-i2m1 9609  ax-1ne0 9610  ax-1rid 9611  ax-rnegex 9612  ax-rrecex 9613  ax-cnre 9614  ax-pre-lttri 9615  ax-pre-lttrn 9616  ax-pre-ltadd 9617  ax-pre-mulgt0 9618  ax-pre-sup 9619  ax-addf 9620  ax-mulf 9621

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-fal 1444  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rmo 2784  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-tp 4002  df-op 4004  df-uni 4218  df-int 4254  df-iun 4299  df-iin 4300  df-br 4422  df-opab 4481  df-mpt 4482  df-tr 4517  df-eprel 4762  df-id 4766  df-po 4772  df-so 4773  df-fr 4810  df-se 4811  df-we 4812  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-pred 5397  df-ord 5443  df-on 5444  df-lim 5445  df-suc 5446  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-isom 5608  df-riota 6265  df-ov 6306  df-oprab 6307  df-mpt2 6308  df-of 6543  df-om 6705  df-1st 6805  df-2nd 6806  df-supp 6924  df-wrecs 7034  df-recs 7096  df-rdg 7134  df-1o 7188  df-2o 7189  df-oadd 7192  df-er 7369  df-map 7480  df-pm 7481  df-ixp 7529  df-en 7576  df-dom 7577  df-sdom 7578  df-fin 7579  df-fsupp 7888  df-fi 7929  df-sup 7960  df-inf 7961  df-oi 8029  df-card 8376  df-cda 8600  df-pnf 9679  df-mnf 9680  df-xr 9681  df-ltxr 9682  df-le 9683  df-sub 9864  df-neg 9865  df-div 10272  df-nn 10612  df-2 10670  df-3 10671  df-4 10672  df-5 10673  df-6 10674  df-7 10675  df-8 10676  df-9 10677  df-10 10678  df-n0 10872  df-z 10940  df-dec 11054  df-uz 11162  df-q 11267  df-rp 11305  df-xneg 11411  df-xadd 11412  df-xmul 11413  df-ioo 11641  df-ioc 11642  df-ico 11643  df-icc 11644  df-fz 11787  df-fzo 11918  df-fl 12029  df-mod 12098  df-seq 12215  df-exp 12274  df-fac 12461  df-bc 12489  df-hash 12517  df-shft 13124  df-cj 13156  df-re 13157  df-im 13158  df-sqrt 13292  df-abs 13293  df-limsup 13519  df-clim 13545  df-rlim 13546  df-sum 13746  df-ef 14114  df-sin 14116  df-cos 14117  df-tan 14118  df-pi 14119  df-struct 15116  df-ndx 15117  df-slot 15118  df-base 15119  df-sets 15120  df-ress 15121  df-plusg 15196  df-mulr 15197  df-starv 15198  df-sca 15199  df-vsca 15200  df-ip 15201  df-tset 15202  df-ple 15203  df-ds 15205  df-unif 15206  df-hom 15207  df-cco 15208  df-rest 15314  df-topn 15315  df-0g 15333  df-gsum 15334  df-topgen 15335  df-pt 15336  df-prds 15339  df-xrs 15393  df-qtop 15399  df-imas 15400  df-xps 15403  df-mre 15485  df-mrc 15486  df-acs 15488  df-mgm 16481  df-sgrp 16520  df-mnd 16530  df-submnd 16576  df-mulg 16669  df-cntz 16964  df-cmn 17425  df-psmet 18955  df-xmet 18956  df-met 18957  df-bl 18958  df-mopn 18959  df-fbas 18960  df-fg 18961  df-cnfld 18964  df-top 19913  df-bases 19914  df-topon 19915  df-topsp 19916  df-cld 20026  df-ntr 20027  df-cls 20028  df-nei 20106  df-lp 20144  df-perf 20145  df-cn 20235  df-cnp 20236  df-haus 20323  df-cmp 20394  df-tx 20569  df-hmeo 20762  df-fil 20853  df-fm 20945  df-flim 20946  df-flf 20947  df-xms 21327  df-ms 21328  df-tms 21329  df-cncf 21902  df-limc 22813  df-dv 22814  df-log 23498  df-cxp 23499  df-asin 23783

This theorem is referenced by:  areacirc  31995