mod_two_eq_one_iff_ne_two — Mathlib

English

For a prime p, p mod 2 = 1 iff p ≠ 2.

Русский

Для простого p остаток от деления на 2 равен 1 тогда и только тогда, когда p ≠ 2.

LaTeX

$$$$ \forall p, \operatorname{Prime}(p) \Rightarrow (p \bmod 2 = 1 \iff p \neq 2). $$$$

Lean4

/-- A prime `p` satisfies `p % 2 = 1` if and only if `p ≠ 2`. -/
theorem mod_two_eq_one_iff_ne_two {p : ℕ} (hp : p.Prime) : p % 2 = 1 ↔ p ≠ 2 :=
  by
  refine ⟨fun h hf => ?_, hp.eq_two_or_odd.resolve_left⟩
  rw [hf] at h
  simp at h

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