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 ) ) )