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 ( 𝐴 ∈ ℂ → ( cos ‘ ( arcsin ‘ 𝐴 ) ) = ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 asincl ⊢ ( 𝐴 ∈ ℂ → ( arcsin ‘ 𝐴 ) ∈ ℂ )
2 cosval ⊢ ( ( arcsin ‘ 𝐴 ) ∈ ℂ → ( cos ‘ ( arcsin ‘ 𝐴 ) ) = ( ( ( exp ‘ ( i · ( arcsin ‘ 𝐴 ) ) ) + ( exp ‘ ( - i · ( arcsin ‘ 𝐴 ) ) ) ) / 2 ) )
3 1 2 syl ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( arcsin ‘ 𝐴 ) ) = ( ( ( exp ‘ ( i · ( arcsin ‘ 𝐴 ) ) ) + ( exp ‘ ( - i · ( arcsin ‘ 𝐴 ) ) ) ) / 2 ) )
4 ax-1cn ⊢ 1 ∈ ℂ
5 sqcl ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) ∈ ℂ )
6 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ) → ( 1 − ( 𝐴 ↑ 2 ) ) ∈ ℂ )
7 4 5 6 sylancr ⊢ ( 𝐴 ∈ ℂ → ( 1 − ( 𝐴 ↑ 2 ) ) ∈ ℂ )
8 7 sqrtcld ⊢ ( 𝐴 ∈ ℂ → ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ∈ ℂ )
9 ax-icn ⊢ i ∈ ℂ
10 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
11 9 10 mpan ⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ )
12 8 11 8 ppncand ⊢ ( 𝐴 ∈ ℂ → ( ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) + ( i · 𝐴 ) ) + ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) − ( i · 𝐴 ) ) ) = ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) )
13 efiasin ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · ( arcsin ‘ 𝐴 ) ) ) = ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) )
14 11 8 13 comraddd ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · ( arcsin ‘ 𝐴 ) ) ) = ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) + ( i · 𝐴 ) ) )
15 mulneg12 ⊢ ( ( i ∈ ℂ ∧ ( arcsin ‘ 𝐴 ) ∈ ℂ ) → ( - i · ( arcsin ‘ 𝐴 ) ) = ( i · - ( arcsin ‘ 𝐴 ) ) )
16 9 1 15 sylancr ⊢ ( 𝐴 ∈ ℂ → ( - i · ( arcsin ‘ 𝐴 ) ) = ( i · - ( arcsin ‘ 𝐴 ) ) )
17 asinneg ⊢ ( 𝐴 ∈ ℂ → ( arcsin ‘ - 𝐴 ) = - ( arcsin ‘ 𝐴 ) )
18 17 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( i · ( arcsin ‘ - 𝐴 ) ) = ( i · - ( arcsin ‘ 𝐴 ) ) )
19 16 18 eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( - i · ( arcsin ‘ 𝐴 ) ) = ( i · ( arcsin ‘ - 𝐴 ) ) )
20 19 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( - i · ( arcsin ‘ 𝐴 ) ) ) = ( exp ‘ ( i · ( arcsin ‘ - 𝐴 ) ) ) )
21 negcl ⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
22 efiasin ⊢ ( - 𝐴 ∈ ℂ → ( exp ‘ ( i · ( arcsin ‘ - 𝐴 ) ) ) = ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) )
23 21 22 syl ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · ( arcsin ‘ - 𝐴 ) ) ) = ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) )
24 mulneg2 ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · - 𝐴 ) = - ( i · 𝐴 ) )
25 9 24 mpan ⊢ ( 𝐴 ∈ ℂ → ( i · - 𝐴 ) = - ( i · 𝐴 ) )
26 sqneg ⊢ ( 𝐴 ∈ ℂ → ( - 𝐴 ↑ 2 ) = ( 𝐴 ↑ 2 ) )
27 26 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( 1 − ( - 𝐴 ↑ 2 ) ) = ( 1 − ( 𝐴 ↑ 2 ) ) )
28 27 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) = ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) )
29 25 28 oveq12d ⊢ ( 𝐴 ∈ ℂ → ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) = ( - ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) )
30 20 23 29 3eqtrd ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( - i · ( arcsin ‘ 𝐴 ) ) ) = ( - ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) )
31 11 negcld ⊢ ( 𝐴 ∈ ℂ → - ( i · 𝐴 ) ∈ ℂ )
32 31 8 addcomd ⊢ ( 𝐴 ∈ ℂ → ( - ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) = ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) + - ( i · 𝐴 ) ) )
33 8 11 negsubd ⊢ ( 𝐴 ∈ ℂ → ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) + - ( i · 𝐴 ) ) = ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) − ( i · 𝐴 ) ) )
34 30 32 33 3eqtrd ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( - i · ( arcsin ‘ 𝐴 ) ) ) = ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) − ( i · 𝐴 ) ) )
35 14 34 oveq12d ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · ( arcsin ‘ 𝐴 ) ) ) + ( exp ‘ ( - i · ( arcsin ‘ 𝐴 ) ) ) ) = ( ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) + ( i · 𝐴 ) ) + ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) − ( i · 𝐴 ) ) ) )
36 8 2timesd ⊢ ( 𝐴 ∈ ℂ → ( 2 · ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) = ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) )
37 12 35 36 3eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · ( arcsin ‘ 𝐴 ) ) ) + ( exp ‘ ( - i · ( arcsin ‘ 𝐴 ) ) ) ) = ( 2 · ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) )
38 37 oveq1d ⊢ ( 𝐴 ∈ ℂ → ( ( ( exp ‘ ( i · ( arcsin ‘ 𝐴 ) ) ) + ( exp ‘ ( - i · ( arcsin ‘ 𝐴 ) ) ) ) / 2 ) = ( ( 2 · ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) / 2 ) )
39 2cnd ⊢ ( 𝐴 ∈ ℂ → 2 ∈ ℂ )
40 2ne0 ⊢ 2 ≠ 0
41 40 a1i ⊢ ( 𝐴 ∈ ℂ → 2 ≠ 0 )
42 8 39 41 divcan3d ⊢ ( 𝐴 ∈ ℂ → ( ( 2 · ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) / 2 ) = ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) )
43 3 38 42 3eqtrd ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( arcsin ‘ 𝐴 ) ) = ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) )