---

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

No Annotations
∀[a,b,c:ℝ].
  ({((b * b) = (r(4) * a * c)) ∧ (quadratic1(a;b;c) = (-(b)/r(2) * a))}) supposing 
     ((quadratic1(a;b;c) = quadratic2(a;b;c)) and 
     (r0 ≤ ((b * b) - r(4) * a * c)) and 
     a ≠ r0)
BY
{ (Unfold `guard` 0
   THEN Auto
   THEN (Assert r(2) * a ≠ r0 BY
               (RepeatFor 2 (ParallelOp 4) THEN Auto THEN nRMul ⌜r(2)⌝ 4⋅ THEN Auto))
   THEN Try (Trivial)
   THEN FLemma `quadratic-1-2-equal-implies` [6]
   THEN Auto) }

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[a,b,c:\mBbbR{}].
    (\{((b  *  b)  =  (r(4)  *  a  *  c))  \mwedge{}  (quadratic1(a;b;c)  =  (-(b)/r(2)  *  a))\})  supposing 
          ((quadratic1(a;b;c)  =  quadratic2(a;b;c))  and 
          (r0  \mleq{}  ((b  *  b)  -  r(4)  *  a  *  c))  and 
          a  \mneq{}  r0)


By

---

Latex:
(Unfold  `guard`  0
  THEN  Auto
  THEN  (Assert  r(2)  *  a  \mneq{}  r0  BY
                          (RepeatFor  2  (ParallelOp  4)  THEN  Auto  THEN  nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  4\mcdot{}  THEN  Auto))
  THEN  Try  (Trivial)
  THEN  FLemma  `quadratic-1-2-equal-implies`  [6]
  THEN  Auto)

---

Home Index