This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = x ∈ ℂ ⟼ − i ⁢ log ⁡ i ⁢ x + 1 − x 2

Detailed syntax breakdown

Step Hyp Ref Expression
0 casin class arcsin
1 vx setvar x
2 cc class ℂ
3 ci class i
4 3 cneg class − i
5 cmul class ×
6 clog class log
7 1 cv setvar x
8 3 7 5 co class i ⁢ x
9 caddc class +
10 csqrt class √
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 1 − x 2
17 16 10 cfv class 1 − x 2
18 8 17 9 co class i ⁢ x + 1 − x 2
19 18 6 cfv class log ⁡ i ⁢ x + 1 − x 2
20 4 19 5 co class − i ⁢ log ⁡ i ⁢ x + 1 − x 2
21 1 2 20 cmpt class x ∈ ℂ ⟼ − i ⁢ log ⁡ i ⁢ x + 1 − x 2
22 0 21 wceq wff arcsin = x ∈ ℂ ⟼ − i ⁢ log ⁡ i ⁢ x + 1 − x 2