---

Step * 1 1 2 1 2 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)])
4. ↑is-qrep(<1, imax-list([1 / map(λp.(snd(p));L)]) + 1>)
5. i : ℕ
6. i < ||L||
7. <1, imax-list([1 / map(λp.(snd(p));L)]) + 1> = L[i] ∈ (ℤ × ℕ+)
8. y1 : ℤ
9. y2 : ℕ+
10. (<y1, y2> ∈ L)
11. (imax-list([1 / map(λp.(snd(p));L)]) + 1) = y2 ∈ ℕ+
⊢ (∃b∈[1 / map(λp.(snd(p));L)]. y2 ≤ b)
BY
{ xxx((BLemma `l_exists_iff` THEN Auto) THEN With ⌜y2⌝ (D 0)⋅ THEN Auto)xxx }

1
1. L : (ℤ × ℕ+) List
2. 0 < ||[1 / map(λp.(snd(p));L)]||
3. 0 ≤ imax-list([1 / map(λp.(snd(p));L)])
4. ↑is-qrep(<1, imax-list([1 / map(λp.(snd(p));L)]) + 1>)
5. i : ℕ
6. i < ||L||
7. <1, imax-list([1 / map(λp.(snd(p));L)]) + 1> = L[i] ∈ (ℤ × ℕ+)
8. y1 : ℤ
9. y2 : ℕ+
10. (<y1, y2> ∈ L)
11. (imax-list([1 / map(λp.(snd(p));L)]) + 1) = y2 ∈ ℕ+
⊢ (y2 ∈ [1 / map(λp.(snd(p));L)])

---

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)])
4.  \muparrow{}is-qrep(ə,  imax-list([1  /  map(\mlambda{}p.(snd(p));L)])  +  1>)
5.  i  :  \mBbbN{}
6.  i  <  ||L||
7.  ə,  imax-list([1  /  map(\mlambda{}p.(snd(p));L)])  +  1>  =  L[i]
8.  y1  :  \mBbbZ{}
9.  y2  :  \mBbbN{}\msupplus{}
10.  (<y1,  y2>  \mmember{}  L)
11.  (imax-list([1  /  map(\mlambda{}p.(snd(p));L)])  +  1)  =  y2
\mvdash{}  (\mexists{}b\mmember{}[1  /  map(\mlambda{}p.(snd(p));L)].  y2  \mleq{}  b)


By

---

Latex:
xxx((BLemma  `l\_exists\_iff`  THEN  Auto)  THEN  With  \mkleeneopen{}y2\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)xxx

---

Home Index