coprime_of_lt_prime — Mathlib

English

If n ≠ 0, n < p with p prime, then p.Coprime n.

Русский

Если n ≠ 0 и n < p, где p — простое, то p и n взаимно просты.

LaTeX

$$$$ \forall n,p \in \mathbb{N},\ n \neq 0 \land n < p \land \text{Prime}(p) \Rightarrow p.Coprime(n). $$$$

Lean4

theorem coprime_of_lt_prime {n p} (ne_zero : n ≠ 0) (hlt : n < p) (pp : Prime p) : Coprime p n :=
  (coprime_or_dvd_of_prime pp n).resolve_right fun h => Nat.lt_le_asymm hlt (le_of_dvd (Nat.pos_of_ne_zero ne_zero) h)

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