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

Definition df-acos 23394
Description: Define the arccosine function. See also remarks for df-asin 23393. Since we define arccos in terms of arcsin, it shares the same branch points and cuts, namely  ( -oo ,  -u
1 )  u.  (
1 , +oo ). (Contributed by Mario Carneiro, 31-Mar-2015.)
Assertion
Ref Expression
df-acos  |- arccos  =  ( x  e.  CC  |->  ( ( pi  /  2
)  -  (arcsin `  x ) ) )

Detailed syntax breakdown of Definition df-acos
StepHypRef Expression
1 cacos 23391 . 2  class arccos
2 vx . . 3  setvar  x
3 cc 9479 . . 3  class  CC
4 cpi 13884 . . . . 5  class  pi
5 c2 10581 . . . . 5  class  2
6 cdiv 10202 . . . . 5  class  /
74, 5, 6co 6270 . . . 4  class  ( pi 
/  2 )
82cv 1397 . . . . 5  class  x
9 casin 23390 . . . . 5  class arcsin
108, 9cfv 5570 . . . 4  class  (arcsin `  x )
11 cmin 9796 . . . 4  class  -
127, 10, 11co 6270 . . 3  class  ( ( pi  /  2 )  -  (arcsin `  x
) )
132, 3, 12cmpt 4497 . 2  class  ( x  e.  CC  |->  ( ( pi  /  2 )  -  (arcsin `  x
) ) )
141, 13wceq 1398 1  wff arccos  =  ( x  e.  CC  |->  ( ( pi  /  2
)  -  (arcsin `  x ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  acosf  23402  acosval  23411  dvacos  30344
  Copyright terms: Public domain W3C validator