src/HOL/Analysis/Complex_Transcendental.thy
changeset 64287 d85d88722745
parent 64267 b9a1486e79be
child 64394 141e1ed8d5a0
     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Oct 18 12:01:54 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Oct 18 15:55:53 2016 +0100
     1.3 @@ -236,6 +236,23 @@
     1.4    finally show ?thesis .
     1.5  qed
     1.6  
     1.7 +lemma exp_plus_2pin [simp]: "exp (z + \<i> * (of_int n * (of_real pi * 2))) = exp z"
     1.8 +  by (simp add: exp_eq)
     1.9 +
    1.10 +lemma inj_on_exp_pi:
    1.11 +  fixes z::complex shows "inj_on exp (ball z pi)"
    1.12 +proof (clarsimp simp: inj_on_def exp_eq)
    1.13 +  fix y n
    1.14 +  assume "dist z (y + 2 * of_int n * of_real pi * \<i>) < pi"
    1.15 +         "dist z y < pi"
    1.16 +  then have "dist y (y + 2 * of_int n * of_real pi * \<i>) < pi+pi"
    1.17 +    using dist_commute_lessI dist_triangle_less_add by blast
    1.18 +  then have "norm (2 * of_int n * of_real pi * \<i>) < 2*pi"
    1.19 +    by (simp add: dist_norm)
    1.20 +  then show "n = 0"
    1.21 +    by (auto simp: norm_mult)
    1.22 +qed
    1.23 +
    1.24  lemma sin_cos_eq_iff: "sin y = sin x \<and> cos y = cos x \<longleftrightarrow> (\<exists>n::int. y = x + 2 * n * pi)"
    1.25  proof -
    1.26    { assume "sin y = sin x" "cos y = cos x"