---

Step * of Lemma rabs-positive

∀x:ℝ. (x ≠ r0 ⇒ rpositive(|x|))
BY
{ ((RWO "rabs-as-rmax" 0 THEN Auto) THEN (FLemma `rneq-zero` [-1] THENA Auto) THEN BLemma `rmax-positive` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  (x  \mneq{}  r0  {}\mRightarrow{}  rpositive(|x|))


By

---

Latex:
((RWO  "rabs-as-rmax"  0  THEN  Auto)
  THEN  (FLemma  `rneq-zero`  [-1]  THENA  Auto)
  THEN  BLemma  `rmax-positive`
  THEN  Auto)

---

Home Index