---

Step * 1 of Lemma zero-rleq-rabs


1. x : ℝ
2. rnonneg(|x|)
⊢ r0 ≤ |x|
BY
{ (Unfold `rleq` 0 THEN nRNorm 0 THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  rnonneg(|x|)
\mvdash{}  r0  \mleq{}  |x|


By

---

Latex:
(Unfold  `rleq`  0  THEN  nRNorm  0  THEN  Auto)

---

Home Index