Step
*
1
1
of Lemma
special-mod4-decomp-unique
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 ∈ ℤ
BY
{ TACTIC:Assert ⌜b = b1 ∈ ℤ⌝⋅ }
1
.....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))
⊢ b = b1 ∈ ℤ
2
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. b = b1 ∈ ℤ
⊢ y = k ∈ ℤ
Latex:
Latex:
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))
\mvdash{}  y  =  k
By
Latex:
TACTIC:Assert  \mkleeneopen{}b  =  b1\mkleeneclose{}\mcdot{}
Home
Index