---

Step * 1 1 1 of Lemma rroot_wf


1. i : {2...}
2. x : ℝ
3. ↑isEven(i)
4. r0 ≤ x
5. x = |x|
6. True
7. n : ℕ+
⊢ (r0 n) ≤ (0 + 4)
BY
{ (RepUR ``int-to-real`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  i  :  \{2...\}
2.  x  :  \mBbbR{}
3.  \muparrow{}isEven(i)
4.  r0  \mleq{}  x
5.  x  =  |x|
6.  True
7.  n  :  \mBbbN{}\msupplus{}
\mvdash{}  (r0  n)  \mleq{}  (0  +  4)


By

---

Latex:
(RepUR  ``int-to-real``  0  THEN  Auto)

---

Home Index