---

Step * of Lemma rnonneg-int

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

1
1. n : ℤ
2. ∀n@0:ℕ+. ((-2) ≤ (2 * n@0 * n))
⊢ 0 ≤ n

2
1. n : ℤ
2. 0 ≤ n
3. n@0 : ℕ+
⊢ (-2) ≤ (2 * n@0 * n)

---

Latex:

---

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


By

---

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

---

Home Index