---

Step * 1 1 1 1 of Lemma atan_approx-property


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))
8. |arctangent(x) - arctan-poly(x;k)| ≤ (|x|^(2 * k) + 3/r((2 * k) + 3))
9. |x|^(2 * k) + 3 ≤ (r1/r(a))^(2 * k) + 3
⊢ (|x|^(2 * k) + 3/r((2 * k) + 3)) ≤ (r1/r(N))
BY
{ ((Assert 0 < a^((2 * k) + 3) BY
          (BLemma `exp-positive` THEN Auto))
   THEN (Assert r0 < r(a)^(2 * k) + 3 BY
               (RWO "rnexp-int" 0 THEN Auto))
   THEN (RWO "rnexp-rdiv<" (-3) THENA Auto)
   THEN RWO "rnexp-int" (-3)
   THEN Auto) }

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))
8. |arctangent(x) - arctan-poly(x;k)| ≤ (|x|^(2 * k) + 3/r((2 * k) + 3))
9. |x|^(2 * k) + 3 ≤ (r(1^((2 * k) + 3))/r(a^((2 * k) + 3)))
10. 0 < a^((2 * k) + 3)
11. r0 < r(a)^(2 * k) + 3
⊢ (|x|^(2 * k) + 3/r((2 * k) + 3)) ≤ (r1/r(N))

---

Latex:

---

Latex:

1.  a  :  \{2...\}
2.  x  :  \mBbbR{}
3.  N  :  \mBbbN{}\msupplus{}
4.  |x|  \mleq{}  (r1/r(a))
5.  k  :  \{k:\mBbbN{}|  N  \mleq{}  (((2  *  k)  +  3)  *  a\^{}((2  *  k)  +  3))\} 
6.  (r1/r(a))  \mleq{}  (r1/r(2))
7.  |arctan-poly(x;k)  -  (r(atan-approx(k;x;N))/r(2  *  N))|  \mleq{}  (r1/r(N))
8.  |arctangent(x)  -  arctan-poly(x;k)|  \mleq{}  (|x|\^{}(2  *  k)  +  3/r((2  *  k)  +  3))
9.  |x|\^{}(2  *  k)  +  3  \mleq{}  (r1/r(a))\^{}(2  *  k)  +  3
\mvdash{}  (|x|\^{}(2  *  k)  +  3/r((2  *  k)  +  3))  \mleq{}  (r1/r(N))


By

---

Latex:
((Assert  0  <  a\^{}((2  *  k)  +  3)  BY
                (BLemma  `exp-positive`  THEN  Auto))
  THEN  (Assert  r0  <  r(a)\^{}(2  *  k)  +  3  BY
                          (RWO  "rnexp-int"  0  THEN  Auto))
  THEN  (RWO  "rnexp-rdiv<"  (-3)  THENA  Auto)
  THEN  RWO  "rnexp-int"  (-3)
  THEN  Auto)

---

Home Index