---

Step * 1 1 1 of Lemma r2-left-right-lemma


1. d : ℝ
2. e : ℝ
3. r0 < d
4. r0 < -(e)
5. r0 < (d - e)
⊢ ∃t:ℝ. (((r0 ≤ t) ∧ (t ≤ r1)) ∧ ((e + (d * t) + -(e * t)) = r0))
BY
{ (D 0 With ⌜(-(e)/d - e)⌝  THEN Auto THEN nRMul ⌜d - e⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  d  :  \mBbbR{}
2.  e  :  \mBbbR{}
3.  r0  <  d
4.  r0  <  -(e)
5.  r0  <  (d  -  e)
\mvdash{}  \mexists{}t:\mBbbR{}.  (((r0  \mleq{}  t)  \mwedge{}  (t  \mleq{}  r1))  \mwedge{}  ((e  +  (d  *  t)  +  -(e  *  t))  =  r0))


By

---

Latex:
(D  0  With  \mkleeneopen{}(-(e)/d  -  e)\mkleeneclose{}    THEN  Auto  THEN  nRMul  \mkleeneopen{}d  -  e\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index