coprime_of_lt_minFac — Mathlib

English

Let n,m be natural numbers with m ≠ 0 and m < minFac(n). Then gcd(n,m) = 1.

Русский

Пусть n,m ∈ ℕ, m ≠ 0 и m < minFac(n). Тогда gcd(n,m) = 1.

LaTeX

$$$$ \forall n,m \in \mathbb{N},\ m \neq 0 \land m < \minFac(n) \Rightarrow \gcd(n,m) = 1. $$$$

Lean4

/-- If `0 < m < minFac n`, then `n` and `m` are coprime. -/
theorem coprime_of_lt_minFac {n m : ℕ} (h₀ : m ≠ 0) (h : m < minFac n) : Coprime n m :=
  by
  rw [← not_not (a := n.Coprime m), Prime.not_coprime_iff_dvd]
  push_neg
  exact fun p hp hn hm ↦ ((le_of_dvd (by cutsat) hm).trans_lt <| h.trans_le <| minFac_le_of_dvd hp.two_le hn).false

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