---

Step * 2 3 of Lemma sine-poly-approx-1

.....antecedent..... 
1. x : {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} 
2. k : ℕ
3. e : {e:ℝ| r0 < e} 
4. k1 : ℕ+
5. (r1/r(k1)) < e
6. N : ℕ
7. ∀i:ℕ. ((N ≤ i) ⇒ (|Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤i} - sine(x)| ≤ (r1/r(k1))))
8. |sine(x) - Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤N}| ≤ (r1/r(k1))
9. ¬(N ≤ k)
⊢ lim n→∞.(x^(2 * n) + 1)/((2 * n) + 1)! = r0
BY
{ (Assert lim i→∞.(x^2 * i)/((2 * i) + 1)! = r0 BY
         ((InstLemma `rdiv-factorial-limit-zero-from-bound2` [⌜x⌝;⌜1⌝]⋅
           THENA (Auto THEN RWO "rabs-of-nonneg" 0 THEN Auto)
           )⋅
          THEN (InstLemma `subsequence-converges` [⌜r0⌝;⌜λ2n.(|x|^n/r((n + 1)!))⌝]⋅ THENM BHyp (-1))⋅
          THEN Auto)) }

1
.....aux..... 
1. x : {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} 
2. k : ℕ
3. e : {e:ℝ| r0 < e} 
4. k1 : ℕ+
5. (r1/r(k1)) < e
6. N : ℕ
7. ∀i:ℕ. ((N ≤ i) ⇒ (|Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤i} - sine(x)| ≤ (r1/r(k1))))
8. |sine(x) - Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤N}| ≤ (r1/r(k1))
9. ¬(N ≤ k)
10. lim n→∞.(|x|^n/r((n + 1)!)) = r0
11. ∀y:ℕ ⟶ ℝ
      ((∃N:ℕ. ∀n:ℕ. ∃m:ℕ. ((n ≤ m) ∧ (y[n] = (|x|^m/r((m + 1)!)))) supposing N ≤ n)
      ⇒ lim n→∞.(|x|^n/r((n + 1)!)) = r0
      ⇒ lim n→∞.y[n] = r0)
⊢ ∃N:ℕ. ∀i:ℕ. ∃m:ℕ. ((i ≤ m) ∧ ((x^2 * i)/((2 * i) + 1)! = (|x|^m/r((m + 1)!)))) supposing N ≤ i

2
1. x : {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} 
2. k : ℕ
3. e : {e:ℝ| r0 < e} 
4. k1 : ℕ+
5. (r1/r(k1)) < e
6. N : ℕ
7. ∀i:ℕ. ((N ≤ i) ⇒ (|Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤i} - sine(x)| ≤ (r1/r(k1))))
8. |sine(x) - Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤N}| ≤ (r1/r(k1))
9. ¬(N ≤ k)
10. lim i→∞.(x^2 * i)/((2 * i) + 1)! = r0
⊢ lim n→∞.(x^(2 * n) + 1)/((2 * n) + 1)! = r0

---

Latex:

---

Latex:
.....antecedent..... 
1.  x  :  \{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\} 
2.  k  :  \mBbbN{}
3.  e  :  \{e:\mBbbR{}|  r0  <  e\} 
4.  k1  :  \mBbbN{}\msupplus{}
5.  (r1/r(k1))  <  e
6.  N  :  \mBbbN{}
7.  \mforall{}i:\mBbbN{}.  ((N  \mleq{}  i)  {}\mRightarrow{}  (|\mSigma{}\{-1\^{}i  *  (x\^{}(2  *  i)  +  1)/((2  *  i)  +  1)!  |  0\mleq{}i\mleq{}i\}  -  sine(x)|  \mleq{}  (r1/r(k1))))
8.  |sine(x)  -  \mSigma{}\{-1\^{}i  *  (x\^{}(2  *  i)  +  1)/((2  *  i)  +  1)!  |  0\mleq{}i\mleq{}N\}|  \mleq{}  (r1/r(k1))
9.  \mneg{}(N  \mleq{}  k)
\mvdash{}  lim  n\mrightarrow{}\minfty{}.(x\^{}(2  *  n)  +  1)/((2  *  n)  +  1)!  =  r0


By

---

Latex:
(Assert  lim  i\mrightarrow{}\minfty{}.(x\^{}2  *  i)/((2  *  i)  +  1)!  =  r0  BY
              ((InstLemma  `rdiv-factorial-limit-zero-from-bound2`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]\mcdot{}
                  THENA  (Auto  THEN  RWO  "rabs-of-nonneg"  0  THEN  Auto)
                  )\mcdot{}
                THEN  (InstLemma  `subsequence-converges`  [\mkleeneopen{}r0\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}n.(|x|\^{}n/r((n  +  1)!))\mkleeneclose{}]\mcdot{}  THENM  BHyp  (-1))\mcdot{}
                THEN  Auto))

---

Home Index