---

Step * 1 1 1 1 1 1 1 of Lemma rneq-if-rabs2

.....assertion..... 
1. v : ℤ
2. v = (((v ÷ 4) * 4) + (v rem 4)) ∈ ℤ
3. |v rem 4| < 4
⊢ (|v rem 4| = (v rem 4) ∈ ℤ) ∨ (|v rem 4| = (-(v rem 4)) ∈ ℤ)
BY
{ ((RWO "absval_unfold2" 0 THENA Auto) THEN AutoSplit) }

---

Latex:

---

Latex:
.....assertion..... 
1.  v  :  \mBbbZ{}
2.  v  =  (((v  \mdiv{}  4)  *  4)  +  (v  rem  4))
3.  |v  rem  4|  <  4
\mvdash{}  (|v  rem  4|  =  (v  rem  4))  \mvee{}  (|v  rem  4|  =  (-(v  rem  4)))


By

---

Latex:
((RWO  "absval\_unfold2"  0  THENA  Auto)  THEN  AutoSplit)

---

Home Index