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 = ( 𝑥 ∈ ℂ ↦ ( ( π / 2 ) − ( arcsin ‘ 𝑥 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cacos	⊢ arccos
1		vx	⊢ 𝑥
2		cc	⊢ ℂ
3		cpi	⊢ π
4		cdiv	⊢ /
5		c2	⊢ 2
6	3 5 4	co	⊢ ( π / 2 )
7		cmin	⊢ −
8		casin	⊢ arcsin
9	1	cv	⊢ 𝑥
10	9 8	cfv	⊢ ( arcsin ‘ 𝑥 )
11	6 10 7	co	⊢ ( ( π / 2 ) − ( arcsin ‘ 𝑥 ) )
12	1 2 11	cmpt	⊢ ( 𝑥 ∈ ℂ ↦ ( ( π / 2 ) − ( arcsin ‘ 𝑥 ) ) )
13	0 12	wceq	⊢ arccos = ( 𝑥 ∈ ℂ ↦ ( ( π / 2 ) − ( arcsin ‘ 𝑥 ) ) )