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 eqtrid
 |-  ( 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 ) ) ) ) ) )