src/HOL/Complex.thy

 lemmas sums_Re = bounded_linear.sums [OF bounded_linear_Re]
 lemmas sums_Im = bounded_linear.sums [OF bounded_linear_Im]
 lemmas Re_suminf = bounded_linear.suminf[OF bounded_linear_Re]
 lemmas Im_suminf = bounded_linear.suminf[OF bounded_linear_Im]
 
+lemma continuous_on_Complex [continuous_intros]:
+  "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. Complex (f x) (g x))"
+  unfolding Complex_eq by (intro continuous_intros)
+
 lemma tendsto_Complex [tendsto_intros]:
   "(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> ((\<lambda>x. Complex (f x) (g x)) \<longlongrightarrow> Complex a b) F"
   unfolding Complex_eq by (auto intro!: tendsto_intros)
 
 lemma tendsto_complex_iff:

   by (metis complex_div_cnj div_by_1 mult_1 of_real_1 power2_eq_square)
 
 lemma i_not_in_Reals [simp, intro]: "\<i> \<notin> \<real>"
   by (auto simp: complex_is_Real_iff)
 
-lemma powr_power_complex: "z \<noteq> 0 \<or> n \<noteq> 0 \<Longrightarrow> (z powr u :: complex) ^ n = z powr (of_nat n * u)"
-  by (induction n) (auto simp: algebra_simps powr_add)
-  
 lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re (cis a ^ n)"
   by (auto simp add: DeMoivre)
 
 lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im (cis a ^ n)"
   by (auto simp add: DeMoivre)