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

Definition df-asin 22258
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 22255 . 2  class arcsin
2 vx . . 3  setvar  x
3 cc 9278 . . 3  class  CC
4 ci 9282 . . . . 5  class  _i
54cneg 9594 . . . 4  class  -u _i
62cv 1368 . . . . . . 7  class  x
7 cmul 9285 . . . . . . 7  class  x.
84, 6, 7co 6089 . . . . . 6  class  ( _i  x.  x )
9 c1 9281 . . . . . . . 8  class  1
10 c2 10369 . . . . . . . . 9  class  2
11 cexp 11863 . . . . . . . . 9  class  ^
126, 10, 11co 6089 . . . . . . . 8  class  ( x ^ 2 )
13 cmin 9593 . . . . . . . 8  class  -
149, 12, 13co 6089 . . . . . . 7  class  ( 1  -  ( x ^
2 ) )
15 csqr 12720 . . . . . . 7  class  sqr
1614, 15cfv 5416 . . . . . 6  class  ( sqr `  ( 1  -  (
x ^ 2 ) ) )
17 caddc 9283 . . . . . 6  class  +
188, 16, 17co 6089 . . . . 5  class  ( ( _i  x.  x )  +  ( sqr `  (
1  -  ( x ^ 2 ) ) ) )
19 clog 22004 . . . . 5  class  log
2018, 19cfv 5416 . . . 4  class  ( log `  ( ( _i  x.  x )  +  ( sqr `  ( 1  -  ( x ^
2 ) ) ) ) )
215, 20, 7co 6089 . . 3  class  ( -u _i  x.  ( log `  (
( _i  x.  x
)  +  ( sqr `  ( 1  -  (
x ^ 2 ) ) ) ) ) )
222, 3, 21cmpt 4348 . 2  class  ( x  e.  CC  |->  ( -u _i  x.  ( log `  (
( _i  x.  x
)  +  ( sqr `  ( 1  -  (
x ^ 2 ) ) ) ) ) ) )
231, 22wceq 1369 1  wff arcsin  =  ( x  e.  CC  |->  (
-u _i  x.  ( log `  ( ( _i  x.  x )  +  ( sqr `  (
1  -  ( x ^ 2 ) ) ) ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  asinf  22265  asinval  22275  dvasin  28477
  Copyright terms: Public domain W3C validator