---

Step * of Lemma sine-approx-for-small

∀a:{2...}. ∀N:ℕ+. ∀x:{x:ℝ| |x| ≤ (r1/r(a))} .  (∃z:ℤ [(|sine(x) - (r(z)/r(2 * N))| ≤ (r(2)/r(N)))])
BY
{ (Auto
   THEN (Assert (r1/r(a)) ≤ (r1/r(2)) BY
               Auto)
   THEN (Assert |x| ≤ (r1/r(2)) BY
               (DVar `x' THEN Unhide THEN Auto))
   THEN (InstLemma `sine-approx-lemma-ext` [⌜a⌝;⌜N⌝]⋅ THENA Auto)
   THEN D -1
   THEN D 0 With ⌜sine-approx(x;k;N)⌝ 
   THEN Auto
   THEN (RWO "sine-poly-approx" 0 THENA Auto)) }

1
1. a : {2...}
2. N : ℕ+
3. x : {x:ℝ| |x| ≤ (r1/r(a))} 
4. (r1/r(a)) ≤ (r1/r(2))
5. |x| ≤ (r1/r(2))
6. k : ℕ
7. N ≤ (a^((2 * k) + 3) * ((2 * k) + 3)!)
⊢ ((|x|^(2 * k) + 3/r(((2 * k) + 3)!)) + (r1/r(N))) ≤ (r(2)/r(N))

---

Latex:

---

Latex:
\mforall{}a:\{2...\}.  \mforall{}N:\mBbbN{}\msupplus{}.  \mforall{}x:\{x:\mBbbR{}|  |x|  \mleq{}  (r1/r(a))\}  .    (\mexists{}z:\mBbbZ{}  [(|sine(x)  -  (r(z)/r(2  *  N))|  \mleq{}  (r(2)/r(N)))])


By

---

Latex:
(Auto
  THEN  (Assert  (r1/r(a))  \mleq{}  (r1/r(2))  BY
                          Auto)
  THEN  (Assert  |x|  \mleq{}  (r1/r(2))  BY
                          (DVar  `x'  THEN  Unhide  THEN  Auto))
  THEN  (InstLemma  `sine-approx-lemma-ext`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}N\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  D  0  With  \mkleeneopen{}sine-approx(x;k;N)\mkleeneclose{} 
  THEN  Auto
  THEN  (RWO  "sine-poly-approx"  0  THENA  Auto))

---

Home Index