English
p is prime iff p ≥ 2 and there does not exist m,n with m < p, n < p and m n = p.
Русский
p простое тогда и только тогда, когда p ≥ 2 и не существует m,n таких, что m < p, n < p и m n = p.
LaTeX
$$$\\\\mathrm{Prime}(p) \\\\iff 2 \\\\le p \\\\land \\\\neg\\\\exists m n, m < p \\\\land n < p \\\\land m \\\\cdot n = p$$$
Lean4
theorem prime_iff_not_exists_mul_eq {p : ℕ} : p.Prime ↔ 2 ≤ p ∧ ¬∃ m n, m < p ∧ n < p ∧ m * n = p :=
by
push_neg
simp_rw [prime_def_lt, dvd_def, exists_imp]
refine and_congr_right fun hp ↦ forall_congr' fun m ↦ (forall_congr' fun h ↦ ?_).trans forall_comm
simp_rw [Ne, forall_comm (β := _ = _), eq_comm, imp_false, not_lt]
refine forall₂_congr fun n hp ↦ ⟨by simp_all, fun hpn ↦ ?_⟩
have := mul_ne_zero_iff.mp (hp ▸ show p ≠ 0 by cutsat)
exact (Nat.mul_eq_right (by cutsat)).mp (hp.symm.trans (hpn.antisymm (hp ▸ Nat.le_mul_of_pos_left _ (by cutsat))))
