[STATEMENT]
lemma nonzero_Complexs_inverse: "a \<in> \<complex> \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> inverse a \<in> \<complex>"
  for a :: "'a::complex_div_algebra"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> \<complex>; a \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> inverse a \<in> \<complex>
[PROOF STEP]
apply (auto simp add: Complexs_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> 0; a = of_complex x\<rbrakk> \<Longrightarrow> inverse (of_complex x) \<in> range of_complex
[PROOF STEP]
by (metis of_complex_inverse range_eqI)