# Metamath Proof Explorer

## Definition df-asin

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 -u 1 and 1 (at which the function is defined), and branch cuts along the real line not between -u 1 and 1 , which is to say ( -oo , -u 1 ) u. ( 1 , +oo )  . (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion df-asin ${⊢}arcsin=\left({x}\in ℂ⟼\left(-\mathrm{i}\right)\mathrm{log}\left(\mathrm{i}{x}+\sqrt{1-{{x}}^{2}}\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 casin ${class}arcsin$
1 vx ${setvar}{x}$
2 cc ${class}ℂ$
3 ci ${class}\mathrm{i}$
4 3 cneg ${class}\left(-\mathrm{i}\right)$
5 cmul ${class}×$
6 clog ${class}log$
7 1 cv ${setvar}{x}$
8 3 7 5 co ${class}\mathrm{i}{x}$
9 caddc ${class}+$
10 csqrt ${class}\surd$
11 c1 ${class}1$
12 cmin ${class}-$
13 cexp ${class}^$
14 c2 ${class}2$
15 7 14 13 co ${class}{{x}}^{2}$
16 11 15 12 co ${class}\left(1-{{x}}^{2}\right)$
17 16 10 cfv ${class}\sqrt{1-{{x}}^{2}}$
18 8 17 9 co ${class}\left(\mathrm{i}{x}+\sqrt{1-{{x}}^{2}}\right)$
19 18 6 cfv ${class}\mathrm{log}\left(\mathrm{i}{x}+\sqrt{1-{{x}}^{2}}\right)$
20 4 19 5 co ${class}\left(-\mathrm{i}\right)\mathrm{log}\left(\mathrm{i}{x}+\sqrt{1-{{x}}^{2}}\right)$
21 1 2 20 cmpt ${class}\left({x}\in ℂ⟼\left(-\mathrm{i}\right)\mathrm{log}\left(\mathrm{i}{x}+\sqrt{1-{{x}}^{2}}\right)\right)$
22 0 21 wceq ${wff}arcsin=\left({x}\in ℂ⟼\left(-\mathrm{i}\right)\mathrm{log}\left(\mathrm{i}{x}+\sqrt{1-{{x}}^{2}}\right)\right)$