---

Step * 1 of Lemma rroot_wf


1. i : {2...}
2. x : ℝ
3. ↑isEven(i)
4. r0 ≤ x
⊢ rroot-abs(i;x) ∈ {y:ℝ| (True ⇒ (r0 ≤ y)) ∧ (y^i = x)} 
BY
{ ((Assert x = |x| BY Auto) THEN MemTypeCD THEN Auto) }

1
1. i : {2...}
2. x : ℝ
3. ↑isEven(i)
4. r0 ≤ x
5. x = |x|
6. True
⊢ r0 ≤ rroot-abs(i;x)

---

Latex:

---

Latex:

1.  i  :  \{2...\}
2.  x  :  \mBbbR{}
3.  \muparrow{}isEven(i)
4.  r0  \mleq{}  x
\mvdash{}  rroot-abs(i;x)  \mmember{}  \{y:\mBbbR{}|  (True  {}\mRightarrow{}  (r0  \mleq{}  y))  \mwedge{}  (y\^{}i  =  x)\} 


By

---

Latex:
((Assert  x  =  |x|  BY  Auto)  THEN  MemTypeCD  THEN  Auto)

---

Home Index