four_dvd_or_exists_odd_prime_and_dvd_of_two_lt

English

If n > 2, then either 4 divides n or there exists a prime p with p ∣ n and p odd.

Русский

Если n > 2, то либо 4 делится на n, либо существует простая p, такая что p делит n и p нечётно.

LaTeX

$$∀ n, n > 2 → 4 ∣ n ∨ ∃ p, Prime(p) ∧ p ∣ n ∧ Odd(p)$$

Lean4

theorem four_dvd_or_exists_odd_prime_and_dvd_of_two_lt {n : ℕ} (n2 : 2 < n) : 4 ∣ n ∨ ∃ p, Prime p ∧ p ∣ n ∧ Odd p :=
  by
  obtain ⟨_ | _ | k, rfl⟩ | ⟨p, hp, hdvd, hodd⟩ := n.eq_two_pow_or_exists_odd_prime_and_dvd
  · contradiction
  · contradiction
  · simp [Nat.pow_succ, mul_assoc]
  · exact Or.inr ⟨p, hp, hdvd, hodd⟩

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