Metamath Proof Explorer

Theorem areacirclem1

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

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

Proof

Step Hyp Ref Expression
1 reelprrecn 
 |-  RR e. { RR , CC }
2 1 a1i 
 |-  ( R e. RR+ -> RR e. { RR , CC } )
3 elioore 
 |-  ( t e. ( -u R (,) R ) -> t e. RR )
4 3 recnd 
 |-  ( t e. ( -u R (,) R ) -> t e. CC )
5 4 adantl 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> t e. CC )
6 rpcn 
 |-  ( R e. RR+ -> R e. CC )
7 6 adantr 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> R e. CC )
8 rpne0 
 |-  ( R e. RR+ -> R =/= 0 )
9 8 adantr 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> R =/= 0 )
10 5 7 9 divcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( t / R ) e. CC )
11 asincl 
 |-  ( ( t / R ) e. CC -> ( arcsin ` ( t / R ) ) e. CC )
12 10 11 syl 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( arcsin ` ( t / R ) ) e. CC )
13 1cnd 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 1 e. CC )
14 10 sqcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) ^ 2 ) e. CC )
15 13 14 subcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 1 - ( ( t / R ) ^ 2 ) ) e. CC )
16 15 sqrtcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) e. CC )
17 10 16 mulcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. CC )
18 12 17 addcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( arcsin ` ( t / R ) ) + ( ( t / R ) x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) e. CC )
19 ovexd 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( 2 x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) x. ( 1 / R ) ) e. _V )
20 rpre 
 |-  ( R e. RR+ -> R e. RR )
21 20 renegcld 
 |-  ( R e. RR+ -> -u R e. RR )
22 21 rexrd 
 |-  ( R e. RR+ -> -u R e. RR* )
23 rpxr 
 |-  ( R e. RR+ -> R e. RR* )
24 elioo2 
 |-  ( ( -u R e. RR* /\ R e. RR* ) -> ( t e. ( -u R (,) R ) <-> ( t e. RR /\ -u R < t /\ t < R ) ) )
25 22 23 24 syl2anc 
 |-  ( R e. RR+ -> ( t e. ( -u R (,) R ) <-> ( t e. RR /\ -u R < t /\ t < R ) ) )
26 simpr 
 |-  ( ( R e. RR+ /\ t e. RR ) -> t e. RR )
27 20 adantr 
 |-  ( ( R e. RR+ /\ t e. RR ) -> R e. RR )
28 8 adantr 
 |-  ( ( R e. RR+ /\ t e. RR ) -> R =/= 0 )
29 26 27 28 redivcld 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( t / R ) e. RR )
30 29 a1d 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) -> ( t / R ) e. RR ) )
31 6 mulm1d 
 |-  ( R e. RR+ -> ( -u 1 x. R ) = -u R )
32 31 adantr 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( -u 1 x. R ) = -u R )
33 32 breq1d 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( -u 1 x. R ) < t <-> -u R < t ) )
34 neg1rr 
 |-  -u 1 e. RR
35 34 a1i 
 |-  ( ( R e. RR+ /\ t e. RR ) -> -u 1 e. RR )
36 simpl 
 |-  ( ( R e. RR+ /\ t e. RR ) -> R e. RR+ )
37 35 26 36 ltmuldivd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( -u 1 x. R ) < t <-> -u 1 < ( t / R ) ) )
38 33 37 bitr3d 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( -u R < t <-> -u 1 < ( t / R ) ) )
39 38 biimpd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( -u R < t -> -u 1 < ( t / R ) ) )
40 39 adantrd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) -> -u 1 < ( t / R ) ) )
41 1red 
 |-  ( ( R e. RR+ /\ t e. RR ) -> 1 e. RR )
42 26 41 36 ltdivmuld 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( t / R ) < 1 <-> t < ( R x. 1 ) ) )
43 6 mulid1d 
 |-  ( R e. RR+ -> ( R x. 1 ) = R )
44 43 adantr 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( R x. 1 ) = R )
45 44 breq2d 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( t < ( R x. 1 ) <-> t < R ) )
46 42 45 bitr2d 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( t < R <-> ( t / R ) < 1 ) )
47 46 biimpd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( t < R -> ( t / R ) < 1 ) )
48 47 adantld 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) -> ( t / R ) < 1 ) )
49 30 40 48 3jcad 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) -> ( ( t / R ) e. RR /\ -u 1 < ( t / R ) /\ ( t / R ) < 1 ) ) )
50 49 exp4b 
 |-  ( R e. RR+ -> ( t e. RR -> ( -u R < t -> ( t < R -> ( ( t / R ) e. RR /\ -u 1 < ( t / R ) /\ ( t / R ) < 1 ) ) ) ) )
51 50 3impd 
 |-  ( R e. RR+ -> ( ( t e. RR /\ -u R < t /\ t < R ) -> ( ( t / R ) e. RR /\ -u 1 < ( t / R ) /\ ( t / R ) < 1 ) ) )
52 25 51 sylbid 
 |-  ( R e. RR+ -> ( t e. ( -u R (,) R ) -> ( ( t / R ) e. RR /\ -u 1 < ( t / R ) /\ ( t / R ) < 1 ) ) )
53 52 imp 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) e. RR /\ -u 1 < ( t / R ) /\ ( t / R ) < 1 ) )
54 34 rexri 
 |-  -u 1 e. RR*
55 1xr 
 |-  1 e. RR*
56 elioo2 
 |-  ( ( -u 1 e. RR* /\ 1 e. RR* ) -> ( ( t / R ) e. ( -u 1 (,) 1 ) <-> ( ( t / R ) e. RR /\ -u 1 < ( t / R ) /\ ( t / R ) < 1 ) ) )
57 54 55 56 mp2an 
 |-  ( ( t / R ) e. ( -u 1 (,) 1 ) <-> ( ( t / R ) e. RR /\ -u 1 < ( t / R ) /\ ( t / R ) < 1 ) )
58 53 57 sylibr 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( t / R ) e. ( -u 1 (,) 1 ) )
59 ovexd 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 1 / R ) e. _V )
60 elioore 
 |-  ( u e. ( -u 1 (,) 1 ) -> u e. RR )
61 60 recnd 
 |-  ( u e. ( -u 1 (,) 1 ) -> u e. CC )
62 asincl 
 |-  ( u e. CC -> ( arcsin ` u ) e. CC )
