Metamath Proof Explorer

Theorem areacirclem4

Description: Endpoint-inclusive continuity of antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 31-Aug-2017) (Revised by Brendan Leahy, 11-Jul-2018)

Ref Expression
Assertion areacirclem4 
|- ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( t / R ) ) + ( ( t / R ) x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 rpcn 
 |-  ( R e. RR+ -> R e. CC )
2 1 sqcld 
 |-  ( R e. RR+ -> ( R ^ 2 ) e. CC )
3 rpre 
 |-  ( R e. RR+ -> R e. RR )
4 3 renegcld 
 |-  ( R e. RR+ -> -u R e. RR )
5 iccssre 
 |-  ( ( -u R e. RR /\ R e. RR ) -> ( -u R [,] R ) C_ RR )
6 4 3 5 syl2anc 
 |-  ( R e. RR+ -> ( -u R [,] R ) C_ RR )
7 ax-resscn 
 |-  RR C_ CC
8 6 7 sstrdi 
 |-  ( R e. RR+ -> ( -u R [,] R ) C_ CC )
9 ssid 
 |-  CC C_ CC
10 9 a1i 
 |-  ( R e. RR+ -> CC C_ CC )
11 cncfmptc 
 |-  ( ( ( R ^ 2 ) e. CC /\ ( -u R [,] R ) C_ CC /\ CC C_ CC ) -> ( t e. ( -u R [,] R ) |-> ( R ^ 2 ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
12 2 8 10 11 syl3anc 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( R ^ 2 ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
13 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
14 13 addcn 
 |-  + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
15 14 a1i 
 |-  ( R e. RR+ -> + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
16 8 sselda 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> t e. CC )
17 1 adantr 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> R e. CC )
18 rpne0 
 |-  ( R e. RR+ -> R =/= 0 )
19 18 adantr 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> R =/= 0 )
20 16 17 19 divcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( t / R ) e. CC )
21 asinval 
 |-  ( ( t / R ) e. CC -> ( arcsin ` ( t / R ) ) = ( -u _i x. ( log ` ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) ) )
22 20 21 syl 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( arcsin ` ( t / R ) ) = ( -u _i x. ( log ` ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) ) )
23 ax-icn 
 |-  _i e. CC
24 23 a1i 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> _i e. CC )
25 24 20 mulcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( _i x. ( t / R ) ) e. CC )
26 1cnd 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> 1 e. CC )
27 20 sqcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( t / R ) ^ 2 ) e. CC )
28 26 27 subcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( 1 - ( ( t / R ) ^ 2 ) ) e. CC )
29 28 sqrtcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) e. CC )
30 25 29 addcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. CC )
31 0lt1 
 |-  0 < 1
32 simp3 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t = 0 ) -> t = 0 )
33 32 oveq1d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t = 0 ) -> ( t / R ) = ( 0 / R ) )
34 1 18 div0d 
 |-  ( R e. RR+ -> ( 0 / R ) = 0 )
35 34 3ad2ant1 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t = 0 ) -> ( 0 / R ) = 0 )
36 33 35 eqtrd 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t = 0 ) -> ( t / R ) = 0 )
37 36 oveq2d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t = 0 ) -> ( _i x. ( t / R ) ) = ( _i x. 0 ) )
38 it0e0 
 |-  ( _i x. 0 ) = 0
39 37 38 eqtrdi 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t = 0 ) -> ( _i x. ( t / R ) ) = 0 )
40 36 oveq1d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t = 0 ) -> ( ( t / R ) ^ 2 ) = ( 0 ^ 2 ) )
41 40 oveq2d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t = 0 ) -> ( 1 - ( ( t / R ) ^ 2 ) ) = ( 1 - ( 0 ^ 2 ) ) )
42 41 fveq2d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t = 0 ) -> ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) = ( sqrt ` ( 1 - ( 0 ^ 2 ) ) ) )
43 sq0 
 |-  ( 0 ^ 2 ) = 0
44 43 oveq2i 
 |-  ( 1 - ( 0 ^ 2 ) ) = ( 1 - 0 )
45 1m0e1 
 |-  ( 1 - 0 ) = 1
46 44 45 eqtri 
 |-  ( 1 - ( 0 ^ 2 ) ) = 1
47 46 fveq2i 
 |-  ( sqrt ` ( 1 - ( 0 ^ 2 ) ) ) = ( sqrt ` 1 )
48 sqrt1 
 |-  ( sqrt ` 1 ) = 1
