---

Step * 2 of Lemma rexp-of-nonneg-stronger


1. x : ℝ
2. r0 ≤ x
3. Σn.(x^n)/(n)! = e^x
4. Σi.if (i =z 0) then r1
if (i =z 1) then x
else r0
fi  = r1 + x
⊢ (r1 + x) ≤ e^x
BY
{ ((All (Unfold `series-sum`) THEN FLemma `rleq-limit` [-1;-2] THEN Auto)
   THEN (BLemma `rsum_functionality_wrt_rleq`  THEN Auto)
   THEN D 0
   THEN Auto
   THEN (RWO  "int-rdiv-req" 0 THENA Auto)) }

1
1. x : ℝ
2. r0 ≤ x
3. lim n→∞.Σ{(x^i)/(i)! | 0≤i≤n} = e^x
4. lim i→∞.Σ{if (i =z 0) then r1
if (i =z 1) then x
else r0
fi  | 0≤i≤i} = r1 + x
5. n : ℕ
6. i : ℤ
7. 0 ≤ i
8. i ≤ n
⊢ if (i =z 0) then r1
if (i =z 1) then x
else r0
fi  ≤ (x^i/r((i)!))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  r0  \mleq{}  x
3.  \mSigma{}n.(x\^{}n)/(n)!  =  e\^{}x
4.  \mSigma{}i.if  (i  =\msubz{}  0)  then  r1
if  (i  =\msubz{}  1)  then  x
else  r0
fi    =  r1  +  x
\mvdash{}  (r1  +  x)  \mleq{}  e\^{}x


By

---

Latex:
((All  (Unfold  `series-sum`)  THEN  FLemma  `rleq-limit`  [-1;-2]  THEN  Auto)
  THEN  (BLemma  `rsum\_functionality\_wrt\_rleq`    THEN  Auto)
  THEN  D  0
  THEN  Auto
  THEN  (RWO    "int-rdiv-req"  0  THENA  Auto))

---

Home Index