63 id 
 |-  ( u e. CC -> u e. CC )
64 1cnd 
 |-  ( u e. CC -> 1 e. CC )
65 sqcl 
 |-  ( u e. CC -> ( u ^ 2 ) e. CC )
66 64 65 subcld 
 |-  ( u e. CC -> ( 1 - ( u ^ 2 ) ) e. CC )
67 66 sqrtcld 
 |-  ( u e. CC -> ( sqrt ` ( 1 - ( u ^ 2 ) ) ) e. CC )
68 63 67 mulcld 
 |-  ( u e. CC -> ( u x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
69 62 68 addcld 
 |-  ( u e. CC -> ( ( arcsin ` u ) + ( u x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) e. CC )
70 61 69 syl 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( ( arcsin ` u ) + ( u x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) e. CC )
71 70 adantl 
 |-  ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( ( arcsin ` u ) + ( u x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) e. CC )
72 ovexd 
 |-  ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( 2 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) e. _V )
73 recn 
 |-  ( t e. RR -> t e. CC )
74 73 adantl 
 |-  ( ( R e. RR+ /\ t e. RR ) -> t e. CC )
75 1cnd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> 1 e. CC )
76 2 dvmptid 
 |-  ( R e. RR+ -> ( RR _D ( t e. RR |-> t ) ) = ( t e. RR |-> 1 ) )
77 ioossre 
 |-  ( -u R (,) R ) C_ RR
78 77 a1i 
 |-  ( R e. RR+ -> ( -u R (,) R ) C_ RR )
79 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
80 79 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
81 iooretop 
 |-  ( -u R (,) R ) e. ( topGen ` ran (,) )
82 81 a1i 
 |-  ( R e. RR+ -> ( -u R (,) R ) e. ( topGen ` ran (,) ) )
83 2 74 75 76 78 80 79 82 dvmptres 
 |-  ( R e. RR+ -> ( RR _D ( t e. ( -u R (,) R ) |-> t ) ) = ( t e. ( -u R (,) R ) |-> 1 ) )
84 2 5 13 83 6 8 dvmptdivc 
 |-  ( R e. RR+ -> ( RR _D ( t e. ( -u R (,) R ) |-> ( t / R ) ) ) = ( t e. ( -u R (,) R ) |-> ( 1 / R ) ) )
85 61 62 syl 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( arcsin ` u ) e. CC )
86 85 adantl 
 |-  ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( arcsin ` u ) e. CC )
87 ovexd 
 |-  ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( 1 / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) e. _V )
88 asinf 
 |-  arcsin : CC --> CC
89 88 a1i 
 |-  ( R e. RR+ -> arcsin : CC --> CC )
90 ioossre 
 |-  ( -u 1 (,) 1 ) C_ RR
91 ax-resscn 
 |-  RR C_ CC
92 90 91 sstri 
 |-  ( -u 1 (,) 1 ) C_ CC
93 92 a1i 
 |-  ( R e. RR+ -> ( -u 1 (,) 1 ) C_ CC )
94 89 93 feqresmpt 
 |-  ( R e. RR+ -> ( arcsin |` ( -u 1 (,) 1 ) ) = ( u e. ( -u 1 (,) 1 ) |-> ( arcsin ` u ) ) )
95 94 oveq2d 
 |-  ( R e. RR+ -> ( RR _D ( arcsin |` ( -u 1 (,) 1 ) ) ) = ( RR _D ( u e. ( -u 1 (,) 1 ) |-> ( arcsin ` u ) ) ) )
96 dvreasin 
 |-  ( RR _D ( arcsin |` ( -u 1 (,) 1 ) ) ) = ( u e. ( -u 1 (,) 1 ) |-> ( 1 / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) )
97 95 96 eqtr3di 
 |-  ( R e. RR+ -> ( RR _D ( u e. ( -u 1 (,) 1 ) |-> ( arcsin ` u ) ) ) = ( u e. ( -u 1 (,) 1 ) |-> ( 1 / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) )
98 61 68 syl 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( u x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
99 98 adantl 
 |-  ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( u x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
100 ovexd 
 |-  ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( ( 1 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( -u u / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) x. u ) ) e. _V )
101 61 adantl 
 |-  ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> u e. CC )
102 1cnd 
 |-  ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> 1 e. CC )
103 recn 
 |-  ( u e. RR -> u e. CC )
104 103 adantl 
 |-  ( ( R e. RR+ /\ u e. RR ) -> u e. CC )
105 1cnd 
 |-  ( ( R e. RR+ /\ u e. RR ) -> 1 e. CC )
106 2 dvmptid 
 |-  ( R e. RR+ -> ( RR _D ( u e. RR |-> u ) ) = ( u e. RR |-> 1 ) )
107 90 a1i 
 |-  ( R e. RR+ -> ( -u 1 (,) 1 ) C_ RR )
