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