Metamath Proof Explorer

Theorem efiasin

Description: The exponential of the arcsine function. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion efiasin ( 𝐴 ∈ ℂ → ( exp ‘ ( i · ( arcsin ‘ 𝐴 ) ) ) = ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 asinval ⊢ ( 𝐴 ∈ ℂ → ( arcsin ‘ 𝐴 ) = ( - i · ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) )
2 1 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( i · ( arcsin ‘ 𝐴 ) ) = ( i · ( - i · ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ) )
3 ax-icn ⊢ i ∈ ℂ
4 3 a1i ⊢ ( 𝐴 ∈ ℂ → i ∈ ℂ )
5 negicn ⊢ - i ∈ ℂ
6 5 a1i ⊢ ( 𝐴 ∈ ℂ → - i ∈ ℂ )
7 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
8 3 7 mpan ⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ )
9 ax-1cn ⊢ 1 ∈ ℂ
10 sqcl ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) ∈ ℂ )
11 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ) → ( 1 − ( 𝐴 ↑ 2 ) ) ∈ ℂ )
12 9 10 11 sylancr ⊢ ( 𝐴 ∈ ℂ → ( 1 − ( 𝐴 ↑ 2 ) ) ∈ ℂ )
13 12 sqrtcld ⊢ ( 𝐴 ∈ ℂ → ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ∈ ℂ )
14 8 13 addcld ⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ∈ ℂ )
15 asinlem ⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ≠ 0 )
16 14 15 logcld ⊢ ( 𝐴 ∈ ℂ → ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ∈ ℂ )
17 4 6 16 mulassd ⊢ ( 𝐴 ∈ ℂ → ( ( i · - i ) · ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) = ( i · ( - i · ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ) )
18 3 3 mulneg2i ⊢ ( i · - i ) = - ( i · i )
19 ixi ⊢ ( i · i ) = - 1
20 19 negeqi ⊢ - ( i · i ) = - - 1
21 negneg1e1 ⊢ - - 1 = 1
22 18 20 21 3eqtri ⊢ ( i · - i ) = 1
23 22 oveq1i ⊢ ( ( i · - i ) · ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) = ( 1 · ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) )
24 16 mulid2d ⊢ ( 𝐴 ∈ ℂ → ( 1 · ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) = ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) )
25 23 24 eqtrid ⊢ ( 𝐴 ∈ ℂ → ( ( i · - i ) · ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) = ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) )
26 2 17 25 3eqtr2d ⊢ ( 𝐴 ∈ ℂ → ( i · ( arcsin ‘ 𝐴 ) ) = ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) )
27 26 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · ( arcsin ‘ 𝐴 ) ) ) = ( exp ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) )
28 eflog ⊢ ( ( ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ∈ ℂ ∧ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ≠ 0 ) → ( exp ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) = ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) )
29 14 15 28 syl2anc ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) = ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) )
30 27 29 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · ( arcsin ‘ 𝐴 ) ) ) = ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) )