[STATEMENT]
lemma of_real_arcsin: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arcsin x) = Arcsin(of_real x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x\<bar> \<le> 1 \<Longrightarrow> complex_of_real (arcsin x) = Arcsin (complex_of_real x)
[PROOF STEP]
by (metis Im_Arcsin_of_real add.right_neutral arcsin_eq_Re_Arcsin complex_eq mult_zero_right of_real_0)