English
Prime p iff p ≥ 2 and no divisor m with 2 ≤ m ≤ sqrt(p) divides p.
Русский
Простое число p эквивалентно p ≥ 2 и не существует делителя m, удовлетворяющего 2 ≤ m ≤ √p и делящего p.
LaTeX
$$$\\\\mathrm{Prime}(p) \\\\iff 2 \\\\le p \\\\land \\\\forall m, \\\\; 2 \\\\le m \\\\to m \\\\le \\\\sqrt{p} \\\\to \\\\neg m \\\\mid p$$$
Lean4
theorem prime_def_lt' {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ∀ m, 2 ≤ m → m < p → ¬m ∣ p :=
prime_def_lt.trans <|
and_congr_right fun p2 =>
forall_congr' fun m =>
⟨fun h m2 l d => not_lt_of_ge m2 ((h l d).symm ▸ by decide), fun h l d =>
by
rcases m with (_ | _ | m)
· omega
· rfl
· exact (h (le_add_left 2 m) l).elim d⟩
