---

Step * of Lemma derivative-rexp

d(e^x)/dx = λx.e^x on (-∞, ∞)
BY
{ (InstLemma `fun-converges-to-rexp` []
   THEN InstLemma `fun-converges-to-derivative` [⌜(-∞, ∞)⌝;⌜λ2n x.Σ{(x^i)/(i)! | 0≤i≤n}⌝;
   ⌜λ2n x.Σ{(x^i)/(i)! | 0≤i≤n - 1}⌝;⌜λ2x.e^x⌝;⌜λ2x.e^x⌝]⋅
   THEN Auto) }

1
.....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 ∈ (-∞, ∞)

2
1. lim n→∞.Σ{(x^i)/(i)! | 0≤i≤n} = λx.e^x for x ∈ (-∞, ∞)
2. n : ℕ
⊢ d(Σ{(x^i)/(i)! | 0≤i≤n})/dx = λx.Σ{(x^i)/(i)! | 0≤i≤n - 1} on (-∞, ∞)

---

Latex:

---

Latex:
d(e\^{}x)/dx  =  \mlambda{}x.e\^{}x  on  (-\minfty{},  \minfty{})


By

---

Latex:
(InstLemma  `fun-converges-to-rexp`  []
  THEN  InstLemma  `fun-converges-to-derivative`  [\mkleeneopen{}(-\minfty{},  \minfty{})\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}n  x.\mSigma{}\{(x\^{}i)/(i)!  |  0\mleq{}i\mleq{}n\}\mkleeneclose{};
  \mkleeneopen{}\mlambda{}\msubtwo{}n  x.\mSigma{}\{(x\^{}i)/(i)!  |  0\mleq{}i\mleq{}n  -  1\}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.e\^{}x\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.e\^{}x\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index