---

Step * of Lemma rabs-bounds

∀[x:ℝ]. ((-(|x|) ≤ x) ∧ (x ≤ |x|))
BY
{ ((D 0 THENA Auto) THEN ((InstLemma `rleq-rmax` [⌜x⌝; ⌜-(x)⌝])⋅ THENA Auto) THEN RWO "rabs-as-rmax<" (-1) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  ((-(|x|)  \mleq{}  x)  \mwedge{}  (x  \mleq{}  |x|))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  ((InstLemma  `rleq-rmax`  [\mkleeneopen{}x\mkleeneclose{};  \mkleeneopen{}-(x)\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  RWO  "rabs-as-rmax<"  (-1)
  THEN  Auto)

---

Home Index