---

Step * of Lemma atan-size-bound_wf

∀[x:{x:ℝ| |x| ≤ (r1/r(2))} ]. (atan-size-bound(x) ∈ {a:{2...}| |x| ≤ (r1/r(a))} )
BY
{ (Auto
   THEN D -1
   THEN (InstLemma `rational-upper-approx-property` [⌜|x|⌝;⌜500⌝]⋅ THENA Auto)
   THEN D -1
   THEN Unfold `rational-upper-approx` -1
   THEN Reduce -1
   THEN (MoveToConcl (-1) THEN Unfold `atan-size-bound` 0)
   THEN ((GenConcl ⌜(|x| 1000) = z ∈ ℤ⌝⋅ THENA Auto)
         THEN (Assert 0 ≤ z BY
                     (Eliminate ⌜z⌝⋅ THEN RepUR ``rabs`` 0 THEN Auto))
         )
   THEN CallByValueReduce 0
   THEN Auto
   THEN MemTypeCD
   THEN Auto) }

1
.....set predicate..... 
1. x : ℝ
2. |x| ≤ (r1/r(2))
3. (above |x| within 1/500 - (r1/r(500))) ≤ |x|
4. z : ℤ
5. (|x| 1000) = z ∈ ℤ
6. 0 ≤ z
7. |x| ≤ (r(z + 2))/2000
⊢ |x| ≤ (r1/r(imax(2000 ÷ z + 2;2)))

---

Latex:

---

Latex:
\mforall{}[x:\{x:\mBbbR{}|  |x|  \mleq{}  (r1/r(2))\}  ].  (atan-size-bound(x)  \mmember{}  \{a:\{2...\}|  |x|  \mleq{}  (r1/r(a))\}  )


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  (InstLemma  `rational-upper-approx-property`  [\mkleeneopen{}|x|\mkleeneclose{};\mkleeneopen{}500\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Unfold  `rational-upper-approx`  -1
  THEN  Reduce  -1
  THEN  (MoveToConcl  (-1)  THEN  Unfold  `atan-size-bound`  0)
  THEN  ((GenConcl  \mkleeneopen{}(|x|  1000)  =  z\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  (Assert  0  \mleq{}  z  BY
                                      (Eliminate  \mkleeneopen{}z\mkleeneclose{}\mcdot{}  THEN  RepUR  ``rabs``  0  THEN  Auto))
              )
  THEN  CallByValueReduce  0
  THEN  Auto
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index