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=\left(x\in ℂ⟼\left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(x\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cacos	$$classarccos$$
1		vx	$$setvarx$$
2		cc	$$classℂ$$
3		cpi	$$class\mathrm{\pi }$$
4		cdiv	$$class÷$$
5		c2	$$class2$$
6	3 5 4	co	$$class\left(\frac{\mathrm{\pi }}{2}\right)$$
7		cmin	$$class-$$
8		casin	$$classarcsin$$
9	1	cv	$$setvarx$$
10	9 8	cfv	$$classarcsin\left(x\right)$$
11	6 10 7	co	$$class\left(\left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(x\right)\right)$$
12	1 2 11	cmpt	$$class\left(x\in ℂ⟼\left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(x\right)\right)$$
13	0 12	wceq	$$wffarccos=\left(x\in ℂ⟼\left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(x\right)\right)$$