eq_zero_of_dvd_of_nonneg_of_lt — Mathlib

English

If integers m,n satisfy m ≥ 0, m < n and n divides m, then m = 0.

Русский

Если целые числа m,n удовлетворяют m ≥ 0, m < n и n делит m, то m = 0.

LaTeX

$$$\\\\forall m,n \\in \\mathbb{Z},\\\\; m \\ge 0, \\\\ m < n \\\\ \\\\land n \\mid m \\Rightarrow m = 0$$$

Lean4

theorem eq_zero_of_dvd_of_nonneg_of_lt (hm : 0 ≤ m) (hmn : m < n) (hnm : n ∣ m) : m = 0 :=
  eq_zero_of_dvd_of_natAbs_lt_natAbs hnm (natAbs_lt_natAbs_of_nonneg_of_lt hm hmn)

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