---

Step * of Lemma rnexp-rminus

∀x:ℝ. ∀n:ℕ.  (-(x)^n = if isOdd(n) then -(x^n) else x^n fi )
BY
{ (Auto
   THEN AutoSplit
   THEN (RWW "rminus-as-rmul rnexp-rmul rnexp-int exp-minusone" 0 THENA Auto)
   THEN Fold `isEven` 0
   THEN AutoSplit) }

1
1. x : ℝ
2. n : ℕ
3. ↑isOdd(n)
4. ↑isEven(n)
⊢ (r1 * x^n) = (r(-1) * x^n)

2
1. x : ℝ
2. n : ℕ
3. ¬↑isEven(n)
4. ¬↑isOdd(n)
⊢ (r(-1) * x^n) = x^n

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  \mforall{}n:\mBbbN{}.    (-(x)\^{}n  =  if  isOdd(n)  then  -(x\^{}n)  else  x\^{}n  fi  )


By

---

Latex:
(Auto
  THEN  AutoSplit
  THEN  (RWW  "rminus-as-rmul  rnexp-rmul  rnexp-int  exp-minusone"  0  THENA  Auto)
  THEN  Fold  `isEven`  0
  THEN  AutoSplit)

---

Home Index