---

Step * of Lemma reciprocal_qle_wf

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

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

---

Latex:

---

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


By

---

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

---

Home Index