108 iooretop 
 |-  ( -u 1 (,) 1 ) e. ( topGen ` ran (,) )
109 108 a1i 
 |-  ( R e. RR+ -> ( -u 1 (,) 1 ) e. ( topGen ` ran (,) ) )
110 2 104 105 106 107 80 79 109 dvmptres 
 |-  ( R e. RR+ -> ( RR _D ( u e. ( -u 1 (,) 1 ) |-> u ) ) = ( u e. ( -u 1 (,) 1 ) |-> 1 ) )
111 61 67 syl 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( sqrt ` ( 1 - ( u ^ 2 ) ) ) e. CC )
112 111 adantl 
 |-  ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( sqrt ` ( 1 - ( u ^ 2 ) ) ) e. CC )
113 ovexd 
 |-  ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( -u u / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) e. _V )
114 1red 
 |-  ( u e. ( -u 1 (,) 1 ) -> 1 e. RR )
115 60 resqcld 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( u ^ 2 ) e. RR )
116 114 115 resubcld 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( 1 - ( u ^ 2 ) ) e. RR )
117 elioo2 
 |-  ( ( -u 1 e. RR* /\ 1 e. RR* ) -> ( u e. ( -u 1 (,) 1 ) <-> ( u e. RR /\ -u 1 < u /\ u < 1 ) ) )
118 54 55 117 mp2an 
 |-  ( u e. ( -u 1 (,) 1 ) <-> ( u e. RR /\ -u 1 < u /\ u < 1 ) )
119 id 
 |-  ( u e. RR -> u e. RR )
120 1red 
 |-  ( u e. RR -> 1 e. RR )
121 119 120 absltd 
 |-  ( u e. RR -> ( ( abs ` u ) < 1 <-> ( -u 1 < u /\ u < 1 ) ) )
122 103 abscld 
 |-  ( u e. RR -> ( abs ` u ) e. RR )
123 103 absge0d 
 |-  ( u e. RR -> 0 <_ ( abs ` u ) )
124 0le1 
 |-  0 <_ 1
125 124 a1i 
 |-  ( u e. RR -> 0 <_ 1 )
126 122 120 123 125 lt2sqd 
 |-  ( u e. RR -> ( ( abs ` u ) < 1 <-> ( ( abs ` u ) ^ 2 ) < ( 1 ^ 2 ) ) )
127 absresq 
 |-  ( u e. RR -> ( ( abs ` u ) ^ 2 ) = ( u ^ 2 ) )
128 sq1 
 |-  ( 1 ^ 2 ) = 1
129 128 a1i 
 |-  ( u e. RR -> ( 1 ^ 2 ) = 1 )
130 127 129 breq12d 
 |-  ( u e. RR -> ( ( ( abs ` u ) ^ 2 ) < ( 1 ^ 2 ) <-> ( u ^ 2 ) < 1 ) )
131 resqcl 
 |-  ( u e. RR -> ( u ^ 2 ) e. RR )
132 131 120 posdifd 
 |-  ( u e. RR -> ( ( u ^ 2 ) < 1 <-> 0 < ( 1 - ( u ^ 2 ) ) ) )
133 126 130 132 3bitrd 
 |-  ( u e. RR -> ( ( abs ` u ) < 1 <-> 0 < ( 1 - ( u ^ 2 ) ) ) )
134 121 133 bitr3d 
 |-  ( u e. RR -> ( ( -u 1 < u /\ u < 1 ) <-> 0 < ( 1 - ( u ^ 2 ) ) ) )
135 134 biimpd 
 |-  ( u e. RR -> ( ( -u 1 < u /\ u < 1 ) -> 0 < ( 1 - ( u ^ 2 ) ) ) )
136 135 3impib 
 |-  ( ( u e. RR /\ -u 1 < u /\ u < 1 ) -> 0 < ( 1 - ( u ^ 2 ) ) )
137 118 136 sylbi 
 |-  ( u e. ( -u 1 (,) 1 ) -> 0 < ( 1 - ( u ^ 2 ) ) )
138 116 137 elrpd 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( 1 - ( u ^ 2 ) ) e. RR+ )
139 138 adantl 
 |-  ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> ( 1 - ( u ^ 2 ) ) e. RR+ )
140 negex 
 |-  -u ( 2 x. u ) e. _V
141 140 a1i 
 |-  ( ( R e. RR+ /\ u e. ( -u 1 (,) 1 ) ) -> -u ( 2 x. u ) e. _V )
142 rpcn 
 |-  ( v e. RR+ -> v e. CC )
143 142 sqrtcld 
 |-  ( v e. RR+ -> ( sqrt ` v ) e. CC )
144 143 adantl 
 |-  ( ( R e. RR+ /\ v e. RR+ ) -> ( sqrt ` v ) e. CC )
