---

Step * 1 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
⊢ ((z + 2) * (2000 ÷ z + 2)) ≤ (1 * 2000)
BY
{ (RWO "div_rem_sum2" 0 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
⊢ (2000 - 2000 rem 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{}  ((z  +  2)  *  (2000  \mdiv{}  z  +  2))  \mleq{}  (1  *  2000)


By

---

Latex:
(RWO  "div\_rem\_sum2"  0  THEN  Auto)

---

Home Index