---

Step * of Lemma atan_approx-property

∀[a:{2...}]. ∀[x:ℝ]. ∀[N:ℕ+].
  |arctangent(x) - (r(atan_approx(a;x;N))/r(2 * N))| ≤ (r(2)/r(N)) supposing |x| ≤ (r1/r(a))
BY
{ ((Auto THEN Unfold `atan_approx` 0)
   THEN (GenConclTerm  ⌜atan-log(a;N)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN RenameVar `k' (-1)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (Assert (r1/r(a)) ≤ (r1/r(2)) BY
               (BLemma `rleq-int-fractions` THEN Auto))
   THEN (InstLemma `atan-approx-property` [⌜k⌝;⌜x⌝;⌜N⌝]⋅ THENA Auto)
   THEN Unfold `ireal-approx` -1) }

1
1. a : {2...}
2. x : ℝ
3. N : ℕ+
4. |x| ≤ (r1/r(a))
5. k : {k:ℕ| N ≤ (((2 * k) + 3) * a^((2 * k) + 3))} 
6. (r1/r(a)) ≤ (r1/r(2))
7. |arctan-poly(x;k) - (r(atan-approx(k;x;N))/r(2 * N))| ≤ (r1/r(N))
⊢ |arctangent(x) - (r(atan-approx(k;x;N))/r(2 * N))| ≤ (r(2)/r(N))

---

Latex:

---

Latex:
\mforall{}[a:\{2...\}].  \mforall{}[x:\mBbbR{}].  \mforall{}[N:\mBbbN{}\msupplus{}].
    |arctangent(x)  -  (r(atan\_approx(a;x;N))/r(2  *  N))|  \mleq{}  (r(2)/r(N))  supposing  |x|  \mleq{}  (r1/r(a))


By

---

Latex:
((Auto  THEN  Unfold  `atan\_approx`  0)
  THEN  (GenConclTerm    \mkleeneopen{}atan-log(a;N)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  RenameVar  `k'  (-1)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (Assert  (r1/r(a))  \mleq{}  (r1/r(2))  BY
                          (BLemma  `rleq-int-fractions`  THEN  Auto))
  THEN  (InstLemma  `atan-approx-property`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}N\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `ireal-approx`  -1)

---

Home Index