not_prime_of_int_mul — Mathlib

English

Let a, b ∈ ℤ with |a| ≠ 1 and |b| ≠ 1, and suppose a b = (c : ℤ) for some c ∈ ℕ. Then c is not prime.

Русский

Пусть a, b ∈ ℤ такие, что |a| ≠ 1 и |b| ≠ 1, и произведение a b равно c ∈ ℕ. Тогда c не является простым.

LaTeX

$$$\forall a,b \in \mathbb{Z}, \forall c \in \mathbb{N}, \\ (a b = (c:\\mathbb{Z})) \Rightarrow (|a| \neq 1) \land (|b| \neq 1) \Rightarrow \neg \mathrm{Nat.Prime}(c).$$$

Lean4

theorem not_prime_of_int_mul {a b : ℤ} {c : ℕ} (ha : a.natAbs ≠ 1) (hb : b.natAbs ≠ 1) (hc : a * b = (c : ℤ)) :
    ¬Nat.Prime c :=
  not_prime_of_mul_eq (natAbs_mul_natAbs_eq hc) ha hb

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