145 ovexd 
 |-  ( ( R e. RR+ /\ v e. RR+ ) -> ( 1 / ( 2 x. ( sqrt ` v ) ) ) e. _V )
146 1cnd 
 |-  ( u e. RR -> 1 e. CC )
147 103 sqcld 
 |-  ( u e. RR -> ( u ^ 2 ) e. CC )
148 146 147 subcld 
 |-  ( u e. RR -> ( 1 - ( u ^ 2 ) ) e. CC )
149 148 adantl 
 |-  ( ( R e. RR+ /\ u e. RR ) -> ( 1 - ( u ^ 2 ) ) e. CC )
150 140 a1i 
 |-  ( ( R e. RR+ /\ u e. RR ) -> -u ( 2 x. u ) e. _V )
151 0red 
 |-  ( ( R e. RR+ /\ u e. RR ) -> 0 e. RR )
152 1cnd 
 |-  ( R e. RR+ -> 1 e. CC )
153 2 152 dvmptc 
 |-  ( R e. RR+ -> ( RR _D ( u e. RR |-> 1 ) ) = ( u e. RR |-> 0 ) )
154 147 adantl 
 |-  ( ( R e. RR+ /\ u e. RR ) -> ( u ^ 2 ) e. CC )
155 ovexd 
 |-  ( ( R e. RR+ /\ u e. RR ) -> ( 2 x. u ) e. _V )
156 79 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
157 toponmax 
 |-  ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) -> CC e. ( TopOpen ` CCfld ) )
158 156 157 mp1i 
 |-  ( R e. RR+ -> CC e. ( TopOpen ` CCfld ) )
159 df-ss 
 |-  ( RR C_ CC <-> ( RR i^i CC ) = RR )
160 91 159 mpbi 
 |-  ( RR i^i CC ) = RR
161 160 a1i 
 |-  ( R e. RR+ -> ( RR i^i CC ) = RR )
162 65 adantl 
 |-  ( ( R e. RR+ /\ u e. CC ) -> ( u ^ 2 ) e. CC )
163 ovexd 
 |-  ( ( R e. RR+ /\ u e. CC ) -> ( 2 x. u ) e. _V )
164 2nn 
 |-  2 e. NN
165 dvexp 
 |-  ( 2 e. NN -> ( CC _D ( u e. CC |-> ( u ^ 2 ) ) ) = ( u e. CC |-> ( 2 x. ( u ^ ( 2 - 1 ) ) ) ) )
166 164 165 ax-mp 
 |-  ( CC _D ( u e. CC |-> ( u ^ 2 ) ) ) = ( u e. CC |-> ( 2 x. ( u ^ ( 2 - 1 ) ) ) )
167 2m1e1 
 |-  ( 2 - 1 ) = 1
168 167 oveq2i 
 |-  ( u ^ ( 2 - 1 ) ) = ( u ^ 1 )
169 exp1 
 |-  ( u e. CC -> ( u ^ 1 ) = u )
170 168 169 syl5eq 
 |-  ( u e. CC -> ( u ^ ( 2 - 1 ) ) = u )
171 170 oveq2d 
 |-  ( u e. CC -> ( 2 x. ( u ^ ( 2 - 1 ) ) ) = ( 2 x. u ) )
172 171 mpteq2ia 
 |-  ( u e. CC |-> ( 2 x. ( u ^ ( 2 - 1 ) ) ) ) = ( u e. CC |-> ( 2 x. u ) )
173 166 172 eqtri 
 |-  ( CC _D ( u e. CC |-> ( u ^ 2 ) ) ) = ( u e. CC |-> ( 2 x. u ) )
174 173 a1i 
 |-  ( R e. RR+ -> ( CC _D ( u e. CC |-> ( u ^ 2 ) ) ) = ( u e. CC |-> ( 2 x. u ) ) )
175 79 2 158 161 162 163 174 dvmptres3 
 |-  ( R e. RR+ -> ( RR _D ( u e. RR |-> ( u ^ 2 ) ) ) = ( u e. RR |-> ( 2 x. u ) ) )
176 2 105 151 153 154 155 175 dvmptsub 
 |-  ( R e. RR+ -> ( RR _D ( u e. RR |-> ( 1 - ( u ^ 2 ) ) ) ) = ( u e. RR |-> ( 0 - ( 2 x. u ) ) ) )
177 df-neg 
 |-  -u ( 2 x. u ) = ( 0 - ( 2 x. u ) )
178 177 mpteq2i 
 |-  ( u e. RR |-> -u ( 2 x. u ) ) = ( u e. RR |-> ( 0 - ( 2 x. u ) ) )
179 176 178 eqtr4di 
 |-  ( R e. RR+ -> ( RR _D ( u e. RR |-> ( 1 - ( u ^ 2 ) ) ) ) = ( u e. RR |-> -u ( 2 x. u ) ) )
180 2 149 150 179 107 80 79 109 dvmptres 
 |-  ( R e. RR+ -> ( RR _D ( u e. ( -u 1 (,) 1 ) |-> ( 1 - ( u ^ 2 ) ) ) ) = ( u e. ( -u 1 (,) 1 ) |-> -u ( 2 x. u ) ) )
181 dvsqrt 
 |-  ( RR _D ( v e. RR+ |-> ( sqrt ` v ) ) ) = ( v e. RR+ |-> ( 1 / ( 2 x. ( sqrt ` v ) ) ) )
182 181 a1i 
 |-  ( R e. RR+ -> ( RR _D ( v e. RR+ |-> ( sqrt ` v ) ) ) = ( v e. RR+ |-> ( 1 / ( 2 x. ( sqrt ` v ) ) ) ) )
183 fveq2 
 |-  ( v = ( 1 - ( u ^ 2 ) ) -> ( sqrt ` v ) = ( sqrt ` ( 1 - ( u ^ 2 ) ) ) )
184 183 oveq2d 
 |-  ( v = ( 1 - ( u ^ 2 ) ) -> ( 2 x. ( sqrt ` v ) ) = ( 2 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) )
185 184 oveq2d 
 |-  ( v = ( 1 - ( u ^ 2 ) ) -> ( 1 / ( 2 x. ( sqrt ` v ) ) ) = ( 1 / ( 2 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) )
186 2 2 139 141 144 145 180 182 183 185 dvmptco 
 |-  ( R e. RR+ -> ( RR _D ( u e. ( -u 1 (,) 1 ) |-> ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) = ( u e. ( -u 1 (,) 1 ) |-> ( ( 1 / ( 2 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) x. -u ( 2 x. u ) ) ) )
187 2cnd 
 |-  ( u e. ( -u 1 (,) 1 ) -> 2 e. CC )
188 187 61 mulneg2d 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( 2 x. -u u ) = -u ( 2 x. u ) )
189 188 oveq1d 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( ( 2 x. -u u ) / ( 2 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) = ( -u ( 2 x. u ) / ( 2 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) )
190 61 negcld 
 |-  ( u e. ( -u 1 (,) 1 ) -> -u u e. CC )
191 137 gt0ne0d 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( 1 - ( u ^ 2 ) ) =/= 0 )
192 61 66 syl 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( 1 - ( u ^ 2 ) ) e. CC )
193 192 adantr 
 |-  ( ( u e. ( -u 1 (,) 1 ) /\ ( sqrt ` ( 1 - ( u ^ 2 ) ) ) = 0 ) -> ( 1 - ( u ^ 2 ) ) e. CC )
194 simpr 
 |-  ( ( u e. ( -u 1 (,) 1 ) /\ ( sqrt ` ( 1 - ( u ^ 2 ) ) ) = 0 ) -> ( sqrt ` ( 1 - ( u ^ 2 ) ) ) = 0 )
195 193 194 sqr00d 
 |-  ( ( u e. ( -u 1 (,) 1 ) /\ ( sqrt ` ( 1 - ( u ^ 2 ) ) ) = 0 ) -> ( 1 - ( u ^ 2 ) ) = 0 )
196 195 ex 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( ( sqrt ` ( 1 - ( u ^ 2 ) ) ) = 0 -> ( 1 - ( u ^ 2 ) ) = 0 ) )
197 196 necon3d 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( ( 1 - ( u ^ 2 ) ) =/= 0 -> ( sqrt ` ( 1 - ( u ^ 2 ) ) ) =/= 0 ) )
198 191 197 mpd 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( sqrt ` ( 1 - ( u ^ 2 ) ) ) =/= 0 )
199 2ne0 
 |-  2 =/= 0
200 199 a1i 
 |-  ( u e. ( -u 1 (,) 1 ) -> 2 =/= 0 )
201 190 111 187 198 200 divcan5d 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( ( 2 x. -u u ) / ( 2 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) = ( -u u / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) )
202 187 61 mulcld 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( 2 x. u ) e. CC )
203 202 negcld 
 |-  ( u e. ( -u 1 (,) 1 ) -> -u ( 2 x. u ) e. CC )
204 187 111 mulcld 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( 2 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
205 187 111 200 198 mulne0d 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( 2 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) =/= 0 )
206 203 204 205 divrec2d 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( -u ( 2 x. u ) / ( 2 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) = ( ( 1 / ( 2 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) x. -u ( 2 x. u ) ) )
207 189 201 206 3eqtr3rd 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( ( 1 / ( 2 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) x. -u ( 2 x. u ) ) = ( -u u / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) )
208 207 mpteq2ia 
 |-  ( u e. ( -u 1 (,) 1 ) |-> ( ( 1 / ( 2 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) x. -u ( 2 x. u ) ) ) = ( u e. ( -u 1 (,) 1 ) |-> ( -u u / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) )
209 186 208 eqtrdi 
 |-  ( R e. RR+ -> ( RR _D ( u e. ( -u 1 (,) 1 ) |-> ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) = ( u e. ( -u 1 (,) 1 ) |-> ( -u u / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) )
210 2 101 102 110 112 113 209 dvmptmul 
 |-  ( R e. RR+ -> ( RR _D ( u e. ( -u 1 (,) 1 ) |-> ( u x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) ) = ( u e. ( -u 1 (,) 1 ) |-> ( ( 1 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( -u u / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) x. u ) ) ) )
211 2 86 87 97 99 100 210 dvmptadd 
 |-  ( R e. RR+ -> ( RR _D ( u e. ( -u 1 (,) 1 ) |-> ( ( arcsin ` u ) + ( u x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) ) ) = ( u e. ( -u 1 (,) 1 ) |-> ( ( 1 / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( 1 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( -u u / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) x. u ) ) ) ) )
212 111 mulid2d 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( 1 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) = ( sqrt ` ( 1 - ( u ^ 2 ) ) ) )
213 190 111 198 divcld 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( -u u / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
214 213 61 mulcomd 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( ( -u u / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) x. u ) = ( u x. ( -u u / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) )
215 61 190 111 198 divassd 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( ( u x. -u u ) / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) = ( u x. ( -u u / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) )
216 61 61 mulneg2d 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( u x. -u u ) = -u ( u x. u ) )
217 61 sqvald 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( u ^ 2 ) = ( u x. u ) )
218 217 negeqd 
 |-  ( u e. ( -u 1 (,) 1 ) -> -u ( u ^ 2 ) = -u ( u x. u ) )
219 216 218 eqtr4d 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( u x. -u u ) = -u ( u ^ 2 ) )
220 219 oveq1d 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( ( u x. -u u ) / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) = ( -u ( u ^ 2 ) / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) )
221 214 215 220 3eqtr2d 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( ( -u u / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) x. u ) = ( -u ( u ^ 2 ) / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) )
222 212 221 oveq12d 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( ( 1 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( -u u / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) x. u ) ) = ( ( sqrt ` ( 1 - ( u ^ 2 ) ) ) + ( -u ( u ^ 2 ) / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) )
223 61 sqcld 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( u ^ 2 ) e. CC )
224 223 negcld 
 |-  ( u e. ( -u 1 (,) 1 ) -> -u ( u ^ 2 ) e. CC )
225 224 111 198 divcld 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( -u ( u ^ 2 ) / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
226 111 225 addcomd 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( ( sqrt ` ( 1 - ( u ^ 2 ) ) ) + ( -u ( u ^ 2 ) / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) = ( ( -u ( u ^ 2 ) / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) + ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) )
227 222 226 eqtrd 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( ( 1 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( -u u / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) x. u ) ) = ( ( -u ( u ^ 2 ) / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) + ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) )
228 227 oveq2d 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( ( 1 / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( 1 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( -u u / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) x. u ) ) ) = ( ( 1 / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( -u ( u ^ 2 ) / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) + ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) )
229 111 2timesd 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( 2 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) = ( ( sqrt ` ( 1 - ( u ^ 2 ) ) ) + ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) )
230 64 65 negsubd 
 |-  ( u e. CC -> ( 1 + -u ( u ^ 2 ) ) = ( 1 - ( u ^ 2 ) ) )
231 66 sqsqrtd 
 |-  ( u e. CC -> ( ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ^ 2 ) = ( 1 - ( u ^ 2 ) ) )
232 67 sqvald 
 |-  ( u e. CC -> ( ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ^ 2 ) = ( ( sqrt ` ( 1 - ( u ^ 2 ) ) ) x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) )
233 230 231 232 3eqtr2d 
 |-  ( u e. CC -> ( 1 + -u ( u ^ 2 ) ) = ( ( sqrt ` ( 1 - ( u ^ 2 ) ) ) x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) )
234 61 233 syl 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( 1 + -u ( u ^ 2 ) ) = ( ( sqrt ` ( 1 - ( u ^ 2 ) ) ) x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) )
235 234 oveq1d 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( ( 1 + -u ( u ^ 2 ) ) / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) = ( ( ( sqrt ` ( 1 - ( u ^ 2 ) ) ) x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) )
236 1cnd 
 |-  ( u e. ( -u 1 (,) 1 ) -> 1 e. CC )
237 236 224 111 198 divdird 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( ( 1 + -u ( u ^ 2 ) ) / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) = ( ( 1 / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) + ( -u ( u ^ 2 ) / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) )
238 111 111 198 divcan3d 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( ( ( sqrt ` ( 1 - ( u ^ 2 ) ) ) x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) = ( sqrt ` ( 1 - ( u ^ 2 ) ) ) )
239 235 237 238 3eqtr3rd 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( sqrt ` ( 1 - ( u ^ 2 ) ) ) = ( ( 1 / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) + ( -u ( u ^ 2 ) / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) )
240 239 oveq1d 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( ( sqrt ` ( 1 - ( u ^ 2 ) ) ) + ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) = ( ( ( 1 / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) + ( -u ( u ^ 2 ) / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) + ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) )
241 111 198 reccld 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( 1 / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) e. CC )
242 241 225 111 addassd 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( ( ( 1 / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) + ( -u ( u ^ 2 ) / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) + ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) = ( ( 1 / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( -u ( u ^ 2 ) / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) + ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) )
243 229 240 242 3eqtrrd 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( ( 1 / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( -u ( u ^ 2 ) / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) + ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) = ( 2 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) )
244 228 243 eqtrd 
 |-  ( u e. ( -u 1 (,) 1 ) -> ( ( 1 / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( 1 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( -u u / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) x. u ) ) ) = ( 2 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) )
245 244 mpteq2ia 
 |-  ( u e. ( -u 1 (,) 1 ) |-> ( ( 1 / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( 1 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) + ( ( -u u / ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) x. u ) ) ) ) = ( u e. ( -u 1 (,) 1 ) |-> ( 2 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) )
246 211 245 eqtrdi 
 |-  ( R e. RR+ -> ( RR _D ( u e. ( -u 1 (,) 1 ) |-> ( ( arcsin ` u ) + ( u x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) ) ) = ( u e. ( -u 1 (,) 1 ) |-> ( 2 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) )
247 fveq2 
 |-  ( u = ( t / R ) -> ( arcsin ` u ) = ( arcsin ` ( t / R ) ) )
248 id 
 |-  ( u = ( t / R ) -> u = ( t / R ) )
249 oveq1 
 |-  ( u = ( t / R ) -> ( u ^ 2 ) = ( ( t / R ) ^ 2 ) )
250 249 oveq2d 
 |-  ( u = ( t / R ) -> ( 1 - ( u ^ 2 ) ) = ( 1 - ( ( t / R ) ^ 2 ) ) )
251 250 fveq2d 
 |-  ( u = ( t / R ) -> ( sqrt ` ( 1 - ( u ^ 2 ) ) ) = ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) )
252 248 251 oveq12d 
 |-  ( u = ( t / R ) -> ( u x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) = ( ( t / R ) x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) )
253 247 252 oveq12d 
 |-  ( u = ( t / R ) -> ( ( arcsin ` u ) + ( u x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) ) = ( ( arcsin ` ( t / R ) ) + ( ( t / R ) x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) )
254 251 oveq2d 
 |-  ( u = ( t / R ) -> ( 2 x. ( sqrt ` ( 1 - ( u ^ 2 ) ) ) ) = ( 2 x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) )
255 2 2 58 59 71 72 84 246 253 254 dvmptco 
 |-  ( R e. RR+ -> ( RR _D ( t e. ( -u R (,) R ) |-> ( ( arcsin ` ( t / R ) ) + ( ( t / R ) x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) ) ) = ( t e. ( -u R (,) R ) |-> ( ( 2 x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) x. ( 1 / R ) ) ) )
256 6 sqcld 
 |-  ( R e. RR+ -> ( R ^ 2 ) e. CC )
257 2 18 19 255 256 dvmptcmul 
 |-  ( R e. RR+ -> ( RR _D ( t e. ( -u R (,) R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( t / R ) ) + ( ( t / R ) x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) ) ) ) = ( t e. ( -u R (,) R ) |-> ( ( R ^ 2 ) x. ( ( 2 x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) x. ( 1 / R ) ) ) ) )
258 2cnd 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 2 e. CC )
259 258 16 mulcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 2 x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. CC )
260 6 8 reccld 
 |-  ( R e. RR+ -> ( 1 / R ) e. CC )
261 260 adantr 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 1 / R ) e. CC )
262 259 261 mulcomd 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( 2 x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) x. ( 1 / R ) ) = ( ( 1 / R ) x. ( 2 x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) )
263 262 oveq2d 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( ( 2 x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) x. ( 1 / R ) ) ) = ( ( R ^ 2 ) x. ( ( 1 / R ) x. ( 2 x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) ) )
264 256 adantr 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( R ^ 2 ) e. CC )
265 264 261 259 mulassd 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( ( R ^ 2 ) x. ( 1 / R ) ) x. ( 2 x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) = ( ( R ^ 2 ) x. ( ( 1 / R ) x. ( 2 x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) ) )
266 6 sqvald 
 |-  ( R e. RR+ -> ( R ^ 2 ) = ( R x. R ) )
267 266 oveq1d 
 |-  ( R e. RR+ -> ( ( R ^ 2 ) / R ) = ( ( R x. R ) / R ) )
268 256 6 8 divrecd 
 |-  ( R e. RR+ -> ( ( R ^ 2 ) / R ) = ( ( R ^ 2 ) x. ( 1 / R ) ) )
269 6 6 8 divcan3d 
 |-  ( R e. RR+ -> ( ( R x. R ) / R ) = R )
270 267 268 269 3eqtr3d 
 |-  ( R e. RR+ -> ( ( R ^ 2 ) x. ( 1 / R ) ) = R )
271 270 adantr 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( 1 / R ) ) = R )
272 271 oveq1d 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( ( R ^ 2 ) x. ( 1 / R ) ) x. ( 2 x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) = ( R x. ( 2 x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) )
273 7 258 16 mul12d 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( R x. ( 2 x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) = ( 2 x. ( R x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) )
274 20 resqcld 
 |-  ( R e. RR+ -> ( R ^ 2 ) e. RR )
275 274 adantr 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( R ^ 2 ) e. RR )
276 20 sqge0d 
 |-  ( R e. RR+ -> 0 <_ ( R ^ 2 ) )
277 276 adantr 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 <_ ( R ^ 2 ) )
278 1red 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 1 e. RR )
279 3 adantl 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> t e. RR )
280 20 adantr 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> R e. RR )
281 279 280 9 redivcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( t / R ) e. RR )
282 281 resqcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) ^ 2 ) e. RR )
283 278 282 resubcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 1 - ( ( t / R ) ^ 2 ) ) e. RR )
284 0red 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 e. RR )
285 26 27 absltd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) < R <-> ( -u R < t /\ t < R ) ) )
286 73 abscld 
 |-  ( t e. RR -> ( abs ` t ) e. RR )
287 286 adantl 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( abs ` t ) e. RR )
288 73 absge0d 
 |-  ( t e. RR -> 0 <_ ( abs ` t ) )
289 288 adantl 
 |-  ( ( R e. RR+ /\ t e. RR ) -> 0 <_ ( abs ` t ) )
290 rpge0 
 |-  ( R e. RR+ -> 0 <_ R )
291 290 adantr 
 |-  ( ( R e. RR+ /\ t e. RR ) -> 0 <_ R )
292 287 27 289 291 lt2sqd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) < R <-> ( ( abs ` t ) ^ 2 ) < ( R ^ 2 ) ) )
293 absresq 
 |-  ( t e. RR -> ( ( abs ` t ) ^ 2 ) = ( t ^ 2 ) )
294 293 adantl 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) ^ 2 ) = ( t ^ 2 ) )
295 256 adantr 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( R ^ 2 ) e. CC )
296 295 mulid1d 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( R ^ 2 ) x. 1 ) = ( R ^ 2 ) )
297 296 eqcomd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( R ^ 2 ) = ( ( R ^ 2 ) x. 1 ) )
298 294 297 breq12d 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( ( abs ` t ) ^ 2 ) < ( R ^ 2 ) <-> ( t ^ 2 ) < ( ( R ^ 2 ) x. 1 ) ) )
299 6 adantr 
 |-  ( ( R e. RR+ /\ t e. RR ) -> R e. CC )
300 74 299 28 sqdivd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( t / R ) ^ 2 ) = ( ( t ^ 2 ) / ( R ^ 2 ) ) )
301 300 breq1d 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( ( t / R ) ^ 2 ) < 1 <-> ( ( t ^ 2 ) / ( R ^ 2 ) ) < 1 ) )
302 29 resqcld 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( t / R ) ^ 2 ) e. RR )
303 302 41 posdifd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( ( t / R ) ^ 2 ) < 1 <-> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
304 resqcl 
 |-  ( t e. RR -> ( t ^ 2 ) e. RR )
