---

Step * 1 of Lemma exp-minusone

.....upcase..... 
1. n : ℤ
2. 0 < n
3. (-1)^(n - 1) = if ((n - 1) mod 2 =z 0) then 1 else -1 fi  ∈ ℤ
⊢ (-1)^n = if (n mod 2 =z 0) then 1 else -1 fi  ∈ ℤ
BY
{ xxx(Unfold `exp` 0
      THEN (RWO "primrec-unroll" 0 THENA Auto)
      THEN OldAutoBoolCase ⌜(n =z 0)⌝⋅
      THEN Fold `exp` 0
      THEN Auto
      THEN (HypSubst' (-2) 0)
      THEN (Thin (-2))
      THEN ((InstLemma `add-one-mod-2` [⌜n - 1⌝])⋅ THENA Auto)
      THEN (Subst' (n - 1) + 1 ~ n -1 THENL [Auto; HypSubst' -1 0])
      THEN ((InstLemma `mod_bounds` [⌜n - 1⌝; ⌜2⌝])⋅ THENA Auto)
      THEN (MoveToConcl (-1))
      THEN (GenConclAtAddr [1; 1; 2])
      THEN Auto)xxx }

---

Latex:

---

Latex:
.....upcase..... 
1.  n  :  \mBbbZ{}
2.  0  <  n
3.  (-1)\^{}(n  -  1)  =  if  ((n  -  1)  mod  2  =\msubz{}  0)  then  1  else  -1  fi 
\mvdash{}  (-1)\^{}n  =  if  (n  mod  2  =\msubz{}  0)  then  1  else  -1  fi 


By

---

Latex:
xxx(Unfold  `exp`  0
        THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
        THEN  OldAutoBoolCase  \mkleeneopen{}(n  =\msubz{}  0)\mkleeneclose{}\mcdot{}
        THEN  Fold  `exp`  0
        THEN  Auto
        THEN  (HypSubst'  (-2)  0)
        THEN  (Thin  (-2))
        THEN  ((InstLemma  `add-one-mod-2`  [\mkleeneopen{}n  -  1\mkleeneclose{}])\mcdot{}  THENA  Auto)
        THEN  (Subst'  (n  -  1)  +  1  \msim{}  n  -1  THENL  [Auto;  HypSubst'  -1  0])
        THEN  ((InstLemma  `mod\_bounds`  [\mkleeneopen{}n  -  1\mkleeneclose{};  \mkleeneopen{}2\mkleeneclose{}])\mcdot{}  THENA  Auto)
        THEN  (MoveToConcl  (-1))
        THEN  (GenConclAtAddr  [1;  1;  2])
        THEN  Auto)xxx

---

Home Index