--- a/src/HOL/Analysis/Interval_Integral.thy Sun Jul 15 18:22:31 2018 +0100
+++ b/src/HOL/Analysis/Interval_Integral.thy Sun Jul 15 21:58:50 2018 +0100
@@ -863,10 +863,10 @@
have lle[simp]: "\<And>i j. i \<le> j \<Longrightarrow> l j \<le> l i" by (rule decseqD, rule approx)
have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> u i \<le> u j" by (rule incseqD, rule approx)
have g_nondec [simp]: "g x \<le> g y" if "a < x" "x \<le> y" "y < b" for x y
- proof (rule DERIV_nonneg_imp_nondecreasing [OF \<open>x \<le> y\<close>], intro exI conjI allI impI)
- show "\<And>u. x \<le> u \<and> u \<le> y \<Longrightarrow> (g has_real_derivative g' u) (at u)"
+ proof (rule DERIV_nonneg_imp_nondecreasing [OF \<open>x \<le> y\<close>], intro exI conjI)
+ show "\<And>u. x \<le> u \<Longrightarrow> u \<le> y \<Longrightarrow> (g has_real_derivative g' u) (at u)"
by (meson deriv_g ereal_less_eq(3) le_less_trans less_le_trans that)
- show "\<And>u. x \<le> u \<and> u \<le> y \<Longrightarrow> 0 \<le> g' u"
+ show "\<And>u. x \<le> u \<Longrightarrow> u \<le> y \<Longrightarrow> 0 \<le> g' u"
by (meson assms(5) dual_order.trans le_ereal_le less_imp_le order_refl that)
qed
have "A \<le> B" and un: "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
@@ -960,10 +960,10 @@
have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> l j \<le> l i" by (rule decseqD, rule approx)
have uleu[simp]: "\<And>i j. i \<le> j \<Longrightarrow> u i \<le> u j" by (rule incseqD, rule approx)
have g_nondec [simp]: "g x \<le> g y" if "a < x" "x \<le> y" "y < b" for x y
- proof (rule DERIV_nonneg_imp_nondecreasing [OF \<open>x \<le> y\<close>], intro exI conjI allI impI)
- show "\<And>u. x \<le> u \<and> u \<le> y \<Longrightarrow> (g has_real_derivative g' u) (at u)"
+ proof (rule DERIV_nonneg_imp_nondecreasing [OF \<open>x \<le> y\<close>], intro exI conjI)
+ show "\<And>u. x \<le> u \<Longrightarrow> u \<le> y \<Longrightarrow> (g has_real_derivative g' u) (at u)"
by (meson deriv_g ereal_less_eq(3) le_less_trans less_le_trans that)
- show "\<And>u. x \<le> u \<and> u \<le> y \<Longrightarrow> 0 \<le> g' u"
+ show "\<And>u. x \<le> u \<Longrightarrow> u \<le> y \<Longrightarrow> 0 \<le> g' u"
by (meson g'_nonneg less_ereal.simps(1) less_trans not_less that)
qed
have "A \<le> B" and un: "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
--- a/src/HOL/Deriv.thy Sun Jul 15 18:22:31 2018 +0100
+++ b/src/HOL/Deriv.thy Sun Jul 15 21:58:50 2018 +0100
@@ -1372,8 +1372,8 @@
theorem MVT:
fixes a b :: real
assumes lt: "a < b"
- and con: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"
- and dif [rule_format]: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable (at x)"
+ and con: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont f x"
+ and dif: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> f differentiable (at x)"
shows "\<exists>l z. a < z \<and> z < b \<and> DERIV f z :> l \<and> f b - f a = (b - a) * l"
proof -
let ?F = "\<lambda>x. f x - ((f b - f a) / (b - a)) * x"
@@ -1384,7 +1384,7 @@
fix x :: real
assume x: "a < x" "x < b"
obtain l where der: "DERIV f x :> l"
- using differentiableD [OF dif [OF conjI [OF x]]] ..
+ using differentiableD [OF dif] x by blast
show "?F differentiable (at x)"
by (rule differentiableI [where D = "l - (f b - f a) / (b - a)"],
blast intro: DERIV_diff DERIV_cmult_Id der)
@@ -1413,9 +1413,9 @@
(f has_real_derivative l) (at z) \<and>
f b - f a = (b - a) * l"
proof (rule MVT [OF \<open>a < b\<close>])
- show "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"
+ show "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont f x"
using assms by (blast intro: DERIV_isCont)
- show "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable at x"
+ show "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> f differentiable (at x)"
using assms by (force dest: order_less_imp_le simp add: real_differentiable_def)
qed
with assms show ?thesis
@@ -1441,34 +1441,21 @@
lemma DERIV_isconst_end:
fixes f :: "real \<Rightarrow> real"
- shows "a < b \<Longrightarrow>
- \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow>
- \<forall>x. a < x \<and> x < b \<longrightarrow> DERIV f x :> 0 \<Longrightarrow> f b = f a"
- apply (drule (1) MVT)
- apply (blast intro: differentiableI)
- apply (auto dest!: DERIV_unique simp add: diff_eq_eq)
- done
-
-lemma DERIV_isconst1:
- fixes f :: "real \<Rightarrow> real"
- shows "a < b \<Longrightarrow>
- \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow>
- \<forall>x. a < x \<and> x < b \<longrightarrow> DERIV f x :> 0 \<Longrightarrow>
- \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x = f a"
- apply safe
- apply (drule_tac x = a in order_le_imp_less_or_eq)
- apply safe
- apply (drule_tac b = x in DERIV_isconst_end)
- apply auto
- done
+ assumes "a < b" and contf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont f x"
+ and 0: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> DERIV f x :> 0"
+ shows "f b = f a"
+ using MVT [OF \<open>a < b\<close>] "0" DERIV_unique contf real_differentiable_def by fastforce
lemma DERIV_isconst2:
fixes f :: "real \<Rightarrow> real"
- shows "a < b \<Longrightarrow>
- \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow>
- \<forall>x. a < x \<and> x < b \<longrightarrow> DERIV f x :> 0 \<Longrightarrow>
- a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> f x = f a"
- by (blast dest: DERIV_isconst1)
+ assumes "a < b" "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont f x" "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> DERIV f x :> 0"
+ and "a \<le> x" "x \<le> b"
+shows "f x = f a"
+proof (cases "x=a")
+ case False
+ show ?thesis
+ by (rule DERIV_isconst_end [where f=f]) (use False assms in auto)
+qed auto
lemma DERIV_isconst3:
fixes a b x y :: real
@@ -1482,17 +1469,15 @@
let ?a = "min x y"
let ?b = "max x y"
- have "\<forall>z. ?a \<le> z \<and> z \<le> ?b \<longrightarrow> DERIV f z :> 0"
- proof (rule allI, rule impI)
- fix z :: real
- assume "?a \<le> z \<and> z \<le> ?b"
- then have "a < z" and "z < b"
- using \<open>x \<in> {a <..< b}\<close> and \<open>y \<in> {a <..< b}\<close> by auto
+ have "DERIV f z :> 0" if "?a \<le> z" "z \<le> ?b" for z
+ proof -
+ have "a < z" and "z < b"
+ using that \<open>x \<in> {a <..< b}\<close> and \<open>y \<in> {a <..< b}\<close> by auto
then have "z \<in> {a<..<b}" by auto
then show "DERIV f z :> 0" by (rule derivable)
qed
- then have isCont: "\<forall>z. ?a \<le> z \<and> z \<le> ?b \<longrightarrow> isCont f z"
- and DERIV: "\<forall>z. ?a < z \<and> z < ?b \<longrightarrow> DERIV f z :> 0"
+ then have isCont: "\<And>z. \<lbrakk>?a \<le> z; z \<le> ?b\<rbrakk> \<Longrightarrow> isCont f z"
+ and DERIV: "\<And>z. \<lbrakk>?a < z; z < ?b\<rbrakk> \<Longrightarrow> DERIV f z :> 0"
using DERIV_isCont by auto
have "?a < ?b" using \<open>x \<noteq> y\<close> by auto
@@ -1509,20 +1494,24 @@
lemma DERIV_const_ratio_const:
fixes f :: "real \<Rightarrow> real"
- shows "a \<noteq> b \<Longrightarrow> \<forall>x. DERIV f x :> k \<Longrightarrow> f b - f a = (b - a) * k"
- apply (rule linorder_cases [of a b])
- apply auto
- apply (drule_tac [!] f = f in MVT)
- apply (auto dest: DERIV_isCont DERIV_unique simp: real_differentiable_def)
- apply (auto dest: DERIV_unique simp: ring_distribs)
- done
+ assumes "a \<noteq> b" and df: "\<And>x. DERIV f x :> k"
+ shows "f b - f a = (b - a) * k"
+proof (cases a b rule: linorder_cases)
+ case less
+ show ?thesis
+ using MVT [OF less] df by (auto dest: DERIV_isCont DERIV_unique simp: real_differentiable_def)
+next
+ case greater
+ show ?thesis
+ using MVT [OF greater] df
+ by (fastforce dest: DERIV_continuous DERIV_unique simp: real_differentiable_def algebra_simps)
+qed auto
lemma DERIV_const_ratio_const2:
fixes f :: "real \<Rightarrow> real"
- shows "a \<noteq> b \<Longrightarrow> \<forall>x. DERIV f x :> k \<Longrightarrow> (f b - f a) / (b - a) = k"
- apply (rule_tac c1 = "b-a" in mult_right_cancel [THEN iffD1])
- apply (auto dest!: DERIV_const_ratio_const simp add: mult.assoc)
- done
+ assumes "a \<noteq> b" and df: "\<And>x. DERIV f x :> k"
+ shows "(f b - f a) / (b - a) = k"
+ using DERIV_const_ratio_const [OF assms] \<open>a \<noteq> b\<close> by auto
lemma real_average_minus_first [simp]: "(a + b) / 2 - a = (b - a) / 2"
for a b :: real
@@ -1538,7 +1527,7 @@
fixes v :: "real \<Rightarrow> real"
and a b :: real
assumes neq: "a \<noteq> b"
- and der: "\<forall>x. DERIV v x :> k"
+ and der: "\<And>x. DERIV v x :> k"
shows "v ((a + b) / 2) = (v a + v b) / 2"
proof (cases rule: linorder_cases [of a b])
case equal
@@ -1598,7 +1587,7 @@
fixes a b :: real
and f :: "real \<Rightarrow> real"
assumes "a \<le> b"
- and "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> (\<exists>y. DERIV f x :> y \<and> y \<ge> 0)"
+ and "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> \<exists>y. DERIV f x :> y \<and> y \<ge> 0"
shows "f a \<le> f b"
proof (rule ccontr, cases "a = b")
assume "\<not> ?thesis" and "a = b"
@@ -1606,13 +1595,11 @@
next
assume *: "\<not> ?thesis"
assume "a \<noteq> b"
+ with \<open>a \<le> b\<close> have "a < b"
+ by linarith
with assms have "\<exists>l z. a < z \<and> z < b \<and> DERIV f z :> l \<and> f b - f a = (b - a) * l"
- apply -
- apply (rule MVT)
- apply auto
- apply (metis DERIV_isCont)
- apply (metis differentiableI less_le)
- done
+ by (metis (no_types) not_le not_less_iff_gr_or_eq
+ MVT [OF \<open>a < b\<close>, of f] DERIV_isCont [of f] differentiableI)
then obtain l z where lz: "a < z" "z < b" "DERIV f z :> l" and **: "f b - f a = (b - a) * l"
by auto
with * have "a < b" "f b < f a" by auto
@@ -1626,16 +1613,16 @@
fixes a b :: real
and f :: "real \<Rightarrow> real"
assumes "a < b"
- and "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (\<exists>y. DERIV f x :> y \<and> y < 0)"
+ and "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> \<exists>y. DERIV f x :> y \<and> y < 0"
and con: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x"
shows "f a > f b"
proof -
have "(\<lambda>x. -f x) a < (\<lambda>x. -f x) b"
- apply (rule DERIV_pos_imp_increasing_open [of a b "\<lambda>x. -f x"])
- using assms
- apply auto
- apply (metis field_differentiable_minus neg_0_less_iff_less)
- done
+ proof (rule DERIV_pos_imp_increasing_open [of a b])
+ show "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> \<exists>y. ((\<lambda>x. - f x) has_real_derivative y) (at x) \<and> 0 < y"
+ using assms
+ by simp (metis field_differentiable_minus neg_0_less_iff_less)
+ qed (use assms in auto)
then show ?thesis
by simp
qed
@@ -1644,7 +1631,7 @@
fixes a b :: real
and f :: "real \<Rightarrow> real"
assumes "a < b"
- and "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> (\<exists>y. DERIV f x :> y \<and> y < 0)"
+ and "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> \<exists>y. DERIV f x :> y \<and> y < 0"
shows "f a > f b"
by (metis DERIV_neg_imp_decreasing_open [of a b f] assms DERIV_continuous less_imp_le)
@@ -1652,15 +1639,11 @@
fixes a b :: real
and f :: "real \<Rightarrow> real"
assumes "a \<le> b"
- and "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> (\<exists>y. DERIV f x :> y \<and> y \<le> 0)"
+ and "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> \<exists>y. DERIV f x :> y \<and> y \<le> 0"
shows "f a \<ge> f b"
proof -
have "(\<lambda>x. -f x) a \<le> (\<lambda>x. -f x) b"
- apply (rule DERIV_nonneg_imp_nondecreasing [of a b "\<lambda>x. -f x"])
- using assms
- apply auto
- apply (metis DERIV_minus neg_0_le_iff_le)
- done
+ using DERIV_nonneg_imp_nondecreasing [of a b "\<lambda>x. -f x"] assms DERIV_minus by fastforce
then show ?thesis
by simp
qed
@@ -1672,11 +1655,9 @@
shows "flim < f b"
proof -
have "\<exists>N. \<forall>n\<le>N. f n \<le> f (b - 1)"
- apply (rule_tac x="b - 2" in exI)
- apply (force intro: order.strict_implies_order DERIV_pos_imp_increasing [where f=f] assms)
- done
+ by (rule_tac x="b - 2" in exI) (force intro: order.strict_implies_order DERIV_pos_imp_increasing assms)
then have "flim \<le> f (b - 1)"
- by (auto simp: trivial_limit_at_bot_linorder eventually_at_bot_linorder tendsto_upperbound [OF lim])
+ by (auto simp: eventually_at_bot_linorder tendsto_upperbound [OF lim])
also have "\<dots> < f b"
by (force intro: DERIV_pos_imp_increasing [where f=f] assms)
finally show ?thesis .
@@ -1684,7 +1665,7 @@
lemma DERIV_neg_imp_decreasing_at_top:
fixes f :: "real \<Rightarrow> real"
- assumes der: "\<And>x. x \<ge> b \<Longrightarrow> (\<exists>y. DERIV f x :> y \<and> y < 0)"
+ assumes der: "\<And>x. x \<ge> b \<Longrightarrow> \<exists>y. DERIV f x :> y \<and> y < 0"
and lim: "(f \<longlongrightarrow> flim) at_top"
shows "flim < f b"
apply (rule DERIV_pos_imp_increasing_at_bot [where f = "\<lambda>i. f (-i)" and b = "-b", simplified])
@@ -1755,9 +1736,9 @@
have "\<exists>l z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l"
proof (rule MVT)
from assms show "a < b" by simp
- show "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?h x"
+ show "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont ?h x"
using fc gc by simp
- show "\<forall>x. a < x \<and> x < b \<longrightarrow> ?h differentiable (at x)"
+ show "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> ?h differentiable (at x)"
using fd gd by simp
qed
then obtain l where l: "\<exists>z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" ..
@@ -1822,15 +1803,20 @@
lemma isCont_If_ge:
fixes a :: "'a :: linorder_topology"
- shows "continuous (at_left a) g \<Longrightarrow> (f \<longlongrightarrow> g a) (at_right a) \<Longrightarrow>
- isCont (\<lambda>x. if x \<le> a then g x else f x) a"
- unfolding isCont_def continuous_within
- apply (intro filterlim_split_at)
- apply (subst filterlim_cong[OF refl refl, where g=g])
- apply (simp_all add: eventually_at_filter less_le)
- apply (subst filterlim_cong[OF refl refl, where g=f])
- apply (simp_all add: eventually_at_filter less_le)
- done
+ assumes "continuous (at_left a) g" and f: "(f \<longlongrightarrow> g a) (at_right a)"
+ shows "isCont (\<lambda>x. if x \<le> a then g x else f x) a" (is "isCont ?gf a")
+proof -
+ have g: "(g \<longlongrightarrow> g a) (at_left a)"
+ using assms continuous_within by blast
+ show ?thesis
+ unfolding isCont_def continuous_within
+ proof (intro filterlim_split_at; simp)
+ show "(?gf \<longlongrightarrow> g a) (at_left a)"
+ by (subst filterlim_cong[OF refl refl, where g=g]) (simp_all add: eventually_at_filter less_le g)
+ show "(?gf \<longlongrightarrow> g a) (at_right a)"
+ by (subst filterlim_cong[OF refl refl, where g=f]) (simp_all add: eventually_at_filter less_le f)
+ qed
+qed
lemma lhopital_right_0:
fixes f0 g0 :: "real \<Rightarrow> real"
@@ -2089,19 +2075,11 @@
show "eventually (\<lambda>x. DERIV ?G x :> ?D g' x) ?R"
unfolding eventually_at_right_to_top
using Dg eventually_ge_at_top[where c=1]
- apply eventually_elim
- apply (rule DERIV_cong)
- apply (rule DERIV_chain'[where f=inverse])
- apply (auto intro!: DERIV_inverse)
- done
+ by eventually_elim (rule derivative_eq_intros DERIV_chain'[where f=inverse] | simp)+
show "eventually (\<lambda>x. DERIV ?F x :> ?D f' x) ?R"
unfolding eventually_at_right_to_top
using Df eventually_ge_at_top[where c=1]
- apply eventually_elim
- apply (rule DERIV_cong)
- apply (rule DERIV_chain'[where f=inverse])
- apply (auto intro!: DERIV_inverse)
- done
+ by eventually_elim (rule derivative_eq_intros DERIV_chain'[where f=inverse] | simp)+
show "eventually (\<lambda>x. ?D g' x \<noteq> 0) ?R"
unfolding eventually_at_right_to_top
using g' eventually_ge_at_top[where c=1]
--- a/src/HOL/Transcendental.thy Sun Jul 15 18:22:31 2018 +0100
+++ b/src/HOL/Transcendental.thy Sun Jul 15 21:58:50 2018 +0100
@@ -2236,7 +2236,7 @@
assume "1 < x"
from dense[OF this] obtain a where "1 < a" "a < x" by blast
from \<open>a < x\<close> have "?l x < ?l a"
- proof (rule DERIV_neg_imp_decreasing, safe)
+ proof (rule DERIV_neg_imp_decreasing)
fix y
assume "a \<le> y" "y \<le> x"
with \<open>1 < a\<close> have "1 / y - 1 < 0" "0 < y"
@@ -2367,10 +2367,8 @@
shows "x \<le> (exp x - inverse(exp x)) / 2"
proof -
have *: "exp a - inverse(exp a) - 2*a \<le> exp b - inverse(exp b) - 2*b" if "a \<le> b" for a b::real
- apply (rule DERIV_nonneg_imp_nondecreasing [OF that])
using exp_plus_inverse_exp
- apply (intro exI allI impI conjI derivative_eq_intros | force)+
- done
+ by (fastforce intro: derivative_eq_intros DERIV_nonneg_imp_nondecreasing [OF that])
show ?thesis
using*[OF assms] by simp
qed
@@ -2559,9 +2557,7 @@
by (simp add: log_def)
lemma log_inverse: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log a (inverse x) = - log a x"
- apply (rule add_left_cancel [THEN iffD1, where a1 = "log a x"])
- apply (simp add: log_mult [symmetric])
- done
+ using ln_inverse log_def by auto
lemma log_divide: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> log a (x/y) = log a x - log a y"
by (simp add: log_mult divide_inverse log_inverse)
@@ -3134,10 +3130,7 @@
show "eventually (\<lambda>xa. exp (ln (1 + x * xa) / xa) = (1 + x * xa) powr (1 / xa)) (at_right 0)"
unfolding eventually_at_right[OF zero_less_one]
using False
- apply (intro exI[of _ "1 / \<bar>x\<bar>"])
- apply (auto simp: field_simps powr_def abs_if)
- apply (metis add_less_same_cancel1 mult_less_0_iff not_less_iff_gr_or_eq zero_less_one)
- done
+ by (intro exI[of _ "1 / \<bar>x\<bar>"]) (auto simp: field_simps powr_def abs_if add_nonneg_eq_0_iff)
qed (simp_all add: at_eq_sup_left_right)
qed
@@ -5758,9 +5751,9 @@
qed
then have DERIV_in_rball: "\<forall>y. a \<le> y \<and> y \<le> b \<longrightarrow> DERIV (\<lambda>x. suminf (?c x) - arctan x) y :> 0"
using \<open>-r < a\<close> \<open>b < r\<close> by auto
- then show "\<forall>y. a < y \<and> y < b \<longrightarrow> DERIV (\<lambda>x. suminf (?c x) - arctan x) y :> 0"
+ then show "\<And>y. \<lbrakk>a < y; y < b\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. suminf (?c x) - arctan x) y :> 0"
using \<open>\<bar>x\<bar> < r\<close> by auto
- show "\<forall>y. a \<le> y \<and> y \<le> b \<longrightarrow> isCont (\<lambda>x. suminf (?c x) - arctan x) y"
+ show "\<And>y. \<lbrakk>a \<le> y; y \<le> b\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. suminf (?c x) - arctan x) y"
using DERIV_in_rball DERIV_isCont by auto
qed
qed