---

Step * 2 2 2 2 1 1 of Lemma sparse-signed-rep-lemma1


1. m : ℤ
2. q : ℤ
3. r : ℤ
4. q = (m ÷ 4) ∈ ℤ
5. r = (m rem 4) ∈ ℤ
6. m = ((4 * q) + r) ∈ ℤ
7. ¬(r = 3 ∈ ℤ)
8. ¬(r = (-3) ∈ ℤ)
9. |r| < 4
10. r ∈ {-2..3-}
11. ¬↑isEven(q)
12. ¬(r = 2 ∈ ℤ)
13. r = (-2) ∈ ℤ
14. m = ((4 * (q - 1)) + 2) ∈ ℤ
15. 2 = 2 ∈ ℤ
⊢ ↑isEven(q - 1)
BY
{ ((Subst' q - 1 ~ q + (-1) 0 THENA Auto)
   THEN BLemma `isEven-add`
   THEN Auto
   THEN Unfold `same-parity` 0
   THEN AutoSplit) }

---

Latex:

---

Latex:

1.  m  :  \mBbbZ{}
2.  q  :  \mBbbZ{}
3.  r  :  \mBbbZ{}
4.  q  =  (m  \mdiv{}  4)
5.  r  =  (m  rem  4)
6.  m  =  ((4  *  q)  +  r)
7.  \mneg{}(r  =  3)
8.  \mneg{}(r  =  (-3))
9.  |r|  <  4
10.  r  \mmember{}  \{-2..3\msupminus{}\}
11.  \mneg{}\muparrow{}isEven(q)
12.  \mneg{}(r  =  2)
13.  r  =  (-2)
14.  m  =  ((4  *  (q  -  1))  +  2)
15.  2  =  2
\mvdash{}  \muparrow{}isEven(q  -  1)


By

---

Latex:
((Subst'  q  -  1  \msim{}  q  +  (-1)  0  THENA  Auto)
  THEN  BLemma  `isEven-add`
  THEN  Auto
  THEN  Unfold  `same-parity`  0
  THEN  AutoSplit)

---

Home Index