---

Step * 3 1 1 of Lemma fast-rexp_wf

.....rewrite subgoal..... 
1. x : ℝ
2. x1 : ℝ
3. (r((x 200) - 2))/400 ≤ x1
4. u : ℝ
5. above x within 1/100 = u ∈ ℝ
6. (u - (r1/r(100))) ≤ x
7. x ≤ u
8. x1 ≤ u
⊢ r0 ≤ e^x1
BY
{ (RWO  "rexp-positive<" 0 THEN Auto) }

---

Latex:

---

Latex:
.....rewrite  subgoal..... 
1.  x  :  \mBbbR{}
2.  x1  :  \mBbbR{}
3.  (r((x  200)  -  2))/400  \mleq{}  x1
4.  u  :  \mBbbR{}
5.  above  x  within  1/100  =  u
6.  (u  -  (r1/r(100)))  \mleq{}  x
7.  x  \mleq{}  u
8.  x1  \mleq{}  u
\mvdash{}  r0  \mleq{}  e\^{}x1


By

---

Latex:
(RWO    "rexp-positive<"  0  THEN  Auto)

---

Home Index