---

Step * 1 of Lemma div_rem_sum2


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
BY
{ (Subst' ⌜(n * (a ÷ n)) = (a - a rem n) ∈ ℤ⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}[a:\mBbbZ{}].  \mforall{}[n:\mBbbZ{}\msupminus{}\msupzero{}].    (a  =  (((a  \mdiv{}  n)  *  n)  +  (a  rem  n)))
2.  [a]  :  \mBbbZ{}
3.  \mforall{}[n:\mBbbZ{}\msupminus{}\msupzero{}].  (a  =  (((a  \mdiv{}  n)  *  n)  +  (a  rem  n)))
4.  [n]  :  \mBbbZ{}\msupminus{}\msupzero{}
5.  a  =  (((a  \mdiv{}  n)  *  n)  +  (a  rem  n))
\mvdash{}  n  *  (a  \mdiv{}  n)  \msim{}  a  -  a  rem  n


By

---

Latex:
(Subst'  \mkleeneopen{}(n  *  (a  \mdiv{}  n))  =  (a  -  a  rem  n)\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index