--- a/src/HOL/MacLaurin.thy Wed Mar 15 21:52:04 2017 +0100
+++ b/src/HOL/MacLaurin.thy Thu Mar 16 13:55:29 2017 +0000
@@ -359,10 +359,17 @@
shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> exp x = (\<Sum>m<n. (x ^ m) / fact m) + (exp t / fact n) * x ^ n"
using Maclaurin_all_le_objl [where diff = "\<lambda>n. exp" and f = exp and x = x and n = n] by auto
-lemma exp_lower_taylor_quadratic: "0 \<le> x \<Longrightarrow> 1 + x + x\<^sup>2 / 2 \<le> exp x"
+corollary exp_lower_taylor_quadratic: "0 \<le> x \<Longrightarrow> 1 + x + x\<^sup>2 / 2 \<le> exp x"
for x :: real
using Maclaurin_exp_le [of x 3] by (auto simp: numeral_3_eq_3 power2_eq_square)
+corollary ln_2_less_1: "ln 2 < (1::real)"
+proof -
+ have "2 < 5/(2::real)" by simp
+ also have "5/2 \<le> exp (1::real)" using exp_lower_taylor_quadratic[of 1, simplified] by simp
+ finally have "exp (ln 2) < exp (1::real)" by simp
+ thus "ln 2 < (1::real)" by (subst (asm) exp_less_cancel_iff) simp
+qed
subsection \<open>Version for Sine Function\<close>