# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1675779008 0
# Node ID 0cdb384bf56a5ed4246689c9e7b0da333622eea8
# Parent  8f2e6186408f742cad316846deb482f0d7bdaf18
More new theorems from the number theory development

diff -r 8f2e6186408f -r 0cdb384bf56a src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Feb 07 14:10:08 2023 +0000
@@ -245,6 +245,22 @@
   shows   "(\<lambda>x. cos (f x)) holomorphic_on A"
   using holomorphic_on_compose[OF assms holomorphic_on_cos] by (simp add: o_def)
 
+lemma analytic_on_sin [analytic_intros]: "sin analytic_on A"
+  using analytic_on_holomorphic holomorphic_on_sin by blast
+
+lemma analytic_on_sin' [analytic_intros]:
+  "f analytic_on A \<Longrightarrow> (\<And>z. z \<in> A \<Longrightarrow> f z \<notin> range (\<lambda>n. complex_of_real pi * of_int n)) \<Longrightarrow>
+   (\<lambda>z. sin (f z)) analytic_on A"
+  using analytic_on_compose_gen[OF _ analytic_on_sin[of UNIV], of f A] by (simp add: o_def)
+
+lemma analytic_on_cos [analytic_intros]: "cos analytic_on A"
+  using analytic_on_holomorphic holomorphic_on_cos by blast
+
+lemma analytic_on_cos' [analytic_intros]:
+  "f analytic_on A \<Longrightarrow> (\<And>z. z \<in> A \<Longrightarrow> f z \<notin> range (\<lambda>n. complex_of_real pi * of_int n)) \<Longrightarrow>
+   (\<lambda>z. cos (f z)) analytic_on A"
+  using analytic_on_compose_gen[OF _ analytic_on_cos[of UNIV], of f A] by (simp add: o_def)
+
 subsection\<^marker>\<open>tag unimportant\<close>\<open>More on the Polar Representation of Complex Numbers\<close>
 
 lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)"
@@ -3160,6 +3176,9 @@
     by simp
 qed
 
+lemma csqrt_conv_powr: "csqrt z = z powr (1/2)"
+  by (auto simp: csqrt_exp_Ln powr_def)
+
 lemma csqrt_mult:
   assumes "Arg z + Arg w \<in> {-pi<..pi}"
   shows   "csqrt (z * w) = csqrt z * csqrt w"
@@ -3237,12 +3256,27 @@
   by (simp add: field_differentiable_imp_continuous_at field_differentiable_within_csqrt)
 
 lemma continuous_on_csqrt [continuous_intros]:
-    "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on s csqrt"
+    "continuous_on (-\<real>\<^sub>\<le>\<^sub>0) csqrt"
   by (simp add: continuous_at_imp_continuous_on continuous_within_csqrt)
 
-lemma holomorphic_on_csqrt:
-    "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> csqrt holomorphic_on s"
-  by (simp add: field_differentiable_within_csqrt holomorphic_on_def)
+lemma holomorphic_on_csqrt [holomorphic_intros]: "csqrt holomorphic_on -\<real>\<^sub>\<le>\<^sub>0"
+proof -
+  have *: "(\<lambda>z. exp (ln z / 2)) holomorphic_on -\<real>\<^sub>\<le>\<^sub>0"
+    by (intro holomorphic_intros) auto
+  then show ?thesis
+    using field_differentiable_within_csqrt holomorphic_on_def by auto
+qed
+
+lemma holomorphic_on_csqrt' [holomorphic_intros]:
+  "f holomorphic_on A \<Longrightarrow> (\<And>z. z \<in> A \<Longrightarrow> f z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> (\<lambda>z. csqrt (f z)) holomorphic_on A"
+  using holomorphic_on_compose_gen[OF _ holomorphic_on_csqrt, of f A] by (auto simp: o_def)
+
+lemma analytic_on_csqrt [analytic_intros]: "csqrt analytic_on -\<real>\<^sub>\<le>\<^sub>0"
+  using holomorphic_on_csqrt by (subst analytic_on_open) auto
+
+lemma analytic_on_csqrt' [analytic_intros]:
+  "f analytic_on A \<Longrightarrow> (\<And>z. z \<in> A \<Longrightarrow> f z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> (\<lambda>z. csqrt (f z)) analytic_on A"
+  using analytic_on_compose_gen[OF _ analytic_on_csqrt, of f A] by (auto simp: o_def)
 
 lemma continuous_within_closed_nontrivial:
     "closed s \<Longrightarrow> a \<notin> s ==> continuous (at a within s) f"
