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

Definition df-asin 20161
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.)
Assertion
Ref Expression
df-asin  |- arcsin  =  ( x  e.  CC  |->  (
-u _i  x.  ( log `  ( ( _i  x.  x )  +  ( sqr `  (
1  -  ( x ^ 2 ) ) ) ) ) ) )

Detailed syntax breakdown of Definition df-asin
StepHypRef Expression
1 casin 20158 . 2  class arcsin
2 vx . . 3  set  x
3 cc 8735 . . 3  class  CC
4 ci 8739 . . . . 5  class  _i
54cneg 9038 . . . 4  class  -u _i
62cv 1622 . . . . . . 7  class  x
7 cmul 8742 . . . . . . 7  class  x.
84, 6, 7co 5858 . . . . . 6  class  ( _i  x.  x )
9 c1 8738 . . . . . . . 8  class  1
10 c2 9795 . . . . . . . . 9  class  2
11 cexp 11104 . . . . . . . . 9  class  ^
126, 10, 11co 5858 . . . . . . . 8  class  ( x ^ 2 )
13 cmin 9037 . . . . . . . 8  class  -
149, 12, 13co 5858 . . . . . . 7  class  ( 1  -  ( x ^
2 ) )
15 csqr 11718 . . . . . . 7  class  sqr
1614, 15cfv 5255 . . . . . 6  class  ( sqr `  ( 1  -  (
x ^ 2 ) ) )
17 caddc 8740 . . . . . 6  class  +
188, 16, 17co 5858 . . . . 5  class  ( ( _i  x.  x )  +  ( sqr `  (
1  -  ( x ^ 2 ) ) ) )
19 clog 19912 . . . . 5  class  log
2018, 19cfv 5255 . . . 4  class  ( log `  ( ( _i  x.  x )  +  ( sqr `  ( 1  -  ( x ^
2 ) ) ) ) )
215, 20, 7co 5858 . . 3  class  ( -u _i  x.  ( log `  (
( _i  x.  x
)  +  ( sqr `  ( 1  -  (
x ^ 2 ) ) ) ) ) )
222, 3, 21cmpt 4077 . 2  class  ( x  e.  CC  |->  ( -u _i  x.  ( log `  (
( _i  x.  x
)  +  ( sqr `  ( 1  -  (
x ^ 2 ) ) ) ) ) ) )
231, 22wceq 1623 1  wff arcsin  =  ( x  e.  CC  |->  (
-u _i  x.  ( log `  ( ( _i  x.  x )  +  ( sqr `  (
1  -  ( x ^ 2 ) ) ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  asinf  20168  asinval  20178
  Copyright terms: Public domain W3C validator