src/HOL/Analysis/Complex_Transcendental.thy
changeset 66466 aec5d9c88d69
parent 66453 cc19f7ca2ed6
child 66480 4b8d1df8933b
     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Sun Aug 20 03:35:20 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Sun Aug 20 18:55:03 2017 +0200
     1.3 @@ -247,6 +247,19 @@
     1.4  lemma exp_plus_2pin [simp]: "exp (z + \<i> * (of_int n * (of_real pi * 2))) = exp z"
     1.5    by (simp add: exp_eq)
     1.6  
     1.7 +lemma exp_integer_2pi_plus1:
     1.8 +  assumes "n \<in> \<int>"
     1.9 +  shows "exp(((2 * n + 1) * pi) * \<i>) = - 1"
    1.10 +proof -
    1.11 +  from assms obtain n' where [simp]: "n = of_int n'"
    1.12 +    by (auto simp: Ints_def)
    1.13 +  have "exp(((2 * n + 1) * pi) * \<i>) = exp (pi * \<i>)"
    1.14 +    using assms by (subst exp_eq) (auto intro!: exI[of _ n'] simp: algebra_simps)
    1.15 +  also have "... = - 1"
    1.16 +    by simp
    1.17 +  finally show ?thesis .
    1.18 +qed
    1.19 +
    1.20  lemma inj_on_exp_pi:
    1.21    fixes z::complex shows "inj_on exp (ball z pi)"
    1.22  proof (clarsimp simp: inj_on_def exp_eq)