equal
deleted
inserted
replaced
55 less_numeral_extra(3) mult_less_0_iff of_nat_less_0_iff) |
55 less_numeral_extra(3) mult_less_0_iff of_nat_less_0_iff) |
56 have "\<And>x. (Suc x) * t ^ x * diff (Suc m + x) 0 / fact (Suc x) = diff (Suc m + x) 0 * t^x / fact x" |
56 have "\<And>x. (Suc x) * t ^ x * diff (Suc m + x) 0 / fact (Suc x) = diff (Suc m + x) 0 * t^x / fact x" |
57 by (rule nonzero_divide_eq_eq[THEN iffD2]) auto |
57 by (rule nonzero_divide_eq_eq[THEN iffD2]) auto |
58 moreover |
58 moreover |
59 have "(n - m) * t ^ (n - Suc m) * B / fact (n - m) = B * (t ^ (n - Suc m) / fact (n - Suc m))" |
59 have "(n - m) * t ^ (n - Suc m) * B / fact (n - m) = B * (t ^ (n - Suc m) / fact (n - Suc m))" |
60 using \<open>0 < n - m\<close> by (simp add: divide_simps fact_reduce) |
60 using \<open>0 < n - m\<close> by (simp add: field_split_simps fact_reduce) |
61 ultimately show "DERIV (difg m) t :> difg (Suc m) t" |
61 ultimately show "DERIV (difg m) t :> difg (Suc m) t" |
62 unfolding difg_def by (simp add: mult.commute) |
62 unfolding difg_def by (simp add: mult.commute) |
63 qed |
63 qed |
64 |
64 |
65 lemma Maclaurin: |
65 lemma Maclaurin: |