---

Step * of Lemma special-mod4-decomp-unique

∀m:ℤ. ∃!k:ℤ. ∃b:{-2..3-}. ((m = ((4 * k) + b) ∈ ℤ) ∧ ((|b| = 2 ∈ ℤ) ⇒ (↑isEven(k))))
BY
{ TACTIC:((D 0 THENA Auto)
          THEN (Evaluate ⌜p
                          = special-mod4-decomp(m)
                          ∈ {p:ℤ × {-2..3-}| let k,b = p in (m = ((4 * k) + b) ∈ ℤ) ∧ ((|b| = 2 ∈ ℤ) ⇒ (↑isEven(k)))} ⌝\000C 
                ⋅
                THENA Auto
                )
          THEN Thin (-1)
          THEN D -1
          THEN D -2
          THEN RenameVar `k' (-3)
          THEN RenameVar `b' (-2)
          THEN Reduce (-1)) }

1
1. m : ℤ
2. k : ℤ
3. b : {-2..3-}
4. [%1] : (m = ((4 * k) + b) ∈ ℤ) ∧ ((|b| = 2 ∈ ℤ) ⇒ (↑isEven(k)))
⊢ ∃!k:ℤ. ∃b:{-2..3-}. ((m = ((4 * k) + b) ∈ ℤ) ∧ ((|b| = 2 ∈ ℤ) ⇒ (↑isEven(k))))

---

Latex:

---

Latex:
\mforall{}m:\mBbbZ{}.  \mexists{}!k:\mBbbZ{}.  \mexists{}b:\{-2..3\msupminus{}\}.  ((m  =  ((4  *  k)  +  b))  \mwedge{}  ((|b|  =  2)  {}\mRightarrow{}  (\muparrow{}isEven(k))))


By

---

Latex:
TACTIC:((D  0  THENA  Auto)
                THEN  (Evaluate  \mkleeneopen{}p  =  special-mod4-decomp(m)\mkleeneclose{}  \mcdot{}  THENA  Auto)
                THEN  Thin  (-1)
                THEN  D  -1
                THEN  D  -2
                THEN  RenameVar  `k'  (-3)
                THEN  RenameVar  `b'  (-2)
                THEN  Reduce  (-1))

---

Home Index