ne_one_iff_exists_prime_dvd — Mathlib

English

For every n, n ≠ 1 if and only if there exists a prime p with p | n.

Русский

Для каждого n: n ≠ 1 тогда и только тогда, когда существует простое p, делящее n.

LaTeX

$$$$ \forall n \in \mathbb{N},\ n \neq 1 \iff \exists p \in \mathbb{N},\ p \text{ prime} \land p \mid n. $$$$

Lean4

theorem ne_one_iff_exists_prime_dvd : ∀ {n}, n ≠ 1 ↔ ∃ p : ℕ, p.Prime ∧ p ∣ n
  | 0 => by simpa using Exists.intro 2 Nat.prime_two
  | 1 => by simp [Nat.not_prime_one]
  | n + 2 => by
    let a := n + 2
    have ha : a ≠ 1 := Nat.succ_succ_ne_one n
    simp only [a, true_iff, Ne, not_false_iff, ha]
    exact ⟨a.minFac, Nat.minFac_prime ha, a.minFac_dvd⟩

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