[STATEMENT]
lemma has_field_derivative_Im[derivative_intros]:
  "(f has_vector_derivative D) F \<Longrightarrow> ((\<lambda>x. Im (f x)) has_field_derivative (Im D)) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f has_vector_derivative D) F \<Longrightarrow> ((\<lambda>x. Im (f x)) has_real_derivative Im D) F
[PROOF STEP]
unfolding has_vector_derivative_complex_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. Re (f x)) has_real_derivative Re D) F \<and> ((\<lambda>x. Im (f x)) has_real_derivative Im D) F \<Longrightarrow> ((\<lambda>x. Im (f x)) has_real_derivative Im D) F
[PROOF STEP]
by safe