le_mod_add_mod_of_dvd_add_of_not_dvd

English

If c divides a + b but does not divide a, then c ≤ a mod c + b mod c.

Русский

Если c делит a + b, но не делит a, то c ≤ a mod c + b mod c.

LaTeX

$$$\\\\forall a,b,c \\\\in \\\\mathbb{N},\\\\ c \\mid (a+b) \\\\land \\\\ ¬(c \\mid a) \\\\Rightarrow c \\le a \\\\bmod c + b \\\\bmod c$$$

Lean4

theorem le_mod_add_mod_of_dvd_add_of_not_dvd {a b c : ℕ} (h : c ∣ a + b) (ha : ¬c ∣ a) : c ≤ a % c + b % c :=
  by_contradiction fun hc =>
    by
    have : (a + b) % c = a % c + b % c := add_mod_of_add_mod_lt (lt_of_not_ge hc)
    simp_all [dvd_iff_mod_eq_zero]

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