---

Step * 1 1 of Lemma req-int


1. a : ℤ
2. b : ℤ
3. ∀n:ℕ+. (|(2 * n * a) - 2 * n * b| ≤ 4)
4. |(2 * 3 * a) - 2 * 3 * b| ≤ 4
⊢ a = b ∈ ℤ
BY
{ (RW IntNormC (-1) THENA Auto) }

1
1. a : ℤ
2. b : ℤ
3. ∀n:ℕ+. (|(2 * n * a) - 2 * n * b| ≤ 4)
4. |(6 * a) + ((-6) * b)| ≤ 4
⊢ a = b ∈ ℤ

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  b  :  \mBbbZ{}
3.  \mforall{}n:\mBbbN{}\msupplus{}.  (|(2  *  n  *  a)  -  2  *  n  *  b|  \mleq{}  4)
4.  |(2  *  3  *  a)  -  2  *  3  *  b|  \mleq{}  4
\mvdash{}  a  =  b


By

---

Latex:
(RW  IntNormC  (-1)  THENA  Auto)

---

Home Index