Step
*
1
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))
⊢ b = b1 ∈ ℤ
BY
{ TACTIC:(Assert 4 | (b - b1) BY
(With ⌜k - y⌝ (D 0)⋅ THEN Auto')) }
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))
10. 4 | (b - b1)
⊢ b = b1 ∈ ℤ
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))
\mvdash{} b = b1
By
Latex:
TACTIC:(Assert 4 | (b - b1) BY
(With \mkleeneopen{}k - y\mkleeneclose{} (D 0)\mcdot{} THEN Auto'))
Home
Index