src/HOL/Complex.thy

 qed
 
 end
 
 
-subsection \<open>Numerals, Arithmetic, and Embedding from Reals\<close>
+subsection \<open>Numerals, Arithmetic, and Embedding from \<real>\<close>
 
 abbreviation complex_of_real :: "real \<Rightarrow> complex"
   where "complex_of_real \<equiv> of_real"
 
 declare [[coercion "of_real :: real \<Rightarrow> complex"]]

   by (simp add: Re_divide power2_eq_square)
 
 lemma Im_divide_of_real [simp]: "Im (z / of_real r) = Im z / r"
   by (simp add: Im_divide power2_eq_square)
 
-lemma Re_divide_Reals: "r \<in> Reals \<Longrightarrow> Re (z / r) = Re z / Re r"
+lemma Re_divide_Reals [simp]: "r \<in> \<real> \<Longrightarrow> Re (z / r) = Re z / Re r"
   by (metis Re_divide_of_real of_real_Re)
 
-lemma Im_divide_Reals: "r \<in> Reals \<Longrightarrow> Im (z / r) = Im z / Re r"
+lemma Im_divide_Reals [simp]: "r \<in> \<real> \<Longrightarrow> Im (z / r) = Im z / Re r"
   by (metis Im_divide_of_real of_real_Re)
 
 lemma Re_sum[simp]: "Re (sum f s) = (\<Sum>x\<in>s. Re (f x))"
   by (induct s rule: infinite_finite_induct) auto
 

 lemma Reals_cnj_iff: "z \<in> \<real> \<longleftrightarrow> cnj z = z"
   by (auto simp: complex_is_Real_iff complex_eq_iff)
 
 lemma in_Reals_norm: "z \<in> \<real> \<Longrightarrow> norm z = \<bar>Re z\<bar>"
   by (simp add: complex_is_Real_iff norm_complex_def)
+
+lemma Re_Reals_divide: "r \<in> \<real> \<Longrightarrow> Re (r / z) = Re r * Re z / (norm z)\<^sup>2"
+  by (simp add: Re_divide complex_is_Real_iff cmod_power2)
+
+lemma Im_Reals_divide: "r \<in> \<real> \<Longrightarrow> Im (r / z) = -Re r * Im z / (norm z)\<^sup>2"
+  by (simp add: Im_divide complex_is_Real_iff cmod_power2)
 
 lemma series_comparison_complex:
   fixes f:: "nat \<Rightarrow> 'a::banach"
   assumes sg: "summable g"
     and "\<And>n. g n \<in> \<real>" "\<And>n. Re (g n) \<ge> 0"