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

Definition df-asin 20710
 Description: Define the arcsine function. Because is not a one-to-one function, the literal inverse is not a function. Rather than attempt to find the right domain on which to restrict in order to get a total function, we just define it in terms of , which we already know is total (except at ). There are branch points at and (at which the function is defined), and branch cuts along the real line not between and , which is to say . (Contributed by Mario Carneiro, 31-Mar-2015.)
Assertion
Ref Expression
df-asin arcsin

Detailed syntax breakdown of Definition df-asin
StepHypRef Expression
1 casin 20707 . 2 arcsin
2 vx . . 3
3 cc 8993 . . 3
4 ci 8997 . . . . 5
54cneg 9297 . . . 4
62cv 1652 . . . . . . 7
7 cmul 9000 . . . . . . 7
84, 6, 7co 6084 . . . . . 6
9 c1 8996 . . . . . . . 8
10 c2 10054 . . . . . . . . 9
11 cexp 11387 . . . . . . . . 9
126, 10, 11co 6084 . . . . . . . 8
13 cmin 9296 . . . . . . . 8
149, 12, 13co 6084 . . . . . . 7
15 csqr 12043 . . . . . . 7
1614, 15cfv 5457 . . . . . 6
17 caddc 8998 . . . . . 6
188, 16, 17co 6084 . . . . 5
19 clog 20457 . . . . 5
2018, 19cfv 5457 . . . 4
215, 20, 7co 6084 . . 3
222, 3, 21cmpt 4269 . 2
231, 22wceq 1653 1 arcsin
 Colors of variables: wff set class This definition is referenced by:  asinf  20717  asinval  20727
 Copyright terms: Public domain W3C validator