---

Step * of Lemma div_rem_sum2

∀[a:ℤ]. ∀[n:ℤ-o].  (n * (a ÷ n) ~ a - a rem n)
BY
{ (InstLemma `div_rem_sum` [] THEN RepeatFor 2 (ParallelLast) THEN Auto') }

1
1. ∀[a:ℤ]. ∀[n:ℤ-o].  (a = (((a ÷ n) * n) + (a rem n)) ∈ ℤ)
2. [a] : ℤ
3. ∀[n:ℤ-o]. (a = (((a ÷ n) * n) + (a rem n)) ∈ ℤ)
4. [n] : ℤ-o
5. a = (((a ÷ n) * n) + (a rem n)) ∈ ℤ
⊢ n * (a ÷ n) ~ a - a rem n

---

Latex:

---

Latex:
\mforall{}[a:\mBbbZ{}].  \mforall{}[n:\mBbbZ{}\msupminus{}\msupzero{}].    (n  *  (a  \mdiv{}  n)  \msim{}  a  -  a  rem  n)


By

---

Latex:
(InstLemma  `div\_rem\_sum`  []  THEN  RepeatFor  2  (ParallelLast)  THEN  Auto')

---

Home Index