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 ⊢ A ∈ ℂ → arcsin ⁡ A = − i ⁢ log ⁡ i ⁢ A + 1 − A 2

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ x = A → i ⁢ x = i ⁢ A
2 oveq1 ⊢ x = A → x 2 = A 2
3 2 oveq2d ⊢ x = A → 1 − x 2 = 1 − A 2
4 3 fveq2d ⊢ x = A → 1 − x 2 = 1 − A 2
5 1 4 oveq12d ⊢ x = A → i ⁢ x + 1 − x 2 = i ⁢ A + 1 − A 2
6 5 fveq2d ⊢ x = A → log ⁡ i ⁢ x + 1 − x 2 = log ⁡ i ⁢ A + 1 − A 2
7 6 oveq2d ⊢ x = A → − i ⁢ log ⁡ i ⁢ x + 1 − x 2 = − i ⁢ log ⁡ i ⁢ A + 1 − A 2
8 df-asin ⊢ arcsin = x ∈ ℂ ⟼ − i ⁢ log ⁡ i ⁢ x + 1 − x 2
9 ovex ⊢ − i ⁢ log ⁡ i ⁢ A + 1 − A 2 ∈ V
10 7 8 9 fvmpt ⊢ A ∈ ℂ → arcsin ⁡ A = − i ⁢ log ⁡ i ⁢ A + 1 − A 2