---

Step * 1 1 of Lemma rroot_wf


1. i : {2...}
2. x : ℝ
3. ↑isEven(i)
4. r0 ≤ x
5. x = |x|
6. True
⊢ r0 ≤ rroot-abs(i;x)
BY
{ ((BLemma `rleq-iff4` THEN Auto) THEN (RWO "rroot-abs-non-neg<" 0 THENA Auto)) }

1
1. i : {2...}
2. x : ℝ
3. ↑isEven(i)
4. r0 ≤ x
5. x = |x|
6. True
7. n : ℕ+
⊢ (r0 n) ≤ (0 + 4)

---

Latex:

---

Latex:

1.  i  :  \{2...\}
2.  x  :  \mBbbR{}
3.  \muparrow{}isEven(i)
4.  r0  \mleq{}  x
5.  x  =  |x|
6.  True
\mvdash{}  r0  \mleq{}  rroot-abs(i;x)


By

---

Latex:
((BLemma  `rleq-iff4`  THEN  Auto)  THEN  (RWO  "rroot-abs-non-neg<"  0  THENA  Auto))

---

Home Index