---

Step * 1 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)/r(2000))
8. 2 < 2000 ÷ z + 2
⊢ (r(z + 2)/r(2000)) ≤ (r1/r(2000 ÷ z + 2))
BY
{ (BLemma `rleq-int-fractions` THEN 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
⊢ ((z + 2) * (2000 ÷ z + 2)) ≤ (1 * 2000)

---

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)/r(2000))
8.  2  <  2000  \mdiv{}  z  +  2
\mvdash{}  (r(z  +  2)/r(2000))  \mleq{}  (r1/r(2000  \mdiv{}  z  +  2))


By

---

Latex:
(BLemma  `rleq-int-fractions`  THEN  Auto)

---

Home Index