---

Step * 3 1 of Lemma fast-rexp_wf


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
⊢ |e^x1| ≤ r(canonical-bound(e^u))
BY
{ (RWO "rabs-of-nonneg" 0 THEN Auto) }

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

2
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
⊢ e^x1 ≤ r(canonical-bound(e^u))

---

Latex:

---

Latex:

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{}  |e\^{}x1|  \mleq{}  r(canonical-bound(e\^{}u))


By

---

Latex:
(RWO  "rabs-of-nonneg"  0  THEN  Auto)

---

Home Index