---

Step * 1 of Lemma gcd-unique-nat


1. n : ℕ@i
2. m : ℕ@i
3. g : ℕ@i
4. g | n@i
5. g | m@i
6. ∀v:ℤ. ((v | n) ⇒ (v | m) ⇒ (v | g))@i
7. ∀y1,y2:ℤ.  (GCD(n;m;y1) ⇒ GCD(n;m;y2) ⇒ (y1 ~ y2))
⊢ GCD(n;m;g)
BY
{ (D 0 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}@i
2.  m  :  \mBbbN{}@i
3.  g  :  \mBbbN{}@i
4.  g  |  n@i
5.  g  |  m@i
6.  \mforall{}v:\mBbbZ{}.  ((v  |  n)  {}\mRightarrow{}  (v  |  m)  {}\mRightarrow{}  (v  |  g))@i
7.  \mforall{}y1,y2:\mBbbZ{}.    (GCD(n;m;y1)  {}\mRightarrow{}  GCD(n;m;y2)  {}\mRightarrow{}  (y1  \msim{}  y2))
\mvdash{}  GCD(n;m;g)


By

---

Latex:
(D  0  THEN  Auto)

---

Home Index