---

Step * 1 1 of Lemma equipollent-nat-rationals


1. L : (ℤ × ℕ+) List
⊢ ∃p:ℤ × ℕ+. ((↑is-qrep(p)) ∧ (¬(p ∈ L)))
BY
{ ((Assert 0 < ||[1 / map(λp.(snd(p));L)]|| BY
          (Reduce  0⋅ THEN RWW "length-map" 0 THEN Auto THEN Auto'))
   THEN (Assert 0 ≤ imax-list([1 / map(λp.(snd(p));L)]) BY
               (BLemma `imax-list-ub` ⋅ THEN Auto THEN With ⌜0⌝ (D 0)⋅ THEN Reduce 0 THEN Auto))⋅
   THEN With ⌜<1, imax-list([1 / map(λp.(snd(p));L)]) + 1>⌝ (D 0)⋅
   THEN Reduce 0
   THEN Auto) }

1
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>)

2
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>)
⊢ ¬(<1, imax-list([1 / map(λp.(snd(p));L)]) + 1> ∈ L)

---

Latex:

---

Latex:

1.  L  :  (\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{})  List
\mvdash{}  \mexists{}p:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}.  ((\muparrow{}is-qrep(p))  \mwedge{}  (\mneg{}(p  \mmember{}  L)))


By

---

Latex:
((Assert  0  <  ||[1  /  map(\mlambda{}p.(snd(p));L)]||  BY
                (Reduce    0\mcdot{}  THEN  RWW  "length-map"  0  THEN  Auto  THEN  Auto'))
  THEN  (Assert  0  \mleq{}  imax-list([1  /  map(\mlambda{}p.(snd(p));L)])  BY
                          (BLemma  `imax-list-ub`  \mcdot{}  THEN  Auto  THEN  With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Reduce  0  THEN  Auto))\mcdot{}
  THEN  With  \mkleeneopen{}ə,  imax-list([1  /  map(\mlambda{}p.(snd(p));L)])  +  1>\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Reduce  0
  THEN  Auto)

---

Home Index