eq_two_pow_or_exists_odd_prime_and_dvd

English

For any n, either n = 2^k for some k, or there exists a prime p with p ∣ n and p odd.

Русский

Для любого n существует либо n = 2^k, либо существует простая p, такая что p ∣ n и p нечётно.

LaTeX

$$∀ n, (∃ k, n = 2^k) ∨ ∃ p, Prime(p) ∧ p ∣ n ∧ Odd(p)$$

Lean4

theorem eq_two_pow_or_exists_odd_prime_and_dvd (n : ℕ) : (∃ k : ℕ, n = 2 ^ k) ∨ ∃ p, Nat.Prime p ∧ p ∣ n ∧ Odd p :=
  (eq_or_ne n 0).elim (fun hn => Or.inr ⟨3, prime_three, hn.symm ▸ dvd_zero 3, ⟨1, rfl⟩⟩) fun hn =>
    or_iff_not_imp_right.mpr fun H =>
      ⟨n.primeFactorsList.length,
        eq_prime_pow_of_unique_prime_dvd hn fun {_} hprime hdvd =>
          hprime.eq_two_or_odd'.resolve_right fun hodd => H ⟨_, hprime, hdvd, hodd⟩⟩

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