---

Step * of Lemma rpositive-implies-rnonneg

∀[x:ℝ]. (rpositive(x) ⇒ rnonneg(x))
BY
{ (Auto THEN (BLemma `rnonneg-iff` THEN Auto) THEN RWO "rpositive-iff" (-1) THEN Auto) }

1
1. x : ℝ
2. rpositive2(x)
⊢ rnonneg2(x)

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (rpositive(x)  {}\mRightarrow{}  rnonneg(x))


By

---

Latex:
(Auto  THEN  (BLemma  `rnonneg-iff`  THEN  Auto)  THEN  RWO  "rpositive-iff"  (-1)  THEN  Auto)

---

Home Index