---

Step * 1 of Lemma special-mod4-decomp-unique


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))))
BY
{ TACTIC:(With ⌜k⌝ (D 0)⋅ THEN Auto THEN Thin (-3) THEN ExRepD THEN SwapVars `b' `b1') }

1
1. m : ℤ
2. k : ℤ
3. b1 : {-2..3-}
4. m = ((4 * k) + b1) ∈ ℤ
5. (|b1| = 2 ∈ ℤ) ⇒ (↑isEven(k))
6. y : ℤ
7. b : {-2..3-}
8. m = ((4 * y) + b) ∈ ℤ
9. (|b| = 2 ∈ ℤ) ⇒ (↑isEven(y))
⊢ y = k ∈ ℤ

---

Latex:

---

Latex:

1.  m  :  \mBbbZ{}
2.  k  :  \mBbbZ{}
3.  b  :  \{-2..3\msupminus{}\}
4.  [\%1]  :  (m  =  ((4  *  k)  +  b))  \mwedge{}  ((|b|  =  2)  {}\mRightarrow{}  (\muparrow{}isEven(k)))
\mvdash{}  \mexists{}!k:\mBbbZ{}.  \mexists{}b:\{-2..3\msupminus{}\}.  ((m  =  ((4  *  k)  +  b))  \mwedge{}  ((|b|  =  2)  {}\mRightarrow{}  (\muparrow{}isEven(k))))


By

---

Latex:
TACTIC:(With  \mkleeneopen{}k\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  Thin  (-3)  THEN  ExRepD  THEN  SwapVars  `b'  `b1')

---

Home Index