---

Step * 1 of Lemma derivative-rexp

.....antecedent..... 
1. lim n→∞.Σ{(x^i)/(i)! | 0≤i≤n} = λx.e^x for x ∈ (-∞, ∞)
⊢ lim n→∞.Σ{(x^i)/(i)! | 0≤i≤n - 1} = λy.e^y for x ∈ (-∞, ∞)
BY
{ (RepeatFor 3 (ParallelLast)
   THEN ExRepD
   THEN (D 0 With ⌜N + 1⌝  THENA Auto)
   THEN ParallelLast
   THEN (D 0 THENA Auto)
   THEN BackThruSomeHyp) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  lim  n\mrightarrow{}\minfty{}.\mSigma{}\{(x\^{}i)/(i)!  |  0\mleq{}i\mleq{}n\}  =  \mlambda{}x.e\^{}x  for  x  \mmember{}  (-\minfty{},  \minfty{})
\mvdash{}  lim  n\mrightarrow{}\minfty{}.\mSigma{}\{(x\^{}i)/(i)!  |  0\mleq{}i\mleq{}n  -  1\}  =  \mlambda{}y.e\^{}y  for  x  \mmember{}  (-\minfty{},  \minfty{})


By

---

Latex:
(RepeatFor  3  (ParallelLast)
  THEN  ExRepD
  THEN  (D  0  With  \mkleeneopen{}N  +  1\mkleeneclose{}    THENA  Auto)
  THEN  ParallelLast
  THEN  (D  0  THENA  Auto)
  THEN  BackThruSomeHyp)

---

Home Index