---

Step * 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)
⊢ v = r0
BY
{ ((Assert (-(b) + rsqrt(v)) = (-(b) - rsqrt(v)) BY (nRMul ⌜v1⌝ 0⋅ THEN Auto)) THEN (nRAdd ⌜b⌝ (-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)
7. rsqrt(v) = -(rsqrt(v))
⊢ 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:
((Assert  (-(b)  +  rsqrt(v))  =  (-(b)  -  rsqrt(v))  BY
                (nRMul  \mkleeneopen{}v1\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  THEN  (nRAdd  \mkleeneopen{}b\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  )

---

Home Index