---

Step * of Lemma rabs-rnexp2

∀[x:ℝ]. (|x|^2 = x^2)
BY
{ ((Auto THEN (RWO "rabs-rnexp<" 0 THENA Auto)) THEN RWO  "rabs-of-nonneg" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (|x|\^{}2  =  x\^{}2)


By

---

Latex:
((Auto  THEN  (RWO  "rabs-rnexp<"  0  THENA  Auto))  THEN  RWO    "rabs-of-nonneg"  0  THEN  Auto)

---

Home Index