diff -r 8f2e6186408f -r 0cdb384bf56a src/HOL/Analysis/FPS_Convergence.thy
--- a/src/HOL/Analysis/FPS_Convergence.thy	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/HOL/Analysis/FPS_Convergence.thy	Tue Feb 07 14:10:08 2023 +0000
@@ -624,6 +624,10 @@
 
 named_theorems fps_expansion_intros
 
+lemma has_fps_expansion_schematicI:
+  "f has_fps_expansion A \<Longrightarrow> A = B \<Longrightarrow> f has_fps_expansion B"
+  by simp
+
 lemma fps_nth_fps_expansion:
   fixes f :: "complex \<Rightarrow> complex"
   assumes "f has_fps_expansion F"
diff -r 8f2e6186408f -r 0cdb384bf56a src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Feb 07 14:10:08 2023 +0000
@@ -105,7 +105,7 @@
   by (intro enn2real_mono emeasure_mono) (auto simp: emeasure_lborel_cbox_eq)
 
 lemma content_lt_nz: "0 < content (cbox a b) \<longleftrightarrow> content (cbox a b) \<noteq> 0"
-  unfolding content_pos_lt_eq content_eq_0 unfolding not_ex not_le by fastforce
+  by (fact zero_less_measure_iff)
 
 lemma content_Pair: "content (cbox (a,c) (b,d)) = content (cbox a b) * content (cbox c d)"
   unfolding measure_lborel_cbox_eq Basis_prod_def
@@ -534,11 +534,23 @@
   shows "(f has_integral y) S \<Longrightarrow> ((\<lambda>x. f x * c) has_integral (y * c)) S"
   using has_integral_linear[OF _ bounded_linear_mult_left] by (simp add: comp_def)
 
+lemma integrable_on_mult_left:
+  fixes c :: "'a :: real_normed_algebra"
+  assumes "f integrable_on A"
+  shows   "(\<lambda>x. f x * c) integrable_on A"
+  using assms has_integral_mult_left by blast
+
 lemma has_integral_divide:
   fixes c :: "_ :: real_normed_div_algebra"
   shows "(f has_integral y) S \<Longrightarrow> ((\<lambda>x. f x / c) has_integral (y / c)) S"
   unfolding divide_inverse by (simp add: has_integral_mult_left)
 
+lemma integrable_on_divide:
+  fixes c :: "'a :: real_normed_div_algebra"
+  assumes "f integrable_on A"
+  shows   "(\<lambda>x. f x / c) integrable_on A"
+  using assms has_integral_divide by blast
+
 text\<open>The case analysis eliminates the condition \<^term>\<open>f integrable_on S\<close> at the cost
      of the type class constraint \<open>division_ring\<close>\<close>
 corollary integral_mult_left [simp]:
@@ -567,9 +579,35 @@
 
 lemma has_integral_mult_right:
   fixes c :: "'a :: real_normed_algebra"
-  shows "(f has_integral y) i \<Longrightarrow> ((\<lambda>x. c * f x) has_integral (c * y)) i"
+  shows "(f has_integral y) A \<Longrightarrow> ((\<lambda>x. c * f x) has_integral (c * y)) A"
   using has_integral_linear[OF _ bounded_linear_mult_right] by (simp add: comp_def)
 
+lemma integrable_on_mult_right:
+  fixes c :: "'a :: real_normed_algebra"
+  assumes "f integrable_on A"
+  shows   "(\<lambda>x. c * f x) integrable_on A"
+  using assms has_integral_mult_right by blast
+
+lemma integrable_on_mult_right_iff [simp]:
+  fixes c :: "'a :: real_normed_field"
+  assumes "c \<noteq> 0"
+  shows   "(\<lambda>x. c * f x) integrable_on A \<longleftrightarrow> f integrable_on A"
+    using integrable_on_mult_right[of f A c]
+          integrable_on_mult_right[of "\<lambda>x. c * f x" A "inverse c"] assms
+    by (auto simp: field_simps)
+
+lemma integrable_on_mult_left_iff [simp]:
+  fixes c :: "'a :: real_normed_field"
+  assumes "c \<noteq> 0"
+  shows   "(\<lambda>x. f x * c) integrable_on A \<longleftrightarrow> f integrable_on A"
+  using integrable_on_mult_right_iff[OF assms, of f A] by (simp add: mult.commute)
+
+lemma integrable_on_div_iff [simp]:
+  fixes c :: "'a :: real_normed_field"
+  assumes "c \<noteq> 0"
+  shows   "(\<lambda>x. f x / c) integrable_on A \<longleftrightarrow> f integrable_on A"
+  using integrable_on_mult_right_iff[of "inverse c" f A] assms by (simp add: field_simps)
+
 lemma has_integral_cmul: "(f has_integral k) S \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) S"
   unfolding o_def[symmetric]
   by (metis has_integral_linear bounded_linear_scaleR_right)
@@ -578,14 +616,7 @@
   fixes c :: real
   assumes "c \<noteq> 0 \<Longrightarrow> (f has_integral x) A"
   shows "((\<lambda>x. c * f x) has_integral c * x) A"
-proof (cases "c = 0")
-  case True
-  then show ?thesis by simp
-next
-  case False
-  from has_integral_cmul[OF assms[OF this], of c] show ?thesis
-    unfolding real_scaleR_def .
-qed
+  by (metis assms has_integral_is_0 has_integral_mult_right lambda_zero)
 
 lemma has_integral_neg: "(f has_integral k) S \<Longrightarrow> ((\<lambda>x. -(f x)) has_integral -k) S"
   by (drule_tac c="-1" in has_integral_cmul) auto
@@ -5028,6 +5059,15 @@
   shows "integral(box a b) f = integral(cbox a b) f"
   by (metis has_integral_integrable_integral has_integral_open_interval not_integrable_integral)
 
+lemma integrable_on_open_interval_real:
+  fixes f :: "real \<Rightarrow> 'b :: banach"
+  shows "f integrable_on {a<..<b} \<longleftrightarrow> f integrable_on {a..b}"
+  using integrable_on_open_interval[of f a b] by simp
+
+lemma integral_open_interval_real:
+  "integral {a..b} (f :: real \<Rightarrow> 'a :: banach) = integral {a<..<(b::real)} f"
+  using integral_open_interval[of a b f] by simp
+
 lemma has_integral_Icc_iff_Ioo:
   fixes f :: "real \<Rightarrow> 'a :: banach"
   shows "(f has_integral I) {a..b} \<longleftrightarrow> (f has_integral I) {a<..<b}"
diff -r 8f2e6186408f -r 0cdb384bf56a src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/HOL/Analysis/Path_Connected.thy	Tue Feb 07 14:10:08 2023 +0000
@@ -3375,6 +3375,12 @@
       shows "closure(outside S) \<subseteq> S \<union> outside S"
   by (metis assms closed_open closure_minimal inside_outside open_inside sup_ge2)
 
+lemma closed_path_image_Un_inside:
+  fixes g :: "real \<Rightarrow> 'a :: real_normed_vector"
+  assumes "path g"
+  shows   "closed (path_image g \<union> inside (path_image g))"
+  by (simp add: assms closed_Compl closed_path_image open_outside union_with_inside)
+
 lemma frontier_outside_subset:
   fixes S :: "'a::real_normed_vector set"
   assumes "closed S"