305 304 adantl 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( t ^ 2 ) e. RR )
306 rpgt0 
 |-  ( R e. RR+ -> 0 < R )
307 0red 
 |-  ( R e. RR+ -> 0 e. RR )
308 0le0 
 |-  0 <_ 0
309 308 a1i 
 |-  ( R e. RR+ -> 0 <_ 0 )
310 307 20 309 290 lt2sqd 
 |-  ( R e. RR+ -> ( 0 < R <-> ( 0 ^ 2 ) < ( R ^ 2 ) ) )
311 sq0 
 |-  ( 0 ^ 2 ) = 0
312 311 a1i 
 |-  ( R e. RR+ -> ( 0 ^ 2 ) = 0 )
313 312 breq1d 
 |-  ( R e. RR+ -> ( ( 0 ^ 2 ) < ( R ^ 2 ) <-> 0 < ( R ^ 2 ) ) )
314 310 313 bitrd 
 |-  ( R e. RR+ -> ( 0 < R <-> 0 < ( R ^ 2 ) ) )
315 306 314 mpbid 
 |-  ( R e. RR+ -> 0 < ( R ^ 2 ) )
316 274 315 elrpd 
 |-  ( R e. RR+ -> ( R ^ 2 ) e. RR+ )
317 316 adantr 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( R ^ 2 ) e. RR+ )
318 305 41 317 ltdivmuld 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( ( t ^ 2 ) / ( R ^ 2 ) ) < 1 <-> ( t ^ 2 ) < ( ( R ^ 2 ) x. 1 ) ) )
319 301 303 318 3bitr3rd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( t ^ 2 ) < ( ( R ^ 2 ) x. 1 ) <-> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
320 292 298 319 3bitrd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) < R <-> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
321 285 320 bitr3d 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) <-> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
322 321 biimpd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) -> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
323 322 exp4b 
 |-  ( R e. RR+ -> ( t e. RR -> ( -u R < t -> ( t < R -> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) )
324 323 3impd 
 |-  ( R e. RR+ -> ( ( t e. RR /\ -u R < t /\ t < R ) -> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
325 25 324 sylbid 
 |-  ( R e. RR+ -> ( t e. ( -u R (,) R ) -> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) ) )
326 325 imp 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 < ( 1 - ( ( t / R ) ^ 2 ) ) )
327 284 283 326 ltled 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 <_ ( 1 - ( ( t / R ) ^ 2 ) ) )
328 275 277 283 327 sqrtmuld 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( sqrt ` ( ( R ^ 2 ) x. ( 1 - ( ( t / R ) ^ 2 ) ) ) ) = ( ( sqrt ` ( R ^ 2 ) ) x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) )
329 264 13 14 subdid 
 |-  ( ( 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 ) ) ) )
