---

Step * of Lemma quadratic2-zero

∀[a,b,c:ℝ].  (quadratic2(a;b;c) = r0) supposing ((b ≤ r0) and (c = r0) and a ≠ r0)
BY
{ (Intros
   THEN (Assert r0 ≤ ((b * b) - r(4) * a * c) BY
               (RWO  "5" 0 THEN Auto))
   THEN (Unhide THENA Auto)
   THEN (Assert ((b * b) - r(4) * a * c) = (b * b) BY
               (RWO "5" 0 THEN Auto))
   THEN (Assert r(2) * a ≠ r0 BY
               (RepeatFor 2 (ParallelOp 4) THEN nRMul ⌜r(2)⌝ 4⋅ THEN Auto))
   THEN Unfold `quadratic2` 0
   THEN (RWO "-2" 0 THENA Auto)
   THEN (RWO  "rsqrt_square" 0 THENA Auto)) }

1
1. a : ℝ
2. b : ℝ
3. c : ℝ
4. a ≠ r0
5. c = r0
6. b ≤ r0
7. r0 ≤ ((b * b) - r(4) * a * c)
8. ((b * b) - r(4) * a * c) = (b * b)
9. r(2) * a ≠ r0
⊢ (-(b) - |b|/r(2) * a) = r0

---

Latex:

---

Latex:
\mforall{}[a,b,c:\mBbbR{}].    (quadratic2(a;b;c)  =  r0)  supposing  ((b  \mleq{}  r0)  and  (c  =  r0)  and  a  \mneq{}  r0)


By

---

Latex:
(Intros
  THEN  (Assert  r0  \mleq{}  ((b  *  b)  -  r(4)  *  a  *  c)  BY
                          (RWO    "5"  0  THEN  Auto))
  THEN  (Unhide  THENA  Auto)
  THEN  (Assert  ((b  *  b)  -  r(4)  *  a  *  c)  =  (b  *  b)  BY
                          (RWO  "5"  0  THEN  Auto))
  THEN  (Assert  r(2)  *  a  \mneq{}  r0  BY
                          (RepeatFor  2  (ParallelOp  4)  THEN  nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  4\mcdot{}  THEN  Auto))
  THEN  Unfold  `quadratic2`  0
  THEN  (RWO  "-2"  0  THENA  Auto)
  THEN  (RWO    "rsqrt\_square"  0  THENA  Auto))

---

Home Index