This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cosacos

Description: The arccosine function is an inverse to cos . (Contributed by Mario Carneiro, 1-Apr-2015)

Ref Expression
Assertion cosacos ⊢ A ∈ ℂ → cos ⁡ arccos ⁡ A = A

Proof

Step Hyp Ref Expression
1 acosval ⊢ A ∈ ℂ → arccos ⁡ A = π 2 − arcsin ⁡ A
2 1 fveq2d ⊢ A ∈ ℂ → cos ⁡ arccos ⁡ A = cos ⁡ π 2 − arcsin ⁡ A
3 asincl ⊢ A ∈ ℂ → arcsin ⁡ A ∈ ℂ
4 coshalfpim ⊢ arcsin ⁡ A ∈ ℂ → cos ⁡ π 2 − arcsin ⁡ A = sin ⁡ arcsin ⁡ A
5 3 4 syl ⊢ A ∈ ℂ → cos ⁡ π 2 − arcsin ⁡ A = sin ⁡ arcsin ⁡ A
6 sinasin ⊢ A ∈ ℂ → sin ⁡ arcsin ⁡ A = A
7 2 5 6 3eqtrd ⊢ A ∈ ℂ → cos ⁡ arccos ⁡ A = A