---

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

∀[a,b,c:ℝ].
  ((b * b) = (r(4) * a * c)) supposing 
     ((quadratic1(a;b;c) = quadratic2(a;b;c)) and 
     (r0 ≤ ((b * b) - r(4) * a * c)) and 
     a ≠ r0)
BY
{ (Auto
   THEN (Assert r(2) * a ≠ r0 BY
               (RepeatFor 2 (ParallelOp 4) THEN Auto THEN nRMul ⌜r(2)⌝ 4⋅ THEN Auto))
   THEN (Assert ⌜((b * b) - r(4) * a * c) = r0⌝⋅ THENM Auto)
   THEN Unfolds ``quadratic1 quadratic2`` -2
   THEN RepeatFor 2 (MoveToConcl (-2))
   THEN (GenConclTerm ⌜(b * b) - r(4) * a * c⌝⋅ THENA Auto)
   THEN MoveToConcl (-3)
   THEN (GenConclTerm ⌜r(2) * a⌝⋅ THENA Auto)
   THEN All Thin
   THEN 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:
\mforall{}[a,b,c:\mBbbR{}].
    ((b  *  b)  =  (r(4)  *  a  *  c))  supposing 
          ((quadratic1(a;b;c)  =  quadratic2(a;b;c))  and 
          (r0  \mleq{}  ((b  *  b)  -  r(4)  *  a  *  c))  and 
          a  \mneq{}  r0)


By

---

Latex:
(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  (Assert  \mkleeneopen{}((b  *  b)  -  r(4)  *  a  *  c)  =  r0\mkleeneclose{}\mcdot{}  THENM  Auto)
  THEN  Unfolds  ``quadratic1  quadratic2``  -2
  THEN  RepeatFor  2  (MoveToConcl  (-2))
  THEN  (GenConclTerm  \mkleeneopen{}(b  *  b)  -  r(4)  *  a  *  c\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-3)
  THEN  (GenConclTerm  \mkleeneopen{}r(2)  *  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  Auto)

---

Home Index