---

Step * of Lemma quadratic2_wf

No Annotations
∀[a,b,c:ℝ].  (quadratic2(a;b;c) ∈ ℝ) supposing ((r0 ≤ ((b * b) - r(4) * a * c)) and a ≠ r0)
BY
{ (ProveWfLemma THEN RepeatFor 2 (ParallelOp -2) THEN nRMul ⌜r(2)⌝ (-2)⋅ THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(ProveWfLemma  THEN  RepeatFor  2  (ParallelOp  -2)  THEN  nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  (-2)\mcdot{}  THEN  Auto)

---

Home Index