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