 Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-asin Structured version   Visualization version   GIF version

Definition df-asin 25043
 Description: Define the arcsine function. Because sin is not a one-to-one function, the literal inverse ◡sin is not a function. Rather than attempt to find the right domain on which to restrict sin in order to get a total function, we just define it in terms of log, which we already know is total (except at 0). There are branch points at -1 and 1 (at which the function is defined), and branch cuts along the real line not between -1 and 1, which is to say (-∞, -1) ∪ (1, +∞). (Contributed by Mario Carneiro, 31-Mar-2015.)
Assertion
Ref Expression
df-asin arcsin = (𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))

Detailed syntax breakdown of Definition df-asin
StepHypRef Expression
1 casin 25040 . 2 class arcsin
2 vx . . 3 setvar 𝑥
3 cc 10270 . . 3 class
4 ci 10274 . . . . 5 class i
54cneg 10607 . . . 4 class -i
62cv 1600 . . . . . . 7 class 𝑥
7 cmul 10277 . . . . . . 7 class ·
84, 6, 7co 6922 . . . . . 6 class (i · 𝑥)
9 c1 10273 . . . . . . . 8 class 1
10 c2 11430 . . . . . . . . 9 class 2
11 cexp 13178 . . . . . . . . 9 class
126, 10, 11co 6922 . . . . . . . 8 class (𝑥↑2)
13 cmin 10606 . . . . . . . 8 class
149, 12, 13co 6922 . . . . . . 7 class (1 − (𝑥↑2))
15 csqrt 14380 . . . . . . 7 class
1614, 15cfv 6135 . . . . . 6 class (√‘(1 − (𝑥↑2)))
17 caddc 10275 . . . . . 6 class +
188, 16, 17co 6922 . . . . 5 class ((i · 𝑥) + (√‘(1 − (𝑥↑2))))
19 clog 24738 . . . . 5 class log
2018, 19cfv 6135 . . . 4 class (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
215, 20, 7co 6922 . . 3 class (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
222, 3, 21cmpt 4965 . 2 class (𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
231, 22wceq 1601 1 wff arcsin = (𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
 Colors of variables: wff setvar class This definition is referenced by:  asinf  25050  asinval  25060  dvasin  34105
 Copyright terms: Public domain W3C validator