---

Step * of Lemma quadratic1-one

No Annotations
∀[a,b,c:ℝ].  (quadratic1(a;b;c) = r1) supposing ((c ≤ a) and (b = -(a + c)) and (r0 < a))
BY
{ (Intros
   THEN (Assert ((b * b) - r(4) * a * c) = ((a - c) * (a - c)) BY
               ((Unhide THENA Auto) THEN (RWO "-2" 0 THENM nRNorm 0) THEN Auto))
   THEN (Assert r0 ≤ ((b * b) - r(4) * a * c) BY
               ((Unhide THENA Auto) THEN RWO "-1" 0 THEN Auto))
   THEN (Unhide THENA Auto)
   THEN DupHyp 4
   THEN nRMul ⌜r(2)⌝ (-1)⋅
   THEN Unfold `quadratic1` 0
   THEN (RWO "-3" 0 THENA Auto)
   THEN (RWO "rsqrt_square" 0 THENA Auto)) }

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[a,b,c:\mBbbR{}].    (quadratic1(a;b;c)  =  r1)  supposing  ((c  \mleq{}  a)  and  (b  =  -(a  +  c))  and  (r0  <  a))


By

---

Latex:
(Intros
  THEN  (Assert  ((b  *  b)  -  r(4)  *  a  *  c)  =  ((a  -  c)  *  (a  -  c))  BY
                          ((Unhide  THENA  Auto)  THEN  (RWO  "-2"  0  THENM  nRNorm  0)  THEN  Auto))
  THEN  (Assert  r0  \mleq{}  ((b  *  b)  -  r(4)  *  a  *  c)  BY
                          ((Unhide  THENA  Auto)  THEN  RWO  "-1"  0  THEN  Auto))
  THEN  (Unhide  THENA  Auto)
  THEN  DupHyp  4
  THEN  nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  (-1)\mcdot{}
  THEN  Unfold  `quadratic1`  0
  THEN  (RWO  "-3"  0  THENA  Auto)
  THEN  (RWO  "rsqrt\_square"  0  THENA  Auto))

---

Home Index