Metamath Proof Explorer

Theorem sinacos

Description: The sine of the arccosine of A is sqrt ( 1 - A ^ 2 ) . (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Assertion sinacos 
|- ( A e. CC -> ( sin ` ( arccos ` A ) ) = ( sqrt ` ( 1 - ( A ^ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 acosval 
 |-  ( A e. CC -> ( arccos ` A ) = ( ( _pi / 2 ) - ( arcsin ` A ) ) )
2 1 oveq2d 
 |-  ( A e. CC -> ( ( _pi / 2 ) - ( arccos ` A ) ) = ( ( _pi / 2 ) - ( ( _pi / 2 ) - ( arcsin ` A ) ) ) )
3 picn 
 |-  _pi e. CC
4 halfcl 
 |-  ( _pi e. CC -> ( _pi / 2 ) e. CC )
5 3 4 ax-mp 
 |-  ( _pi / 2 ) e. CC
6 asincl 
 |-  ( A e. CC -> ( arcsin ` A ) e. CC )
7 nncan 
 |-  ( ( ( _pi / 2 ) e. CC /\ ( arcsin ` A ) e. CC ) -> ( ( _pi / 2 ) - ( ( _pi / 2 ) - ( arcsin ` A ) ) ) = ( arcsin ` A ) )
8 5 6 7 sylancr 
 |-  ( A e. CC -> ( ( _pi / 2 ) - ( ( _pi / 2 ) - ( arcsin ` A ) ) ) = ( arcsin ` A ) )
9 2 8 eqtrd 
 |-  ( A e. CC -> ( ( _pi / 2 ) - ( arccos ` A ) ) = ( arcsin ` A ) )
10 9 fveq2d 
 |-  ( A e. CC -> ( cos ` ( ( _pi / 2 ) - ( arccos ` A ) ) ) = ( cos ` ( arcsin ` A ) ) )
11 acoscl 
 |-  ( A e. CC -> ( arccos ` A ) e. CC )
12 coshalfpim 
 |-  ( ( arccos ` A ) e. CC -> ( cos ` ( ( _pi / 2 ) - ( arccos ` A ) ) ) = ( sin ` ( arccos ` A ) ) )
13 11 12 syl 
 |-  ( A e. CC -> ( cos ` ( ( _pi / 2 ) - ( arccos ` A ) ) ) = ( sin ` ( arccos ` A ) ) )
14 cosasin 
 |-  ( A e. CC -> ( cos ` ( arcsin ` A ) ) = ( sqrt ` ( 1 - ( A ^ 2 ) ) ) )
15 10 13 14 3eqtr3d 
 |-  ( A e. CC -> ( sin ` ( arccos ` A ) ) = ( sqrt ` ( 1 - ( A ^ 2 ) ) ) )