---

Step * 1 of Lemma exp-exists


1. ∀x:ℝ. Σn.(x^n)/(n)!↓
⊢ ∀x:ℝ. ∃a:ℝ. Σn.(x^n)/(n)! = a
BY
{ xxx((D 0 THENA Auto) THEN (Evaluate ⌜y = x ∈ ℝ⌝⋅ THENA (Auto THEN D 0 THEN With ⌜1⌝ (D 0)⋅ THEN Auto)))xxx }

1
1. ∀x:ℝ. Σn.(x^n)/(n)!↓
2. x : ℝ
3. y : ℝ
4. y = x ∈ ℝ
⊢ ∃a:ℝ. Σn.(x^n)/(n)! = a

---

Latex:

---

Latex:

1.  \mforall{}x:\mBbbR{}.  \mSigma{}n.(x\^{}n)/(n)!\mdownarrow{}
\mvdash{}  \mforall{}x:\mBbbR{}.  \mexists{}a:\mBbbR{}.  \mSigma{}n.(x\^{}n)/(n)!  =  a


By

---

Latex:
xxx((D  0  THENA  Auto)
        THEN  (Evaluate  \mkleeneopen{}y  =  x\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  D  0  THEN  With  \mkleeneopen{}1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))
        )xxx

---

Home Index