49 47 48 eqtri 
 |-  ( sqrt ` ( 1 - ( 0 ^ 2 ) ) ) = 1
50 42 49 eqtrdi 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t = 0 ) -> ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) = 1 )
51 39 50 oveq12d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t = 0 ) -> ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) = ( 0 + 1 ) )
52 0p1e1 
 |-  ( 0 + 1 ) = 1
53 51 52 eqtrdi 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t = 0 ) -> ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) = 1 )
54 53 breq2d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t = 0 ) -> ( 0 < ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) <-> 0 < 1 ) )
55 0red 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t = 0 ) -> 0 e. RR )
56 1red 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t = 0 ) -> 1 e. RR )
57 53 56 eqeltrd 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t = 0 ) -> ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. RR )
58 55 57 ltnled 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t = 0 ) -> ( 0 < ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) <-> -. ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) <_ 0 ) )
59 54 58 bitr3d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t = 0 ) -> ( 0 < 1 <-> -. ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) <_ 0 ) )
60 31 59 mpbii 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t = 0 ) -> -. ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) <_ 0 )
61 60 3expa 
 |-  ( ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) /\ t = 0 ) -> -. ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) <_ 0 )
62 61 olcd 
 |-  ( ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) /\ t = 0 ) -> ( -. ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. RR \/ -. ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) <_ 0 ) )
63 inelr 
 |-  -. _i e. RR
64 25 29 pncand 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) - ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) = ( _i x. ( t / R ) ) )
65 64 3adant3 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) -> ( ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) - ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) = ( _i x. ( t / R ) ) )
66 65 oveq1d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) -> ( ( ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) - ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) x. ( R / t ) ) = ( ( _i x. ( t / R ) ) x. ( R / t ) ) )
67 23 a1i 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) -> _i e. CC )
68 20 3adant3 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) -> ( t / R ) e. CC )
69 1 3ad2ant1 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) -> R e. CC )
70 16 3adant3 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) -> t e. CC )
71 simp3 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) -> t =/= 0 )
72 69 70 71 divcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) -> ( R / t ) e. CC )
73 67 68 72 mulassd 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) -> ( ( _i x. ( t / R ) ) x. ( R / t ) ) = ( _i x. ( ( t / R ) x. ( R / t ) ) ) )
74 66 73 eqtrd 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) -> ( ( ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) - ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) x. ( R / t ) ) = ( _i x. ( ( t / R ) x. ( R / t ) ) ) )
75 18 3ad2ant1 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) -> R =/= 0 )
76 70 69 71 75 divcan6d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) -> ( ( t / R ) x. ( R / t ) ) = 1 )
77 76 oveq2d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) -> ( _i x. ( ( t / R ) x. ( R / t ) ) ) = ( _i x. 1 ) )
78 67 mulid1d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) -> ( _i x. 1 ) = _i )
79 74 77 78 3eqtrrd 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) -> _i = ( ( ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) - ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) x. ( R / t ) ) )
80 79 adantr 
 |-  ( ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) /\ ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. RR ) -> _i = ( ( ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) - ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) x. ( R / t ) ) )
81 simpr 
 |-  ( ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) /\ ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. RR ) -> ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. RR )
82 1red 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> 1 e. RR )
83 6 sselda 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> t e. RR )
84 3 adantr 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> R e. RR )
85 83 84 19 redivcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( t / R ) e. RR )
86 85 resqcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( t / R ) ^ 2 ) e. RR )
87 82 86 resubcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( 1 - ( ( t / R ) ^ 2 ) ) e. RR )
88 elicc2 
 |-  ( ( -u R e. RR /\ R e. RR ) -> ( t e. ( -u R [,] R ) <-> ( t e. RR /\ -u R <_ t /\ t <_ R ) ) )
89 4 3 88 syl2anc 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) <-> ( t e. RR /\ -u R <_ t /\ t <_ R ) ) )
90 1red 
 |-  ( ( R e. RR+ /\ t e. RR ) -> 1 e. RR )
91 simpr 
 |-  ( ( R e. RR+ /\ t e. RR ) -> t e. RR )
92 3 adantr 
 |-  ( ( R e. RR+ /\ t e. RR ) -> R e. RR )
93 18 adantr 
 |-  ( ( R e. RR+ /\ t e. RR ) -> R =/= 0 )
94 91 92 93 redivcld 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( t / R ) e. RR )
95 94 resqcld 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( t / R ) ^ 2 ) e. RR )
96 90 95 subge0d 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( 0 <_ ( 1 - ( ( t / R ) ^ 2 ) ) <-> ( ( t / R ) ^ 2 ) <_ 1 ) )
97 recn 
 |-  ( t e. RR -> t e. CC )
98 97 adantl 
 |-  ( ( R e. RR+ /\ t e. RR ) -> t e. CC )
99 1 adantr 
 |-  ( ( R e. RR+ /\ t e. RR ) -> R e. CC )
100 98 99 93 sqdivd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( t / R ) ^ 2 ) = ( ( t ^ 2 ) / ( R ^ 2 ) ) )
101 100 breq1d 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( ( t / R ) ^ 2 ) <_ 1 <-> ( ( t ^ 2 ) / ( R ^ 2 ) ) <_ 1 ) )
102 resqcl 
 |-  ( t e. RR -> ( t ^ 2 ) e. RR )
103 102 adantl 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( t ^ 2 ) e. RR )
104 3 resqcld 
 |-  ( R e. RR+ -> ( R ^ 2 ) e. RR )
105 rpgt0 
 |-  ( R e. RR+ -> 0 < R )
106 0red 
 |-  ( R e. RR+ -> 0 e. RR )
107 0le0 
 |-  0 <_ 0
108 107 a1i 
 |-  ( R e. RR+ -> 0 <_ 0 )
109 rpge0 
 |-  ( R e. RR+ -> 0 <_ R )
110 106 3 108 109 lt2sqd 
 |-  ( R e. RR+ -> ( 0 < R <-> ( 0 ^ 2 ) < ( R ^ 2 ) ) )
111 43 a1i 
 |-  ( R e. RR+ -> ( 0 ^ 2 ) = 0 )
112 111 breq1d 
 |-  ( R e. RR+ -> ( ( 0 ^ 2 ) < ( R ^ 2 ) <-> 0 < ( R ^ 2 ) ) )
113 110 112 bitrd 
 |-  ( R e. RR+ -> ( 0 < R <-> 0 < ( R ^ 2 ) ) )
114 105 113 mpbid 
 |-  ( R e. RR+ -> 0 < ( R ^ 2 ) )
115 104 114 elrpd 
 |-  ( R e. RR+ -> ( R ^ 2 ) e. RR+ )
116 115 adantr 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( R ^ 2 ) e. RR+ )
117 103 90 116 ledivmuld 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( ( t ^ 2 ) / ( R ^ 2 ) ) <_ 1 <-> ( t ^ 2 ) <_ ( ( R ^ 2 ) x. 1 ) ) )
118 absresq 
 |-  ( t e. RR -> ( ( abs ` t ) ^ 2 ) = ( t ^ 2 ) )
