Database
BASIC REAL AND COMPLEX FUNCTIONS
Basic trigonometry
Inverse trigonometric functions
asinf
Next ⟩
asincl
Metamath Proof Explorer
Ascii
Unicode
Theorem
asinf
Description:
Domain and range of the arcsin function.
(Contributed by
Mario Carneiro
, 31-Mar-2015)
Ref
Expression
Assertion
asinf
⊢
arcsin
:
ℂ
⟶
ℂ
Proof
Step
Hyp
Ref
Expression
1
df-asin
⊢
arcsin
=
x
∈
ℂ
⟼
−
i
⁢
log
⁡
i
⁢
x
+
1
−
x
2
2
negicn
⊢
−
i
∈
ℂ
3
ax-icn
⊢
i
∈
ℂ
4
mulcl
⊢
i
∈
ℂ
∧
x
∈
ℂ
→
i
⁢
x
∈
ℂ
5
3
4
mpan
⊢
x
∈
ℂ
→
i
⁢
x
∈
ℂ
6
ax-1cn
⊢
1
∈
ℂ
7
sqcl
⊢
x
∈
ℂ
→
x
2
∈
ℂ
8
subcl
⊢
1
∈
ℂ
∧
x
2
∈
ℂ
→
1
−
x
2
∈
ℂ
9
6
7
8
sylancr
⊢
x
∈
ℂ
→
1
−
x
2
∈
ℂ
10
9
sqrtcld
⊢
x
∈
ℂ
→
1
−
x
2
∈
ℂ
11
5
10
addcld
⊢
x
∈
ℂ
→
i
⁢
x
+
1
−
x
2
∈
ℂ
12
asinlem
⊢
x
∈
ℂ
→
i
⁢
x
+
1
−
x
2
≠
0
13
11
12
logcld
⊢
x
∈
ℂ
→
log
⁡
i
⁢
x
+
1
−
x
2
∈
ℂ
14
mulcl
⊢
−
i
∈
ℂ
∧
log
⁡
i
⁢
x
+
1
−
x
2
∈
ℂ
→
−
i
⁢
log
⁡
i
⁢
x
+
1
−
x
2
∈
ℂ
15
2
13
14
sylancr
⊢
x
∈
ℂ
→
−
i
⁢
log
⁡
i
⁢
x
+
1
−
x
2
∈
ℂ
16
1
15
fmpti
⊢
arcsin
:
ℂ
⟶
ℂ