---

Step * 1 1 1 1 of Lemma quadratic-1-2-equal-implies


1. b : ℝ
2. v : ℝ
3. v1 : ℝ
4. v1 ≠ r0
5. r0 ≤ v
6. ((-(b) + rsqrt(v)) * v1) = ((-(b) - rsqrt(v)) * v1)
7. (r(2) * rsqrt(v)) = r0
⊢ v = r0
BY
{ (Assert rsqrt(v) = r0 BY
         (nRMul ⌜r(2)⌝ 0⋅ THEN Auto)) }

1
1. b : ℝ
2. v : ℝ
3. v1 : ℝ
4. v1 ≠ r0
5. r0 ≤ v
6. ((-(b) + rsqrt(v)) * v1) = ((-(b) - rsqrt(v)) * v1)
7. (r(2) * rsqrt(v)) = r0
8. rsqrt(v) = r0
⊢ v = r0

---

Latex:

---

Latex:

1.  b  :  \mBbbR{}
2.  v  :  \mBbbR{}
3.  v1  :  \mBbbR{}
4.  v1  \mneq{}  r0
5.  r0  \mleq{}  v
6.  ((-(b)  +  rsqrt(v))  *  v1)  =  ((-(b)  -  rsqrt(v))  *  v1)
7.  (r(2)  *  rsqrt(v))  =  r0
\mvdash{}  v  =  r0


By

---

Latex:
(Assert  rsqrt(v)  =  r0  BY
              (nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  0\mcdot{}  THEN  Auto))

---

Home Index