---

Step * of Lemma exp-equal-minusone

∀[x:ℤ]. ∀[n:ℕ].  uiff(x^n = (-1) ∈ ℤ;(x = (-1) ∈ ℤ) ∧ ((n mod 2) = 1 ∈ ℤ))
BY
{ (Auto THEN SplitOrHyps) }

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

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

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

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  \mforall{}[n:\mBbbN{}].    uiff(x\^{}n  =  (-1);(x  =  (-1))  \mwedge{}  ((n  mod  2)  =  1))


By

---

Latex:
(Auto  THEN  SplitOrHyps)

---

Home Index