English
For any real x and RCLike z, 0 < x·z is equivalent to x and z having the same nonzero sign structure: either x < 0 and z < 0, or x > 0 and z > 0.
Русский
Для вещественного x и элемента z из RCLike верно: 0 < x·z тогда и только тогда, когда x и z имеют один и тот же знаковый характер: либо x < 0 и z < 0, либо x > 0 и z > 0.
LaTeX
$$$0 < x \cdot z \iff (x < 0 \land z < 0) \lor (0 < x \land 0 < z)$$$
Lean4
theorem ofReal_mul_pos_iff (x : ℝ) (z : K) : 0 < x * z ↔ (x < 0 ∧ z < 0) ∨ (0 < x ∧ 0 < z) :=
by
simp only [pos_iff (K := K), neg_iff (K := K), re_ofReal_mul, im_ofReal_mul]
obtain hx | hx | hx := lt_trichotomy x 0
· simp only [mul_pos_iff, not_lt_of_gt hx, false_and, hx, true_and, false_or, mul_eq_zero, hx.ne, or_false]
· simp only [hx, zero_mul, lt_self_iff_false, false_and, false_or]
· simp only [mul_pos_iff, hx, true_and, not_lt_of_gt hx, false_and, or_false, mul_eq_zero, hx.ne', false_or]
