---

Step * 1 of Lemma atan-size-bound_wf

.....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)))
BY
{ (Decide ⌜2 < 2000 ÷ z + 2⌝⋅ 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))/2000
8. 2 < 2000 ÷ z + 2
⊢ |x| ≤ (r1/r(imax(2000 ÷ z + 2;2)))

2
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(imax(2000 ÷ z + 2;2)))

---

Latex:

---

Latex:
.....set  predicate..... 
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
\mvdash{}  |x|  \mleq{}  (r1/r(imax(2000  \mdiv{}  z  +  2;2)))


By

---

Latex:
(Decide  \mkleeneopen{}2  <  2000  \mdiv{}  z  +  2\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index