---

Step * 3 1 2 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
{ (FLemma `rexp-non-decreasing` [-1] THENA Auto) }

1
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
9. e^x1 ≤ e^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:
(FLemma  `rexp-non-decreasing`  [-1]  THENA  Auto)

---

Home Index