---

Step * of Lemma exp-minus

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

---

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:
xxx(Auto
        THEN  (Subst'  -x  \msim{}  (-1)  *  x  0  THENA  Auto)
        THEN  (RWW  "exp-of-mul  exp-minusone"  0  THENA  Auto)
        THEN  AutoSplit)xxx

---

Home Index