---

Step * 1 of Lemma general-iroot-property


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
BY
{ TACTIC:(D -2 THEN HypSubst' (-2) 0 THEN Reduce 0) }

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

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  x  :  \mBbbZ{}
3.  x  <  0  \mwedge{}  ((n  mod  2)  =  1)
4.  x  <  0
\mvdash{}  (x  \mleq{}  if  n  mod  2=1  then  TERMOF\{integer-nth-root2:o,  1:l\}  n  x  else  0\^{}n)
\mwedge{}  (if  n  mod  2=1  then  TERMOF\{integer-nth-root2:o,  1:l\}  n  x  else  0  -  1)\^{}n  <  x


By

---

Latex:
TACTIC:(D  -2  THEN  HypSubst'  (-2)  0  THEN  Reduce  0)

---

Home Index