src/HOL/Analysis/Weierstrass_Theorems.thy
changeset 65578 e4997c181cce
parent 65204 d23eded35a33
child 65583 8d53b3bebab4
     1.1 --- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Tue Apr 25 08:38:23 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Tue Apr 25 16:39:54 2017 +0100
     1.3 @@ -398,12 +398,17 @@
     1.4      using \<open>k>0\<close> \<open>\<delta>>0\<close> NN  k\<delta>
     1.5      apply (force simp add: field_simps)+
     1.6      done
     1.7 -  have NN0: "\<And>e. e>0 \<Longrightarrow> (1/(k*\<delta>))^NN e < e"
     1.8 -    apply (subst Transcendental.ln_less_cancel_iff [symmetric])
     1.9 -      prefer 3 apply (subst ln_realpow)
    1.10 -    using \<open>k>0\<close> \<open>\<delta>>0\<close> NN k\<delta>
    1.11 -    apply (force simp add: field_simps ln_div)+
    1.12 -    done
    1.13 +  have NN0: "(1/(k*\<delta>)) ^ (NN e) < e" if "e>0" for e
    1.14 +  proof -
    1.15 +    have "0 < ln (real k) + ln \<delta>"
    1.16 +      using \<delta>01(1) \<open>0 < k\<close> k\<delta>(1) ln_gt_zero by fastforce
    1.17 +    then have "real (NN e) * ln (1 / (real k * \<delta>)) < ln e"
    1.18 +      using k\<delta>(1) NN(2) [of e] that by (simp add: ln_div divide_simps)
    1.19 +    then have "exp (real (NN e) * ln (1 / (real k * \<delta>))) < e"
    1.20 +      by (metis exp_less_mono exp_ln that)
    1.21 +    then show ?thesis
    1.22 +      by (simp add: \<delta>01(1) \<open>0 < k\<close>)
    1.23 +  qed
    1.24    { fix t and e::real
    1.25      assume "e>0"
    1.26      have "t \<in> S \<inter> V \<Longrightarrow> 1 - q (NN e) t < e" "t \<in> S - U \<Longrightarrow> q (NN e) t < e"