---

Step * of Lemma rpositive-int

∀[n:ℤ]. uiff(rpositive(r(n));0 < n)
BY
{ (RepUR ``int-to-real rpositive`` 0 THEN Auto THEN ExRepD) }

1
1. n : ℤ
2. n@0 : ℕ+
3. 4 < 2 * n@0 * n
⊢ 0 < n

2
1. [n] : ℤ
2. 0 < n
⊢ ∃n@0:{ℕ+| 4 < 2 * n@0 * n}

---

Latex:

---

Latex:
\mforall{}[n:\mBbbZ{}].  uiff(rpositive(r(n));0  <  n)


By

---

Latex:
(RepUR  ``int-to-real  rpositive``  0  THEN  Auto  THEN  ExRepD)

---

Home Index