src/HOL/Analysis/Complex_Transcendental.thy
 changeset 65583 8d53b3bebab4 parent 65578 e4997c181cce child 65585 a043de9ad41e
```     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Apr 25 21:31:28 2017 +0200
1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Wed Apr 26 15:53:35 2017 +0100
1.3 @@ -1046,6 +1046,9 @@
1.4    apply auto
1.5    done
1.6
1.7 +lemma Ln_eq_zero_iff [simp]: "x \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Ln x = 0 \<longleftrightarrow> x = 1"
1.8 +  by auto (metis exp_Ln exp_zero nonpos_Reals_zero_I)
1.9 +
1.10  subsection\<open>Relation to Real Logarithm\<close>
1.11
1.12  lemma Ln_of_real:
1.13 @@ -1679,23 +1682,19 @@
1.14    fixes n::nat and z::complex shows "z powr n = (if z = 0 then 0 else z^n)"
1.15    by (simp add: exp_of_nat_mult powr_def)
1.16
1.17 -lemma powr_add_complex:
1.18 -  fixes w::complex shows "w powr (z1 + z2) = w powr z1 * w powr z2"
1.19 -  by (simp add: powr_def algebra_simps exp_add)
1.20 -
1.21 -lemma powr_minus_complex:
1.22 -  fixes w::complex shows  "w powr (-z) = inverse(w powr z)"
1.23 -  by (simp add: powr_def exp_minus)
1.24 -
1.25 -lemma powr_diff_complex:
1.26 -  fixes w::complex shows  "w powr (z1 - z2) = w powr z1 / w powr z2"
1.27 -  by (simp add: powr_def algebra_simps exp_diff)
1.28 -
1.29  lemma norm_powr_real: "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = exp(Re z * ln(Re w))"
1.30    apply (simp add: powr_def)
1.31    using Im_Ln_eq_0 complex_is_Real_iff norm_complex_def
1.32    by auto
1.33
1.34 +lemma powr_complexpow [simp]:
1.35 +  fixes x::complex shows "x \<noteq> 0 \<Longrightarrow> x powr (of_nat n) = x^n"
1.36 +  by (induct n) (auto simp: ac_simps powr_add)
1.37 +
1.38 +lemma powr_complexnumeral [simp]:
1.39 +  fixes x::complex shows "x \<noteq> 0 \<Longrightarrow> x powr (numeral n) = x ^ (numeral n)"
1.40 +  by (metis of_nat_numeral powr_complexpow)
1.41 +
1.42  lemma cnj_powr:
1.43    assumes "Im a = 0 \<Longrightarrow> Re a \<ge> 0"
1.44    shows   "cnj (a powr b) = cnj a powr cnj b"
1.45 @@ -1759,16 +1758,15 @@
1.46    apply (intro derivative_eq_intros | simp)+
1.47    done
1.48
1.49 -lemma field_differentiable_powr_right:
1.50 +lemma field_differentiable_powr_right [derivative_intros]:
1.51    fixes w::complex
1.52 -  shows
1.53 -    "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) field_differentiable (at z)"
1.54 +  shows "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) field_differentiable (at z)"
1.55  using field_differentiable_def has_field_derivative_powr_right by blast
1.56
1.57 -lemma holomorphic_on_powr_right:
1.58 +lemma holomorphic_on_powr_right [holomorphic_intros]:
1.59      "f holomorphic_on s \<Longrightarrow> w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr (f z)) holomorphic_on s"
1.60 -    unfolding holomorphic_on_def field_differentiable_def
1.61 -by (metis (full_types) DERIV_chain' has_field_derivative_powr_right)
1.62 +  unfolding holomorphic_on_def field_differentiable_def
1.63 +  by (metis (full_types) DERIV_chain' has_field_derivative_powr_right)
1.64
1.65  lemma norm_powr_real_powr:
1.66    "w \<in> \<real> \<Longrightarrow> 0 \<le> Re w \<Longrightarrow> cmod (w powr z) = Re w powr Re z"
1.67 @@ -2562,6 +2560,9 @@
1.68    using arctan_bounds[of "1/5"   4]
1.69          arctan_bounds[of "1/239" 4]
1.70    by (simp_all add: eval_nat_numeral)
1.71 +
1.72 +corollary pi_gt3: "pi > 3"
1.73 +  using pi_approx by simp
1.74
1.75
1.76  subsection\<open>Inverse Sine\<close>
```