---

Step * 1 of Lemma reciprocal_qle_wf


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index