---

Step * 1 1 1 of Lemma atan-size-bound_wf


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
8. 2 < 2000 ÷ z + 2
⊢ |x| ≤ (r1/r(2000 ÷ z + 2))
BY
{ ((RWO "int-rdiv-req" (-2) THENA Auto) THEN (RWO "-2" 0 THENA Auto)) }

1
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)/r(2000))
8. 2 < 2000 ÷ z + 2
⊢ (r(z + 2)/r(2000)) ≤ (r1/r(2000 ÷ z + 2))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  |x|  \mleq{}  (r1/r(2))
3.  (above  |x|  within  1/500  -  (r1/r(500)))  \mleq{}  |x|
4.  z  :  \mBbbZ{}
5.  (|x|  1000)  =  z
6.  0  \mleq{}  z
7.  |x|  \mleq{}  (r(z  +  2))/2000
8.  2  <  2000  \mdiv{}  z  +  2
\mvdash{}  |x|  \mleq{}  (r1/r(2000  \mdiv{}  z  +  2))


By

---

Latex:
((RWO  "int-rdiv-req"  (-2)  THENA  Auto)  THEN  (RWO  "-2"  0  THENA  Auto))

---

Home Index