not_dvd_mul — Mathlib

English

If p is prime and p ∤ m and p ∤ n, then p ∤ m n.

Русский

Пусть p — простое, и p не делит m, и p не делит n. Тогда p не делит произведение m n.

LaTeX

$$$$ \forall p,m,n \in \mathbb{N},\ \text{Prime}(p) \rightarrow \neg(p \mid m) \rightarrow \neg(p \mid n) \rightarrow \neg(p \mid m n). $$$$

Lean4

theorem not_dvd_mul {p m n : ℕ} (pp : Prime p) (Hm : ¬p ∣ m) (Hn : ¬p ∣ n) : ¬p ∣ m * n :=
  mt pp.dvd_mul.1 <| by simp [Hm, Hn]

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