---

Step * of Lemma exp-minus

∀[n:ℕ]. ∀[x:ℤ].  (-x^n = if (n mod 2 =z 0) then x^n else -x^n fi  ∈ ℤ)
BY
{ (Auto THEN (Subst' -x ~ (-1) * x 0 THENA Auto) THEN (RWW "exp-of-mul exp-minusone" 0 THENA Auto) THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x:\mBbbZ{}].    (-x\^{}n  =  if  (n  mod  2  =\msubz{}  0)  then  x\^{}n  else  -x\^{}n  fi  )


By

---

Latex:
(Auto
  THEN  (Subst'  -x  \msim{}  (-1)  *  x  0  THENA  Auto)
  THEN  (RWW  "exp-of-mul  exp-minusone"  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index