828 qed |
828 qed |
829 qed |
829 qed |
830 then show "a * b \<noteq> 0" by (simp add: neq_iff) |
830 then show "a * b \<noteq> 0" by (simp add: neq_iff) |
831 qed |
831 qed |
832 |
832 |
833 lemma zero_less_mult_iff: |
833 lemma zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0" |
834 "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0" |
834 by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases]) |
835 apply (auto simp add: mult_pos_pos mult_neg_neg) |
835 (auto simp add: mult_pos_pos mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2) |
836 apply (simp_all add: not_less le_less) |
836 |
837 apply (erule disjE) apply assumption defer |
837 lemma zero_le_mult_iff: "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0" |
838 apply (erule disjE) defer apply (drule sym) apply simp |
838 by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff) |
839 apply (erule disjE) defer apply (drule sym) apply simp |
|
840 apply (erule disjE) apply assumption apply (drule sym) apply simp |
|
841 apply (drule sym) apply simp |
|
842 apply (blast dest: zero_less_mult_pos) |
|
843 apply (blast dest: zero_less_mult_pos2) |
|
844 done |
|
845 |
|
846 lemma zero_le_mult_iff: |
|
847 "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0" |
|
848 by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff) |
|
849 |
839 |
850 lemma mult_less_0_iff: |
840 lemma mult_less_0_iff: |
851 "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b" |
841 "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b" |
852 apply (insert zero_less_mult_iff [of "-a" b]) |
842 apply (insert zero_less_mult_iff [of "-a" b]) |
853 apply force |
843 apply force |