---

Step * 2 1 1 1 2 1 of Lemma rroot_wf


1. i : {2...}
2. x : ℝ
3. ¬↑isEven(i)
4. r0 ≤ x
⊢ accelerate(2;rroot-odd(i;x))^i = rroot-abs(i;x)^i
BY
{ TACTIC:((Assert ∀n:ℕ+. ((-4) ≤ (x n)) BY
                 ((RWO "rleq-iff4" (-1) THENA Auto) THEN RepUR ``int-to-real`` -1 THEN ParallelLast THEN Auto))
          THEN BLemma `rnexp_functionality`
          THEN Auto) }

1
1. i : {2...}
2. x : ℝ
3. ¬↑isEven(i)
4. r0 ≤ x
5. ∀n:ℕ+. ((-4) ≤ (x n))
⊢ accelerate(2;rroot-odd(i;x)) = rroot-abs(i;x)

---

Latex:

---

Latex:

1.  i  :  \{2...\}
2.  x  :  \mBbbR{}
3.  \mneg{}\muparrow{}isEven(i)
4.  r0  \mleq{}  x
\mvdash{}  accelerate(2;rroot-odd(i;x))\^{}i  =  rroot-abs(i;x)\^{}i


By

---

Latex:
TACTIC:((Assert  \mforall{}n:\mBbbN{}\msupplus{}.  ((-4)  \mleq{}  (x  n))  BY
                              ((RWO  "rleq-iff4"  (-1)  THENA  Auto)
                                THEN  RepUR  ``int-to-real``  -1
                                THEN  ParallelLast
                                THEN  Auto))
                THEN  BLemma  `rnexp\_functionality`
                THEN  Auto)

---

Home Index