---

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

.....assertion..... 
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))
10. 4 | (b - b1)
11. ¬((b - b1) = 4 ∈ ℤ)
12. ¬((b - b1) = (-4) ∈ ℤ)
13. b - b1 ∈ {-3..4-}
⊢ (b - b1) = 0 ∈ ℤ
BY
{ TACTIC:((RWO "divides_iff_rem_zero" (-4) THENA Auto)
          THEN MoveToConcl (-4)
          THEN (GenConclTerm ⌜b - b1⌝⋅ THENA Auto)
          THEN All Thin) }

1
1. v : {-3..4-}
⊢ ((v rem 4) = 0 ∈ ℤ) ⇒ (v = 0 ∈ ℤ)

---

Latex:

---

Latex:
.....assertion..... 
1.  m  :  \mBbbZ{}
2.  k  :  \mBbbZ{}
3.  b1  :  \{-2..3\msupminus{}\}
4.  m  =  ((4  *  k)  +  b1)
5.  (|b1|  =  2)  {}\mRightarrow{}  (\muparrow{}isEven(k))
6.  y  :  \mBbbZ{}
7.  b  :  \{-2..3\msupminus{}\}
8.  m  =  ((4  *  y)  +  b)
9.  (|b|  =  2)  {}\mRightarrow{}  (\muparrow{}isEven(y))
10.  4  |  (b  -  b1)
11.  \mneg{}((b  -  b1)  =  4)
12.  \mneg{}((b  -  b1)  =  (-4))
13.  b  -  b1  \mmember{}  \{-3..4\msupminus{}\}
\mvdash{}  (b  -  b1)  =  0


By

---

Latex:
TACTIC:((RWO  "divides\_iff\_rem\_zero"  (-4)  THENA  Auto)
                THEN  MoveToConcl  (-4)
                THEN  (GenConclTerm  \mkleeneopen{}b  -  b1\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  All  Thin)

---

Home Index