---

Step * of Lemma square-req-iff

∀x,y:ℝ.  ((r0 ≤ x) ⇒ (r0 ≤ y) ⇒ (x = y ⇐⇒ x^2 = y^2))
BY
{ ((UnivCD THENA Auto) THEN RWO  "rnexp-req-iff-even<" 0 THEN Auto THEN RWO  "rabs-of-nonneg" (-1) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    ((r0  \mleq{}  x)  {}\mRightarrow{}  (r0  \mleq{}  y)  {}\mRightarrow{}  (x  =  y  \mLeftarrow{}{}\mRightarrow{}  x\^{}2  =  y\^{}2))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RWO    "rnexp-req-iff-even<"  0
  THEN  Auto
  THEN  RWO    "rabs-of-nonneg"  (-1)
  THEN  Auto)

---

Home Index