642 by (simp add: le_less sum_power2_eq_zero_iff not_sum_power2_lt_zero) |
642 by (simp add: le_less sum_power2_eq_zero_iff not_sum_power2_lt_zero) |
643 |
643 |
644 lemma sum_power2_gt_zero_iff: |
644 lemma sum_power2_gt_zero_iff: |
645 "0 < x\<^sup>2 + y\<^sup>2 \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0" |
645 "0 < x\<^sup>2 + y\<^sup>2 \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0" |
646 unfolding not_le [symmetric] by (simp add: sum_power2_le_zero_iff) |
646 unfolding not_le [symmetric] by (simp add: sum_power2_le_zero_iff) |
|
647 |
|
648 lemma abs_le_square_iff: |
|
649 "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> x\<^sup>2 \<le> y\<^sup>2" |
|
650 proof |
|
651 assume "\<bar>x\<bar> \<le> \<bar>y\<bar>" |
|
652 then have "\<bar>x\<bar>\<^sup>2 \<le> \<bar>y\<bar>\<^sup>2" by (rule power_mono, simp) |
|
653 then show "x\<^sup>2 \<le> y\<^sup>2" by simp |
|
654 next |
|
655 assume "x\<^sup>2 \<le> y\<^sup>2" |
|
656 then show "\<bar>x\<bar> \<le> \<bar>y\<bar>" |
|
657 by (auto intro!: power2_le_imp_le [OF _ abs_ge_zero]) |
|
658 qed |
|
659 |
|
660 lemma abs_square_le_1:"x\<^sup>2 \<le> 1 \<longleftrightarrow> abs(x) \<le> 1" |
|
661 using abs_le_square_iff [of x 1] |
|
662 by simp |
|
663 |
|
664 lemma abs_square_eq_1: "x\<^sup>2 = 1 \<longleftrightarrow> abs(x) = 1" |
|
665 by (auto simp add: abs_if power2_eq_1_iff) |
|
666 |
|
667 lemma abs_square_less_1: "x\<^sup>2 < 1 \<longleftrightarrow> abs(x) < 1" |
|
668 using abs_square_eq_1 [of x] abs_square_le_1 [of x] |
|
669 by (auto simp add: le_less) |
647 |
670 |
648 end |
671 end |
649 |
672 |
650 |
673 |
651 subsection {* Miscellaneous rules *} |
674 subsection {* Miscellaneous rules *} |