coprime_sub_mul_floor_rat_div_of_coprime

English

Let n and d be coprime naturals. Then the integer (n − d floor(n/d)) is coprime to d; equivalently, gcd(|n − d floor(n/d)|, d) = 1.

Русский

Пусть n и d — взаимно простые naturals. Тогда число n − d ⌊n/d⌋ взаимно прозрачно с d; то есть gcd(|n − d ⌊n/d⌋|, d) = 1.

LaTeX

$$$$ \\gcd(\\,n - d \\left\\lfloor \\frac{n}{d} \\right\\rfloor, d) = 1, \\quad \\gcd(n,d)=1. $$$$

Lean4

theorem coprime_sub_mul_floor_rat_div_of_coprime {n d : ℕ} (n_coprime_d : n.Coprime d) :
    ((n : ℤ) - d * ⌊(n : ℚ) / d⌋).natAbs.Coprime d :=
  by
  have : (n : ℤ) % d = n - d * ⌊(n : ℚ) / d⌋ := Int.mod_nat_eq_sub_mul_floor_rat_div
  rw [← this]
  have : d.Coprime n := n_coprime_d.symm
  rwa [Nat.Coprime, Nat.gcd_rec] at this

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