Metamath Proof Explorer

Theorem cosasin

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

Ref Expression
Assertion cosasin 
|- ( A e. CC -> ( cos ` ( arcsin ` A ) ) = ( sqrt ` ( 1 - ( A ^ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 asincl 
 |-  ( A e. CC -> ( arcsin ` A ) e. CC )
2 cosval 
 |-  ( ( arcsin ` A ) e. CC -> ( cos ` ( arcsin ` A ) ) = ( ( ( exp ` ( _i x. ( arcsin ` A ) ) ) + ( exp ` ( -u _i x. ( arcsin ` A ) ) ) ) / 2 ) )
3 1 2 syl 
 |-  ( A e. CC -> ( cos ` ( arcsin ` A ) ) = ( ( ( exp ` ( _i x. ( arcsin ` A ) ) ) + ( exp ` ( -u _i x. ( arcsin ` A ) ) ) ) / 2 ) )
4 ax-1cn 
 |-  1 e. CC
5 sqcl 
 |-  ( A e. CC -> ( A ^ 2 ) e. CC )
6 subcl 
 |-  ( ( 1 e. CC /\ ( A ^ 2 ) e. CC ) -> ( 1 - ( A ^ 2 ) ) e. CC )
7 4 5 6 sylancr 
 |-  ( A e. CC -> ( 1 - ( A ^ 2 ) ) e. CC )
8 7 sqrtcld 
 |-  ( A e. CC -> ( sqrt ` ( 1 - ( A ^ 2 ) ) ) e. CC )
9 ax-icn 
 |-  _i e. CC
10 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
11 9 10 mpan 
 |-  ( A e. CC -> ( _i x. A ) e. CC )
12 8 11 8 ppncand 
 |-  ( A e. CC -> ( ( ( sqrt ` ( 1 - ( A ^ 2 ) ) ) + ( _i x. A ) ) + ( ( sqrt ` ( 1 - ( A ^ 2 ) ) ) - ( _i x. A ) ) ) = ( ( sqrt ` ( 1 - ( A ^ 2 ) ) ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) )
13 efiasin 
 |-  ( A e. CC -> ( exp ` ( _i x. ( arcsin ` A ) ) ) = ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) )
14 11 8 13 comraddd 
 |-  ( A e. CC -> ( exp ` ( _i x. ( arcsin ` A ) ) ) = ( ( sqrt ` ( 1 - ( A ^ 2 ) ) ) + ( _i x. A ) ) )
15 mulneg12 
 |-  ( ( _i e. CC /\ ( arcsin ` A ) e. CC ) -> ( -u _i x. ( arcsin ` A ) ) = ( _i x. -u ( arcsin ` A ) ) )
16 9 1 15 sylancr 
 |-  ( A e. CC -> ( -u _i x. ( arcsin ` A ) ) = ( _i x. -u ( arcsin ` A ) ) )
17 asinneg 
 |-  ( A e. CC -> ( arcsin ` -u A ) = -u ( arcsin ` A ) )
18 17 oveq2d 
 |-  ( A e. CC -> ( _i x. ( arcsin ` -u A ) ) = ( _i x. -u ( arcsin ` A ) ) )
19 16 18 eqtr4d 
 |-  ( A e. CC -> ( -u _i x. ( arcsin ` A ) ) = ( _i x. ( arcsin ` -u A ) ) )
20 19 fveq2d 
 |-  ( A e. CC -> ( exp ` ( -u _i x. ( arcsin ` A ) ) ) = ( exp ` ( _i x. ( arcsin ` -u A ) ) ) )
21 negcl 
 |-  ( A e. CC -> -u A e. CC )
22 efiasin 
 |-  ( -u A e. CC -> ( exp ` ( _i x. ( arcsin ` -u A ) ) ) = ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) )
23 21 22 syl 
 |-  ( A e. CC -> ( exp ` ( _i x. ( arcsin ` -u A ) ) ) = ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) )
24 mulneg2 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. -u A ) = -u ( _i x. A ) )
25 9 24 mpan 
 |-  ( A e. CC -> ( _i x. -u A ) = -u ( _i x. A ) )
26 sqneg 
 |-  ( A e. CC -> ( -u A ^ 2 ) = ( A ^ 2 ) )
27 26 oveq2d 
 |-  ( A e. CC -> ( 1 - ( -u A ^ 2 ) ) = ( 1 - ( A ^ 2 ) ) )
28 27 fveq2d 
 |-  ( A e. CC -> ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) = ( sqrt ` ( 1 - ( A ^ 2 ) ) ) )
29 25 28 oveq12d 
 |-  ( A e. CC -> ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) = ( -u ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) )
30 20 23 29 3eqtrd 
 |-  ( A e. CC -> ( exp ` ( -u _i x. ( arcsin ` A ) ) ) = ( -u ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) )
31 11 negcld 
 |-  ( A e. CC -> -u ( _i x. A ) e. CC )
32 31 8 addcomd 
 |-  ( A e. CC -> ( -u ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) = ( ( sqrt ` ( 1 - ( A ^ 2 ) ) ) + -u ( _i x. A ) ) )
33 8 11 negsubd 
 |-  ( A e. CC -> ( ( sqrt ` ( 1 - ( A ^ 2 ) ) ) + -u ( _i x. A ) ) = ( ( sqrt ` ( 1 - ( A ^ 2 ) ) ) - ( _i x. A ) ) )
34 30 32 33 3eqtrd 
 |-  ( A e. CC -> ( exp ` ( -u _i x. ( arcsin ` A ) ) ) = ( ( sqrt ` ( 1 - ( A ^ 2 ) ) ) - ( _i x. A ) ) )
35 14 34 oveq12d 
 |-  ( A e. CC -> ( ( exp ` ( _i x. ( arcsin ` A ) ) ) + ( exp ` ( -u _i x. ( arcsin ` A ) ) ) ) = ( ( ( sqrt ` ( 1 - ( A ^ 2 ) ) ) + ( _i x. A ) ) + ( ( sqrt ` ( 1 - ( A ^ 2 ) ) ) - ( _i x. A ) ) ) )
36 8 2timesd 
 |-  ( A e. CC -> ( 2 x. ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) = ( ( sqrt ` ( 1 - ( A ^ 2 ) ) ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) )
37 12 35 36 3eqtr4d 
 |-  ( A e. CC -> ( ( exp ` ( _i x. ( arcsin ` A ) ) ) + ( exp ` ( -u _i x. ( arcsin ` A ) ) ) ) = ( 2 x. ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) )
38 37 oveq1d 
 |-  ( A e. CC -> ( ( ( exp ` ( _i x. ( arcsin ` A ) ) ) + ( exp ` ( -u _i x. ( arcsin ` A ) ) ) ) / 2 ) = ( ( 2 x. ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) / 2 ) )
39 2cnd 
 |-  ( A e. CC -> 2 e. CC )
40 2ne0 
 |-  2 =/= 0
41 40 a1i 
 |-  ( A e. CC -> 2 =/= 0 )
42 8 39 41 divcan3d 
 |-  ( A e. CC -> ( ( 2 x. ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) / 2 ) = ( sqrt ` ( 1 - ( A ^ 2 ) ) ) )
43 3 38 42 3eqtrd 
 |-  ( A e. CC -> ( cos ` ( arcsin ` A ) ) = ( sqrt ` ( 1 - ( A ^ 2 ) ) ) )