src/HOL/Analysis/Complex_Transcendental.thy
changeset 65587 16a8991ab398
parent 65585 a043de9ad41e
child 65719 7c57d79d61b7
     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu Apr 27 11:06:47 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Apr 27 15:59:00 2017 +0100
     1.3 @@ -1401,7 +1401,7 @@
     1.4          Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z]
     1.5    by (simp add: Ln_times) auto
     1.6  
     1.7 -lemma Ln_of_nat: "0 < n \<Longrightarrow> Ln (of_nat n) = of_real (ln (of_nat n))"
     1.8 +lemma Ln_of_nat [simp]: "0 < n \<Longrightarrow> Ln (of_nat n) = of_real (ln (of_nat n))"
     1.9    by (subst of_real_of_nat_eq[symmetric], subst Ln_of_real[symmetric]) simp_all
    1.10  
    1.11  lemma Ln_of_nat_over_of_nat:
    1.12 @@ -1936,14 +1936,13 @@
    1.13  qed
    1.14  
    1.15  lemma lim_Ln_over_n: "((\<lambda>n. Ln(of_nat n) / of_nat n) \<longlongrightarrow> 0) sequentially"
    1.16 -  using lim_Ln_over_power [of 1]
    1.17 -  by simp
    1.18 -
    1.19 -lemma Ln_Reals_eq: "x \<in> \<real> \<Longrightarrow> Re x > 0 \<Longrightarrow> Ln x = of_real (ln (Re x))"
    1.20 +  using lim_Ln_over_power [of 1] by simp
    1.21 +
    1.22 +lemma Ln_Reals_eq: "\<lbrakk>x \<in> \<real>; Re x > 0\<rbrakk> \<Longrightarrow> Ln x = of_real (ln (Re x))"
    1.23    using Ln_of_real by force
    1.24  
    1.25 -lemma powr_Reals_eq: "x \<in> \<real> \<Longrightarrow> Re x > 0 \<Longrightarrow> x powr complex_of_real y = of_real (x powr y)"
    1.26 -  by (simp add: powr_of_real)
    1.27 +lemma powr_Reals_eq: "\<lbrakk>x \<in> \<real>; y \<in> \<real>; Re x > 0\<rbrakk> \<Longrightarrow> x powr y = of_real (Re x powr Re y)"
    1.28 +  by (metis linear not_le of_real_Re powr_of_real)
    1.29  
    1.30  lemma lim_ln_over_power:
    1.31    fixes s :: real