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

Definition df-acos 20178
Description: Define the arccosine function. See also remarks for df-asin 20177. 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 20175 . 2  class arccos
2 vx . . 3  set  x
3 cc 8751 . . 3  class  CC
4 cpi 12364 . . . . 5  class  pi
5 c2 9811 . . . . 5  class  2
6 cdiv 9439 . . . . 5  class  /
74, 5, 6co 5874 . . . 4  class  ( pi 
/  2 )
82cv 1631 . . . . 5  class  x
9 casin 20174 . . . . 5  class arcsin
108, 9cfv 5271 . . . 4  class  (arcsin `  x )
11 cmin 9053 . . . 4  class  -
127, 10, 11co 5874 . . 3  class  ( ( pi  /  2 )  -  (arcsin `  x
) )
132, 3, 12cmpt 4093 . 2  class  ( x  e.  CC  |->  ( ( pi  /  2 )  -  (arcsin `  x
) ) )
141, 13wceq 1632 1  wff arccos  =  ( x  e.  CC  |->  ( ( pi  /  2
)  -  (arcsin `  x ) ) )
Colors of variables: wff set class
This definition is referenced by:  acosf  20186  acosval  20195
  Copyright terms: Public domain W3C validator