428 apply (rule abs_triangle_ineq [THEN [2] order_trans]) |
428 apply (rule abs_triangle_ineq [THEN [2] order_trans]) |
429 apply (simp add: right_diff_distrib, arith) |
429 apply (simp add: right_diff_distrib, arith) |
430 apply (rule_tac t = "e* (v - u)" in real_sum_of_halves [THEN subst]) |
430 apply (rule_tac t = "e* (v - u)" in real_sum_of_halves [THEN subst]) |
431 apply (rule add_mono) |
431 apply (rule add_mono) |
432 apply (rule_tac y = "(e/2) * \<bar>v - x\<bar>" in order_trans) |
432 apply (rule_tac y = "(e/2) * \<bar>v - x\<bar>" in order_trans) |
433 prefer 2 apply (simp, arith) |
433 prefer 2 apply simp |
434 apply (erule_tac [!] V= "\<forall>x'. x' ~= x & \<bar>x' + - x\<bar> < s --> ?P x'" in thin_rl) |
434 apply (erule_tac [!] V= "\<forall>x'. x' ~= x & \<bar>x' + - x\<bar> < s --> ?P x'" in thin_rl) |
435 apply (drule_tac x = v in spec, simp, arith) |
435 apply (drule_tac x = v in spec, simp) |
436 apply (drule_tac x = u in spec, auto, arith) |
436 apply (drule_tac x = u in spec, auto, arith) |
437 apply (subgoal_tac "\<bar>f u - f x - f' x * (u - x)\<bar> = \<bar>f x - f u - f' x * (x - u)\<bar>") |
437 apply (subgoal_tac "\<bar>f u - f x - f' x * (u - x)\<bar> = \<bar>f x - f u - f' x * (x - u)\<bar>") |
438 apply (rule order_trans) |
438 apply (rule order_trans) |
439 apply (auto simp add: abs_le_interval_iff) |
439 apply (auto simp add: abs_le_interval_iff) |
440 apply (simp add: right_diff_distrib, arith) |
440 apply (simp add: right_diff_distrib, arith) |