---

Step * of Lemma exp-assoced-one

∀x:ℤ. ∀n:ℕ+.  ((x^n ~ 1) ⇒ (x ~ 1))
BY
{ xxx(RepeatFor 2 ((D 0 THENA Auto))
      THEN Unfold `exp` 0
      THEN (RWO "primrec-unroll" 0 THENA Auto)
      THEN AutoBoolCase ⌜n <z 1⌝⋅
      THEN Fold `exp` 0
      THEN Auto)xxx }

1
1. x : ℤ
2. n : ℕ+
3. ¬n < 1
4. (x * x^(n - 1)) ~ 1
⊢ x ~ 1

---

Latex:

---

Latex:
\mforall{}x:\mBbbZ{}.  \mforall{}n:\mBbbN{}\msupplus{}.    ((x\^{}n  \msim{}  1)  {}\mRightarrow{}  (x  \msim{}  1))


By

---

Latex:
xxx(RepeatFor  2  ((D  0  THENA  Auto))
        THEN  Unfold  `exp`  0
        THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
        THEN  AutoBoolCase  \mkleeneopen{}n  <z  1\mkleeneclose{}\mcdot{}
        THEN  Fold  `exp`  0
        THEN  Auto)xxx

---

Home Index