---

Step * of Lemma gcd-list-property

∀L:ℤ List+
  ((∃R:ℤ List. (L = gcd-list(L) * R ∈ (ℤ List))) ∧ (∃S:ℤ List. ((||S|| = ||L|| ∈ ℤ) ∧ (gcd-list(L) = S ⋅ L ∈ ℤ))))
BY
{ ((D 0 THENA Auto) THEN D 1 THEN D 1) }

1
1. [%1] : 0 < ||[]||
⊢ (∃R:ℤ List. ([] = gcd-list([]) * R ∈ (ℤ List))) ∧ (∃S:ℤ List. ((||S|| = ||[]|| ∈ ℤ) ∧ (gcd-list([]) = S ⋅ [] ∈ ℤ)))

2
1. u : ℤ
2. v : ℤ List
3. [%1] : 0 < ||[u / v]||
⊢ (∃R:ℤ List. ([u / v] = gcd-list([u / v]) * R ∈ (ℤ List)))
∧ (∃S:ℤ List. ((||S|| = ||[u / v]|| ∈ ℤ) ∧ (gcd-list([u / v]) = S ⋅ [u / v] ∈ ℤ)))

---

Latex:

---

Latex:
\mforall{}L:\mBbbZ{}  List\msupplus{}
    ((\mexists{}R:\mBbbZ{}  List.  (L  =  gcd-list(L)  *  R))  \mwedge{}  (\mexists{}S:\mBbbZ{}  List.  ((||S||  =  ||L||)  \mwedge{}  (gcd-list(L)  =  S  \mcdot{}  L))))


By

---

Latex:
((D  0  THENA  Auto)  THEN  D  1  THEN  D  1)

---

Home Index