---

Step * 1 of Lemma exp-equal-minusone


1. x : ℤ
2. n : ℕ
3. x^n = (-1) ∈ ℤ
⊢ x = (-1) ∈ ℤ
BY
{ xxx((CaseNat 0 `n'
       THENL [(HypSubst' (-1) (-2) THEN Reduce (-2) THEN Auto)
             ; (InstLemma `exp-assoced-one` [⌜x⌝;⌜n⌝]⋅
                THENA (Auto THEN HypSubst' (-2) 0 THEN D 0 THEN RWO "divides_iff_rem_zero" 0 THEN Reduce 0 THEN Auto)
                )⋅]
      )
      THEN RWO "assoced_elim" (-1)
      THEN Auto
      THEN D -1
      THEN Auto)xxx }

1
1. x : ℤ
2. n : ℕ
3. x^n = (-1) ∈ ℤ
4. ¬(n = 0 ∈ ℤ)
5. x = 1 ∈ ℤ
⊢ x = (-1) ∈ ℤ

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  n  :  \mBbbN{}
3.  x\^{}n  =  (-1)
\mvdash{}  x  =  (-1)


By

---

Latex:
xxx((CaseNat  0  `n'
          THENL  [(HypSubst'  (-1)  (-2)  THEN  Reduce  (-2)  THEN  Auto)
                      ;  (InstLemma  `exp-assoced-one`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}
                            THENA  (Auto
                                          THEN  HypSubst'  (-2)  0
                                          THEN  D  0
                                          THEN  RWO  "divides\_iff\_rem\_zero"  0
                                          THEN  Reduce  0
                                          THEN  Auto)
                            )\mcdot{}]
        )
        THEN  RWO  "assoced\_elim"  (-1)
        THEN  Auto
        THEN  D  -1
        THEN  Auto)xxx

---

Home Index