119 118 eqcomd 
 |-  ( t e. RR -> ( t ^ 2 ) = ( ( abs ` t ) ^ 2 ) )
120 2 mulid1d 
 |-  ( R e. RR+ -> ( ( R ^ 2 ) x. 1 ) = ( R ^ 2 ) )
121 119 120 breqan12rd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( t ^ 2 ) <_ ( ( R ^ 2 ) x. 1 ) <-> ( ( abs ` t ) ^ 2 ) <_ ( R ^ 2 ) ) )
122 97 abscld 
 |-  ( t e. RR -> ( abs ` t ) e. RR )
123 122 adantl 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( abs ` t ) e. RR )
124 97 absge0d 
 |-  ( t e. RR -> 0 <_ ( abs ` t ) )
125 124 adantl 
 |-  ( ( R e. RR+ /\ t e. RR ) -> 0 <_ ( abs ` t ) )
126 109 adantr 
 |-  ( ( R e. RR+ /\ t e. RR ) -> 0 <_ R )
127 123 92 125 126 le2sqd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) <_ R <-> ( ( abs ` t ) ^ 2 ) <_ ( R ^ 2 ) ) )
128 91 92 absled 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) <_ R <-> ( -u R <_ t /\ t <_ R ) ) )
129 121 127 128 3bitr2d 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( t ^ 2 ) <_ ( ( R ^ 2 ) x. 1 ) <-> ( -u R <_ t /\ t <_ R ) ) )
130 117 129 bitrd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( ( t ^ 2 ) / ( R ^ 2 ) ) <_ 1 <-> ( -u R <_ t /\ t <_ R ) ) )
131 96 101 130 3bitrrd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R <_ t /\ t <_ R ) <-> 0 <_ ( 1 - ( ( t / R ) ^ 2 ) ) ) )
132 131 biimpd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R <_ t /\ t <_ R ) -> 0 <_ ( 1 - ( ( t / R ) ^ 2 ) ) ) )
133 132 exp4b 
 |-  ( R e. RR+ -> ( t e. RR -> ( -u R <_ t -> ( t <_ R -> 0 <_ ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) )
134 133 3impd 
 |-  ( R e. RR+ -> ( ( t e. RR /\ -u R <_ t /\ t <_ R ) -> 0 <_ ( 1 - ( ( t / R ) ^ 2 ) ) ) )
135 89 134 sylbid 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) -> 0 <_ ( 1 - ( ( t / R ) ^ 2 ) ) ) )
136 135 imp 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> 0 <_ ( 1 - ( ( t / R ) ^ 2 ) ) )
137 87 136 resqrtcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) e. RR )
138 137 3adant3 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) -> ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) e. RR )
139 138 adantr 
 |-  ( ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) /\ ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. RR ) -> ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) e. RR )
140 81 139 resubcld 
 |-  ( ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) /\ ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. RR ) -> ( ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) - ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. RR )
141 3 3ad2ant1 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) -> R e. RR )
142 83 3adant3 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) -> t e. RR )
143 141 142 71 redivcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) -> ( R / t ) e. RR )
144 143 adantr 
 |-  ( ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) /\ ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. RR ) -> ( R / t ) e. RR )
145 140 144 remulcld 
 |-  ( ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) /\ ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. RR ) -> ( ( ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) - ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) x. ( R / t ) ) e. RR )
146 80 145 eqeltrd 
 |-  ( ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) /\ ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. RR ) -> _i e. RR )
147 146 ex 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) /\ t =/= 0 ) -> ( ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. RR -> _i e. RR ) )
148 147 3expa 
 |-  ( ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) /\ t =/= 0 ) -> ( ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. RR -> _i e. RR ) )
149 63 148 mtoi 
 |-  ( ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) /\ t =/= 0 ) -> -. ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. RR )
150 149 orcd 
 |-  ( ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) /\ t =/= 0 ) -> ( -. ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. RR \/ -. ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) <_ 0 ) )
151 62 150 pm2.61dane 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( -. ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. RR \/ -. ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) <_ 0 ) )
152 ianor 
 |-  ( -. ( ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. RR /\ ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) <_ 0 ) <-> ( -. ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. RR \/ -. ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) <_ 0 ) )
153 151 152 sylibr 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> -. ( ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. RR /\ ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) <_ 0 ) )
154 mnfxr 
 |-  -oo e. RR*
155 0re 
 |-  0 e. RR
156 elioc2 
 |-  ( ( -oo e. RR* /\ 0 e. RR ) -> ( ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. ( -oo (,] 0 ) <-> ( ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. RR /\ -oo < ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) /\ ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) <_ 0 ) ) )
157 154 155 156 mp2an 
 |-  ( ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. ( -oo (,] 0 ) <-> ( ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. RR /\ -oo < ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) /\ ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) <_ 0 ) )
158 3simpb 
 |-  ( ( ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. RR /\ -oo < ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) /\ ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) <_ 0 ) -> ( ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. RR /\ ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) <_ 0 ) )
159 157 158 sylbi 
 |-  ( ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. ( -oo (,] 0 ) -> ( ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. RR /\ ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) <_ 0 ) )
160 153 159 nsyl 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> -. ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. ( -oo (,] 0 ) )
161 30 160 eldifd 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. ( CC \ ( -oo (,] 0 ) ) )
162 fvres 
 |-  ( ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. ( CC \ ( -oo (,] 0 ) ) -> ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) ` ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) = ( log ` ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) )
163 161 162 syl 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) ` ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) = ( log ` ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) )
164 163 oveq2d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( -u _i x. ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) ` ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) ) = ( -u _i x. ( log ` ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) ) )
165 22 164 eqtr4d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( arcsin ` ( t / R ) ) = ( -u _i x. ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) ` ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) ) )
166 165 mpteq2dva 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( arcsin ` ( t / R ) ) ) = ( t e. ( -u R [,] R ) |-> ( -u _i x. ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) ` ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) ) ) )
167 negicn 
 |-  -u _i e. CC
168 167 a1i 
 |-  ( R e. RR+ -> -u _i e. CC )
169 cncfmptc 
 |-  ( ( -u _i e. CC /\ ( -u R [,] R ) C_ CC /\ CC C_ CC ) -> ( t e. ( -u R [,] R ) |-> -u _i ) e. ( ( -u R [,] R ) -cn-> CC ) )
170 168 8 10 169 syl3anc 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> -u _i ) e. ( ( -u R [,] R ) -cn-> CC ) )
171 13 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
172 171 a1i 
 |-  ( R e. RR+ -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
173 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( -u R [,] R ) C_ CC ) -> ( ( TopOpen ` CCfld ) |`t ( -u R [,] R ) ) e. ( TopOn ` ( -u R [,] R ) ) )
174 172 8 173 syl2anc 
 |-  ( R e. RR+ -> ( ( TopOpen ` CCfld ) |`t ( -u R [,] R ) ) e. ( TopOn ` ( -u R [,] R ) ) )
175 161 fmpttd 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) : ( -u R [,] R ) --> ( CC \ ( -oo (,] 0 ) ) )
176 difssd 
 |-  ( R e. RR+ -> ( CC \ ( -oo (,] 0 ) ) C_ CC )
177 16 17 19 divrec2d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( t / R ) = ( ( 1 / R ) x. t ) )
178 177 oveq2d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( _i x. ( t / R ) ) = ( _i x. ( ( 1 / R ) x. t ) ) )
179 1 18 reccld 
 |-  ( R e. RR+ -> ( 1 / R ) e. CC )
180 179 adantr 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( 1 / R ) e. CC )
181 24 180 16 mulassd 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( _i x. ( 1 / R ) ) x. t ) = ( _i x. ( ( 1 / R ) x. t ) ) )
182 178 181 eqtr4d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( _i x. ( t / R ) ) = ( ( _i x. ( 1 / R ) ) x. t ) )
183 182 mpteq2dva 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( _i x. ( t / R ) ) ) = ( t e. ( -u R [,] R ) |-> ( ( _i x. ( 1 / R ) ) x. t ) ) )
184 23 a1i 
 |-  ( R e. RR+ -> _i e. CC )
185 184 179 mulcld 
 |-  ( R e. RR+ -> ( _i x. ( 1 / R ) ) e. CC )
186 cncfmptc 
 |-  ( ( ( _i x. ( 1 / R ) ) e. CC /\ ( -u R [,] R ) C_ CC /\ CC C_ CC ) -> ( t e. ( -u R [,] R ) |-> ( _i x. ( 1 / R ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
187 185 8 10 186 syl3anc 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( _i x. ( 1 / R ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
188 cncfmptid 
 |-  ( ( ( -u R [,] R ) C_ CC /\ CC C_ CC ) -> ( t e. ( -u R [,] R ) |-> t ) e. ( ( -u R [,] R ) -cn-> CC ) )
189 8 10 188 syl2anc 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> t ) e. ( ( -u R [,] R ) -cn-> CC ) )
190 187 189 mulcncf 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( ( _i x. ( 1 / R ) ) x. t ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
191 183 190 eqeltrd 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( _i x. ( t / R ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
192 17 29 mulcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( R x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. CC )
193 192 17 19 divrec2d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( R x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) / R ) = ( ( 1 / R ) x. ( R x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) )
194 29 17 19 divcan3d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( R x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) / R ) = ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) )
195 104 adantr 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( R ^ 2 ) e. RR )
196 3 sqge0d 
 |-  ( R e. RR+ -> 0 <_ ( R ^ 2 ) )
197 196 adantr 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> 0 <_ ( R ^ 2 ) )
198 195 197 87 136 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 ) ) ) ) )
199 2 adantr 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( R ^ 2 ) e. CC )
200 199 26 27 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 ) ) ) )
201 199 mulid1d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( R ^ 2 ) x. 1 ) = ( R ^ 2 ) )
202 16 17 19 sqdivd 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( t / R ) ^ 2 ) = ( ( t ^ 2 ) / ( R ^ 2 ) ) )
203 202 oveq2d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( R ^ 2 ) x. ( ( t / R ) ^ 2 ) ) = ( ( R ^ 2 ) x. ( ( t ^ 2 ) / ( R ^ 2 ) ) ) )
204 16 sqcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( t ^ 2 ) e. CC )
205 sqne0 
 |-  ( R e. CC -> ( ( R ^ 2 ) =/= 0 <-> R =/= 0 ) )
206 1 205 syl 
 |-  ( R e. RR+ -> ( ( R ^ 2 ) =/= 0 <-> R =/= 0 ) )
207 18 206 mpbird 
 |-  ( R e. RR+ -> ( R ^ 2 ) =/= 0 )
208 207 adantr 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( R ^ 2 ) =/= 0 )
209 204 199 208 divcan2d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( R ^ 2 ) x. ( ( t ^ 2 ) / ( R ^ 2 ) ) ) = ( t ^ 2 ) )
210 203 209 eqtrd 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( R ^ 2 ) x. ( ( t / R ) ^ 2 ) ) = ( t ^ 2 ) )
211 201 210 oveq12d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( ( R ^ 2 ) x. 1 ) - ( ( R ^ 2 ) x. ( ( t / R ) ^ 2 ) ) ) = ( ( R ^ 2 ) - ( t ^ 2 ) ) )
212 200 211 eqtrd 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( R ^ 2 ) x. ( 1 - ( ( t / R ) ^ 2 ) ) ) = ( ( R ^ 2 ) - ( t ^ 2 ) ) )
213 212 fveq2d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( sqrt ` ( ( R ^ 2 ) x. ( 1 - ( ( t / R ) ^ 2 ) ) ) ) = ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
214 109 adantr 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> 0 <_ R )
215 84 214 sqrtsqd 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( sqrt ` ( R ^ 2 ) ) = R )
216 215 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 ) ) ) ) )
217 198 213 216 3eqtr3rd 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( R x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) = ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
218 217 oveq2d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( 1 / R ) x. ( R x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) = ( ( 1 / R ) x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
219 193 194 218 3eqtr3d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) = ( ( 1 / R ) x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
220 219 mpteq2dva 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) = ( t e. ( -u R [,] R ) |-> ( ( 1 / R ) x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
221 cncfmptc 
 |-  ( ( ( 1 / R ) e. CC /\ ( -u R [,] R ) C_ CC /\ CC C_ CC ) -> ( t e. ( -u R [,] R ) |-> ( 1 / R ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
222 179 8 10 221 syl3anc 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( 1 / R ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
223 areacirclem2 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( -u R [,] R ) |-> ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
224 3 109 223 syl2anc 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
225 222 224 mulcncf 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( ( 1 / R ) x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
226 220 225 eqeltrd 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
227 13 15 191 226 cncfmpt2f 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
228 cncffvrn 
 |-  ( ( ( CC \ ( -oo (,] 0 ) ) C_ CC /\ ( t e. ( -u R [,] R ) |-> ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) ) -> ( ( t e. ( -u R [,] R ) |-> ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) e. ( ( -u R [,] R ) -cn-> ( CC \ ( -oo (,] 0 ) ) ) <-> ( t e. ( -u R [,] R ) |-> ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) : ( -u R [,] R ) --> ( CC \ ( -oo (,] 0 ) ) ) )
229 176 227 228 syl2anc 
 |-  ( R e. RR+ -> ( ( t e. ( -u R [,] R ) |-> ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) e. ( ( -u R [,] R ) -cn-> ( CC \ ( -oo (,] 0 ) ) ) <-> ( t e. ( -u R [,] R ) |-> ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) : ( -u R [,] R ) --> ( CC \ ( -oo (,] 0 ) ) ) )
230 175 229 mpbird 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) e. ( ( -u R [,] R ) -cn-> ( CC \ ( -oo (,] 0 ) ) ) )
231 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( -u R [,] R ) ) = ( ( TopOpen ` CCfld ) |`t ( -u R [,] R ) )
232 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) = ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) )
233 13 231 232 cncfcn 
 |-  ( ( ( -u R [,] R ) C_ CC /\ ( CC \ ( -oo (,] 0 ) ) C_ CC ) -> ( ( -u R [,] R ) -cn-> ( CC \ ( -oo (,] 0 ) ) ) = ( ( ( TopOpen ` CCfld ) |`t ( -u R [,] R ) ) Cn ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) ) )
234 8 176 233 syl2anc 
 |-  ( R e. RR+ -> ( ( -u R [,] R ) -cn-> ( CC \ ( -oo (,] 0 ) ) ) = ( ( ( TopOpen ` CCfld ) |`t ( -u R [,] R ) ) Cn ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) ) )
235 230 234 eleqtrd 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( -u R [,] R ) ) Cn ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) ) )
236 eqid 
 |-  ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) )
237 236 logcn 
 |-  ( log |` ( CC \ ( -oo (,] 0 ) ) ) e. ( ( CC \ ( -oo (,] 0 ) ) -cn-> CC )
