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 \in ℂ ⟼ (\frac{π}{2}) - arcsin (x))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cacos	$class arccos$
1		vx	$setvar x$
2		cc	$class ℂ$
3		cpi	$class π$
4		cdiv	$class \div$
5		c2	$class 2$
6	3 5 4	co	$class (\frac{π}{2})$
7		cmin	$class -$
8		casin	$class arcsin$
9	1	cv	$setvar x$
10	9 8	cfv	$class arcsin (x)$
11	6 10 7	co	$class ((\frac{π}{2}) - arcsin (x))$
12	1 2 11	cmpt	$class (x \in ℂ ⟼ (\frac{π}{2}) - arcsin (x))$
13	0 12	wceq	$wff arccos = (x \in ℂ ⟼ (\frac{π}{2}) - arcsin (x))$