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"
```