English
If (n−1)! ≡ −1 (mod n) and n ≠ 1, then n is prime.
Русский
Если (n−1)! ≡ −1 (mod n) и n ≠ 1, тогда n — простое число.
LaTeX
$$$$ \\text{If } (n-1)! \\equiv -1 \\pmod{n} \\text{ and } n \\ne 1, \\text{ then } n \\text{ is prime}. $$$$
Lean4
/-- For `n ≠ 1`, `(n-1)!` is congruent to `-1` modulo `n` only if n is prime. -/
theorem prime_of_fac_equiv_neg_one (h : ((n - 1)! : ZMod n) = -1) (h1 : n ≠ 1) : Prime n :=
by
rcases eq_or_ne n 0 with (rfl | h0)
· norm_num at h
replace h1 : 1 < n := n.two_le_iff.mpr ⟨h0, h1⟩
by_contra h2
obtain ⟨m, hm1, hm2 : 1 < m, hm3⟩ := exists_dvd_of_not_prime2 h1 h2
have hm : m ∣ (n - 1)! := Nat.dvd_factorial (pos_of_gt hm2) (le_pred_of_lt hm3)
refine hm2.ne' (Nat.dvd_one.mp ((Nat.dvd_add_right hm).mp (hm1.trans ?_)))
rw [← ZMod.natCast_eq_zero_iff, cast_add, cast_one, h, neg_add_cancel]
