---

Step * of Lemma sine-poly-approx-1

No Annotations
∀[x:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} ]. ∀[k:ℕ].
  (|sine(x) - Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤k}| ≤ (x^(2 * k) + 3/r(((2 * k) + 3)!)))
BY
{ (Auto
   THEN BLemma `rleq-iff-all-rless`
   THEN Auto
   THEN (InstLemma `small-reciprocal-real` [⌜e⌝]⋅ THENA Auto)
   THEN D -1
   THEN (InstLemma `sine-is-limit` [⌜x⌝]⋅ THENA Auto)
   THEN (D -1 With ⌜k1⌝  THENA Auto)
   THEN ExRepD
   THEN (InstHyp [⌜N⌝] (-1)⋅ THENA Auto)
   THEN ((Decide ⌜N ≤ k⌝⋅ THENA Auto)
         THENL [((FHyp (-3) [-1] THENA Auto)
                 THEN (RWO  "rabs-difference-symmetry" 0 THENA Auto)
                 THEN (RWO "-1" 0 THENA Auto))
               ; UseTriangleInequality [⌜Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤N}⌝]⋅]
   )) }

1
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. |Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤N} - sine(x)| ≤ (r1/r(k1))
9. N ≤ k
10. |Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤k} - sine(x)| ≤ (r1/r(k1))
⊢ (r1/r(k1)) ≤ ((x^(2 * k) + 3/r(((2 * k) + 3)!)) + e)

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)
⊢ ((r1/r(k1))
+ |Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤N} - Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤k}|) ≤ ((x^(2 * k)
+ 3/r(((2 * k) + 3)!))
+ e)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[x:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  ].  \mforall{}[k:\mBbbN{}].
    (|sine(x)  -  \mSigma{}\{-1\^{}i  *  (x\^{}(2  *  i)  +  1)/((2  *  i)  +  1)!  |  0\mleq{}i\mleq{}k\}|  \mleq{}  (x\^{}(2  *  k)  +  3/r(((2  *  k)  +  3)!)))


By

---

Latex:
(Auto
  THEN  BLemma  `rleq-iff-all-rless`
  THEN  Auto
  THEN  (InstLemma  `small-reciprocal-real`  [\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  (InstLemma  `sine-is-limit`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}k1\mkleeneclose{}    THENA  Auto)
  THEN  ExRepD
  THEN  (InstHyp  [\mkleeneopen{}N\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  ((Decide  \mkleeneopen{}N  \mleq{}  k\mkleeneclose{}\mcdot{}  THENA  Auto)
              THENL  [((FHyp  (-3)  [-1]  THENA  Auto)
                              THEN  (RWO    "rabs-difference-symmetry"  0  THENA  Auto)
                              THEN  (RWO  "-1"  0  THENA  Auto))
                          ;  UseTriangleInequality  [\mkleeneopen{}\mSigma{}\{-1\^{}i  *  (x\^{}(2  *  i)  +  1)/((2  *  i)  +  1)!  |  0\mleq{}i\mleq{}N\}\mkleeneclose{}]\mcdot{}]
  ))

---

Home Index