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 e. CC -> ( cos ` ( arccos ` A ) ) = A )

Proof

Step Hyp Ref Expression
1 acosval 
 |-  ( A e. CC -> ( arccos ` A ) = ( ( _pi / 2 ) - ( arcsin ` A ) ) )
2 1 fveq2d 
 |-  ( A e. CC -> ( cos ` ( arccos ` A ) ) = ( cos ` ( ( _pi / 2 ) - ( arcsin ` A ) ) ) )
3 asincl 
 |-  ( A e. CC -> ( arcsin ` A ) e. CC )
4 coshalfpim 
 |-  ( ( arcsin ` A ) e. CC -> ( cos ` ( ( _pi / 2 ) - ( arcsin ` A ) ) ) = ( sin ` ( arcsin ` A ) ) )
5 3 4 syl 
 |-  ( A e. CC -> ( cos ` ( ( _pi / 2 ) - ( arcsin ` A ) ) ) = ( sin ` ( arcsin ` A ) ) )
6 sinasin 
 |-  ( A e. CC -> ( sin ` ( arcsin ` A ) ) = A )
7 2 5 6 3eqtrd 
 |-  ( A e. CC -> ( cos ` ( arccos ` A ) ) = A )