330 264 mulid1d 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. 1 ) = ( R ^ 2 ) )
331 5 7 9 sqdivd 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( t / R ) ^ 2 ) = ( ( t ^ 2 ) / ( R ^ 2 ) ) )
332 331 oveq2d 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( ( t / R ) ^ 2 ) ) = ( ( R ^ 2 ) x. ( ( t ^ 2 ) / ( R ^ 2 ) ) ) )
333 4 sqcld 
 |-  ( t e. ( -u R (,) R ) -> ( t ^ 2 ) e. CC )
334 333 adantl 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( t ^ 2 ) e. CC )
335 sqne0 
 |-  ( R e. CC -> ( ( R ^ 2 ) =/= 0 <-> R =/= 0 ) )
336 6 335 syl 
 |-  ( R e. RR+ -> ( ( R ^ 2 ) =/= 0 <-> R =/= 0 ) )
337 8 336 mpbird 
 |-  ( R e. RR+ -> ( R ^ 2 ) =/= 0 )
338 337 adantr 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( R ^ 2 ) =/= 0 )
339 334 264 338 divcan2d 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( ( t ^ 2 ) / ( R ^ 2 ) ) ) = ( t ^ 2 ) )
340 332 339 eqtrd 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( ( t / R ) ^ 2 ) ) = ( t ^ 2 ) )
341 330 340 oveq12d 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( ( R ^ 2 ) x. 1 ) - ( ( R ^ 2 ) x. ( ( t / R ) ^ 2 ) ) ) = ( ( R ^ 2 ) - ( t ^ 2 ) ) )
342 329 341 eqtrd 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( 1 - ( ( t / R ) ^ 2 ) ) ) = ( ( R ^ 2 ) - ( t ^ 2 ) ) )
343 342 fveq2d 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( sqrt ` ( ( R ^ 2 ) x. ( 1 - ( ( t / R ) ^ 2 ) ) ) ) = ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
344 20 290 sqrtsqd 
 |-  ( R e. RR+ -> ( sqrt ` ( R ^ 2 ) ) = R )
345 344 adantr 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( sqrt ` ( R ^ 2 ) ) = R )
346 345 oveq1d 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( sqrt ` ( R ^ 2 ) ) x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) = ( R x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) )
347 328 343 346 3eqtr3rd 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( R x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) = ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
348 347 oveq2d 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 2 x. ( R x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) = ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
349 272 273 348 3eqtrd 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( ( R ^ 2 ) x. ( 1 / R ) ) x. ( 2 x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) = ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
350 263 265 349 3eqtr2d 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) x. ( ( 2 x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) x. ( 1 / R ) ) ) = ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
351 350 mpteq2dva 
 |-  ( R e. RR+ -> ( t e. ( -u R (,) R ) |-> ( ( R ^ 2 ) x. ( ( 2 x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) x. ( 1 / R ) ) ) ) = ( t e. ( -u R (,) R ) |-> ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
352 257 351 eqtrd 
 |-  ( R e. RR+ -> ( RR _D ( t e. ( -u R (,) R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( t / R ) ) + ( ( t / R ) x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) ) ) ) = ( t e. ( -u R (,) R ) |-> ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )