--- a/src/HOL/Transcendental.thy Sat Feb 03 20:46:28 2018 +0100
+++ b/src/HOL/Transcendental.thy Mon Feb 05 08:30:19 2018 +0100
@@ -2495,6 +2495,9 @@
for x y :: real
by (simp add: powr_def)
+lemma powr_non_neg[simp]: "\<not>a powr x < 0" for a x::real
+ using powr_ge_pzero[of a x] by arith
+
lemma powr_divide: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powr a = (x powr a) / (y powr a)"
for a b x :: real
apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult)
@@ -2606,6 +2609,10 @@
for a x :: real
by (simp add: powr_def)
+lemma powr_nonneg_iff[simp]: "a powr x \<le> 0 \<longleftrightarrow> a = 0"
+ for a x::real
+ by (meson not_less powr_gt_zero)
+
lemma log_add_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log b x + y = log b (x * b powr y)"
and add_log_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> y + log b x = log b (b powr y * x)"
and log_minus_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log b x - y = log b (x * b powr -y)"