not_prime_of_dvd_of_lt

Mathlib.Data.Nat.Prime.Basic

URI: https://scilib.ai/kg/mathlib#Nat.not_prime_of_dvd_of_lt

English

If m | n, 2 ≤ m and m < n, then n is not prime.

Русский

Если m делит n, 2 ≤ m и m < n, то n не простое.

LaTeX

$$$$ m \mid n \land 2 \le m \land m < n \Rightarrow \neg \operatorname{Prime}(n). $$$$

Lean4

theorem not_prime_of_dvd_of_lt {m n : ℕ} (h1 : m ∣ n) (h2 : 2 ≤ m) (h3 : m < n) : ¬Prime n :=
  not_prime_of_dvd_of_ne h1 (ne_of_gt h2) (ne_of_lt h3)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru