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