---

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


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

1
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))

---

Latex:

---

Latex:

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


By

---

Latex:
(Assert  r0  <  (d  -  e)  BY
              ((nRAdd  \mkleeneopen{}e\mkleeneclose{}  0\mcdot{}  THEN  Auto)  THEN  nRAdd  \mkleeneopen{}e\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto))

---

Home Index