---

Step * 1 of Lemma req-int


1. a : ℤ
2. b : ℤ
3. r(a) = r(b)
⊢ a = b ∈ ℤ
BY
{ (RepUR ``req int-to-real`` (-1) THEN (InstHyp [⌜3⌝] (-1)⋅ THENA Auto)) }

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

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  b  :  \mBbbZ{}
3.  r(a)  =  r(b)
\mvdash{}  a  =  b


By

---

Latex:
(RepUR  ``req  int-to-real``  (-1)  THEN  (InstHyp  [\mkleeneopen{}3\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto))

---

Home Index