---

Step * of Lemma rsqrt-unique2

∀[x:{x:ℝ| r0 ≤ x} ]. ∀[s:ℝ].  uiff((s * s) = x;¬¬((s = rsqrt(x)) ∨ (s = -(rsqrt(x)))))
BY
{ Auto }

1
1. x : {x:ℝ| r0 ≤ x} 
2. s : ℝ
3. (s * s) = x
⊢ ¬¬((s = rsqrt(x)) ∨ (s = -(rsqrt(x))))

2
1. x : {x:ℝ| r0 ≤ x} 
2. s : ℝ
3. ¬¬((s = rsqrt(x)) ∨ (s = -(rsqrt(x))))
⊢ (s * s) = x

---

Latex:

---

Latex:
\mforall{}[x:\{x:\mBbbR{}|  r0  \mleq{}  x\}  ].  \mforall{}[s:\mBbbR{}].    uiff((s  *  s)  =  x;\mneg{}\mneg{}((s  =  rsqrt(x))  \mvee{}  (s  =  -(rsqrt(x)))))


By

---

Latex:
Auto

---

Home Index