---

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


1. k : ℤ
2. m : ℤ
3. b1 : {-2..3-}
4. m = ((4 * k) + 2) ∈ ℤ
5. (2 = 2 ∈ ℤ) ⇒ (↑isEven(k))
6. y : ℤ
7. b : {-2..3-}
8. m = ((4 * (k + 1)) + (-2)) ∈ ℤ
9. (2 = 2 ∈ ℤ) ⇒ (↑isEven(k + 1))
10. 4 | (-4)
11. ¬((-4) = 4 ∈ ℤ)
12. (-4) = (-4) ∈ ℤ
13. b1 = 2 ∈ ℤ
14. b = (-2) ∈ ℤ
15. y = (k + 1) ∈ ℤ
16. ↑isEven(k)
17. ↑same-parity(k;1)
⊢ (-2) = 2 ∈ ℤ
BY
{ TACTIC:(Unfold `same-parity` -1 THEN SplitOnHypITE -1  THEN Auto) }

1
1. k : ℤ
2. m : ℤ
3. b1 : {-2..3-}
4. m = ((4 * k) + 2) ∈ ℤ
5. y : ℤ
6. b : {-2..3-}
7. m = ((4 * (k + 1)) + (-2)) ∈ ℤ
8. 4 | (-4)
9. ¬((-4) = 4 ∈ ℤ)
10. (-4) = (-4) ∈ ℤ
11. b1 = 2 ∈ ℤ
12. b = (-2) ∈ ℤ
13. y = (k + 1) ∈ ℤ
14. ↑isEven(k)
15. ↑isEven(1)
16. ↑isEven(k)
17. ↑isEven(k + 1)
18. ↑isEven(k)
⊢ (-2) = 2 ∈ ℤ

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  m  :  \mBbbZ{}
3.  b1  :  \{-2..3\msupminus{}\}
4.  m  =  ((4  *  k)  +  2)
5.  (2  =  2)  {}\mRightarrow{}  (\muparrow{}isEven(k))
6.  y  :  \mBbbZ{}
7.  b  :  \{-2..3\msupminus{}\}
8.  m  =  ((4  *  (k  +  1))  +  (-2))
9.  (2  =  2)  {}\mRightarrow{}  (\muparrow{}isEven(k  +  1))
10.  4  |  (-4)
11.  \mneg{}((-4)  =  4)
12.  (-4)  =  (-4)
13.  b1  =  2
14.  b  =  (-2)
15.  y  =  (k  +  1)
16.  \muparrow{}isEven(k)
17.  \muparrow{}same-parity(k;1)
\mvdash{}  (-2)  =  2


By

---

Latex:
TACTIC:(Unfold  `same-parity`  -1  THEN  SplitOnHypITE  -1    THEN  Auto)

---

Home Index