---

Step * 1 of Lemma small_reciprocal_wf


1. e : {q:ℚ| 0 < q} 
2. v : ∃m:ℕ+. (1/m) < e supposing 0 < e
3. (TERMOF{small-reciprocal:o, 1:l} e) = v ∈ ∃m:ℕ+. (1/m) < e supposing 0 < e
⊢ fst(v) ∈ {n:ℕ+| (1/n) < e} 
BY
{ xxx(D 1 THEN D 3 THEN Auto THEN D (-1) THEN Auto)xxx }

---

Latex:

---

Latex:

1.  e  :  \{q:\mBbbQ{}|  0  <  q\} 
2.  v  :  \mexists{}m:\mBbbN{}\msupplus{}.  (1/m)  <  e  supposing  0  <  e
3.  (TERMOF\{small-reciprocal:o,  1:l\}  e)  =  v
\mvdash{}  fst(v)  \mmember{}  \{n:\mBbbN{}\msupplus{}|  (1/n)  <  e\} 


By

---

Latex:
xxx(D  1  THEN  D  3  THEN  Auto  THEN  D  (-1)  THEN  Auto)xxx

---

Home Index