---

Step * of Lemma small_reciprocal_wf

∀e:{q:ℚ| 0 < q} . (small_reciprocal(e) ∈ {n:ℕ+| (1/n) < e} )
BY
{ xxx((D 0 THENA Auto) THEN Unfold `small_reciprocal` 0 THEN GenConclAtAddr [2;1])xxx }

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

---

Latex:

---

Latex:
\mforall{}e:\{q:\mBbbQ{}|  0  <  q\}  .  (small\_reciprocal(e)  \mmember{}  \{n:\mBbbN{}\msupplus{}|  (1/n)  <  e\}  )


By

---

Latex:
xxx((D  0  THENA  Auto)  THEN  Unfold  `small\_reciprocal`  0  THEN  GenConclAtAddr  [2;1])xxx

---

Home Index