equal
deleted
inserted
replaced
519 mult_assoc [symmetric]) |
519 mult_assoc [symmetric]) |
520 apply (subgoal_tac "inverse (z - x) * (f z - f x - f' x * (z - x)) |
520 apply (subgoal_tac "inverse (z - x) * (f z - f x - f' x * (z - x)) |
521 = (f z - f x) / (z - x) - f' x") |
521 = (f z - f x) / (z - x) - f' x") |
522 apply (simp add: abs_mult [symmetric] mult_ac diff_minus) |
522 apply (simp add: abs_mult [symmetric] mult_ac diff_minus) |
523 apply (subst mult_commute) |
523 apply (subst mult_commute) |
524 apply (simp add: left_distrib diff_minus) |
524 apply (simp add: distrib_right diff_minus) |
525 apply (simp add: mult_assoc divide_inverse) |
525 apply (simp add: mult_assoc divide_inverse) |
526 apply (simp add: left_distrib) |
526 apply (simp add: distrib_right) |
527 done |
527 done |
528 |
528 |
529 lemma lemma_straddle: |
529 lemma lemma_straddle: |
530 assumes f': "\<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x)" and "0 < e" |
530 assumes f': "\<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x)" and "0 < e" |
531 shows "\<exists>g. gauge {a..b} g & |
531 shows "\<exists>g. gauge {a..b} g & |