---

Step * 2 of Lemma exp-equal-minusone


1. x : ℤ
2. n : ℕ
3. x^n = (-1) ∈ ℤ
⊢ (n mod 2) = 1 ∈ ℤ
BY
{ ((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) }

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

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

---

Latex:

---

Latex:

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


By

---

Latex:
((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)

---

Home Index