---

Step * of Lemma fun-converges-to-sine

No Annotations
lim n→∞.Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤n} = λx.sine(x) for x ∈ (-∞, ∞)
BY
{ (InstLemma `sine-is-limit` []⋅
   THEN InstLemma `fun-series-converges-to-everywhere` 
   [⌜λ2i x.-1^i * (x^(2 * i) + 1)/((2 * i) + 1)!⌝;⌜λ2x.sine(x)⌝]⋅
   THEN Auto
   THEN D 0 With ⌜(r1/r(4))⌝ 
   THEN Auto
   THEN Try ((nRMul ⌜r(4)⌝ 0⋅ THEN Auto))
   THEN D 0 With ⌜m⌝ 
   THEN Auto
   THEN (RWO "rabs-int-rmul-unit" 0 THENA Auto)
   THEN (D -2 THENA Auto)
   THEN DupHyp (-2)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜n = nn ∈ ℕ⌝⋅ THENA Auto)
   THEN ThinVar `n'
   THEN RenameVar `n' (-1)
   THEN (D 0 THENA Auto)) }

1
1. ∀x:ℝ. Σi.-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! = sine(x)
2. m : ℕ+
3. r0 ≤ (r1/r(4))
4. (r1/r(4)) < r1
5. x : {x:ℝ| |x| ≤ r(m)} 
6. n : ℕ
7. m ≤ n
⊢ |(x^(2 * (n + 1)) + 1)/((2 * (n + 1)) + 1)!| ≤ ((r1/r(4)) * |(x^(2 * n) + 1)/((2 * n) + 1)!|)

---

Latex:

---

Latex:
No  Annotations
lim  n\mrightarrow{}\minfty{}.\mSigma{}\{-1\^{}i  *  (x\^{}(2  *  i)  +  1)/((2  *  i)  +  1)!  |  0\mleq{}i\mleq{}n\}  =  \mlambda{}x.sine(x)  for  x  \mmember{}  (-\minfty{},  \minfty{})


By

---

Latex:
(InstLemma  `sine-is-limit`  []\mcdot{}
  THEN  InstLemma  `fun-series-converges-to-everywhere` 
  [\mkleeneopen{}\mlambda{}\msubtwo{}i  x.-1\^{}i  *  (x\^{}(2  *  i)  +  1)/((2  *  i)  +  1)!\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.sine(x)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  D  0  With  \mkleeneopen{}(r1/r(4))\mkleeneclose{} 
  THEN  Auto
  THEN  Try  ((nRMul  \mkleeneopen{}r(4)\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  THEN  D  0  With  \mkleeneopen{}m\mkleeneclose{} 
  THEN  Auto
  THEN  (RWO  "rabs-int-rmul-unit"  0  THENA  Auto)
  THEN  (D  -2  THENA  Auto)
  THEN  DupHyp  (-2)
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}n  =  nn\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `n'
  THEN  RenameVar  `n'  (-1)
  THEN  (D  0  THENA  Auto))

---

Home Index