divInt_le_divInt — Mathlib

English

For integers a,b,c,d with b>0,d>0, a/b ≤ c/d iff a d ≤ c b (in the sense of integer division comparison).

Русский

Для целых a,b,c,d с b>0 и d>0, a/b ≤ c/d тогда и только тогда a d ≤ c b (с учётом целочисленного деления).

LaTeX

$$$$\\frac{a}{b} \\le \\frac{c}{d} \\iff a d \\le c b \\quad (b>0, d>0).$$$$

Lean4

protected theorem divInt_le_divInt {a b c d : ℤ} (b0 : 0 < b) (d0 : 0 < d) : a /. b ≤ c /. d ↔ a * d ≤ c * b :=
  by
  rw [Rat.le_iff_sub_nonneg, ← Int.sub_nonneg]
  simp [sub_eq_add_neg, ne_of_gt b0, ne_of_gt d0, Int.mul_pos d0 b0]

Похожие утверждения