exists_dvd_of_not_prime2 — Mathlib

English

If n ≥ 2 and not prime, there exists m with m | n, 2 ≤ m and m < n.

Русский

Если n ≥ 2 и не простое, существует m: m | n, 2 ≤ m и m < n.

LaTeX

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

Lean4

theorem exists_dvd_of_not_prime2 {n : ℕ} (n2 : 2 ≤ n) (np : ¬Prime n) : ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n :=
  ⟨minFac n, minFac_dvd _, (minFac_prime (ne_of_gt n2)).two_le, (not_prime_iff_minFac_lt n2).1 np⟩

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