---

Step * 1 1 1 of Lemma sign-inverse


1. v : ℤ
2. |v| = 1 ∈ ℤ
3. v1 : ℤ
4. |v1| = 1 ∈ ℤ
5. 1 = (v * v1) ∈ {s:ℤ| |s| = 1 ∈ ℤ} 
⊢ v1 = v ∈ {s:ℤ| |s| = 1 ∈ ℤ} 
BY
{ (∀h:hyp. ((RWO  "absval_cases" h THENA Complete (Auto)) THEN D h) 
   THEN Auto
   THEN Eliminate ⌜v⌝⋅
   THEN Eliminate ⌜v1⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  v  :  \mBbbZ{}
2.  |v|  =  1
3.  v1  :  \mBbbZ{}
4.  |v1|  =  1
5.  1  =  (v  *  v1)
\mvdash{}  v1  =  v


By

---

Latex:
(\mforall{}h:hyp.  ((RWO    "absval\_cases"  h  THENA  Complete  (Auto))  THEN  D  h) 
  THEN  Auto
  THEN  Eliminate  \mkleeneopen{}v\mkleeneclose{}\mcdot{}
  THEN  Eliminate  \mkleeneopen{}v1\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index