equal
deleted
inserted
replaced
615 of_nat n * x ^ (n - Suc 0))) -- 0 --> 0" |
615 of_nat n * x ^ (n - Suc 0))) -- 0 --> 0" |
616 by (rule termdiffs_aux [OF 3 4]) |
616 by (rule termdiffs_aux [OF 3 4]) |
617 qed |
617 qed |
618 qed |
618 qed |
619 |
619 |
620 |
|
621 subsection{* Some properties of factorials *} |
|
622 |
|
623 lemma real_of_nat_fact_not_zero [simp]: "real (fact (n::nat)) \<noteq> 0" |
|
624 by auto |
|
625 |
|
626 lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact (n::nat))" |
|
627 by auto |
|
628 |
|
629 lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact (n::nat))" |
|
630 by simp |
|
631 |
|
632 lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact (n::nat)))" |
|
633 by (auto simp add: positive_imp_inverse_positive) |
|
634 |
|
635 lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact (n::nat)))" |
|
636 by (auto intro: order_less_imp_le) |
|
637 |
620 |
638 subsection {* Derivability of power series *} |
621 subsection {* Derivability of power series *} |
639 |
622 |
640 lemma DERIV_series': fixes f :: "real \<Rightarrow> nat \<Rightarrow> real" |
623 lemma DERIV_series': fixes f :: "real \<Rightarrow> nat \<Rightarrow> real" |
641 assumes DERIV_f: "\<And> n. DERIV (\<lambda> x. f x n) x0 :> (f' x0 n)" |
624 assumes DERIV_f: "\<And> n. DERIV (\<lambda> x. f x n) x0 :> (f' x0 n)" |
1699 apply (erule sums_summable, safe) |
1682 apply (erule sums_summable, safe) |
1700 unfolding One_nat_def |
1683 unfolding One_nat_def |
1701 apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric] |
1684 apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric] |
1702 del: fact_Suc) |
1685 del: fact_Suc) |
1703 apply (rule real_mult_inverse_cancel2) |
1686 apply (rule real_mult_inverse_cancel2) |
1704 apply (rule real_of_nat_fact_gt_zero)+ |
1687 apply (simp del: fact_Suc) |
|
1688 apply (simp del: fact_Suc) |
1705 apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc) |
1689 apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc) |
1706 apply (subst fact_lemma) |
1690 apply (subst fact_lemma) |
1707 apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"]) |
1691 apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"]) |
1708 apply (simp only: real_of_nat_mult) |
1692 apply (simp only: real_of_nat_mult) |
1709 apply (rule mult_strict_mono, force) |
1693 apply (rule mult_strict_mono, force) |