equal
deleted
inserted
replaced
319 next |
319 next |
320 case False then have "0 \<le> a" by auto |
320 case False then have "0 \<le> a" by auto |
321 with \<open>a \<le> b\<close> show ?thesis using power_mono by auto |
321 with \<open>a \<le> b\<close> show ?thesis using power_mono by auto |
322 qed |
322 qed |
323 qed |
323 qed |
324 |
324 |
|
325 lemma (in comm_ring_1) uminus_power_if: "(- x) ^ n = (if even n then x^n else - (x ^ n))" |
|
326 by auto |
|
327 |
325 text \<open>Simplify, when the exponent is a numeral\<close> |
328 text \<open>Simplify, when the exponent is a numeral\<close> |
326 |
329 |
327 lemma zero_le_power_eq_numeral [simp]: |
330 lemma zero_le_power_eq_numeral [simp]: |
328 "0 \<le> a ^ numeral w \<longleftrightarrow> even (numeral w :: nat) \<or> odd (numeral w :: nat) \<and> 0 \<le> a" |
331 "0 \<le> a ^ numeral w \<longleftrightarrow> even (numeral w :: nat) \<or> odd (numeral w :: nat) \<and> 0 \<le> a" |
329 by (fact zero_le_power_eq) |
332 by (fact zero_le_power_eq) |