---

Step * of Lemma atan-approx_wf

∀[k:ℕ]. ∀[x:ℝ]. ∀[N:ℕ+].  (atan-approx(k;x;N) ∈ ℤ)
BY
{ (Auto
   THEN Unfold `atan-approx` 0
   THEN (GenConcl ⌜poly-approx(λi.(r1)/(2 * i) + 1;x * x;k;N) = u ∈ ℤ⌝⋅ THENA Auto)
   THEN (CallByValueReduce 0⋅ THENA Auto)
   THEN GenConcl ⌜(((2 * |u|) ÷ N) + 1) = b ∈ ℕ+⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[x:\mBbbR{}].  \mforall{}[N:\mBbbN{}\msupplus{}].    (atan-approx(k;x;N)  \mmember{}  \mBbbZ{})


By

---

Latex:
(Auto
  THEN  Unfold  `atan-approx`  0
  THEN  (GenConcl  \mkleeneopen{}poly-approx(\mlambda{}i.(r1)/(2  *  i)  +  1;x  *  x;k;N)  =  u\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduce  0\mcdot{}  THENA  Auto)
  THEN  GenConcl  \mkleeneopen{}(((2  *  |u|)  \mdiv{}  N)  +  1)  =  b\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index