src/HOL/Complex.thy
changeset 55759 fe3d8f585c20
parent 55734 3f5b2745d659
child 56217 dc429a5b13c4
equal deleted inserted replaced
55758:385f7573f8f5 55759:fe3d8f585c20
   621 
   621 
   622 lemma im_complex_div_ge_0: "Im(a / b) \<ge> 0 \<longleftrightarrow> Im(a * cnj b) \<ge> 0"
   622 lemma im_complex_div_ge_0: "Im(a / b) \<ge> 0 \<longleftrightarrow> Im(a * cnj b) \<ge> 0"
   623   by (metis im_complex_div_eq_0 im_complex_div_gt_0 le_less)
   623   by (metis im_complex_div_eq_0 im_complex_div_gt_0 le_less)
   624 
   624 
   625 lemma re_complex_div_lt_0: "Re(a / b) < 0 \<longleftrightarrow> Re(a * cnj b) < 0"
   625 lemma re_complex_div_lt_0: "Re(a / b) < 0 \<longleftrightarrow> Re(a * cnj b) < 0"
   626   by (smt re_complex_div_eq_0 re_complex_div_gt_0)
   626   by (metis less_asym neq_iff re_complex_div_eq_0 re_complex_div_gt_0)
   627 
   627 
   628 lemma im_complex_div_lt_0: "Im(a / b) < 0 \<longleftrightarrow> Im(a * cnj b) < 0"
   628 lemma im_complex_div_lt_0: "Im(a / b) < 0 \<longleftrightarrow> Im(a * cnj b) < 0"
   629   by (metis im_complex_div_eq_0 im_complex_div_gt_0 less_asym neq_iff)
   629   by (metis im_complex_div_eq_0 im_complex_div_gt_0 less_asym neq_iff)
   630 
   630 
   631 lemma re_complex_div_le_0: "Re(a / b) \<le> 0 \<longleftrightarrow> Re(a * cnj b) \<le> 0"
   631 lemma re_complex_div_le_0: "Re(a / b) \<le> 0 \<longleftrightarrow> Re(a * cnj b) \<le> 0"