---

Step * 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. rsqrt(v) = -(rsqrt(v))
⊢ v = r0
BY
{ nRAdd ⌜rsqrt(v)⌝ (-1)⋅ }

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
⊢ 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.  rsqrt(v)  =  -(rsqrt(v))
\mvdash{}  v  =  r0


By

---

Latex:
nRAdd  \mkleeneopen{}rsqrt(v)\mkleeneclose{}  (-1)\mcdot{}

---

Home Index