らくがき

ツノの形状を変えました。

らくがき

5時間かけて描いてたイラストがアプリがクラッシュして消滅したので前回と前々回のらくがきのボテ差分置いてお茶を濁しておきます。つらい。

整数の割算について

早くは小学校で習う整数の除算ですが、その性質については意外と訓練を積む機会がありません。
例えば次の等式は成り立つでしょうか？

(a * b + c) ÷ b = a + c ÷ b

これが実数の除算であれば、

(x * y + z) / y = (x * y) / y + z / y = x + z / y

と分配してあげることで簡単に求まりますが、整数の加算上で整数の除算の分配律は成り立ちません。
例えば(1 + 1) ÷ 2 = 1ですが、1 ÷ 2 + 1 ÷ 2 = 0です。
したがって、実数の除算と同じように考えることはできません。

b > 0の時、整数の除算a ÷ bは(∃r : a = q * b + r ∧ 0 ≦ r < b)の（唯一の）解qとして定義されます。
ただ、この定義は実用的な計算では少し使いにくいです。
そこで、b > 0の時、整数の除算a ÷ bを(∀n : n ≦ q ⇔ n * b ≦ a)の解qと定義することにします。
実際これら2つの定義は同値です。

証明

  ∃r : a = q * b + r ∧ 0 ≦ r < b
⇔ { 算術 }
  ∃r : r = a - q * b ∧ 0 ≦ r < b
⇔ { one-point rule }
  0 ≦ a - q * b < b
⇔ { 算術 }
  q * b ≦ a < (q + 1) * b

なので、

  q * b ≦ a < (q + 1) * b ⇔ (∀n : n ≦ q ⇔ n * b ≦ a)

を相互含意によって証明する。

左辺⇒右辺:

左辺q * b ≦ a < (q + 1) * bを仮定し、nを任意に1つとる。

  n ≦ q
⇔ { b > 0の際の(*b)の単調性 }
  n * b ≦ q * b
⇒ { 仮定と≦の推移律 }
  n * b ≦ a
⇒ { 仮定と≦と<の推移律 }
  n * b < (q + 1) * b
⇔ { b > 0の際の(*b)の単調性 }
  n < q + 1
⇔ { 整数の特性 }
  n ≦ q

右辺⇒左辺:

  ∀n : n ≦ q ⇔ n * b ≦ a
⇒ { nをqとq+1でそれぞれ具現化 }
  (q ≦ q ⇔ q * b ≦ a) ∧ (q + 1 ≦ q ⇔ (q + 1) * b ≦ a)
⇔ { ≦の反射律、¬(q + 1 ≦ q) }
  q * b ≦ a < (q + 1) * b

∎

この定義を用いれば、任意のnについて、

n ≦ (a * b + c) ÷ b
⇔ n * b ≦ a * b + c
⇔ (n - a) * b ≦ c
⇔ n - a ≦ c ÷ b
⇔ n ≦ a + c ÷ b

が言えます。
任意の整数a,bについてa = b ⇔ (∀n : n ≦ a ⇔ n ≦ b)ですから、(a * b + c) ÷ b = a + c ÷ bは実際に成り立つことが分かります。

らくがき

ゴートンさんもここまでやりませんでした（やると話が行き詰まりそうなので）

らくがき

勇者ちゃん。