not_prime_iff_exists_dvd_lt — Mathlib

English

For n ≥ 2, not Prime n iff there exists m with m | n, 2 ≤ m and m < n.

Русский

Для n ≥ 2, Not Prime n эквивалентно существованию m, такого что m | n, 2 ≤ m и m < n.

LaTeX

$$$$ \forall n \ge 2: \neg \operatorname{Prime}(n) \iff \exists m \big( m \mid n \land 2 \le m \land m < n \big). $$$$

Lean4

theorem not_prime_iff_exists_dvd_lt {n : ℕ} (h : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n :=
  ⟨exists_dvd_of_not_prime2 h, fun ⟨_, h1, h2, h3⟩ => not_prime_of_dvd_of_lt h1 h2 h3⟩

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