---

Step * of Lemma quadratic-formula-simple

No Annotations
∀a,b,c:ℝ.
  ((r0 < a)
  ⇒ (c < r0)
  ⇒ (∀x:ℝ. (((x = quadratic1(a;b;c)) ∨ (x = quadratic2(a;b;c))) ⇒ (((a * x^2) + (b * x) + c) = r0))))
BY
{ (InstLemma `quadratic-formula1` [] THEN RepeatFor 5 ((ParallelLast' THENA Auto))) }

1
.....antecedent..... 
1. a : ℝ
2. b : ℝ
3. c : ℝ
4. r0 < a
5. c < r0
⊢ r0 ≤ ((b * b) - r(4) * a * c)

---

Latex:

---

Latex:
No  Annotations
\mforall{}a,b,c:\mBbbR{}.
    ((r0  <  a)
    {}\mRightarrow{}  (c  <  r0)
    {}\mRightarrow{}  (\mforall{}x:\mBbbR{}
                (((x  =  quadratic1(a;b;c))  \mvee{}  (x  =  quadratic2(a;b;c)))  {}\mRightarrow{}  (((a  *  x\^{}2)  +  (b  *  x)  +  c)  =  r0))))


By

---

Latex:
(InstLemma  `quadratic-formula1`  []  THEN  RepeatFor  5  ((ParallelLast'  THENA  Auto)))

---

Home Index