---

Step * of Lemma rexp-approx-property

∀[x:ℝ]. ∀[k:ℕ]. ∀[N:ℕ+].  ((|x| ≤ (r1/r(4))) ⇒ 1-approx(Σ{(x^i)/(i)! | 0≤i≤k};N;rexp-approx(x;k;N)))
BY
{ (Auto
   THEN ((InstLemma `poly-approx-property` 
          [⌜k⌝;⌜λi.(r1)/(i)!⌝;⌜x⌝;⌜N⌝]⋅
          THENA Auto
          )
         THEN Reduce -1
         THEN Fold `rexp-approx` (-1)
         THEN (Assert Σ{(r1)/(i)! * x^i | 0≤i≤k} = Σ{(x^i)/(i)! | 0≤i≤k} BY
                     ((BLemma `rsum_functionality` THENM D 0)
                      THEN Auto
                      THEN (GenConcl ⌜(i)! = M ∈ ℕ+⌝⋅ THENA Auto)
                      THEN (RWW "int-rdiv-req" 0 THENM nRNorm 0)
                      THEN Auto))
         THEN RWO  "-1" (-2)
         THEN Auto)⋅
   ) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  \mforall{}[k:\mBbbN{}].  \mforall{}[N:\mBbbN{}\msupplus{}].
    ((|x|  \mleq{}  (r1/r(4)))  {}\mRightarrow{}  1-approx(\mSigma{}\{(x\^{}i)/(i)!  |  0\mleq{}i\mleq{}k\};N;rexp-approx(x;k;N)))


By

---

Latex:
(Auto
  THEN  ((InstLemma  `poly-approx-property` 
                [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}\mlambda{}i.(r1)/(i)!\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}N\mkleeneclose{}]\mcdot{}
                THENA  Auto
                )
              THEN  Reduce  -1
              THEN  Fold  `rexp-approx`  (-1)
              THEN  (Assert  \mSigma{}\{(r1)/(i)!  *  x\^{}i  |  0\mleq{}i\mleq{}k\}  =  \mSigma{}\{(x\^{}i)/(i)!  |  0\mleq{}i\mleq{}k\}  BY
                                      ((BLemma  `rsum\_functionality`  THENM  D  0)
                                        THEN  Auto
                                        THEN  (GenConcl  \mkleeneopen{}(i)!  =  M\mkleeneclose{}\mcdot{}  THENA  Auto)
                                        THEN  (RWW  "int-rdiv-req"  0  THENM  nRNorm  0)
                                        THEN  Auto))
              THEN  RWO    "-1"  (-2)
              THEN  Auto)\mcdot{}
  )

---

Home Index