1382 theorem mvt: |
1382 theorem mvt: |
1383 fixes f :: "real \<Rightarrow> real" |
1383 fixes f :: "real \<Rightarrow> real" |
1384 assumes "a < b" |
1384 assumes "a < b" |
1385 and contf: "continuous_on {a..b} f" |
1385 and contf: "continuous_on {a..b} f" |
1386 and derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)" |
1386 and derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)" |
1387 obtains z where "a < z" "z < b" "f b - f a = (f' z) (b - a)" |
1387 obtains \<xi> where "a < \<xi>" "\<xi> < b" "f b - f a = (f' \<xi>) (b - a)" |
1388 proof - |
1388 proof - |
1389 have "\<exists>x. a < x \<and> x < b \<and> (\<lambda>y. f' x y - (f b - f a) / (b - a) * y) = (\<lambda>v. 0)" |
1389 have "\<exists>x. a < x \<and> x < b \<and> (\<lambda>y. f' x y - (f b - f a) / (b - a) * y) = (\<lambda>v. 0)" |
1390 proof (intro Rolle_deriv[OF \<open>a < b\<close>]) |
1390 proof (intro Rolle_deriv[OF \<open>a < b\<close>]) |
1391 fix x |
1391 fix x |
1392 assume x: "a < x" "x < b" |
1392 assume x: "a < x" "x < b" |
1393 show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative |
1393 show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) |
1394 (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)" |
1394 has_derivative (\<lambda>y. f' x y - (f b - f a) / (b - a) * y)) (at x)" |
1395 by (intro derivative_intros derf[OF x]) |
1395 by (intro derivative_intros derf[OF x]) |
1396 qed (use assms in \<open>auto intro!: continuous_intros simp: field_simps\<close>) |
1396 qed (use assms in \<open>auto intro!: continuous_intros simp: field_simps\<close>) |
1397 then obtain x where |
1397 then obtain \<xi> where |
1398 "a < x" "x < b" |
1398 "a < \<xi>" "\<xi> < b" "(\<lambda>y. f' \<xi> y - (f b - f a) / (b - a) * y) = (\<lambda>v. 0)" |
1399 "(\<lambda>y. f' x y - (f b - f a) / (b - a) * y) = (\<lambda>v. 0)" by metis |
1399 by metis |
1400 then show ?thesis |
1400 then show ?thesis |
1401 by (metis (no_types, hide_lams) that add.right_neutral add_diff_cancel_left' add_diff_eq \<open>a < b\<close> |
1401 by (metis (no_types, hide_lams) that add.right_neutral add_diff_cancel_left' add_diff_eq \<open>a < b\<close> |
1402 less_irrefl nonzero_eq_divide_eq) |
1402 less_irrefl nonzero_eq_divide_eq) |
1403 qed |
1403 qed |
1404 |
1404 |