238 difss 
 |-  ( CC \ ( -oo (,] 0 ) ) C_ CC
239 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t CC ) = ( ( TopOpen ` CCfld ) |`t CC )
240 13 232 239 cncfcn 
 |-  ( ( ( CC \ ( -oo (,] 0 ) ) C_ CC /\ CC C_ CC ) -> ( ( CC \ ( -oo (,] 0 ) ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) Cn ( ( TopOpen ` CCfld ) |`t CC ) ) )
241 238 9 240 mp2an 
 |-  ( ( CC \ ( -oo (,] 0 ) ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) Cn ( ( TopOpen ` CCfld ) |`t CC ) )
242 237 241 eleqtri 
 |-  ( log |` ( CC \ ( -oo (,] 0 ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) Cn ( ( TopOpen ` CCfld ) |`t CC ) )
243 242 a1i 
 |-  ( R e. RR+ -> ( log |` ( CC \ ( -oo (,] 0 ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) Cn ( ( TopOpen ` CCfld ) |`t CC ) ) )
244 174 235 243 cnmpt11f 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) ` ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( -u R [,] R ) ) Cn ( ( TopOpen ` CCfld ) |`t CC ) ) )
245 13 231 239 cncfcn 
 |-  ( ( ( -u R [,] R ) C_ CC /\ CC C_ CC ) -> ( ( -u R [,] R ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( -u R [,] R ) ) Cn ( ( TopOpen ` CCfld ) |`t CC ) ) )
246 8 10 245 syl2anc 
 |-  ( R e. RR+ -> ( ( -u R [,] R ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( -u R [,] R ) ) Cn ( ( TopOpen ` CCfld ) |`t CC ) ) )
247 244 246 eleqtrrd 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) ` ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
248 170 247 mulcncf 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( -u _i x. ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) ` ( ( _i x. ( t / R ) ) + ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
249 166 248 eqeltrd 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( arcsin ` ( t / R ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
250 219 oveq2d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( t / R ) x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) = ( ( t / R ) x. ( ( 1 / R ) x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
251 199 204 subcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( R ^ 2 ) - ( t ^ 2 ) ) e. CC )
252 251 sqrtcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. CC )
253 20 180 252 mulassd 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( ( t / R ) x. ( 1 / R ) ) x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) = ( ( t / R ) x. ( ( 1 / R ) x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
254 16 17 19 divrecd 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( t / R ) = ( t x. ( 1 / R ) ) )
255 254 oveq1d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( t / R ) x. ( 1 / R ) ) = ( ( t x. ( 1 / R ) ) x. ( 1 / R ) ) )
256 16 180 180 mulassd 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( t x. ( 1 / R ) ) x. ( 1 / R ) ) = ( t x. ( ( 1 / R ) x. ( 1 / R ) ) ) )
257 255 256 eqtrd 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( t / R ) x. ( 1 / R ) ) = ( t x. ( ( 1 / R ) x. ( 1 / R ) ) ) )
258 257 oveq1d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( ( t / R ) x. ( 1 / R ) ) x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) = ( ( t x. ( ( 1 / R ) x. ( 1 / R ) ) ) x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
259 250 253 258 3eqtr2d 
 |-  ( ( R e. RR+ /\ t e. ( -u R [,] R ) ) -> ( ( t / R ) x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) = ( ( t x. ( ( 1 / R ) x. ( 1 / R ) ) ) x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
260 259 mpteq2dva 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( ( t / R ) x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) = ( t e. ( -u R [,] R ) |-> ( ( t x. ( ( 1 / R ) x. ( 1 / R ) ) ) x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
261 179 179 mulcld 
 |-  ( R e. RR+ -> ( ( 1 / R ) x. ( 1 / R ) ) e. CC )
262 cncfmptc 
 |-  ( ( ( ( 1 / R ) x. ( 1 / R ) ) e. CC /\ ( -u R [,] R ) C_ CC /\ CC C_ CC ) -> ( t e. ( -u R [,] R ) |-> ( ( 1 / R ) x. ( 1 / R ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
263 261 8 10 262 syl3anc 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( ( 1 / R ) x. ( 1 / R ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
264 189 263 mulcncf 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( t x. ( ( 1 / R ) x. ( 1 / R ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
265 264 224 mulcncf 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( ( t x. ( ( 1 / R ) x. ( 1 / R ) ) ) x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
266 260 265 eqeltrd 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( ( t / R ) x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
267 13 15 249 266 cncfmpt2f 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( ( arcsin ` ( t / R ) ) + ( ( t / R ) x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
268 12 267 mulcncf 
 |-  ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( t / R ) ) + ( ( t / R ) x. ( sqrt ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )