equal
deleted
inserted
replaced
386 (exp t / real (fact n)) * x ^ n" |
386 (exp t / real (fact n)) * x ^ n" |
387 by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto) |
387 by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto) |
388 |
388 |
389 |
389 |
390 subsection{*Version for Sine Function*} |
390 subsection{*Version for Sine Function*} |
391 |
|
392 lemma MVT2: |
|
393 "[| a < b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |] |
|
394 ==> \<exists>z::real. a < z & z < b & (f b - f a = (b - a) * f'(z))" |
|
395 apply (drule MVT) |
|
396 apply (blast intro: DERIV_isCont) |
|
397 apply (force dest: order_less_imp_le simp add: differentiable_def) |
|
398 apply (blast dest: DERIV_unique order_less_imp_le) |
|
399 done |
|
400 |
391 |
401 lemma mod_exhaust_less_4: |
392 lemma mod_exhaust_less_4: |
402 "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)" |
393 "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)" |
403 by auto |
394 by auto |
404 |
395 |