equal
deleted
inserted
replaced
538 \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))" |
538 \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))" |
539 proof (clarsimp) |
539 proof (clarsimp) |
540 fix x :: real assume "a \<le> x" and "x \<le> b" |
540 fix x :: real assume "a \<le> x" and "x \<le> b" |
541 with f' have "DERIV f x :> f'(x)" by simp |
541 with f' have "DERIV f x :> f'(x)" by simp |
542 then have "\<forall>r>0. \<exists>s>0. \<forall>z. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < r" |
542 then have "\<forall>r>0. \<exists>s>0. \<forall>z. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < r" |
543 by (simp add: DERIV_iff2 LIM_eq) |
543 by (simp add: has_field_derivative_iff LIM_eq) |
544 with \<open>0 < e\<close> obtain s |
544 with \<open>0 < e\<close> obtain s |
545 where "z \<noteq> x \<Longrightarrow> \<bar>z - x\<bar> < s \<Longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2" and "0 < s" for z |
545 where "z \<noteq> x \<Longrightarrow> \<bar>z - x\<bar> < s \<Longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2" and "0 < s" for z |
546 by (drule_tac x="e/2" in spec, auto) |
546 by (drule_tac x="e/2" in spec, auto) |
547 with strad1 [of x s f f' e] have strad: |
547 with strad1 [of x s f f' e] have strad: |
548 "\<And>z. \<bar>z - x\<bar> < s \<Longrightarrow> \<bar>f z - f x - f' x * (z - x)\<bar> \<le> e/2 * \<bar>z - x\<bar>" |
548 "\<And>z. \<bar>z - x\<bar> < s \<Longrightarrow> \<bar>f z - f x - f' x * (z - x)\<bar> \<le> e/2 * \<bar>z - x\<bar>" |