English
For integers a,b and natural n, gcd(a,b) divides n if and only if there exist integers x,y with n = a x + b y.
Русский
Для целых a,b и натурального n: gcd(a,b) делит n тогда и только тогда, когда существуют целые x,y такие, что n = a x + b y.
LaTeX
$$$$\\gcd(a,b) \\mid n \\quad\\Leftrightarrow\\quad \\exists x,y \\in \\mathbb{Z},\\; \\uparrow n = a x + b y.$$$$
Lean4
theorem gcd_dvd_iff {a b : ℤ} {n : ℕ} : gcd a b ∣ n ↔ ∃ x y : ℤ, ↑n = a * x + b * y :=
by
constructor
· intro h
rw [← Nat.mul_div_cancel' h, Int.natCast_mul, gcd_eq_gcd_ab, Int.add_mul, mul_assoc, mul_assoc]
exact ⟨_, _, rfl⟩
· rintro ⟨x, y, h⟩
rw [← Int.natCast_dvd_natCast, h]
exact Int.dvd_add (dvd_mul_of_dvd_left (gcd_dvd_left ..) _) (dvd_mul_of_dvd_left (gcd_dvd_right ..) y)
