---

Step * 3 of Lemma fast-rexp_wf


1. x : ℝ
2. x1 : {x1:ℝ| x1 ∈ [(r((x 200) - 2))/400, (r((x 200) + 2))/400]} 
⊢ |e^x1| ≤ r(canonical-bound(e^(r((x 200) + 2))/400))
BY
{ ((D -1 THEN (Unhide THENA Auto))
   THEN Reduce -1
   THEN D -1
   THEN MoveToConcl (-1)
   THEN (Subst' (r((x 200) + 2))/400 ~ above x within 1/100 0
         THENA (Unfold `rational-upper-approx` 0 THEN Reduce 0 THEN CallByValueReduce 0 THEN Auto)
         )
   THEN (InstLemma `rational-upper-approx-property` [⌜x⌝;⌜100⌝]⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN GenConcl ⌜above x within 1/100 = u ∈ ℝ⌝⋅
   THEN 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
⊢ |e^x1| ≤ r(canonical-bound(e^u))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  x1  :  \{x1:\mBbbR{}|  x1  \mmember{}  [(r((x  200)  -  2))/400,  (r((x  200)  +  2))/400]\} 
\mvdash{}  |e\^{}x1|  \mleq{}  r(canonical-bound(e\^{}(r((x  200)  +  2))/400))


By

---

Latex:
((D  -1  THEN  (Unhide  THENA  Auto))
  THEN  Reduce  -1
  THEN  D  -1
  THEN  MoveToConcl  (-1)
  THEN  (Subst'  (r((x  200)  +  2))/400  \msim{}  above  x  within  1/100  0
              THENA  (Unfold  `rational-upper-approx`  0  THEN  Reduce  0  THEN  CallByValueReduce  0  THEN  Auto)
              )
  THEN  (InstLemma  `rational-upper-approx-property`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}100\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  GenConcl  \mkleeneopen{}above  x  within  1/100  =  u\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index