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