---

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


∀u:ℤ. ((∃R:ℤ List. ([u] = u * R ∈ (ℤ List))) ∧ (∃S:ℤ List. ((||S|| = 1 ∈ ℤ) ∧ (u = S ⋅ [u] ∈ ℤ))))
BY
{ Auto }

1
1. u : ℤ
⊢ ∃R:ℤ List. ([u] = u * R ∈ (ℤ List))

2
1. u : ℤ
2. ∃R:ℤ List. ([u] = u * R ∈ (ℤ List))
⊢ ∃S:ℤ List. ((||S|| = 1 ∈ ℤ) ∧ (u = S ⋅ [u] ∈ ℤ))

---

Latex:

---

Latex:

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


By

---

Latex:
Auto

---

Home Index