---

Step * of Lemma quadratic1_functionality

No Annotations
∀[a,b,c,a',b',c':ℝ].
  (quadratic1(a;b;c) = quadratic1(a';b';c')) supposing 
     ((c = c') and 
     (b = b') and 
     (a = a') and 
     (r0 ≤ ((b * b) - r(4) * a * c)) and 
     a ≠ r0)
BY
{ (Intros
   THEN Unfold `quadratic1` 0
   THEN BLemma `rdiv_functionality`
   THEN Try (BLemma `radd_functionality`)
   THEN Try (Complete ((Auto THEN MemTypeCD THEN Auto THEN RWO "-1< -2< -3<" 0 THEN Auto)))
   THEN RWO "-1 -2 -3" 0
   THEN Auto
   THEN MemTypeCD
   THEN Auto
   THEN RWO "-1< -2< -3<" 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  Unfold  `quadratic1`  0
  THEN  BLemma  `rdiv\_functionality`
  THEN  Try  (BLemma  `radd\_functionality`)
  THEN  Try  (Complete  ((Auto  THEN  MemTypeCD  THEN  Auto  THEN  RWO  "-1<  -2<  -3<"  0  THEN  Auto)))
  THEN  RWO  "-1  -2  -3"  0
  THEN  Auto
  THEN  MemTypeCD
  THEN  Auto
  THEN  RWO  "-1<  -2<  -3<"  0
  THEN  Auto)

---

Home Index