---

Step * 2 2 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) ∈ ℤ)
⊢ ∃p:ℤ × {-2..3-} [let k,b = p 
                   in (m = ((4 * k) + b) ∈ ℤ) ∧ ((|b| = 2 ∈ ℤ) ⇒ (↑isEven(k)))]
BY
{ ((Assert |r| < 4 BY
          (InstLemma `rem_bounds_absval` [⌜4⌝;⌜m⌝]⋅ THEN Auto))
   THEN (Assert r ∈ {-2..3-} BY
               ((RWO "absval_ifthenelse" (-1) THENA Auto) THEN SplitOnHypITE -1  THEN Auto'))
   THEN (Decide ⌜↑isEven(q)⌝⋅ THENA Auto)) }

1
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)
⊢ ∃p:ℤ × {-2..3-} [let k,b = p 
                   in (m = ((4 * k) + b) ∈ ℤ) ∧ ((|b| = 2 ∈ ℤ) ⇒ (↑isEven(k)))]

2
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)
⊢ ∃p:ℤ × {-2..3-} [let k,b = p 
                   in (m = ((4 * k) + b) ∈ ℤ) ∧ ((|b| = 2 ∈ ℤ) ⇒ (↑isEven(k)))]

---

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))
\mvdash{}  \mexists{}p:\mBbbZ{}  \mtimes{}  \{-2..3\msupminus{}\}  [let  k,b  =  p 
                                      in  (m  =  ((4  *  k)  +  b))  \mwedge{}  ((|b|  =  2)  {}\mRightarrow{}  (\muparrow{}isEven(k)))]


By

---

Latex:
((Assert  |r|  <  4  BY
                (InstLemma  `rem\_bounds\_absval`  [\mkleeneopen{}4\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  (Assert  r  \mmember{}  \{-2..3\msupminus{}\}  BY
                          ((RWO  "absval\_ifthenelse"  (-1)  THENA  Auto)  THEN  SplitOnHypITE  -1    THEN  Auto'))
  THEN  (Decide  \mkleeneopen{}\muparrow{}isEven(q)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index