---

Step * of Lemma rnexp-minus-one

∀n:ℕ. (r(-1)^n = if (n rem 2 =z 0) then r1 else r(-1) fi )
BY
{ (Auto
   THEN RWO "rnexp-int" 0
   THEN Auto
   THEN AutoSplit
   THEN BLemma `req-int`
   THEN Auto
   THEN (BLemma `exp-equal-one` ORELSE BLemma `exp-equal-minusone`)
   THEN Auto
   THEN Try (RepeatFor 2 ((OrRight THEN Auto)))
   THEN (RWO "modulus-is-rem" 0 THEN Auto)
   THEN InstLemma `rem_bounds_1` [⌜n⌝;⌜2⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  (r(-1)\^{}n  =  if  (n  rem  2  =\msubz{}  0)  then  r1  else  r(-1)  fi  )


By

---

Latex:
(Auto
  THEN  RWO  "rnexp-int"  0
  THEN  Auto
  THEN  AutoSplit
  THEN  BLemma  `req-int`
  THEN  Auto
  THEN  (BLemma  `exp-equal-one`  ORELSE  BLemma  `exp-equal-minusone`)
  THEN  Auto
  THEN  Try  (RepeatFor  2  ((OrRight  THEN  Auto)))
  THEN  (RWO  "modulus-is-rem"  0  THEN  Auto)
  THEN  InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index