---

Step * 1 1 1 of Lemma req-int


1. a : ℤ
2. b : ℤ
3. ∀n:ℕ+. (|(2 * n * a) - 2 * n * b| ≤ 4)
4. |(6 * a) + ((-6) * b)| ≤ 4
⊢ a = b ∈ ℤ
BY
{ ((RWO "absval_ifthenelse" (-1) THENA Auto) THEN SplitOnHypITE -1  THEN Auto') }

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "absval\_ifthenelse"  (-1)  THENA  Auto)  THEN  SplitOnHypITE  -1    THEN  Auto')

---

Home Index