---

Step * 1 2 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(imax(2000 ÷ z + 2;2)))
BY
{ ((Subst' imax(2000 ÷ z + 2;2) ~ 2 0 THENA ((RWO "imax_unfold" 0 THENA Auto) THEN AutoSplit)) THEN Auto) }

---

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


By

---

Latex:
((Subst'  imax(2000  \mdiv{}  z  +  2;2)  \msim{}  2  0  THENA  ((RWO  "imax\_unfold"  0  THENA  Auto)  THEN  AutoSplit))
  THEN  Auto
  )

---

Home Index