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 ‘ 𝐴 ) ) = 𝐴 )