src/HOL/Deriv.thy
changeset 37891 c26f9d06e82c
parent 37888 d78a3cdbd615
child 41368 8afa26855137
equal deleted inserted replaced
37890:aae46a9ef66c 37891:c26f9d06e82c
  1253   shows "f a \<le> f b"
  1253   shows "f a \<le> f b"
  1254 proof (rule ccontr, cases "a = b")
  1254 proof (rule ccontr, cases "a = b")
  1255   assume "~ f a \<le> f b"
  1255   assume "~ f a \<le> f b"
  1256   assume "a = b"
  1256   assume "a = b"
  1257   with prems show False by auto
  1257   with prems show False by auto
  1258   next assume "~ f a \<le> f b"
  1258 next
  1259   assume "a ~= b"
  1259   assume A: "~ f a \<le> f b"
       
  1260   assume B: "a ~= b"
  1260   with assms have "EX l z. a < z & z < b & DERIV f z :> l
  1261   with assms have "EX l z. a < z & z < b & DERIV f z :> l
  1261       & f b - f a = (b - a) * l"
  1262       & f b - f a = (b - a) * l"
  1262     apply -
  1263     apply -
  1263     apply (rule MVT)
  1264     apply (rule MVT)
  1264       apply auto
  1265       apply auto
  1265       apply (metis DERIV_isCont)
  1266       apply (metis DERIV_isCont)
  1266      apply (metis differentiableI less_le)
  1267      apply (metis differentiableI less_le)
  1267     done
  1268     done
  1268   then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
  1269   then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
  1269       and "f b - f a = (b - a) * l"
  1270       and C: "f b - f a = (b - a) * l"
  1270     by auto
  1271     by auto
  1271   from prems have "~(l >= 0)"
  1272   with A have "a < b" "f b < f a" by auto
  1272     by (metis diff_self diff_eq_diff_less_eq le_iff_diff_le_0 order_antisym linear
  1273   with C have "\<not> l \<ge> 0" by (auto simp add: not_le algebra_simps)
  1273               split_mult_pos_le)
  1274     (metis A add_le_cancel_right assms(1) less_eq_real_def mult_right_mono real_add_left_mono real_le_linear real_le_refl)
  1274   with prems show False
  1275   with prems show False
  1275     by (metis DERIV_unique order_less_imp_le)
  1276     by (metis DERIV_unique order_less_imp_le)
  1276 qed
  1277 qed
  1277 
  1278 
  1278 lemma DERIV_neg_imp_decreasing:
  1279 lemma DERIV_neg_imp_decreasing: