---

Step * 2 1 1 2 of Lemma gcd-list-property


1. u : ℤ
2. ∃R:ℤ List. ([u] = u * R ∈ (ℤ List))
⊢ ∃S:ℤ List. ((||S|| = 1 ∈ ℤ) ∧ (u = S ⋅ [u] ∈ ℤ))
BY
{ (With ⌜[1]⌝ (D 0)⋅ THEN Auto THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  u  :  \mBbbZ{}
2.  \mexists{}R:\mBbbZ{}  List.  ([u]  =  u  *  R)
\mvdash{}  \mexists{}S:\mBbbZ{}  List.  ((||S||  =  1)  \mwedge{}  (u  =  S  \mcdot{}  [u]))


By

---

Latex:
(With  \mkleeneopen{}[1]\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  Reduce  0  THEN  Auto)

---

Home Index