---

Step * 1 of Lemma quadratic-formula-simple

.....antecedent..... 
1. a : ℝ
2. b : ℝ
3. c : ℝ
4. r0 < a
5. c < r0
⊢ r0 ≤ ((b * b) - r(4) * a * c)
BY
{ (nRMul ⌜r(-4)⌝ (-1)⋅ THEN nRMul ⌜a⌝ (-1)⋅) }

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

---

Latex:

---

Latex:
.....antecedent..... 
1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  c  :  \mBbbR{}
4.  r0  <  a
5.  c  <  r0
\mvdash{}  r0  \mleq{}  ((b  *  b)  -  r(4)  *  a  *  c)


By

---

Latex:
(nRMul  \mkleeneopen{}r(-4)\mkleeneclose{}  (-1)\mcdot{}  THEN  nRMul  \mkleeneopen{}a\mkleeneclose{}  (-1)\mcdot{})

---

Home Index