---

Step * of Lemma general-iroot-property

∀[n:ℕ+]. ∀[x:ℤ].
  (((0 ≤ x) ⇒ ((general-iroot(n;x)^n ≤ x) ∧ x < (general-iroot(n;x) + 1)^n))
  ∧ ((x < 0 ∧ ((n mod 2) = 1 ∈ ℤ)) ⇒ ((x ≤ general-iroot(n;x)^n) ∧ (general-iroot(n;x) - 1)^n < x))
  ∧ ((x < 0 ∧ ((n mod 2) = 0 ∈ ℤ)) ⇒ (general-iroot(n;x) = 0 ∈ ℤ)))
BY
{ TACTIC:((RepeatFor 2 ((D 0 THENA Auto)) THEN SplitAndConcl  THEN (D 0 THENA Auto))
          THEN Unfold `general-iroot` 0
          THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
          THEN AutoSplit) }

1
1. n : ℕ+
2. x : ℤ
3. x < 0 ∧ ((n mod 2) = 1 ∈ ℤ)
4. x < 0
⊢ (x ≤ if n mod 2=1 then TERMOF{integer-nth-root2:o, 1:l} n x else 0^n)
∧ (if n mod 2=1 then TERMOF{integer-nth-root2:o, 1:l} n x else 0 - 1)^n < x

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[x:\mBbbZ{}].
    (((0  \mleq{}  x)  {}\mRightarrow{}  ((general-iroot(n;x)\^{}n  \mleq{}  x)  \mwedge{}  x  <  (general-iroot(n;x)  +  1)\^{}n))
    \mwedge{}  ((x  <  0  \mwedge{}  ((n  mod  2)  =  1))  {}\mRightarrow{}  ((x  \mleq{}  general-iroot(n;x)\^{}n)  \mwedge{}  (general-iroot(n;x)  -  1)\^{}n  <  x))
    \mwedge{}  ((x  <  0  \mwedge{}  ((n  mod  2)  =  0))  {}\mRightarrow{}  (general-iroot(n;x)  =  0)))


By

---

Latex:
TACTIC:((RepeatFor  2  ((D  0  THENA  Auto))  THEN  SplitAndConcl    THEN  (D  0  THENA  Auto))
                THEN  Unfold  `general-iroot`  0
                THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
                THEN  AutoSplit)

---

Home Index