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

Definition df-acos 20711
 Description: Define the arccosine function. See also remarks for df-asin 20710. Since we define arccos in terms of arcsin, it shares the same branch points and cuts, namely . (Contributed by Mario Carneiro, 31-Mar-2015.)
Assertion
Ref Expression
df-acos arccos arcsin

Detailed syntax breakdown of Definition df-acos
StepHypRef Expression
1 cacos 20708 . 2 arccos
2 vx . . 3
3 cc 8993 . . 3
4 cpi 12674 . . . . 5
5 c2 10054 . . . . 5
6 cdiv 9682 . . . . 5
74, 5, 6co 6084 . . . 4
82cv 1652 . . . . 5
9 casin 20707 . . . . 5 arcsin
108, 9cfv 5457 . . . 4 arcsin
11 cmin 9296 . . . 4
127, 10, 11co 6084 . . 3 arcsin
132, 3, 12cmpt 4269 . 2 arcsin
141, 13wceq 1653 1 arccos arcsin
 Colors of variables: wff set class This definition is referenced by:  acosf  20719  acosval  20728
 Copyright terms: Public domain W3C validator