---

Step * of Lemma converges-to-rexp

∀x:ℝ. lim n→∞.approx-rexp(x;n) = e^x
BY
{ ((Unfold `approx-rexp` 0 THEN Auto)
   THEN (InstLemma `cheap-real-upper-bound` [⌜x⌝]⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜((((x 1) + 1) ÷ 2) + 1) = b ∈ ℤ⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN (D 0 THENA Auto)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN Assert ⌜e^x ≤ r(if (b) < (0)  then 1  else 3^b)⌝⋅) }

1
.....assertion..... 
1. x : ℝ
2. b : ℤ
3. x ≤ r(b)
⊢ e^x ≤ r(if (b) < (0)  then 1  else 3^b)

2
1. x : ℝ
2. b : ℤ
3. x ≤ r(b)
4. e^x ≤ r(if (b) < (0)  then 1  else 3^b)
⊢ lim n→∞.if n=0
          then r0
          else eval c = if (b) < (0)  then 1  else 3^b in
               eval nc = n * c in
               eval m = 2 * nc in
               eval a = (x m) - 2 in
                 (e^(r(a))/2 * m within 1/nc) = e^x

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  lim  n\mrightarrow{}\minfty{}.approx-rexp(x;n)  =  e\^{}x


By

---

Latex:
((Unfold  `approx-rexp`  0  THEN  Auto)
  THEN  (InstLemma  `cheap-real-upper-bound`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}((((x  1)  +  1)  \mdiv{}  2)  +  1)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  (D  0  THENA  Auto)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  Assert  \mkleeneopen{}e\^{}x  \mleq{}  r(if  (b)  <  (0)    then  1    else  3\^{}b)\mkleeneclose{}\mcdot{})

---

Home Index