dvd_mul_of_dvd_ne — Mathlib

English

If p1 ≠ p2 and p1,p2 are primes and p1 | n and p2 | n, then p1 p2 | n.

Русский

Если p1 и p2 — простые числа, различны, и оба делят n, то p1 p2 делит n.

LaTeX

$$$$ \forall {p1,p2,n} \in \mathbb{N},\ h_neq : p1 \neq p2,\text{Prime}(p1) \rightarrow \text{Prime}(p2) \rightarrow p1 \mid n \rightarrow p2 \mid n \rightarrow p1 \cdot p2 \mid n. $$$$

Lean4

theorem dvd_mul_of_dvd_ne {p1 p2 n : ℕ} (h_neq : p1 ≠ p2) (pp1 : Prime p1) (pp2 : Prime p2) (h1 : p1 ∣ n)
    (h2 : p2 ∣ n) : p1 * p2 ∣ n :=
  Coprime.mul_dvd_of_dvd_of_dvd ((coprime_primes pp1 pp2).mpr h_neq) h1 h2

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