equal
deleted
inserted
replaced
1756 by (simp add: power_inverse [symmetric]) |
1756 by (simp add: power_inverse [symmetric]) |
1757 hence "inverse (fact (n + 2)) * (x^n * x\<^sup>2) \<le> 1/2 * (1/2)^n * (1 * x\<^sup>2)" |
1757 hence "inverse (fact (n + 2)) * (x^n * x\<^sup>2) \<le> 1/2 * (1/2)^n * (1 * x\<^sup>2)" |
1758 by (rule mult_mono) |
1758 by (rule mult_mono) |
1759 (rule mult_mono, simp_all add: power_le_one a b) |
1759 (rule mult_mono, simp_all add: power_le_one a b) |
1760 hence "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<^sup>2/2) * ((1/2)^n)" |
1760 hence "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<^sup>2/2) * ((1/2)^n)" |
1761 unfolding power_add by (simp add: ac_simps del: fact.simps) } |
1761 unfolding power_add by (simp add: ac_simps del: fact_Suc) } |
1762 note aux1 = this |
1762 note aux1 = this |
1763 have "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))" |
1763 have "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))" |
1764 by (intro sums_mult geometric_sums, simp) |
1764 by (intro sums_mult geometric_sums, simp) |
1765 hence aux2: "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums x\<^sup>2" |
1765 hence aux2: "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums x\<^sup>2" |
1766 by simp |
1766 by simp |
3317 done |
3317 done |
3318 |
3318 |
3319 lemma cos_two_less_zero [simp]: |
3319 lemma cos_two_less_zero [simp]: |
3320 "cos 2 < (0::real)" |
3320 "cos 2 < (0::real)" |
3321 proof - |
3321 proof - |
3322 note fact.simps(2) [simp del] |
3322 note fact_Suc [simp del] |
3323 from sums_minus [OF cos_paired] |
3323 from sums_minus [OF cos_paired] |
3324 have *: "(\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / fact (2 * n))) sums - cos (2::real)" |
3324 have *: "(\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / fact (2 * n))) sums - cos (2::real)" |
3325 by simp |
3325 by simp |
3326 then have sm: "summable (\<lambda>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))" |
3326 then have sm: "summable (\<lambda>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))" |
3327 by (rule sums_summable) |
3327 by (rule sums_summable) |
3333 { fix d |
3333 { fix d |
3334 let ?six4d = "Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))" |
3334 let ?six4d = "Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))" |
3335 have "(4::real) * (fact (?six4d)) < (Suc (Suc (?six4d)) * fact (Suc (?six4d)))" |
3335 have "(4::real) * (fact (?six4d)) < (Suc (Suc (?six4d)) * fact (Suc (?six4d)))" |
3336 unfolding of_nat_mult by (rule mult_strict_mono) (simp_all add: fact_less_mono) |
3336 unfolding of_nat_mult by (rule mult_strict_mono) (simp_all add: fact_less_mono) |
3337 then have "(4::real) * (fact (?six4d)) < (fact (Suc (Suc (?six4d))))" |
3337 then have "(4::real) * (fact (?six4d)) < (fact (Suc (Suc (?six4d))))" |
3338 by (simp only: fact.simps(2) [of "Suc (?six4d)"] of_nat_mult of_nat_fact) |
3338 by (simp only: fact_Suc [of "Suc (?six4d)"] of_nat_mult of_nat_fact) |
3339 then have "(4::real) * inverse (fact (Suc (Suc (?six4d)))) < inverse (fact (?six4d))" |
3339 then have "(4::real) * inverse (fact (Suc (Suc (?six4d)))) < inverse (fact (?six4d))" |
3340 by (simp add: inverse_eq_divide less_divide_eq) |
3340 by (simp add: inverse_eq_divide less_divide_eq) |
3341 } |
3341 } |
3342 then show ?thesis |
3342 then show ?thesis |
3343 by (force intro!: sumr_pos_lt_pair [OF sm] simp add: divide_inverse algebra_simps) |
3343 by (force intro!: sumr_pos_lt_pair [OF sm] simp add: divide_inverse algebra_simps) |