---

Step * 1 of Lemma div_floor_mod_sum


1. a : ℤ
2. n : ℕ+
3. ¬n < 0
4. v : ℤ
5. (a rem n) = v ∈ ℤ
6. v1 : ℤ
7. (a ÷ n) = v1 ∈ ℤ
8. |v| < |n|
9. a = ((v1 * n) + v) ∈ ℤ
10. v < 0
⊢ ((v1 * n) + v) = (((v1 - 1) * n) + |n| + v) ∈ ℤ
BY
{ (RWO "absval_pos" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  n  :  \mBbbN{}\msupplus{}
3.  \mneg{}n  <  0
4.  v  :  \mBbbZ{}
5.  (a  rem  n)  =  v
6.  v1  :  \mBbbZ{}
7.  (a  \mdiv{}  n)  =  v1
8.  |v|  <  |n|
9.  a  =  ((v1  *  n)  +  v)
10.  v  <  0
\mvdash{}  ((v1  *  n)  +  v)  =  (((v1  -  1)  *  n)  +  |n|  +  v)


By

---

Latex:
(RWO  "absval\_pos"  0  THEN  Auto)

---

Home Index