---

Step * of Lemma sparse-signed-rep-lemma1

∀m:ℤ. (∃p:ℤ × {-2..3-} [let k,b = p in (m = ((4 * k) + b) ∈ ℤ) ∧ ((|b| = 2 ∈ ℤ) ⇒ (↑isEven(k)))])
BY
{ ((D 0 THENA Auto)
   THEN (Evaluate ⌜qr = divrem(m; 4) ∈ (ℤ × ℤ)⌝⋅ THENA Auto)
   THEN (RWO "divrem-sq" (-1) THENA Auto)
   THEN D -2
   THEN (EqHD (-1) THENA Auto)
   THEN All Reduce
   THEN RenameVar `r' (-3)
   THEN RenameVar `q' (-4)
   THEN (Assert m = ((4 * q) + r) ∈ ℤ BY
               (InstLemma `div_rem_sum` [⌜m⌝;⌜4⌝]⋅ THEN Auto'))
   THEN (Decide ⌜r = 3 ∈ ℤ⌝⋅ 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 ∈ ℤ
⊢ ∃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 ∈ ℤ)
⊢ ∃p:ℤ × {-2..3-} [let k,b = p 
                   in (m = ((4 * k) + b) ∈ ℤ) ∧ ((|b| = 2 ∈ ℤ) ⇒ (↑isEven(k)))]

---

Latex:

---

Latex:
\mforall{}m:\mBbbZ{}.  (\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:
((D  0  THENA  Auto)
  THEN  (Evaluate  \mkleeneopen{}qr  =  divrem(m;  4)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (RWO  "divrem-sq"  (-1)  THENA  Auto)
  THEN  D  -2
  THEN  (EqHD  (-1)  THENA  Auto)
  THEN  All  Reduce
  THEN  RenameVar  `r'  (-3)
  THEN  RenameVar  `q'  (-4)
  THEN  (Assert  m  =  ((4  *  q)  +  r)  BY
                          (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}4\mkleeneclose{}]\mcdot{}  THEN  Auto'))
  THEN  (Decide  \mkleeneopen{}r  =  3\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index