dvd_prime_two_le — Mathlib

English

Let p be a prime and m ≥ 2. Then m divides p if and only if m = p.

Русский

Пусть p — простое число и m ≥ 2. Тогда m делит p тогда же, когда m = p.

LaTeX

$$$\\\\forall p,m \\\\in \\\\mathbb{N}, \\\\mathrm{Prime}(p) \\\\rightarrow 2 \\\\le m \\\\rightarrow (m \\\\mid p) \\\\\\leftrightarrow (m = p).$$$

Lean4

theorem dvd_prime_two_le {p m : ℕ} (pp : Prime p) (H : 2 ≤ m) : m ∣ p ↔ m = p :=
  (dvd_prime pp).trans <| or_iff_right_of_imp <| Not.elim <| ne_of_gt H

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