This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem asinval

Description: Value of the arcsin function. (Contributed by Mario Carneiro, 31-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑥 = 𝐴 → ( i · 𝑥 ) = ( i · 𝐴 ) )
2 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ↑ 2 ) = ( 𝐴 ↑ 2 ) )
3 2 oveq2d ⊢ ( 𝑥 = 𝐴 → ( 1 − ( 𝑥 ↑ 2 ) ) = ( 1 − ( 𝐴 ↑ 2 ) ) )
4 3 fveq2d ⊢ ( 𝑥 = 𝐴 → ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) = ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) )
5 1 4 oveq12d ⊢ ( 𝑥 = 𝐴 → ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) = ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) )
6 5 fveq2d ⊢ ( 𝑥 = 𝐴 → ( log ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) = ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) )
7 6 oveq2d ⊢ ( 𝑥 = 𝐴 → ( - i · ( log ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) = ( - i · ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) )
8 df-asin ⊢ arcsin = ( 𝑥 ∈ ℂ ↦ ( - i · ( log ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) )
9 ovex ⊢ ( - i · ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ∈ V
10 7 8 9 fvmpt ⊢ ( 𝐴 ∈ ℂ → ( arcsin ‘ 𝐴 ) = ( - i · ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) )