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 ( 𝐴 ∈ ℂ → ( cos ‘ ( arccos ‘ 𝐴 ) ) = 𝐴 )

Proof

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