---

Step * 1 1 1 of Lemma equipollent-nat-rationals


1. L : (ℤ × ℕ+) List
2. 0 < ||[1 / map(λp.(snd(p));L)]||
3. 0 ≤ imax-list([1 / map(λp.(snd(p));L)])
⊢ ↑is-qrep(<1, imax-list([1 / map(λp.(snd(p));L)]) + 1>)
BY
{ xxxRepUR ``is-qrep`` 0xxx }

1
1. L : (ℤ × ℕ+) List
2. 0 < ||[1 / map(λp.(snd(p));L)]||
3. 0 ≤ imax-list([1 / map(λp.(snd(p));L)])
⊢ ↑eval g = better-gcd(1;imax-list([1 / map(λp.(snd(p));L)]) + 1) in
   (g =z 1) ∨b(g =z -1)

---

Latex:

---

Latex:

1.  L  :  (\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{})  List
2.  0  <  ||[1  /  map(\mlambda{}p.(snd(p));L)]||
3.  0  \mleq{}  imax-list([1  /  map(\mlambda{}p.(snd(p));L)])
\mvdash{}  \muparrow{}is-qrep(ə,  imax-list([1  /  map(\mlambda{}p.(snd(p));L)])  +  1>)


By

---

Latex:
xxxRepUR  ``is-qrep``  0xxx

---

Home Index