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: |