diff -r 8f2e6186408f -r 0cdb384bf56a src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/HOL/Complex.thy	Tue Feb 07 14:10:08 2023 +0000
@@ -1297,6 +1297,11 @@
         field_simps real_sqrt_mult[symmetric] real_sqrt_divide)
 qed
 
+lemma csqrt_power_even:
+  assumes "even n"
+  shows   "csqrt z ^ n = z ^ (n div 2)"
+  by (metis assms dvd_mult_div_cancel power2_csqrt power_mult)
+
 lemma norm_csqrt [simp]: "norm (csqrt z) = sqrt (norm z)"
   by (metis abs_of_nonneg norm_ge_zero norm_mult power2_csqrt power2_eq_square real_sqrt_abs)
 
diff -r 8f2e6186408f -r 0cdb384bf56a src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/HOL/Filter.thy	Tue Feb 07 14:10:08 2023 +0000
@@ -1287,6 +1287,10 @@
 translations
   "LIM x F1. f :> F2" == "CONST filterlim (\<lambda>x. f) F2 F1"
 
+lemma filterlim_filtercomapI: "filterlim f F G \<Longrightarrow> filterlim (\<lambda>x. f (g x)) F (filtercomap g G)"
+  unfolding filterlim_def
+  by (metis order_trans filtermap_filtercomap filtermap_filtermap filtermap_mono)
+
 lemma filterlim_top [simp]: "filterlim f top F"
   by (simp add: filterlim_def)
 
diff -r 8f2e6186408f -r 0cdb384bf56a src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/HOL/Limits.thy	Tue Feb 07 14:10:08 2023 +0000
@@ -1270,6 +1270,13 @@
   shows "continuous_on s (\<lambda>x. power_int (f x) n)"
   using assms unfolding continuous_on_def by (blast intro: tendsto_power_int)
 
+lemma tendsto_power_int' [tendsto_intros]:
+  fixes a :: "'a::real_normed_div_algebra"
+  assumes f: "(f \<longlongrightarrow> a) F"
+    and a: "a \<noteq> 0 \<or> n \<ge> 0"
+  shows "((\<lambda>x. power_int (f x) n) \<longlongrightarrow> power_int a n) F"
+  using assms by (cases n rule: int_cases4) (auto intro!: tendsto_intros simp: power_int_minus)
+
 lemma tendsto_sgn [tendsto_intros]: "(f \<longlongrightarrow> l) F \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> ((\<lambda>x. sgn (f x)) \<longlongrightarrow> sgn l) F"
   for l :: "'a::real_normed_vector"
   unfolding sgn_div_norm by (simp add: tendsto_intros)
@@ -1782,6 +1789,22 @@
     by (subst filterlim_inverse_at_iff[symmetric]) simp_all
 qed
 
+lemma filterlim_power_int_neg_at_infinity:
+  fixes f :: "_ \<Rightarrow> 'a::{real_normed_div_algebra, division_ring}"
+  assumes "n < 0" and lim: "(f \<longlongrightarrow> 0) F" and ev: "eventually (\<lambda>x. f x \<noteq> 0) F"
+  shows   "filterlim (\<lambda>x. f x powi n) at_infinity F"
+proof -
+  have lim': "((\<lambda>x. f x ^ nat (- n)) \<longlongrightarrow> 0) F"
+    by (rule tendsto_eq_intros lim)+ (use \<open>n < 0\<close> in auto)
+  have ev': "eventually (\<lambda>x. f x ^ nat (-n) \<noteq> 0) F"
+    using ev by eventually_elim (use \<open>n < 0\<close> in auto)
+  have "filterlim (\<lambda>x. inverse (f x ^ nat (-n))) at_infinity F"
+    by (intro filterlim_compose[OF filterlim_inverse_at_infinity])
+       (use lim' ev' in \<open>auto simp: filterlim_at\<close>)
+  thus ?thesis
+    using \<open>n < 0\<close> by (simp add: power_int_def power_inverse)
+qed
+  
 lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) \<longlongrightarrow> 0) F"
   by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
 
