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 ) ) ) ) ) ) )