Metamath Proof Explorer

Theorem dvasin

Description: Derivative of arcsine. (Contributed by Brendan Leahy, 18-Dec-2018)

Ref Expression
Hypothesis dvasin.d ⊢D=ℂ∖−∞−1∪1+∞
Assertion dvasin ⊢ℂDarcsin↾D=x∈D⟼11−x2

Proof

Step Hyp Ref Expression
1 dvasin.d ⊢D=ℂ∖−∞−1∪1+∞
2 df-asin ⊢arcsin=x∈ℂ⟼−i⁢log⁡i⁢x+1−x2
3 2 reseq1i ⊢arcsin↾D=x∈ℂ⟼−i⁢log⁡i⁢x+1−x2↾D
4 difss ⊢ℂ∖−∞−1∪1+∞⊆ℂ
5 1 4 eqsstri ⊢D⊆ℂ
6 resmpt ⊢D⊆ℂ→x∈ℂ⟼−i⁢log⁡i⁢x+1−x2↾D=x∈D⟼−i⁢log⁡i⁢x+1−x2
7 5 6 ax-mp ⊢x∈ℂ⟼−i⁢log⁡i⁢x+1−x2↾D=x∈D⟼−i⁢log⁡i⁢x+1−x2
8 3 7 eqtri ⊢arcsin↾D=x∈D⟼−i⁢log⁡i⁢x+1−x2
9 8 oveq2i ⊢ℂDarcsin↾D=dx∈D−i⁢log⁡i⁢x+1−x2dℂx
10 cnelprrecn ⊢ℂ∈ℝℂ
11 10 a1i ⊢⊤→ℂ∈ℝℂ
12 5 sseli ⊢x∈D→x∈ℂ
13 ax-icn ⊢i∈ℂ
14 mulcl ⊢i∈ℂ∧x∈ℂ→i⁢x∈ℂ
15 13 14 mpan ⊢x∈ℂ→i⁢x∈ℂ
16 ax-1cn ⊢1∈ℂ
17 sqcl ⊢x∈ℂ→x2∈ℂ
18 subcl ⊢1∈ℂ∧x2∈ℂ→1−x2∈ℂ
19 16 17 18 sylancr ⊢x∈ℂ→1−x2∈ℂ
20 19 sqrtcld ⊢x∈ℂ→1−x2∈ℂ
21 15 20 addcld ⊢x∈ℂ→i⁢x+1−x2∈ℂ
22 12 21 syl ⊢x∈D→i⁢x+1−x2∈ℂ
23 asinlem ⊢x∈ℂ→i⁢x+1−x2≠0
24 12 23 syl ⊢x∈D→i⁢x+1−x2≠0
25 22 24 logcld ⊢x∈D→log⁡i⁢x+1−x2∈ℂ
26 25 adantl ⊢⊤∧x∈D→log⁡i⁢x+1−x2∈ℂ
27 ovexd ⊢⊤∧x∈D→i1−x2∈V
28 simpr ⊢x∈ℂ∧i⁢x+1−x2∈ℝ→i⁢x+1−x2∈ℝ
29 asinlem3 ⊢x∈ℂ→0≤ℜ⁡i⁢x+1−x2
30 rere ⊢i⁢x+1−x2∈ℝ→ℜ⁡i⁢x+1−x2=i⁢x+1−x2
31 30 breq2d ⊢i⁢x+1−x2∈ℝ→0≤ℜ⁡i⁢x+1−x2↔0≤i⁢x+1−x2
32 31 biimpac ⊢0≤ℜ⁡i⁢x+1−x2∧i⁢x+1−x2∈ℝ→0≤i⁢x+1−x2
33 29 32 sylan ⊢x∈ℂ∧i⁢x+1−x2∈ℝ→0≤i⁢x+1−x2
34 23 adantr ⊢x∈ℂ∧i⁢x+1−x2∈ℝ→i⁢x+1−x2≠0
35 28 33 34 ne0gt0d ⊢x∈ℂ∧i⁢x+1−x2∈ℝ→0<i⁢x+1−x2
36 0re ⊢0∈ℝ
37 ltnle ⊢0∈ℝ∧i⁢x+1−x2∈ℝ→0<i⁢x+1−x2↔¬i⁢x+1−x2≤0
38 36 37 mpan ⊢i⁢x+1−x2∈ℝ→0<i⁢x+1−x2↔¬i⁢x+1−x2≤0
39 38 adantl ⊢x∈ℂ∧i⁢x+1−x2∈ℝ→0<i⁢x+1−x2↔¬i⁢x+1−x2≤0
40 35 39 mpbid ⊢x∈ℂ∧i⁢x+1−x2∈ℝ→¬i⁢x+1−x2≤0
41 40 ex ⊢x∈ℂ→i⁢x+1−x2∈ℝ→¬i⁢x+1−x2≤0
42 12 41 syl ⊢x∈D→i⁢x+1−x2∈ℝ→¬i⁢x+1−x2≤0
43 imor ⊢i⁢x+1−x2∈ℝ→¬i⁢x+1−x2≤0↔¬i⁢x+1−x2∈ℝ∨¬i⁢x+1−x2≤0
44 42 43 sylib ⊢x∈D→¬i⁢x+1−x2∈ℝ∨¬i⁢x+1−x2≤0
45 44 orcomd ⊢x∈D→¬i⁢x+1−x2≤0∨¬i⁢x+1−x2∈ℝ
46 45 olcd ⊢x∈D→¬−∞<i⁢x+1−x2∨¬i⁢x+1−x2≤0∨¬i⁢x+1−x2∈ℝ
47 3ianor ⊢¬i⁢x+1−x2∈ℝ∧−∞<i⁢x+1−x2∧i⁢x+1−x2≤0↔¬i⁢x+1−x2∈ℝ∨¬−∞<i⁢x+1−x2∨¬i⁢x+1−x2≤0
48 3orrot ⊢¬i⁢x+1−x2∈ℝ∨¬−∞<i⁢x+1−x2∨¬i⁢x+1−x2≤0↔¬−∞<i⁢x+1−x2∨¬i⁢x+1−x2≤0∨¬i⁢x+1−x2∈ℝ
49 3orass ⊢¬−∞<i⁢x+1−x2∨¬i⁢x+1−x2≤0∨¬i⁢x+1−x2∈ℝ↔¬−∞<i⁢x+1−x2∨¬i⁢x+1−x2≤0∨¬i⁢x+1−x2∈ℝ
50 47 48 49 3bitrri ⊢¬−∞<i⁢x+1−x2∨¬i⁢x+1−x2≤0∨¬i⁢x+1−x2∈ℝ↔¬i⁢x+1−x2∈ℝ∧−∞<i⁢x+1−x2∧i⁢x+1−x2≤0
51 mnfxr ⊢−∞∈ℝ*
52 elioc2 ⊢−∞∈ℝ*∧0∈ℝ→i⁢x+1−x2∈−∞0↔i⁢x+1−x2∈ℝ∧−∞<i⁢x+1−x2∧i⁢x+1−x2≤0
53 51 36 52 mp2an ⊢i⁢x+1−x2∈−∞0↔i⁢x+1−x2∈ℝ∧−∞<i⁢x+1−x2∧i⁢x+1−x2≤0
54 50 53 xchbinxr ⊢¬−∞<i⁢x+1−x2∨¬i⁢x+1−x2≤0∨¬i⁢x+1−x2∈ℝ↔¬i⁢x+1−x2∈−∞0
55 46 54 sylib ⊢x∈D→¬i⁢x+1−x2∈−∞0
56 22 55 eldifd ⊢x∈D→i⁢x+1−x2∈ℂ∖−∞0
57 56 adantl ⊢⊤∧x∈D→i⁢x+1−x2∈ℂ∖−∞0
58 ovexd ⊢⊤∧x∈D→i⁢i⁢x+1−x21−x2∈V
59 eldifi ⊢y∈ℂ∖−∞0→y∈ℂ
60 eldifn ⊢y∈ℂ∖−∞0→¬y∈−∞0
61 0xr ⊢0∈ℝ*
62 mnflt0 ⊢−∞<0
63 ubioc1 ⊢−∞∈ℝ*∧0∈ℝ*∧−∞<0→0∈−∞0
64 51 61 62 63 mp3an ⊢0∈−∞0
65 eleq1 ⊢y=0→y∈−∞0↔0∈−∞0
66 64 65 mpbiri ⊢y=0→y∈−∞0
67 66 necon3bi ⊢¬y∈−∞0→y≠0
68 60 67 syl ⊢y∈ℂ∖−∞0→y≠0
69 59 68 logcld ⊢y∈ℂ∖−∞0→log⁡y∈ℂ
70 69 adantl ⊢⊤∧y∈ℂ∖−∞0→log⁡y∈ℂ
71 ovexd ⊢⊤∧y∈ℂ∖−∞0→1y∈V
72 13 a1i ⊢x∈D→i∈ℂ
73 72 12 mulcld ⊢x∈D→i⁢x∈ℂ
74 73 adantl ⊢⊤∧x∈D→i⁢x∈ℂ
75 13 a1i ⊢⊤∧x∈D→i∈ℂ
76 12 adantl ⊢⊤∧x∈D→x∈ℂ
77 1cnd ⊢⊤∧x∈D→1∈ℂ
78 simpr ⊢⊤∧x∈ℂ→x∈ℂ
79 1cnd ⊢⊤∧x∈ℂ→1∈ℂ
80 11 dvmptid ⊢⊤→dx∈ℂxdℂx=x∈ℂ⟼1
81 5 a1i ⊢⊤→D⊆ℂ
82 eqid ⊢TopOpen⁡ℂfld=TopOpen⁡ℂfld
83 82 cnfldtopon ⊢TopOpen⁡ℂfld∈TopOn⁡ℂ
84 83 toponrestid ⊢TopOpen⁡ℂfld=TopOpen⁡ℂfld↾𝑡ℂ
85 82 recld2 ⊢ℝ∈Clsd⁡TopOpen⁡ℂfld
86 neg1rr ⊢−1∈ℝ
87 iocmnfcld ⊢−1∈ℝ→−∞−1∈Clsd⁡topGen⁡ran⁡.
88 86 87 ax-mp ⊢−∞−1∈Clsd⁡topGen⁡ran⁡.
89 1re ⊢1∈ℝ
90 icopnfcld ⊢1∈ℝ→1+∞∈Clsd⁡topGen⁡ran⁡.
91 89 90 ax-mp ⊢1+∞∈Clsd⁡topGen⁡ran⁡.
92 uncld ⊢−∞−1∈Clsd⁡topGen⁡ran⁡.∧1+∞∈Clsd⁡topGen⁡ran⁡.→−∞−1∪1+∞∈Clsd⁡topGen⁡ran⁡.
93 88 91 92 mp2an ⊢−∞−1∪1+∞∈Clsd⁡topGen⁡ran⁡.
94 82 tgioo2 ⊢topGen⁡ran⁡.=TopOpen⁡ℂfld↾𝑡ℝ
95 94 fveq2i ⊢Clsd⁡topGen⁡ran⁡.=Clsd⁡TopOpen⁡ℂfld↾𝑡ℝ
96 93 95 eleqtri ⊢−∞−1∪1+∞∈Clsd⁡TopOpen⁡ℂfld↾𝑡ℝ
97 restcldr ⊢ℝ∈Clsd⁡TopOpen⁡ℂfld∧−∞−1∪1+∞∈Clsd⁡TopOpen⁡ℂfld↾𝑡ℝ→−∞−1∪1+∞∈Clsd⁡TopOpen⁡ℂfld
98 85 96 97 mp2an ⊢−∞−1∪1+∞∈Clsd⁡TopOpen⁡ℂfld
99 83 toponunii ⊢ℂ=⋃TopOpen⁡ℂfld
100 99 cldopn ⊢−∞−1∪1+∞∈Clsd⁡TopOpen⁡ℂfld→ℂ∖−∞−1∪1+∞∈TopOpen⁡ℂfld
101 98 100 ax-mp ⊢ℂ∖−∞−1∪1+∞∈TopOpen⁡ℂfld
102 1 101 eqeltri ⊢D∈TopOpen⁡ℂfld
103 102 a1i ⊢⊤→D∈TopOpen⁡ℂfld
104 11 78 79 80 81 84 82 103 dvmptres ⊢⊤→dx∈Dxdℂx=x∈D⟼1
105 13 a1i ⊢⊤→i∈ℂ
106 11 76 77 104 105 dvmptcmul ⊢⊤→dx∈Di⁢xdℂx=x∈D⟼i⋅1
107 13 mulridi ⊢i⋅1=i
108 107 mpteq2i ⊢x∈D⟼i⋅1=x∈D⟼i
109 106 108 eqtrdi ⊢⊤→dx∈Di⁢xdℂx=x∈D⟼i
110 12 sqcld ⊢x∈D→x2∈ℂ
111 16 110 18 sylancr ⊢x∈D→1−x2∈ℂ
112 111 sqrtcld ⊢x∈D→1−x2∈ℂ
113 112 adantl ⊢⊤∧x∈D→1−x2∈ℂ
114 ovexd ⊢⊤∧x∈D→−x1−x2∈V
115 elin ⊢x∈D∩ℝ↔x∈D∧x∈ℝ
116 1 asindmre ⊢D∩ℝ=−11
117 116 eqimssi ⊢D∩ℝ⊆−11
118 117 sseli ⊢x∈D∩ℝ→x∈−11
119 115 118 sylbir ⊢x∈D∧x∈ℝ→x∈−11
120 incom ⊢0+∞∩−∞0=−∞0∩0+∞
121 pnfxr ⊢+∞∈ℝ*
122 df-ioc ⊢.=x∈ℝ*,y∈ℝ*⟼z∈ℝ*|x<z∧z≤y
123 df-ioo ⊢.=x∈ℝ*,y∈ℝ*⟼z∈ℝ*|x<z∧z<y
124 xrltnle ⊢0∈ℝ*∧w∈ℝ*→0<w↔¬w≤0
125 122 123 124 ixxdisj ⊢−∞∈ℝ*∧0∈ℝ*∧+∞∈ℝ*→−∞0∩0+∞=∅
126 51 61 121 125 mp3an ⊢−∞0∩0+∞=∅
127 120 126 eqtri ⊢0+∞∩−∞0=∅
128 elioore ⊢x∈−11→x∈ℝ
129 128 resqcld ⊢x∈−11→x2∈ℝ
130 resubcl ⊢1∈ℝ∧x2∈ℝ→1−x2∈ℝ
131 89 129 130 sylancr ⊢x∈−11→1−x2∈ℝ
132 86 rexri ⊢−1∈ℝ*
133 1xr ⊢1∈ℝ*
134 elioo2 ⊢−1∈ℝ*∧1∈ℝ*→x∈−11↔x∈ℝ∧−1<x∧x<1
135 132 133 134 mp2an ⊢x∈−11↔x∈ℝ∧−1<x∧x<1
136 recn ⊢x∈ℝ→x∈ℂ
137 136 abscld ⊢x∈ℝ→x∈ℝ
138 136 absge0d ⊢x∈ℝ→0≤x
139 0le1 ⊢0≤1
140 lt2sq ⊢x∈ℝ∧0≤x∧1∈ℝ∧0≤1→x<1↔x2<12
141 89 139 140 mpanr12 ⊢x∈ℝ∧0≤x→x<1↔x2<12
142 137 138 141 syl2anc ⊢x∈ℝ→x<1↔x2<12
143 abslt ⊢x∈ℝ∧1∈ℝ→x<1↔−1<x∧x<1
144 89 143 mpan2 ⊢x∈ℝ→x<1↔−1<x∧x<1
145 absresq ⊢x∈ℝ→x2=x2
146 sq1 ⊢12=1
147 146 a1i ⊢x∈ℝ→12=1
148 145 147 breq12d ⊢x∈ℝ→x2<12↔x2<1
149 resqcl ⊢x∈ℝ→x2∈ℝ
150 posdif ⊢x2∈ℝ∧1∈ℝ→x2<1↔0<1−x2
151 149 89 150 sylancl ⊢x∈ℝ→x2<1↔0<1−x2
152 148 151 bitrd ⊢x∈ℝ→x2<12↔0<1−x2
153 142 144 152 3bitr3d ⊢x∈ℝ→−1<x∧x<1↔0<1−x2
154 153 biimpd ⊢x∈ℝ→−1<x∧x<1→0<1−x2
155 154 3impib ⊢x∈ℝ∧−1<x∧x<1→0<1−x2
156 135 155 sylbi ⊢x∈−11→0<1−x2
157 131 156 elrpd ⊢x∈−11→1−x2∈ℝ+
158 ioorp ⊢0+∞=ℝ+
159 157 158 eleqtrrdi ⊢x∈−11→1−x2∈0+∞
160 disjel ⊢0+∞∩−∞0=∅∧1−x2∈0+∞→¬1−x2∈−∞0
161 127 159 160 sylancr ⊢x∈−11→¬1−x2∈−∞0
162 119 161 syl ⊢x∈D∧x∈ℝ→¬1−x2∈−∞0
163 elioc2 ⊢−∞∈ℝ*∧0∈ℝ→1−x2∈−∞0↔1−x2∈ℝ∧−∞<1−x2∧1−x2≤0
164 51 36 163 mp2an ⊢1−x2∈−∞0↔1−x2∈ℝ∧−∞<1−x2∧1−x2≤0
165 164 biimpi ⊢1−x2∈−∞0→1−x2∈ℝ∧−∞<1−x2∧1−x2≤0
166 165 simp1d ⊢1−x2∈−∞0→1−x2∈ℝ
167 resubcl ⊢1∈ℝ∧1−x2∈ℝ→1−1−x2∈ℝ
168 89 166 167 sylancr ⊢1−x2∈−∞0→1−1−x2∈ℝ
169 nncan ⊢1∈ℂ∧x2∈ℂ→1−1−x2=x2
170 16 169 mpan ⊢x2∈ℂ→1−1−x2=x2
171 170 eleq1d ⊢x2∈ℂ→1−1−x2∈ℝ↔x2∈ℝ
172 171 biimpa ⊢x2∈ℂ∧1−1−x2∈ℝ→x2∈ℝ
173 168 172 sylan2 ⊢x2∈ℂ∧1−x2∈−∞0→x2∈ℝ
174 166 adantl ⊢x2∈ℂ∧1−x2∈−∞0→1−x2∈ℝ
175 165 simp3d ⊢1−x2∈−∞0→1−x2≤0
176 175 adantl ⊢x2∈ℂ∧1−x2∈−∞0→1−x2≤0
177 letr ⊢1−x2∈ℝ∧0∈ℝ∧1∈ℝ→1−x2≤0∧0≤1→1−x2≤1
178 36 89 177 mp3an23 ⊢1−x2∈ℝ→1−x2≤0∧0≤1→1−x2≤1
179 139 178 mpan2i ⊢1−x2∈ℝ→1−x2≤0→1−x2≤1
180 174 176 179 sylc ⊢x2∈ℂ∧1−x2∈−∞0→1−x2≤1
181 subge0 ⊢1∈ℝ∧1−x2∈ℝ→0≤1−1−x2↔1−x2≤1
182 89 174 181 sylancr ⊢x2∈ℂ∧1−x2∈−∞0→0≤1−1−x2↔1−x2≤1
183 180 182 mpbird ⊢x2∈ℂ∧1−x2∈−∞0→0≤1−1−x2
184 170 adantr ⊢x2∈ℂ∧1−x2∈−∞0→1−1−x2=x2
185 183 184 breqtrd ⊢x2∈ℂ∧1−x2∈−∞0→0≤x2
186 173 185 resqrtcld ⊢x2∈ℂ∧1−x2∈−∞0→x2∈ℝ
187 17 186 sylan ⊢x∈ℂ∧1−x2∈−∞0→x2∈ℝ
188 eleq1 ⊢x=x2→x∈ℝ↔x2∈ℝ
189 187 188 syl5ibrcom ⊢x∈ℂ∧1−x2∈−∞0→x=x2→x∈ℝ
190 187 renegcld ⊢x∈ℂ∧1−x2∈−∞0→−x2∈ℝ
191 eleq1 ⊢x=−x2→x∈ℝ↔−x2∈ℝ
192 190 191 syl5ibrcom ⊢x∈ℂ∧1−x2∈−∞0→x=−x2→x∈ℝ
193 eqid ⊢x2=x2
194 eqsqrtor ⊢x∈ℂ∧x2∈ℂ→x2=x2↔x=x2∨x=−x2
195 17 194 mpdan ⊢x∈ℂ→x2=x2↔x=x2∨x=−x2
196 193 195 mpbii ⊢x∈ℂ→x=x2∨x=−x2
197 196 adantr ⊢x∈ℂ∧1−x2∈−∞0→x=x2∨x=−x2
198 189 192 197 mpjaod ⊢x∈ℂ∧1−x2∈−∞0→x∈ℝ
199 198 stoic1a ⊢x∈ℂ∧¬x∈ℝ→¬1−x2∈−∞0
200 12 199 sylan ⊢x∈D∧¬x∈ℝ→¬1−x2∈−∞0
201 162 200 pm2.61dan ⊢x∈D→¬1−x2∈−∞0
202 111 201 eldifd ⊢x∈D→1−x2∈ℂ∖−∞0
203 202 adantl ⊢⊤∧x∈D→1−x2∈ℂ∖−∞0
204 2cnd ⊢x∈ℂ→2∈ℂ
205 id ⊢x∈ℂ→x∈ℂ
206 204 205 mulcld ⊢x∈ℂ→2⁢x∈ℂ
207 206 negcld ⊢x∈ℂ→−2⁢x∈ℂ
208 207 adantl ⊢⊤∧x∈ℂ→−2⁢x∈ℂ
209 12 208 sylan2 ⊢⊤∧x∈D→−2⁢x∈ℂ
210 59 sqrtcld ⊢y∈ℂ∖−∞0→y∈ℂ
211 210 adantl ⊢⊤∧y∈ℂ∖−∞0→y∈ℂ
212 ovexd ⊢⊤∧y∈ℂ∖−∞0→12⁢y∈V
213 19 adantl ⊢⊤∧x∈ℂ→1−x2∈ℂ
214 36 a1i ⊢⊤∧x∈ℂ→0∈ℝ
215 1cnd ⊢⊤→1∈ℂ
216 11 215 dvmptc ⊢⊤→dx∈ℂ1dℂx=x∈ℂ⟼0
217 17 adantl ⊢⊤∧x∈ℂ→x2∈ℂ
218 2cn ⊢2∈ℂ
219 mulcl ⊢2∈ℂ∧x∈ℂ→2⁢x∈ℂ
220 218 219 mpan ⊢x∈ℂ→2⁢x∈ℂ
221 220 adantl ⊢⊤∧x∈ℂ→2⁢x∈ℂ
222 2nn ⊢2∈ℕ
223 dvexp ⊢2∈ℕ→dx∈ℂx2dℂx=x∈ℂ⟼2⁢x2−1
224 222 223 ax-mp ⊢dx∈ℂx2dℂx=x∈ℂ⟼2⁢x2−1
225 2m1e1 ⊢2−1=1
226 225 oveq2i ⊢x2−1=x1
227 exp1 ⊢x∈ℂ→x1=x
228 226 227 eqtrid ⊢x∈ℂ→x2−1=x
229 228 oveq2d ⊢x∈ℂ→2⁢x2−1=2⁢x
230 229 mpteq2ia ⊢x∈ℂ⟼2⁢x2−1=x∈ℂ⟼2⁢x
231 224 230 eqtri ⊢dx∈ℂx2dℂx=x∈ℂ⟼2⁢x
232 231 a1i ⊢⊤→dx∈ℂx2dℂx=x∈ℂ⟼2⁢x
233 11 79 214 216 217 221 232 dvmptsub ⊢⊤→dx∈ℂ1−x2dℂx=x∈ℂ⟼0−2⁢x
234 df-neg ⊢−2⁢x=0−2⁢x
235 234 mpteq2i ⊢x∈ℂ⟼−2⁢x=x∈ℂ⟼0−2⁢x
236 233 235 eqtr4di ⊢⊤→dx∈ℂ1−x2dℂx=x∈ℂ⟼−2⁢x
237 11 213 208 236 81 84 82 103 dvmptres ⊢⊤→dx∈D1−x2dℂx=x∈D⟼−2⁢x
238 eqid ⊢ℂ∖−∞0=ℂ∖−∞0
239 238 dvcnsqrt ⊢dy∈ℂ∖−∞0ydℂy=y∈ℂ∖−∞0⟼12⁢y
240 239 a1i ⊢⊤→dy∈ℂ∖−∞0ydℂy=y∈ℂ∖−∞0⟼12⁢y
241 fveq2 ⊢y=1−x2→y=1−x2
242 241 oveq2d ⊢y=1−x2→2⁢y=2⁢1−x2
243 242 oveq2d ⊢y=1−x2→12⁢y=12⁢1−x2
244 11 11 203 209 211 212 237 240 241 243 dvmptco ⊢⊤→dx∈D1−x2dℂx=x∈D⟼12⁢1−x2⁢−2⁢x
245 mulneg2 ⊢2∈ℂ∧x∈ℂ→2⁢−x=−2⁢x
246 218 12 245 sylancr ⊢x∈D→2⁢−x=−2⁢x
247 246 oveq1d ⊢x∈D→2⁢−x2⁢1−x2=−2⁢x2⁢1−x2
248 12 negcld ⊢x∈D→−x∈ℂ
249 eldifn ⊢x∈ℂ∖−∞−1∪1+∞→¬x∈−∞−1∪1+∞
250 249 1 eleq2s ⊢x∈D→¬x∈−∞−1∪1+∞
251 id ⊢x=−1→x=−1
252 mnflt ⊢−1∈ℝ→−∞<−1
253 86 252 ax-mp ⊢−∞<−1
254 ubioc1 ⊢−∞∈ℝ*∧−1∈ℝ*∧−∞<−1→−1∈−∞−1
255 51 132 253 254 mp3an ⊢−1∈−∞−1
256 251 255 eqeltrdi ⊢x=−1→x∈−∞−1
257 id ⊢x=1→x=1
258 ltpnf ⊢1∈ℝ→1<+∞
259 89 258 ax-mp ⊢1<+∞
260 lbico1 ⊢1∈ℝ*∧+∞∈ℝ*∧1<+∞→1∈1+∞
261 133 121 259 260 mp3an ⊢1∈1+∞
262 257 261 eqeltrdi ⊢x=1→x∈1+∞
263 256 262 orim12i ⊢x=−1∨x=1→x∈−∞−1∨x∈1+∞
264 263 orcoms ⊢x=1∨x=−1→x∈−∞−1∨x∈1+∞
265 elun ⊢x∈−∞−1∪1+∞↔x∈−∞−1∨x∈1+∞
266 264 265 sylibr ⊢x=1∨x=−1→x∈−∞−1∪1+∞
267 250 266 nsyl ⊢x∈D→¬x=1∨x=−1
268 1cnd ⊢x∈ℂ∧1−x2=0→1∈ℂ
269 17 adantr ⊢x∈ℂ∧1−x2=0→x2∈ℂ
270 19 adantr ⊢x∈ℂ∧1−x2=0→1−x2∈ℂ
271 simpr ⊢x∈ℂ∧1−x2=0→1−x2=0
272 270 271 sqr00d ⊢x∈ℂ∧1−x2=0→1−x2=0
273 268 269 272 subeq0d ⊢x∈ℂ∧1−x2=0→1=x2
274 146 273 eqtr2id ⊢x∈ℂ∧1−x2=0→x2=12
275 274 ex ⊢x∈ℂ→1−x2=0→x2=12
276 sqeqor ⊢x∈ℂ∧1∈ℂ→x2=12↔x=1∨x=−1
277 16 276 mpan2 ⊢x∈ℂ→x2=12↔x=1∨x=−1
278 275 277 sylibd ⊢x∈ℂ→1−x2=0→x=1∨x=−1
279 278 necon3bd ⊢x∈ℂ→¬x=1∨x=−1→1−x2≠0
280 12 267 279 sylc ⊢x∈D→1−x2≠0
281 2cnne0 ⊢2∈ℂ∧2≠0
282 divcan5 ⊢−x∈ℂ∧1−x2∈ℂ∧1−x2≠0∧2∈ℂ∧2≠0→2⁢−x2⁢1−x2=−x1−x2
283 281 282 mp3an3 ⊢−x∈ℂ∧1−x2∈ℂ∧1−x2≠0→2⁢−x2⁢1−x2=−x1−x2
284 248 112 280 283 syl12anc ⊢x∈D→2⁢−x2⁢1−x2=−x1−x2
285 218 12 219 sylancr ⊢x∈D→2⁢x∈ℂ
286 285 negcld ⊢x∈D→−2⁢x∈ℂ
287 mulcl ⊢2∈ℂ∧1−x2∈ℂ→2⁢1−x2∈ℂ
288 218 112 287 sylancr ⊢x∈D→2⁢1−x2∈ℂ
289 mulne0 ⊢2∈ℂ∧2≠0∧1−x2∈ℂ∧1−x2≠0→2⁢1−x2≠0
290 281 289 mpan ⊢1−x2∈ℂ∧1−x2≠0→2⁢1−x2≠0
291 112 280 290 syl2anc ⊢x∈D→2⁢1−x2≠0
292 286 288 291 divrec2d ⊢x∈D→−2⁢x2⁢1−x2=12⁢1−x2⁢−2⁢x
293 247 284 292 3eqtr3rd ⊢x∈D→12⁢1−x2⁢−2⁢x=−x1−x2
294 293 mpteq2ia ⊢x∈D⟼12⁢1−x2⁢−2⁢x=x∈D⟼−x1−x2
295 244 294 eqtrdi ⊢⊤→dx∈D1−x2dℂx=x∈D⟼−x1−x2
296 11 74 75 109 113 114 295 dvmptadd ⊢⊤→dx∈Di⁢x+1−x2dℂx=x∈D⟼i+−x1−x2
297 mulcl ⊢i∈ℂ∧1−x2∈ℂ→i⁢1−x2∈ℂ
298 13 20 297 sylancr ⊢x∈ℂ→i⁢1−x2∈ℂ
299 12 298 syl ⊢x∈D→i⁢1−x2∈ℂ
300 299 248 112 280 divdird ⊢x∈D→i⁢1−x2+−x1−x2=i⁢1−x21−x2+−x1−x2
301 ixi ⊢i⁢i=−1
302 301 eqcomi ⊢−1=i⁢i
303 302 oveq1i ⊢-1⁢x=i⁢i⁢x
304 mulm1 ⊢x∈ℂ→-1⁢x=−x
305 mulass ⊢i∈ℂ∧i∈ℂ∧x∈ℂ→i⁢i⁢x=i⁢i⁢x
306 13 13 305 mp3an12 ⊢x∈ℂ→i⁢i⁢x=i⁢i⁢x
307 303 304 306 3eqtr3a ⊢x∈ℂ→−x=i⁢i⁢x
308 307 oveq1d ⊢x∈ℂ→-x+i⁢1−x2=i⁢i⁢x+i⁢1−x2
309 negcl ⊢x∈ℂ→−x∈ℂ
310 298 309 addcomd ⊢x∈ℂ→i⁢1−x2+−x=-x+i⁢1−x2
311 13 a1i ⊢x∈ℂ→i∈ℂ
312 311 15 20 adddid ⊢x∈ℂ→i⁢i⁢x+1−x2=i⁢i⁢x+i⁢1−x2
313 308 310 312 3eqtr4d ⊢x∈ℂ→i⁢1−x2+−x=i⁢i⁢x+1−x2
314 12 313 syl ⊢x∈D→i⁢1−x2+−x=i⁢i⁢x+1−x2
315 314 oveq1d ⊢x∈D→i⁢1−x2+−x1−x2=i⁢i⁢x+1−x21−x2
316 72 112 280 divcan4d ⊢x∈D→i⁢1−x21−x2=i
317 316 oveq1d ⊢x∈D→i⁢1−x21−x2+−x1−x2=i+−x1−x2
318 300 315 317 3eqtr3rd ⊢x∈D→i+−x1−x2=i⁢i⁢x+1−x21−x2
319 318 mpteq2ia ⊢x∈D⟼i+−x1−x2=x∈D⟼i⁢i⁢x+1−x21−x2
320 296 319 eqtrdi ⊢⊤→dx∈Di⁢x+1−x2dℂx=x∈D⟼i⁢i⁢x+1−x21−x2
321 logf1o ⊢log:ℂ∖0⟶1-1 ontoran⁡log
322 f1of ⊢log:ℂ∖0⟶1-1 ontoran⁡log→log:ℂ∖0⟶ran⁡log
323 321 322 mp1i ⊢⊤→log:ℂ∖0⟶ran⁡log
324 snssi ⊢0∈−∞0→0⊆−∞0
325 64 324 ax-mp ⊢0⊆−∞0
326 sscon ⊢0⊆−∞0→ℂ∖−∞0⊆ℂ∖0
327 325 326 mp1i ⊢⊤→ℂ∖−∞0⊆ℂ∖0
328 323 327 feqresmpt ⊢⊤→log↾ℂ∖−∞0=y∈ℂ∖−∞0⟼log⁡y
329 328 oveq2d ⊢⊤→ℂDlog↾ℂ∖−∞0=dy∈ℂ∖−∞0log⁡ydℂy
330 238 dvlog ⊢ℂDlog↾ℂ∖−∞0=y∈ℂ∖−∞0⟼1y
331 329 330 eqtr3di ⊢⊤→dy∈ℂ∖−∞0log⁡ydℂy=y∈ℂ∖−∞0⟼1y
332 fveq2 ⊢y=i⁢x+1−x2→log⁡y=log⁡i⁢x+1−x2
333 oveq2 ⊢y=i⁢x+1−x2→1y=1i⁢x+1−x2
334 11 11 57 58 70 71 320 331 332 333 dvmptco ⊢⊤→dx∈Dlog⁡i⁢x+1−x2dℂx=x∈D⟼1i⁢x+1−x2⁢i⁢i⁢x+1−x21−x2
335 22 24 reccld ⊢x∈D→1i⁢x+1−x2∈ℂ
336 mulcl ⊢i∈ℂ∧i⁢x+1−x2∈ℂ→i⁢i⁢x+1−x2∈ℂ
337 13 21 336 sylancr ⊢x∈ℂ→i⁢i⁢x+1−x2∈ℂ
338 12 337 syl ⊢x∈D→i⁢i⁢x+1−x2∈ℂ
339 335 338 112 280 divassd ⊢x∈D→1i⁢x+1−x2⁢i⁢i⁢x+1−x21−x2=1i⁢x+1−x2⁢i⁢i⁢x+1−x21−x2
340 338 22 24 divrec2d ⊢x∈D→i⁢i⁢x+1−x2i⁢x+1−x2=1i⁢x+1−x2⁢i⁢i⁢x+1−x2
341 72 22 24 divcan4d ⊢x∈D→i⁢i⁢x+1−x2i⁢x+1−x2=i
342 340 341 eqtr3d ⊢x∈D→1i⁢x+1−x2⁢i⁢i⁢x+1−x2=i
343 342 oveq1d ⊢x∈D→1i⁢x+1−x2⁢i⁢i⁢x+1−x21−x2=i1−x2
344 339 343 eqtr3d ⊢x∈D→1i⁢x+1−x2⁢i⁢i⁢x+1−x21−x2=i1−x2
345 344 mpteq2ia ⊢x∈D⟼1i⁢x+1−x2⁢i⁢i⁢x+1−x21−x2=x∈D⟼i1−x2
346 334 345 eqtrdi ⊢⊤→dx∈Dlog⁡i⁢x+1−x2dℂx=x∈D⟼i1−x2
347 negicn ⊢−i∈ℂ
348 347 a1i ⊢⊤→−i∈ℂ
349 11 26 27 346 348 dvmptcmul ⊢⊤→dx∈D−i⁢log⁡i⁢x+1−x2dℂx=x∈D⟼−i⁢i1−x2
350 349 mptru ⊢dx∈D−i⁢log⁡i⁢x+1−x2dℂx=x∈D⟼−i⁢i1−x2
351 divass ⊢−i∈ℂ∧i∈ℂ∧1−x2∈ℂ∧1−x2≠0→−i⁢i1−x2=−i⁢i1−x2
352 347 13 351 mp3an12 ⊢1−x2∈ℂ∧1−x2≠0→−i⁢i1−x2=−i⁢i1−x2
353 112 280 352 syl2anc ⊢x∈D→−i⁢i1−x2=−i⁢i1−x2
354 13 13 mulneg1i ⊢−i⁢i=−i⁢i
355 301 negeqi ⊢−i⁢i=−-1
356 negneg1e1 ⊢−-1=1
357 354 355 356 3eqtri ⊢−i⁢i=1
358 357 oveq1i ⊢−i⁢i1−x2=11−x2
359 353 358 eqtr3di ⊢x∈D→−i⁢i1−x2=11−x2
360 359 mpteq2ia ⊢x∈D⟼−i⁢i1−x2=x∈D⟼11−x2
361 9 350 360 3eqtri ⊢ℂDarcsin↾D=x∈D⟼11−x2