This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-acos

Description: Define the arccosine function. See also remarks for df-asin . 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)

Ref Expression
Assertion df-acos 
|- arccos = ( x e. CC |-> ( ( _pi / 2 ) - ( arcsin ` x ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cacos 
 |-  arccos
1 vx 
 |-  x
2 cc 
 |-  CC
3 cpi 
 |-  _pi
4 cdiv 
 |-  /
5 c2 
 |-  2
6 3 5 4 co 
 |-  ( _pi / 2 )
7 cmin 
 |-  -
8 casin 
 |-  arcsin
9 1 cv 
 |-  x
10 9 8 cfv 
 |-  ( arcsin ` x )
11 6 10 7 co 
 |-  ( ( _pi / 2 ) - ( arcsin ` x ) )
12 1 2 11 cmpt 
 |-  ( x e. CC |-> ( ( _pi / 2 ) - ( arcsin ` x ) ) )
13 0 12 wceq 
 |-  arccos = ( x e. CC |-> ( ( _pi / 2 ) - ( arcsin ` x ) ) )