---

Step * 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)
⊢ v = r0
BY
{ (RWO "fractions-req" (-1) THENA Auto) }

1
1. b : ℝ
2. v : ℝ
3. v1 : ℝ
4. v1 ≠ r0
5. r0 ≤ v
6. ((-(b) + rsqrt(v)) * v1) = ((-(b) - rsqrt(v)) * v1)
⊢ 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)
\mvdash{}  v  =  r0


By

---

Latex:
(RWO  "fractions-req"  (-1)  THENA  Auto)

---

Home Index