equal
deleted
inserted
replaced
797 by (auto simp add: inner_diff_left) |
797 by (auto simp add: inner_diff_left) |
798 also have "\<dots> \<le> norm (f b - f a) * norm (f' x (b - a))" |
798 also have "\<dots> \<le> norm (f b - f a) * norm (f' x (b - a))" |
799 by (rule norm_cauchy_schwarz) |
799 by (rule norm_cauchy_schwarz) |
800 finally show ?thesis |
800 finally show ?thesis |
801 using False x(1) |
801 using False x(1) |
802 by (auto simp add: real_mult_left_cancel) |
802 by (auto simp add: mult_left_cancel) |
803 next |
803 next |
804 case True |
804 case True |
805 then show ?thesis |
805 then show ?thesis |
806 using assms(1) |
806 using assms(1) |
807 apply (rule_tac x="(a + b) /2" in bexI) |
807 apply (rule_tac x="(a + b) /2" in bexI) |