---

Step * of Lemma square-req-1-iff

∀x:ℝ. (x ≠ -(r1) ⇒ (x^2 = r1 ⇐⇒ x = r1))
BY
{ (RWO "square-is-one" 0 THEN Auto) }

1
1. x : ℝ
2. x ≠ -(r1)
3. x = -(r1)
⊢ x = r1

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  (x  \mneq{}  -(r1)  {}\mRightarrow{}  (x\^{}2  =  r1  \mLeftarrow{}{}\mRightarrow{}  x  =  r1))


By

---

Latex:
(RWO  "square-is-one"  0  THEN  Auto)

---

Home Index