@@ -1937,6 +1960,13 @@
   using c filterlim_tendsto_pos_mult_at_top[of "\<lambda>x. - f x" "- c" F, OF _ _ g]
   unfolding filterlim_uminus_at_bot tendsto_minus_cancel_left by simp
 
+
+lemma filterlim_cmult_at_bot_at_top:
+  assumes "filterlim (h :: _ \<Rightarrow> real) at_top F" "c \<noteq> 0" "G = (if c > 0 then at_top else at_bot)"
+  shows   "filterlim (\<lambda>x. c * h x) G F"
+  using assms filterlim_tendsto_pos_mult_at_top[OF tendsto_const[of c], of h F]
+              filterlim_tendsto_neg_mult_at_bot[OF tendsto_const[of c], of h F] by simp
+
 lemma filterlim_pow_at_top:
   fixes f :: "'a \<Rightarrow> real"
   assumes "0 < n"
@@ -2688,10 +2718,9 @@
   assumes "0 \<le> x" "x < 1"
   shows "(\<lambda>n. x ^ n) \<longlonglongrightarrow> 0"
 proof (cases "x = 0")
-  case False
-  with \<open>0 \<le> x\<close> have x0: "0 < x" by simp
-  then have "1 < inverse x"
-    using \<open>x < 1\<close> by (rule one_less_inverse)
+  case False 
+  with \<open>0 \<le> x\<close> have "1 < inverse x"
+    using \<open>x < 1\<close> by (simp add: one_less_inverse)
   then have "(\<lambda>n. inverse (inverse x ^ n)) \<longlonglongrightarrow> 0"
     by (rule LIMSEQ_inverse_realpow_zero)
   then show ?thesis by (simp add: power_inverse)
diff -r 8f2e6186408f -r 0cdb384bf56a src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/HOL/Real_Vector_Spaces.thy	Tue Feb 07 14:10:08 2023 +0000
@@ -986,6 +986,9 @@
   for a b :: "'a::{real_normed_field,field}"
   by (simp add: divide_inverse norm_mult norm_inverse)
 
+lemma dist_divide_right: "dist (a/c) (b/c) = dist a b / norm c" for c :: "'a :: real_normed_field"
+  by (metis diff_divide_distrib dist_norm norm_divide)
+
 lemma norm_inverse_le_norm:
   fixes x :: "'a::real_normed_div_algebra"
   shows "r \<le> norm x \<Longrightarrow> 0 < r \<Longrightarrow> norm (inverse x) \<le> inverse r"
@@ -1134,7 +1137,6 @@
   finally show ?thesis .
 qed
 
-
 subsection \<open>Metric spaces\<close>
 
 class metric_space = uniformity_dist + open_uniformity +
diff -r 8f2e6186408f -r 0cdb384bf56a src/HOL/Series.thy
--- a/src/HOL/Series.thy	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/HOL/Series.thy	Tue Feb 07 14:10:08 2023 +0000
@@ -860,6 +860,26 @@
 
 end
 
+text \<open>Application to convergence of the log function\<close>
+lemma norm_summable_ln_series:
+  fixes z :: "'a :: {real_normed_field, banach}"
+  assumes "norm z < 1"
+  shows   "summable (\<lambda>n. norm (z ^ n / of_nat n))"
+proof (rule summable_comparison_test)
+  show "summable (\<lambda>n. norm (z ^ n))"
+    using assms unfolding norm_power by (intro summable_geometric) auto
+  have "norm z ^ n / real n \<le> norm z ^ n" for n
+  proof (cases "n = 0")
+    case False
+    hence "norm z ^ n * 1 \<le> norm z ^ n * real n"
+      by (intro mult_left_mono) auto
+    thus ?thesis
+      using False by (simp add: field_simps)
+  qed auto
+  thus "\<exists>N. \<forall>n\<ge>N. norm (norm (z ^ n / of_nat n)) \<le> norm (z ^ n)"
+    by (intro exI[of _ 0]) (auto simp: norm_power norm_divide)
+qed
+
 
 text \<open>Relations among convergence and absolute convergence for power series.\<close>
 
diff -r 8f2e6186408f -r 0cdb384bf56a src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/HOL/Transcendental.thy	Tue Feb 07 14:10:08 2023 +0000
@@ -6731,14 +6731,6 @@
 
 subsubsection \<open>More specific properties of the real functions\<close>
 
-lemma sinh_real_zero_iff [simp]: "sinh (x::real) = 0 \<longleftrightarrow> x = 0"
-proof -
-  have "(-1 :: real) < 0" by simp
-  also have "0 < exp x" by simp
-  finally have "exp x \<noteq> -1" by (intro notI) simp
-  thus ?thesis by (subst sinh_zero_iff) simp
-qed
-
 lemma plus_inverse_ge_2:
   fixes x :: real
   assumes "x > 0"
@@ -6773,21 +6765,6 @@
 lemma cosh_real_nonzero [simp]: "cosh (x :: real) \<noteq> 0"
   using cosh_real_ge_1[of x] by simp
 
-lemma tanh_real_nonneg_iff [simp]: "tanh (x :: real) \<ge> 0 \<longleftrightarrow> x \<ge> 0"
-  by (simp add: tanh_def field_simps)
-
-lemma tanh_real_pos_iff [simp]: "tanh (x :: real) > 0 \<longleftrightarrow> x > 0"
-  by (simp add: tanh_def field_simps)
-
-lemma tanh_real_nonpos_iff [simp]: "tanh (x :: real) \<le> 0 \<longleftrightarrow> x \<le> 0"
-  by (simp add: tanh_def field_simps)
-
-lemma tanh_real_neg_iff [simp]: "tanh (x :: real) < 0 \<longleftrightarrow> x < 0"
-  by (simp add: tanh_def field_simps)
-
-lemma tanh_real_zero_iff [simp]: "tanh (x :: real) = 0 \<longleftrightarrow> x = 0"
-  by (simp add: tanh_def field_simps)
-
 lemma arsinh_real_def: "arsinh (x::real) = ln (x + sqrt (x^2 + 1))"
   by (simp add: arsinh_def powr_half_sqrt)
 
@@ -6860,8 +6837,29 @@
   finally show ?thesis .
 qed
 
+lemma sinh_real_zero_iff [simp]: "sinh x = 0 \<longleftrightarrow> x = 0"
+  by (metis arsinh_0 arsinh_sinh_real sinh_0)
+
+lemma cosh_real_one_iff [simp]: "cosh x = 1 \<longleftrightarrow> x = 0"
+  by (smt (verit, best) Transcendental.arcosh_cosh_real cosh_0 cosh_minus)
+
+lemma tanh_real_nonneg_iff [simp]: "tanh x \<ge> 0 \<longleftrightarrow> x \<ge> 0"
+  by (simp add: tanh_def field_simps)
+
+lemma tanh_real_pos_iff [simp]: "tanh x > 0 \<longleftrightarrow> x > 0"
+  by (simp add: tanh_def field_simps)
+
+lemma tanh_real_nonpos_iff [simp]: "tanh x \<le> 0 \<longleftrightarrow> x \<le> 0"
+  by (simp add: tanh_def field_simps)
+
+lemma tanh_real_neg_iff [simp]: "tanh x < 0 \<longleftrightarrow> x < 0"
+  by (simp add: tanh_def field_simps)
+
+lemma tanh_real_zero_iff [simp]: "tanh x = 0 \<longleftrightarrow> x = 0"
+  by (simp add: tanh_def field_simps)
+
 end
-
+  
 lemma sinh_real_strict_mono: "strict_mono (sinh :: real \<Rightarrow> real)"
   by (rule pos_deriv_imp_strict_mono derivative_intros)+ auto